Positioning: one promise, one reader — and a second mode for the question replay can't answer
I read the README end to end, then again to check I'd understood it. That second pass is the problem I want to describe. Two parts: a positioning argument with a concrete rewrite, and a feature request that the README itself already argues for.
Part 1 — The README makes a technical reader work too hard
What happens on first read
The opening line is flowproof produces evidence that a control still holds.
That sentence is true and it is precise, and it asks the reader to already own the word control. A compliance lead owns it. The engineer who is about to let an agent click through SAP does not — they have a fear, not a vocabulary. So the first line lands as abstract, and the reader starts scanning for the concrete thing.
They then have to assemble the actual promise from four places:
- paragraph 2 has the mechanism (record once, replay with zero LLM calls),
- paragraph 3 has the reach (web, Windows, SAP GUI, Citrix, HTTP),
- How it works has the category claim (Selenium → Robot Framework → Playwright → flowproof),
- Two kinds of claim has the fear — and it is the best writing in the document.
That lineage paragraph is where the generic framing does real damage. Positioned as the next step after Playwright, flowproof is a general browser/RPA automation framework, and it is read against Playwright and Tosca, on their terms, where "deterministic to execute and cheap to review" is a nice-to-have. Positioned as proof that an agent with real system access hasn't started misbehaving, it is read against nothing — the eval vendors can't see SAP GUI, and the RPA suites can't see the model boundary. The lineage story is a genuinely good slide. It is a bad opening, because it invites the wrong comparison.
The other cost: assert_no_tool_call, the sharpest thing in the project, is first mentioned in a parenthetical under the GIF and only explained in section 3.
The ask: one promise, one reader, one before-and-after
Cut the opening to a single reader — the engineer who has to sign off on an agent touching a production system — and lead with what they are afraid of, not with how the engine works. Mechanism is the second paragraph's job, and only as far as it makes the promise believable.
Concrete rewrite
flowproof
Your agent behaved today. Prove it'll behave tomorrow.
AI agents don't just call APIs anymore — they click through real systems, including the old ones nobody gave an API. That's power, and it's risk. flowproof captures what your agent does in one recording, then replays it on every commit with zero model calls. Define the lines it must never cross — the wrong tool, a system it shouldn't reach — and the build breaks the instant one is crossed. Not a suite you hope still passes. Evidence, every push.
Everywhere your agents work: web, desktop, SAP, Citrix.
Then keep the current opening paragraphs as the second section, where "control" arrives with the reader already leaning in. The lineage graphic keeps working under How it works — as supporting history rather than as the category claim.
One thing to preserve. "Lines it must never cross" reads as a cannot, and the README is careful — rightly — that assert_no_tool_call is a did not, re-checked on every change. Either pair the headline with the enforcement path (allow_egress + assert_no_egress on Linux) or make the second paragraph carry "re-proved on every commit" as it already does. Don't let the punchier copy quietly collapse the two-kinds-of-claim distinction; that distinction is a credibility asset, not a caveat.
Part 2 — Feature request: a hybrid live mode
The gap, in the README's own words
This is regression evidence, not proof of impossibility: a model that behaved on the day you recorded is not a model that always will.
That is exactly right, and it defines the shape of the missing half. Deterministic replay is the right backbone — it is cheap, it is honest, it is the only thing you can afford on every push. But replay never thinks. It proves the recorded path didn't break. It cannot surface new misbehavior on:
- a rephrased prompt — same intent, wording the recording never saw,
- changed data — a different order number, an empty result set, a hostile field value,
- an updated model — the one change most likely to break a behaviour claim, and the one replay is structurally blind to, because the cassette answers instead of the model.
Today a provider ships a new default model and every flowproof suite stays green. That green is accurate about what it measures and misleading about what a reader will take from it.
The proposal: two questions, two tools
| Question |
Mode |
Cost |
Where it runs |
| Did my known-good behavior break? |
run — deterministic replay |
zero model calls |
every commit |
| Can my agent be made to misbehave on something new? |
exploratory live mode |
real model calls |
nightly, pre-release, on model bump |
Sketch, deliberately reusing what exists:
- Same flow file, no cassette.
flowproof explore <flow> executes against the real model, with the same assert_no_tool_call / assert_no_secret_leak / assert_no_egress assertions the recorded flow already declares. The controls are already written down; this just stops replaying them and starts testing them.
- Input mutation. Paraphrase the
prompt: step N ways; perturb tools: results (empty, oversized, adversarial strings); vary ${VAR} data from a small corpus. Report per-variant, not pass/fail on the aggregate.
- Containment makes it safe to let it fail. This is the part flowproof is unusually well placed for: on Linux the seccomp filter and MCP stand-ins mean an exploratory run can be allowed to misbehave without touching a real system. Most eval tooling has to simulate that. flowproof enforces it.
- The loop that makes it worth building: any live violation is captured as a recording and promoted into the deterministic suite. Exploration finds it once; replay pins it forever. That closes the circle back to
flowproof audit --since rather than sitting beside it.
Framed for the README: replay is your regression proof, explore is your adversary. Two questions, two tools, one spec format — and it stays honest about which claim each one supports.
Happy to open a separate issue for either half, or to send a PR for the README rewrite if the direction is welcome. Thanks for a genuinely well-written project — the "Two kinds of claim" section is the reason I bothered to write this much.
Positioning: one promise, one reader — and a second mode for the question replay can't answer
I read the README end to end, then again to check I'd understood it. That second pass is the problem I want to describe. Two parts: a positioning argument with a concrete rewrite, and a feature request that the README itself already argues for.
Part 1 — The README makes a technical reader work too hard
What happens on first read
The opening line is
flowproof produces evidence that a control still holds.That sentence is true and it is precise, and it asks the reader to already own the word control. A compliance lead owns it. The engineer who is about to let an agent click through SAP does not — they have a fear, not a vocabulary. So the first line lands as abstract, and the reader starts scanning for the concrete thing.
They then have to assemble the actual promise from four places:
That lineage paragraph is where the generic framing does real damage. Positioned as the next step after Playwright, flowproof is a general browser/RPA automation framework, and it is read against Playwright and Tosca, on their terms, where "deterministic to execute and cheap to review" is a nice-to-have. Positioned as proof that an agent with real system access hasn't started misbehaving, it is read against nothing — the eval vendors can't see SAP GUI, and the RPA suites can't see the model boundary. The lineage story is a genuinely good slide. It is a bad opening, because it invites the wrong comparison.
The other cost:
assert_no_tool_call, the sharpest thing in the project, is first mentioned in a parenthetical under the GIF and only explained in section 3.The ask: one promise, one reader, one before-and-after
Cut the opening to a single reader — the engineer who has to sign off on an agent touching a production system — and lead with what they are afraid of, not with how the engine works. Mechanism is the second paragraph's job, and only as far as it makes the promise believable.
Concrete rewrite
Then keep the current opening paragraphs as the second section, where "control" arrives with the reader already leaning in. The lineage graphic keeps working under How it works — as supporting history rather than as the category claim.
One thing to preserve. "Lines it must never cross" reads as a cannot, and the README is careful — rightly — that
assert_no_tool_callis a did not, re-checked on every change. Either pair the headline with the enforcement path (allow_egress+assert_no_egresson Linux) or make the second paragraph carry "re-proved on every commit" as it already does. Don't let the punchier copy quietly collapse the two-kinds-of-claim distinction; that distinction is a credibility asset, not a caveat.Part 2 — Feature request: a hybrid live mode
The gap, in the README's own words
That is exactly right, and it defines the shape of the missing half. Deterministic replay is the right backbone — it is cheap, it is honest, it is the only thing you can afford on every push. But replay never thinks. It proves the recorded path didn't break. It cannot surface new misbehavior on:
Today a provider ships a new default model and every flowproof suite stays green. That green is accurate about what it measures and misleading about what a reader will take from it.
The proposal: two questions, two tools
run— deterministic replaySketch, deliberately reusing what exists:
flowproof explore <flow>executes against the real model, with the sameassert_no_tool_call/assert_no_secret_leak/assert_no_egressassertions the recorded flow already declares. The controls are already written down; this just stops replaying them and starts testing them.prompt:step N ways; perturbtools:results (empty, oversized, adversarial strings); vary${VAR}data from a small corpus. Report per-variant, not pass/fail on the aggregate.flowproof audit --sincerather than sitting beside it.Framed for the README: replay is your regression proof, explore is your adversary. Two questions, two tools, one spec format — and it stays honest about which claim each one supports.
Happy to open a separate issue for either half, or to send a PR for the README rewrite if the direction is welcome. Thanks for a genuinely well-written project — the "Two kinds of claim" section is the reason I bothered to write this much.