Skip to content

0.8.0: two more third-party defects fixed, docs corrected, version bumped - #184

Merged
AminChirazi merged 4 commits into
mainfrom
claude/flowproof-goose-adoption-hiwd67
Jul 27, 2026
Merged

0.8.0: two more third-party defects fixed, docs corrected, version bumped#184
AminChirazi merged 4 commits into
mainfrom
claude/flowproof-goose-adoption-hiwd67

Conversation

@AminChirazi

Copy link
Copy Markdown
Contributor

Three commits: two behavioural fixes from the goose campaign, then the release bump that lets any of it reach an adopter.

The fixes

The MCP stand-in lost its whole recording when the agent killed it. The lane was written only at stdin EOF, which needs the agent to close the stand-in's stdin and let it reap the real server. goose terminates its MCP subprocess before that, so the recording was lost and the record failed. Now the lane is persisted after every captured call — write_out_atomic is a temp-file rename, so a partial flush is never observable and the last write wins.

This composes with #178's fix rather than duplicating it: that one is diagnosis (splitting "no out file" from "empty lane" so the message stops asserting a cause it cannot know), this one is behavioural (the record succeeds instead of needing a better error). #178's message even names the cause this fixes — "If the stand-in DID run, it was killed before it could write."

The unprotected-tool warning now understands MCP tool namespacing. A client normally namespaces a server's tools, so a tool intercepted under mcp: as delete_all reaches the model as files__delete_all. Comparing literally warned that a correctly intercepted tool was unprotected — the worst false positive for this particular warning, since an adopter who learns to ignore it stops reading the true ones. Matching is now on a namespace separator (__, ., /, :) and never a bare substring; two tests pin both halves, because silencing a real warning would be worse than the false positive.

Docs

Corrected one this campaign made stale. mcp_stdio's module header still said the lane is "written ATOMICALLY at stdin EOF". It now says it is also rewritten after every captured call, and why.

Added two limits to docs/adopting.md that the campaign measured and the guide did not have:

  • An agent that stamps wall-clock time into its prompt cannot replay under byte-exact matching. This was the single largest blocker with goose. Documented with the libfaketime workaround, the mandatory FAKETIME_DONT_FAKE_MONOTONIC=1 (or the agent hangs forever), the fact that it is Linux-only, and the cheap Step-1 detection: record twice and diff.
  • The tool name an assertion matches is the model-boundary name, not the MCP name — read it off a recorded trajectory, because a guard asserting a name that never appears passes for the wrong reason.

The version bump

Cargo.toml, sdk/js/package.json (including the four platform packages) and sdk/python/pyproject.toml move together, so the versions-agree gate passes.

This closes D4. Released 0.7.0 contains none of the six fixes, which is why no CI job for the goose suite could honestly be committed — a job pinned to the release would fail, one pinned to a local build would not be testing the release. A 0.8.0 release makes that job possible.

CHANGELOG.md records all six defects, with the measurements.

Verification

  • cargo test --workspace --all-features: 649 passed, 0 failed. cargo fmt --check clean.
  • One earlier run reported a single failure that did not reproduce across three subsequent full runs. Recording it as a flake rather than pretending it did not happen.

Standing

3 of 4 goose flows green. Flow 3 still does not replay, and its blocker is measured, not guessed: at replay goose is offered [] tools against [flowproof__delete_all, flowproof__list_files] recorded. That is the next target.


Generated by Claude Code

claude added 3 commits July 27, 2026 09:48
…n EOF

An agent that terminates its MCP subprocess abruptly lost the ENTIRE recording,
and flowproof then blamed the adopter's wiring for it.

The stand-in writes <server>.out.json atomically at stdin EOF, after joining its
pump threads and reaping the real server. goose kills its MCP subprocess before
that point, so the write never happened. The orchestrator read the missing file
and reported "the agent never spawned flowproof's MCP stand-in; its config still
points at the real server" — which is the most expensive shape of wrong error
message, because it sends you to debug the one thing that is working.

Measured in two commands rather than reasoned about. Listing the run dir straight
after goose exits showed only files.plan.json; four seconds later still no
out.json, and no stand-in process alive. Separately, the real server's parent
process is "flowproof mcp-stdio --server files" — the stand-in — so it had
spawned, served tools/list and a tools/call, and forwarded to the real server
before dying. An earlier suspicion that flowproof's double-quoted executable path
broke goose's --with-extension parsing was wrong; goose dequotes it fine.

