docs: an adoption guide written to be handed to a coding agent - #181
Merged
Conversation
flowproof says it is written for developers and their agents, and ships
nothing that tells an agent how to adopt it. There is no `init`, no
AGENTS.md, no skill - so every adopter starts from the reference docs and
rediscovers the same path.
Two real adoptions now show what that path is, and both spent their entire
first session on the same reconnaissance before a spec was worth writing:
1. How is the agent started, and does the process that actually calls the
model inherit the environment? One stack was three processes deep with
the model call in the grandchild.
2. Where does the model client get its base URL? If it is not one of the
injected variables, it needs a `${flowproof.*}` handle, and which of the
two forms depends on whether the client appends its own `/v1`.
3. Which tools have side effects? That is the judgement call that decides
`tools:` versus `mcp:`, and getting it wrong means a RECORDING run
mutates real data.
So the guide leads with the audit and says outright not to write specs
until it is answered. Then one smoke flow, then the flows worth having in
value order, then CI.
It also states what these tests do NOT prove - that the model is any good -
because that is the easy overclaim, and an adopter who repeats it to their
team will be wrong in a way that costs trust.
Every claim in it was checked against the code by symbol before writing:
the injected variables, the three handles, the zero-capture guard, the
unprotected-tool warning, the `/mcp` substring match, `strict:`, and
`FLOWPROOF_BIN`. The example YAML parses.
Linked from README and getting-started, which is where an adopter or their
agent will look first.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The gap
flowproof says it is written for developers and their agents, and ships nothing that tells an agent how to adopt it:
record/run/capture/audit/healinitor audit-my-repoSo every adopter starts from the reference docs and rediscovers the same path.
What two real adoptions showed
Both spent their entire first session on reconnaissance, and both answered the same three questions before a spec was worth writing:
command:only helps if the child inherits.${flowproof.*}handle, and which form depends on whether the client appends its own/v1.tools:versusmcp:- and getting it wrong means a recording run mutates real data.That is the audit step, and it was being rediscovered every time. The guide leads with it and says outright not to write specs until it is answered. Then one smoke flow, then the flows worth having in value order, then CI.
It also says what these tests do not prove
That the model is any good. Its decisions are recorded, not judged. This is the easy overclaim, and an adopter who repeats it to their team will be wrong in a way that costs trust - so it is stated plainly, next to the honest version.
Verification
Every claim checked against the code by symbol before writing: the injected variables, all three
${flowproof.*}handles, the zero-capture guard, the unprotected-tool warning, the/mcpsubstring match,strict:, andFLOWPROOF_BIN. No unsupported claims. The example YAML parses through the real engine.Linked from README and getting-started, which is where an adopter or their agent looks first.
Change class
Docs only - self-merge class under the loop's mandate. No spec vocabulary, no behaviour change.
Deliberately not in this PR
A
flowproof initcommand. Most of the audit is judgement (isexport_to_endpointdestructive?), which a subcommand cannot do and an agent reading the codebase can. Ifinitis built later it should scaffold and report what it found - never generate specs from guesses. That is new CLI surface, so it wants a design pass rather than being slipped in here.🤖 Generated with Claude Code