From 283550e7638a96989088f17039239ca95ae8a803 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 30 Jul 2026 22:38:27 +0000 Subject: [PATCH 1/3] [false-green] MCP lane loses the final call when the agent kills the stand-in EVIDENCE, NOT A FIX. This test is expected to FAIL. Do not merge. 0.8.0 fixed "the MCP stand-in no longer loses its recording when the agent kills it" -- the lane had been written only at stdin EOF, so an abrupt kill lost everything. The lane is now persisted after every captured call. It is not enough. An agent that kills the stand-in immediately after reading a response loses THAT call from the lane, while every earlier call survives. Observed, with the real server's own 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. So a tool the agent demonstrably invoked is absent from the evidence, and nothing said so. That is the defect class this milestone exists to eliminate, in the artifact the MCP boundary's claims rest on. A lane that silently runs short understates what the agent did, and every assertion evaluated over it inherits the omission. The fixture is an agent identical to the suite's polite one but for its last act: proc.kill() instead of stdin.close(); wait(). Every existing MCP test closes politely, which is exactly the path the 0.8.0 defect did not affect. Reported rather than fixed: the brief forbids self-authorising a fix for a defect the same run discovered. Refs #257 Co-Authored-By: Claude Opus 5 --- .../tests/falsifiability_mcp_kill.rs | 197 ++++++++++++++++++ .../fixtures/mcp-killing-agent.py | 51 +++++ 2 files changed, 248 insertions(+) create mode 100644 crates/flowproof-cli/tests/falsifiability_mcp_kill.rs create mode 100644 tests/falsifiability/fixtures/mcp-killing-agent.py diff --git a/crates/flowproof-cli/tests/falsifiability_mcp_kill.rs b/crates/flowproof-cli/tests/falsifiability_mcp_kill.rs new file mode 100644 index 0000000..13692b2 --- /dev/null +++ b/crates/flowproof-cli/tests/falsifiability_mcp_kill.rs @@ -0,0 +1,197 @@ +//! Falsifiability proof for the MCP stand-in's recording durability (#257). +//! +//! Before 0.8.0 the MCP lane was written only at stdin EOF. An agent that +//! terminated its stand-in abruptly never got there, and the ENTIRE recording +//! was lost. The fix persists the lane after every captured call, atomically. +//! +//! Nothing exercised it. Every MCP test in the suite closes stdin politely and +//! waits -- exactly the path the defect did not affect -- so all of them would +//! stay green if the fix were reverted tomorrow. That is the shape of an +//! unguarded fix: the bug is gone, and nothing would notice its return. +//! +//! The violating input is one hostile agent +//! (`tests/falsifiability/fixtures/mcp-killing-agent.py`), identical to the +//! suite's polite one but for its last act: `proc.kill()` instead of +//! `stdin.close(); wait()`. +//! +//! Two layers, and the second is the one that matters. A trace merely EXISTING +//! proves nothing -- the model cassette would still be written even with the +//! MCP lane empty, which is precisely what the defect produced. So the test +//! reads the lane and requires the captured call to be in it. + +use std::io::{Read, Write}; +use std::net::TcpListener; +use std::path::{Path, PathBuf}; + +const FLOWPROOF_BIN: &str = env!("CARGO_BIN_EXE_flowproof"); + +/// The deterministic stdio MCP server, logging every request it receives. +const FAKE_MCP_SERVER: &str = r#" +import json, sys +log = open(sys.argv[1], "a") +for line in sys.stdin: + line = line.strip() + if not line: + continue + msg = json.loads(line) + log.write(line + "\n"); log.flush() + mid = msg.get("id") + if mid is None: + continue + method = msg.get("method") + if method == "initialize": + result = {"protocolVersion": "2024-11-05", + "serverInfo": {"name": "weather", "version": "1"}, + "capabilities": {"tools": {}}} + elif method == "tools/list": + result = {"tools": [{"name": "get_weather"}]} + elif method == "tools/call": + result = {"content": [{"type": "text", "text": "REAL:" + msg["params"]["name"]}], + "isError": False} + else: + result = {} + sys.stdout.write(json.dumps({"jsonrpc": "2.0", "id": mid, "result": result}) + "\n") + sys.stdout.flush() +"#; + +fn fixture() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")) + .join("../../tests/falsifiability/fixtures/mcp-killing-agent.py") +} + +fn work_dir(name: &str) -> PathBuf { + let dir = std::env::temp_dir().join(format!("flowproof-fals-mcpkill-{name}")); + std::fs::remove_dir_all(&dir).ok(); + std::fs::create_dir_all(&dir).expect("work dir"); + dir +} + +fn read_http_request(stream: &mut std::net::TcpStream) -> String { + let mut buf = Vec::new(); + let mut chunk = [0u8; 1024]; + while let Ok(n) = stream.read(&mut chunk) { + if n == 0 { + break; + } + buf.extend_from_slice(&chunk[..n]); + let text = String::from_utf8_lossy(&buf).to_string(); + let Some(head_end) = text.find("\r\n\r\n") else { + continue; + }; + let len = text + .lines() + .find_map(|l| { + let (k, v) = l.split_once(':')?; + k.eq_ignore_ascii_case("content-length") + .then(|| v.trim().parse::().ok())? + }) + .unwrap_or(0); + if buf.len() >= head_end + 4 + len { + break; + } + } + String::from_utf8_lossy(&buf).to_string() +} + +/// Replies `done` to everything: enough to satisfy the model-boundary guard. +/// The MCP boundary is what is under test here, not the model one. +fn fake_model() -> String { + let listener = TcpListener::bind("127.0.0.1:0").expect("bind"); + let port = listener.local_addr().expect("addr").port(); + std::thread::spawn(move || { + for stream in listener.incoming().take(16) { + let Ok(mut stream) = stream else { continue }; + let _ = read_http_request(&mut stream); + let reply = serde_json::json!({ + "choices": [{"index": 0, "finish_reason": "stop", + "message": {"role": "assistant", "content": "done"}}] + }) + .to_string(); + let _ = stream.write_all( + format!( + "HTTP/1.1 200 OK\r\ncontent-type: application/json\r\n\ + content-length: {}\r\nconnection: close\r\n\r\n{reply}", + reply.len() + ) + .as_bytes(), + ); + let _ = stream.flush(); + let _ = stream.shutdown(std::net::Shutdown::Write); + } + }); + format!("http://127.0.0.1:{port}/v1") +} + +/// An agent that kills its stand-in must not take the recording with it. +#[test] +fn an_agent_that_kills_the_stand_in_still_leaves_a_recorded_lane() { + let dir = work_dir("kill"); + let agent_py = dir.join("agent.py"); + let server_py = dir.join("server.py"); + let log = dir.join("server.log"); + std::fs::copy(fixture(), &agent_py).expect("stage the hostile agent"); + std::fs::write(&server_py, FAKE_MCP_SERVER).expect("server"); + + let spec = dir.join("weather.flow.yaml"); + std::fs::write( + &spec, + format!( + "name: MCP weather, agent kills the stand-in\n\ + app: agent\n\ + agent:\n command: python3 {agent}\n\ + mcp:\n - name: weather\n command: python3 {server} {log}\n\ + steps:\n\ + \x20 - prompt: What is the weather?\n\ + \x20 - assert: reply contains done\n", + agent = agent_py.display(), + server = server_py.display(), + log = log.display(), + ), + ) + .expect("spec"); + + let out = std::process::Command::new(FLOWPROOF_BIN) + .arg("record") + .arg(&spec) + .current_dir(&dir) + .env("FLOWPROOF_AGENT_UPSTREAM", fake_model()) + .env("FLOWPROOF_AGENT_KEY", "not-a-real-key") + .env("FLOWPROOF_MCP_EXE", FLOWPROOF_BIN) + .output() + .expect("record with the hostile agent"); + + let stdout = String::from_utf8_lossy(&out.stdout).to_string(); + let stderr = String::from_utf8_lossy(&out.stderr).to_string(); + assert!( + out.status.success(), + "an agent that kills its stand-in is rude, not wrong: the record must \ + still succeed. stdout={stdout} stderr={stderr}" + ); + + // The real server WAS asked -- otherwise the exchange never happened and + // the lane would be legitimately empty, proving nothing. + let logged = std::fs::read_to_string(&log).expect("server log readable"); + assert!( + logged.contains("get_weather"), + "the exchange must actually have happened, or an empty lane is \ + vacuously 'preserved': {logged}" + ); + + // Layer 2: the lane survived the kill. A trace merely existing proves + // nothing -- the model cassette is written regardless, and an empty MCP + // lane beside it is exactly what the pre-0.8.0 defect produced. + let trace = dir.join("weather.trace.jsonl"); + let contents = std::fs::read_to_string(&trace).expect("trace readable"); + for needle in ["\"mcp\"", "\"weather\"", "initialize", "tools/call", "get_weather"] { + assert!( + contents.contains(needle), + "the MCP lane must survive an abrupt kill, missing {needle}: {contents}" + ); + } + assert!( + contents.contains("REAL:get_weather"), + "and the captured RESULT survived too, not just the request: {contents}" + ); + + std::fs::remove_dir_all(&dir).ok(); +} diff --git a/tests/falsifiability/fixtures/mcp-killing-agent.py b/tests/falsifiability/fixtures/mcp-killing-agent.py new file mode 100644 index 0000000..1bcd686 --- /dev/null +++ b/tests/falsifiability/fixtures/mcp-killing-agent.py @@ -0,0 +1,51 @@ +# Falsifiability fixture for the MCP stand-in's recording durability (#257). +# +# A HOSTILE agent, and hostile in exactly one way: it drives a normal MCP +# exchange and then KILLS the stand-in outright instead of closing its stdin. +# +# That single difference is the whole fixture. Before 0.8.0 the lane was +# written only at stdin EOF, so an agent that terminated its MCP subprocess +# abruptly never got there and the ENTIRE recording was lost. The fix persists +# the lane after every captured call, atomically. +# +# Nothing in the suite exercised it. Every other MCP test closes stdin politely +# and waits, which is precisely the path the defect did NOT affect — so all of +# them would stay green if the fix were reverted tomorrow. +# +# Do not "fix" this agent to shut down gracefully. Its rudeness is the evidence. +import json, os, shlex, subprocess, urllib.request + +here = os.path.dirname(os.path.abspath(__file__)) +base = os.environ["OPENAI_BASE_URL"] +prompt = os.environ["FLOWPROOF_PROMPT"] + +payload = json.dumps({"model": "gpt-4o", + "messages": [{"role": "user", "content": prompt}]}).encode() +req = urllib.request.Request(base + "/chat/completions", data=payload, + headers={"content-type": "application/json"}) +with urllib.request.urlopen(req) as resp: + reply = json.load(resp)["choices"][0]["message"].get("content", "") + +cmd = os.environ["FLOWPROOF_MCP_SERVER_WEATHER"] +proc = subprocess.Popen(shlex.split(cmd), stdin=subprocess.PIPE, stdout=subprocess.PIPE) + +def rpc(obj): + proc.stdin.write((json.dumps(obj) + "\n").encode()); proc.stdin.flush() + return json.loads(proc.stdout.readline()) + +def notify(obj): + proc.stdin.write((json.dumps(obj) + "\n").encode()); proc.stdin.flush() + +rpc({"jsonrpc": "2.0", "id": 1, "method": "initialize", + "params": {"protocolVersion": "2024-11-05", + "clientInfo": {"name": "killing-agent", "version": "1"}, + "capabilities": {}}}) +notify({"jsonrpc": "2.0", "method": "notifications/initialized"}) +rpc({"jsonrpc": "2.0", "id": 2, "method": "tools/list", "params": {}}) +weather = rpc({"jsonrpc": "2.0", "id": 3, "method": "tools/call", + "params": {"name": "get_weather", "arguments": {"city": "Nairobi"}}}) +print("WEATHER", json.dumps(weather)) + +# The violation: no stdin.close(), no wait(). SIGKILL, mid-session. +proc.kill() +print(reply) From 00c234000ed75d6266966749feceabd7bef89a20 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 31 Jul 2026 04:01:43 +0000 Subject: [PATCH 2/3] style: rustfmt the falsifiability_mcp_kill evidence test Formatting only. The single intended CI failure on this branch is the assertion that documents the finding, not a lint. Co-Authored-By: Claude Opus 5 --- crates/flowproof-cli/tests/falsifiability_mcp_kill.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/crates/flowproof-cli/tests/falsifiability_mcp_kill.rs b/crates/flowproof-cli/tests/falsifiability_mcp_kill.rs index 13692b2..922e5cb 100644 --- a/crates/flowproof-cli/tests/falsifiability_mcp_kill.rs +++ b/crates/flowproof-cli/tests/falsifiability_mcp_kill.rs @@ -182,7 +182,13 @@ fn an_agent_that_kills_the_stand_in_still_leaves_a_recorded_lane() { // lane beside it is exactly what the pre-0.8.0 defect produced. let trace = dir.join("weather.trace.jsonl"); let contents = std::fs::read_to_string(&trace).expect("trace readable"); - for needle in ["\"mcp\"", "\"weather\"", "initialize", "tools/call", "get_weather"] { + for needle in [ + "\"mcp\"", + "\"weather\"", + "initialize", + "tools/call", + "get_weather", + ] { assert!( contents.contains(needle), "the MCP lane must survive an abrupt kill, missing {needle}: {contents}" From 865ffc6c6f5cc6b1946c21fb39546c8b541f00ed Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 31 Jul 2026 04:24:38 +0000 Subject: [PATCH 3/3] fix(adapters): persist the MCP lane before the agent can see the response 0.8.0 fixed the stand-in losing its whole recording when an agent killed it, by persisting the lane after every captured call. It was not enough. The stand-in forwarded the server's response to the agent BEFORE persisting it. The moment the agent has a response it may kill the stand-in, so the final call of a session was lost -- while `record` still exited 0. A tool the agent really invoked was simply absent from the evidence, silently. Found by the falsifiability suite (#273), with the real server's own request log as the oracle: the server was asked for `tools/call get_weather`, the lane held only `initialize` and `tools/list`, and nothing said so. That matters more than a lost line. A lane that silently runs short UNDERSTATES what the agent did, and every assertion evaluated over it inherits the omission -- including a guard claim that a tool was never called. Capture and persistence now happen before the response is forwarded. By the time the agent can act on a response, the evidence for it is on disk. The mocked-tool path already had this ordering and never raced; only the forwarded path did. And a failed flush is no longer swallowed. The old code deliberately ignored it, on the reasoning that the write at stdin EOF might still save the run -- but that write is exactly what an abrupt kill skips, so it was never a fallback. A flush that fails now fails the record by name rather than minting a partial lane. Evidence lost silently is the one outcome this tool cannot ship. Ships with the test that found it, cherry-picked from the evidence branch unchanged: it failed on the old code and passes here. Closes #273 Closes #257 Co-Authored-By: Claude Opus 5 --- CHANGELOG.md | 25 ++++++++ crates/flowproof-adapters/src/mcp_stdio.rs | 67 ++++++++++++++-------- 2 files changed, 69 insertions(+), 23 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9a1cdef..9484bc4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,31 @@ together). ## Unreleased +### Fixed + +- **A tool call the agent really made could be missing from the evidence.** + 0.8.0 fixed the MCP stand-in losing its whole recording when an agent killed + it, by persisting the lane after every captured call. It was not enough. The + stand-in forwarded the server's response to the agent BEFORE persisting it, + and the moment the agent has a response it may kill the stand-in — so the + final call of a session was lost while `record` still exited 0. + + Found by the falsifiability suite, with the real server's own request log as + the oracle: the server was asked for `tools/call get_weather`, the lane held + only `initialize` and `tools/list`, and nothing said so. A lane that silently + runs short understates what the agent did, and every assertion evaluated over + it inherits the omission — including a guard claim that a tool was never + called. + + Capture and persistence now happen BEFORE the response is forwarded. That + ordering is the fix: by the time the agent can act on a response, the evidence + for it is already on disk. + + And a failed flush is no longer swallowed. With the write at stdin EOF no + longer load-bearing, an incremental flush that fails means evidence was lost, + so it now fails the record by name instead of minting a partial lane. Evidence + lost silently is the one outcome this tool cannot ship. + ### Changed - **A control that stopped being certifiable passed the gate.** diff --git a/crates/flowproof-adapters/src/mcp_stdio.rs b/crates/flowproof-adapters/src/mcp_stdio.rs index 856c24e..5cf9421 100644 --- a/crates/flowproof-adapters/src/mcp_stdio.rs +++ b/crates/flowproof-adapters/src/mcp_stdio.rs @@ -227,21 +227,26 @@ fn run_replay(plan: &McpPlan, out_path: &Path) -> Result<(), String> { /// Persist the captured lane NOW, so an abrupt shutdown cannot lose it. /// -/// The authoritative write is still the one at stdin EOF, but reaching it -/// requires the agent to close the stand-in's stdin and let it reap the real -/// server. An agent that terminates its MCP subprocess abruptly never gets -/// there - goose does exactly this - and the whole recording was lost, which -/// then read as "the agent never spawned flowproof's MCP stand-in": a false -/// negative pointing the adopter at wiring that was already correct. +/// This is THE durability guarantee, not a best-effort supplement to the write +/// at stdin EOF. Reaching EOF requires the agent to close the stand-in's stdin +/// and let it reap the real server; an agent that terminates its MCP +/// subprocess abruptly never gets there - goose does exactly this. +/// +/// It runs BEFORE the response is forwarded to the agent. That ordering is the +/// whole point: once the agent has the response it may kill the stand-in at +/// any moment, so anything not yet persisted is lost. Forwarding first left a +/// window in which the final call of a session vanished from the lane while +/// `record` still exited 0 (#273). /// /// `write_out_atomic` is a temp-file rename, so a partial flush is never -/// observable and the last one wins. Errors are swallowed: a failed -/// incremental flush must not break a run that the EOF write may still save. +/// observable and the last one wins. Errors are RETURNED rather than swallowed: +/// with the EOF write no longer load-bearing, a failed flush means evidence was +/// lost, and evidence lost silently is the one outcome this tool cannot ship. fn flush_lane( out_path: &std::path::Path, calls: &Mutex>, events: &Mutex>, -) { +) -> Result<(), String> { let captured: Vec = calls .lock() .unwrap_or_else(|e| e.into_inner()) @@ -249,14 +254,14 @@ fn flush_lane( .cloned() .collect(); let events: Vec = events.lock().unwrap_or_else(|e| e.into_inner()).clone(); - let _ = write_out_atomic( + write_out_atomic( out_path, &McpOut { calls: captured, events, ..Default::default() }, - ); + ) } /// RECORD: two threads bridge the agent and the REAL server. @@ -359,16 +364,12 @@ fn run_record(plan: &McpPlan, out_path: &Path) -> Result<(), String> { if line.trim().is_empty() { continue; } - // Forward the server's line to the agent verbatim, so record - // is transparent. - { - let mut out = write_lock.lock().unwrap_or_else(|e| e.into_inner()); - let _ = out.write_all(line.as_bytes()); - let _ = out.flush(); - } - // Classify the server line by the JSON-RPC shape. It was - // already forwarded verbatim above; here we decide what, if - // anything, to CAPTURE from it. + // Classify and CAPTURE first, then forward. The order is + // load-bearing: the moment the agent has the response it may + // kill the stand-in, so anything not yet persisted is lost. + // Forwarding first left a window in which the final call of a + // session vanished from the lane while `record` still exited 0 + // (#273). if let Ok(msg) = serde_json::from_str::(line.trim()) { let has_method = msg.get("method").and_then(Value::as_str); let has_id = msg.get("id"); @@ -413,12 +414,29 @@ fn run_record(plan: &McpPlan, out_path: &Path) -> Result<(), String> { result, }, ); - flush_lane(&out_path_b, &calls, &events); + if let Err(detail) = flush_lane(&out_path_b, &calls, &events) { + let mut slot = + record_error.lock().unwrap_or_else(|e| e.into_inner()); + if slot.is_none() { + *slot = Some(format!( + "the MCP lane for this server could not be \ + persisted, so the recording is incomplete: \ + {detail}" + )); + } + } } } (None, None) => {} } } + // Forwarded verbatim, and only now: record stays transparent + // to the agent, but never at the cost of the evidence. + { + let mut out = write_lock.lock().unwrap_or_else(|e| e.into_inner()); + let _ = out.write_all(line.as_bytes()); + let _ = out.flush(); + } } }) }; @@ -475,7 +493,10 @@ fn run_record(plan: &McpPlan, out_path: &Path) -> Result<(), String> { result: result.clone(), }, ); - flush_lane(out_path, &calls, &events); + // Already in the right order: the mocked answer is persisted + // before the agent is told, so this path never raced. It only + // needed the failure to stop being invisible. + flush_lane(out_path, &calls, &events)?; let mut out = write_lock.lock().unwrap_or_else(|e| e.into_inner()); write_result(&mut *out, &id, &result)?; } else {