[false-green] MCP lane loses the final call when the agent kills the stand-in

[AminChirazi]

DRAFT — evidence, not a fix. The test in this PR is expected to FAIL. Do not merge as-is.

Discovery from the Milestone 2 falsifiability suite while writing #257. Full write-up in #273.

The finding

0.8.0 fixed "the MCP stand-in no longer loses its recording when the agent kills it" by persisting the lane after every captured call. An agent that kills the stand-in immediately after reading a response still loses that call.

With the real server's own request log as the oracle:

Server received	initialize, notifications/initialized, tools/list, tools/call get_weather
Lane recorded	initialize, tools/list

record exited 0 and minted a trace. A tool the agent demonstrably invoked is absent from the evidence.

Why it matters

CHARTER §5 ranks a false green as the only defect class that destroys the product's value. The lane is the record of what the agent did at the tool boundary; one that silently runs short understates it, and every assertion over that lane inherits the omission — including guard-path claims that a tool was never called.

What is in this PR

• tests/falsifiability/fixtures/mcp-killing-agent.py — identical to the suite's polite agent but for its last act: proc.kill() instead of stdin.close(); wait()
• crates/flowproof-cli/tests/falsifiability_mcp_kill.rs — the red-path proof, which currently fails on tools/call

The test deliberately checks the server log first, so an exchange that never happened cannot pass as a vacuously "preserved" lane.

Why nothing caught it

mcp_stdio_e2e.rs has no kill or signal coverage — every test closes stdin politely and waits, exactly the path the 0.8.0 defect did not affect. The fix shipped with no test that could fail for its own bug: the same pattern 0.9.1's credential leak was described in, "working by inspection rather than by measurement."

Next

Per the brief, the fix is a separate change I must not self-authorise. When it lands, this test should go green and stay in the suite as the permanent guard. #273 also raises whether an incomplete lane should be detectable at all rather than silently minted.

🤖 Generated with Claude Code

[AminChirazi]

Rebased onto main, and the CI noise is gone

CI was failing twice, and only one of those was the point. rustfmt failed — my sloppiness: I went straight from the discovery to the commit and never ran cargo fmt on this branch. A reviewer opening this saw two red checks with no way to tell which one was the evidence.

Now rebased onto main (picking up #270 and #272), formatted, and re-verified locally:

cargo fmt --check	0
cargo clippy -p flowproof-cli --all-targets -- -D warnings	0
cargo test -p flowproof-cli --test falsifiability_mcp_kill	101 — intended

The single remaining failure is the assertion that is the finding:

the MCP lane must survive an abrupt kill, missing tools/call

So CI red on this PR now means exactly one thing, which is what an evidence PR needs to mean.

Still not a merge candidate

Unchanged: this is evidence for #273, not a fix. The test is expected to fail until the underlying defect is addressed, and the fix is a separate change — the brief forbids the finder self-authorising it.

When the fix lands, this test should go green and stay in the suite as the permanent guard. #273 also raises the question worth more than the fix: whether an incomplete lane should be detectable at all, rather than silently minted.

[AminChirazi]

Superseded by #279, which merged as 0a463ab.

This PR was evidence, not a fix: the test in it was expected to fail, and did — on this box and on GitHub's runners. #279 fixes the defect it documented and carries this exact test cherry-picked unchanged, where it now passes. The test was never adjusted to fit the fix.

Verified on origin/main: falsifiability_mcp_kill.rs, mcp-killing-agent.py, and the ordering change in mcp_stdio.rs are all present. #273 and #257 closed with it.

The evidence did its job — the branch can go.