feat(cli): flowproof doctor, a wiring check before you spend a key

[AminChirazi]

Do not merge without review - this is new CLI surface, which the loop's mandate puts in the open-PR-do-not-merge class. The design pass is recorded in LOOP-STATE.md and summarised below.

The design call: doctor, not init

Adoption splits in two. The audit half is judgement (is this tool destructive? does the grandchild inherit env?) and cannot be mechanised. The verification half is mechanical, and its dominant failure is a client that never reaches the proxy - discovered today only after a spec has been written and a key spent on record.

init was considered and rejected. The hard part is judgement, and detecting "the agent entry point" in an arbitrary repo is unreliable. A scaffold that guesses the command or the tools:/mcp: boundary wrong sends an adopter down a false path with false confidence, which is the one artifact this product must not ship. The YAML it would save is six lines.

What it does

flowproof doctor --agent "./start-agent"

Starts the proxy, runs the command once against a synthetic one-turn cassette, and reports how many model requests arrived. No spec, no assertions, no key - the canned reply comes from the proxy. A request that diverges from that cassette still arrived, which is the fact being measured.

Zero arrivals prints the injected variables, the two ${flowproof.*} handles to map, and the reminder that a model call in a child process needs that child to inherit the environment.

It never prints a green verdict

Deliberate, and the sharpest point in the design audit. An agent with more than one client can reach the proxy with one and the real provider with another - so an arriving request proves a client found it, not that all of them did. It reports the observation and says record is what settles it. Same posture as the zero-capture guard, which names causes as possibilities rather than facts.

A defect found while testing this, reported rather than hidden

The agent deadline stops the process flowproof started, not the tree. An agent that spawns a child which outlives it keeps the inherited stdout pipe open, so wall clock can exceed --timeout substantially.

Verified both directions: exec sleep 300 (no grandchild) honours --timeout 5 exactly; a spawned sleep 300 ran past three minutes.

This affects record and run too, not just doctor - and it is precisely the shape of a real adopter whose model call happens in a grandchild. Fixing it is a behaviour change to shared process handling, so it wants its own design pass rather than being slipped in here. Both the command output and the docs state the limit so it does not read as an unexplained hang.

Tests

Three e2e: a wired agent passes; an agent reading its own variable fails (the case the command exists for - a green doctor there would send someone off to waste a key); a command that cannot start is an error. They run under the normal workspace test, so no browser-job listing is needed.

41 suites green, clippy clean under --all-features.

Also in here

A doc-comment placement bug I introduced and caught: the new variant absorbed heal's description, leaving heal --help blank. Fixed, and both are verified in the help output.

🤖 Generated with Claude Code

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.