[BryanFRD]

The CLI runs in print mode, so the session ends as soon as the model stops calling tools. Monitor, ScheduleWakeup and CronCreate only pay off on a later turn that never comes: a formal-verify run on FerrVault-Cloud#1199 started cargo kani under a Monitor, said it was waiting for results and exited with no result, failing the review step. Three of the last fifteen failed formal-verify runs ended this way. They are now always disallowed, on top of the run's own list.

Signed-off-by: BryanFRD bryanferrando59@gmail.com

[ferrfleet-interne]

Approve. The three turn-deferring tools (Monitor, ScheduleWakeup, CronCreate) are now always passed as --disallowed-tools, after the configured ones and without duplicating an entry the config already has. The change is correct and tested.

Suggestions

• Nit, runner/src/claude.rs:98: HEADLESS_DISALLOWED_TOOLS has no comment saying why it exists. Every other constant and flag in this function explains itself. The reason (a -p run has no later turn, so anything the agent schedules never fires and the run ends having done nothing) is only in the PR title. Without it, someone may remove an entry or forget to add the next tool of the same kind. Suggested comment:

/// Tools that hand control back and wait for a later turn. A `-p` run has no
/// later turn: the process exits and whatever the agent scheduled never fires.
const HEADLESS_DISALLOWED_TOOLS: [&str; 3] = ["Monitor", "ScheduleWakeup", "CronCreate"];

Formal verification

No counterexamples. These are exhaustive bounded tests over the real build_claude_command, not Kani proofs: 1555 disallowed_tools lists (length 0 to 4 over Monitor, ScheduleWakeup, CronCreate, WebFetch, monitor, ""), each with allowed_tools empty or containing all three headless tools, so 3110 configs.

Property	Result
Operator's disallowed_tools emitted first, verbatim, in order	tested
The three headless tools are always denied, whatever disallowed_tools and allowed_tools contain	tested
Runner adds only headless tools, never re-adds one already denied, never adds one twice	tested
Flag count equals config length plus the headless tools missing from it	tested

1 harness (headless_denylist_verification, 1 test) covers these four properties.

Harness code

#[cfg(test)]
mod headless_denylist_verification {
    use super::*;

    const ALPHABET: [&str; 6] = ["Monitor", "ScheduleWakeup", "CronCreate", "WebFetch", "monitor", ""];

    fn cfg_with(disallowed: Vec<String>, allowed: Vec<String>) -> RunConfig {
        let mut cfg: RunConfig = serde_json::from_value(serde_json::json!({
            "run_id": "01999999-9999-7999-9999-999999999988",
            "agent_id": "pr-agent",
            "prompt": "p",
            "working_dir": "/workdir",
        }))
        .expect("a minimal config");
        cfg.disallowed_tools = disallowed;
        cfg.allowed_tools = allowed;
        cfg
    }

    fn env() -> Env {
        Env {
            api_url: "http://api.invalid".to_owned(),
            run_id: "run".to_owned(),
            run_token: "token".to_owned(),
            working_dir: Some("/workdir".to_owned()),
            runner_name: None,
        }
    }

    fn emitted(cfg: &RunConfig) -> Vec<String> {
        let inv = build_claude_command(cfg, &env(), None).expect("building");
        let args: Vec<String> = inv
            .command
            .as_std()
            .get_args()
            .map(|a| a.to_string_lossy().into_owned())
            .collect();
        args.windows(2)
            .filter(|p| p[0] == "--disallowed-tools")
            .map(|p| p[1].clone())
            .collect()
    }

    /// Every list over ALPHABET of length 0..=4 (6^0+..+6^4 = 1555 lists),
    /// each also tried with every headless tool in --allowed-tools.
    #[test]
    fn headless_denylist_exhaustive_to_len_4() {
        let mut lists: Vec<Vec<String>> = vec![vec![]];
        let mut frontier = lists.clone();
        for _ in 0..4 {
            let mut next = Vec::new();
            for l in &frontier {
                for a in ALPHABET {
                    let mut n = l.clone();
                    n.push(a.to_string());
                    next.push(n);
                }
            }
            lists.extend(next.iter().cloned());
            frontier = next;
        }
        assert_eq!(lists.len(), 1555);
        let allowed_variants: Vec<Vec<String>> = vec![
            vec![],
            HEADLESS_DISALLOWED_TOOLS.iter().map(|s| s.to_string()).collect(),
        ];
        let mut checked = 0;
        for allowed in &allowed_variants {
            for cfg_list in &lists {
                let cfg = cfg_with(cfg_list.clone(), allowed.clone());
                let out = emitted(&cfg);
                // P1: the operator's list is passed through first, verbatim and in order.
                assert_eq!(&out[..cfg_list.len()], &cfg_list[..], "{cfg_list:?}");
                // P2: every headless tool is denied, whatever the config and --allowed-tools say.
                for t in HEADLESS_DISALLOWED_TOOLS {
                    assert!(out.iter().any(|o| o == t), "{t} missing for {cfg_list:?}");
                }
                // P3: the runner adds nothing that is neither configured nor headless,
                // and never duplicates a tool the config already denies.
                let extra = &out[cfg_list.len()..];
                for (i, e) in extra.iter().enumerate() {
                    assert!(HEADLESS_DISALLOWED_TOOLS.contains(&e.as_str()));
                    assert!(!cfg_list.contains(e), "{e} duplicated for {cfg_list:?}");
                    assert!(!extra[..i].contains(e));
                }
                // P4: output is exactly cfg ∪ headless in size.
                let missing = HEADLESS_DISALLOWED_TOOLS
                    .iter()
                    .filter(|t| !cfg_list.iter().any(|c| c == *t))
                    .count();
                assert_eq!(out.len(), cfg_list.len() + missing);
                checked += 1;
            }
        }
        assert_eq!(checked, 3110);
    }
}

Not verified:

• Whether the claude CLI really removes a tool given via repeated --disallowed-tools flags, and whether these three names match its current tool names. Only the CLI itself can confirm this.
• Matching is case-sensitive: a config entry monitor does not suppress the added Monitor. Both are emitted, which looks intended and harmless.
• The rest of the file (credentials, system prompt, MCP config) was not in the diff and was not checked.