Fix: flush the captured lane after each captured call, at both capture sites.
write_out_atomic is a temp-file rename, so a partial flush is never observable and
the last write wins; an abrupt kill can no longer lose the recording. The EOF
write stays authoritative.

Full suite: 642 passed, 0 failed. fmt clean.

Flow 3 now RECORDS but is NOT green, and is committed saying so: goose namespaces
MCP tools (delete_all -> flowproof__delete_all) so the unprotected-tool check
false-positives on a correctly intercepted tool, and replay diverges differently
each run. Both are written up as open in tests/flowproof/LOOP.md. The mcp:
boundary itself held: the destructive tool's marker file never appeared.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wy4h95hiVfoAnf5kKovtyu
…espacing

An MCP client routinely namespaces a server's tools before offering them to the
model, so a tool intercepted under `mcp:` as `delete_all` reaches the model
boundary as `files__delete_all`. The check compared the two names literally and
warned that a CORRECTLY intercepted tool was unprotected.

That is the worst kind of false positive for this warning specifically: it fires
on exactly the flows that did the right thing, and an adopter who learns to ignore
it stops reading the true ones.

The fix matches only on a namespace SEPARATOR (__, ., /, :) and never on a bare
substring, so a genuinely unprotected tool is still named. Two tests pin both
halves: files__delete_all, files.delete_all, files/delete_all and
files:delete_all ARE the intercepted delete_all; soft_delete_all, predelete_all,
delete_all_now, __delete_all and .delete_all are NOT. Silencing a real warning
would have been a worse outcome than the false positive.

644 passed, 0 failed. fmt clean.

Flow 3 still does not replay, and its blocker is now measured rather than guessed:

  turn 2: tools offered changed
    recorded: [flowproof__delete_all, flowproof__list_files]
    replayed: []

At replay goose is offered no tools at all, so the stand-in is not serving the
tool list in replay mode or the handshake never completes. Written up in
tests/flowproof/LOOP.md as the next iteration's target, with the alternating
"message 0 (system) content changed" failure flagged as INFERRED to be the same
cause one turn earlier.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wy4h95hiVfoAnf5kKovtyu
Bumps Cargo.toml, sdk/js/package.json (including the four platform packages)
and sdk/python/pyproject.toml together, so the versions-agree gate passes and a
release can finally carry the fixes. This closes D4 from the goose campaign: the
released 0.7.0 contained none of them, so no CI job for that suite could honestly
be committed.

Also corrects a doc this campaign made stale. mcp_stdio's module header still
said the lane is "written ATOMICALLY at stdin EOF"; it is now also rewritten
after every captured call, and the header says so and says why.

And adds two limits to docs/adopting.md that the campaign measured and the guide
did not have: an agent that stamps wall-clock time into its prompt cannot replay
under byte-exact matching (with the libfaketime workaround, its mandatory
FAKETIME_DONT_FAKE_MONOTONIC, and the fact that it is Linux-only), and the tool
name an assertion matches is the model-boundary name, not the MCP name, so it
must be read off a recorded trajectory rather than guessed.

Rebased onto main, which had landed its own D7 fix. That one is diagnosis — it
splits "no out file" from "empty lane" so the message stops asserting a cause it
cannot know. This branch's is behavioural: the lane survives an abrupt kill, so
the record succeeds instead of needing a better error. They compose.

649 passed, 0 failed, fmt clean. One earlier run reported a single failure that
did not reproduce across three subsequent full runs; recording it here as a flake
rather than pretending it did not happen.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wy4h95hiVfoAnf5kKovtyu
Copilot AI review requested due to automatic review settings July 27, 2026 10:04

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

CI caught what my search missed. sdk/python/flowproof/__init__.py carries
__version__ independently of pyproject.toml, and I bumped three manifests by
grepping for them ad hoc instead of using the canonical list the "versions agree"
job already maintains.

Two independent guards caught it — the versions-agree gate and
test_every_version_location_agrees — which is the system working as designed.

Verified this time by running CI's own check verbatim against every location it
lists: pyproject.toml, __init__.py, package.json, all four platform packages, and
Cargo.lock. All 0.8.0, exit 0.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Wy4h95hiVfoAnf5kKovtyu
@AminChirazi
AminChirazi merged commit e50f975 into main Jul 27, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants