Counterexamples and verified fixes

The search runs sequences of up to 12 steps, so the first sequence that breaks a rule usually carries steps and values that have nothing to do with the bug. The shrinker removes them in two passes:

1. Steps. Delta debugging removes parts of the sequence and runs each shorter candidate for real, on fresh entities. A candidate is kept only if it still breaks the same rule. Steps whose requirements are no longer met are dropped with it.
2. Values. Each param is moved toward its smallest or edge value for as long as the rule still breaks.

The result is minimal in a precise sense: take away any single step and the rule no longer breaks. Nothing is estimated; every candidate was executed against your running app.

A sequence that failed once might have been luck or timing. So the engine replays the exact minimal sequence 10 times by default, on fresh entities each time, and reports how many replays broke the rule.

• Every replay breaks the rule, shown as 10/10: a deterministic bug.
• Some replays break it and some do not: the counterexample is marked flaky and still reported, with its count. Bugs that need two requests at the same moment usually look like this.

The counterexample is then saved as a JSON file together with a regression test. The test is run on the unfixed code first and must fail there, which shows it tests the bug.

Every value here comes from a recorded Roook run on minishop, Roook's own small test shop: one of the two example repos you can run with Try Roook.

--- a/app.py+++ b/app.py     @app.post("/orders/{order_id}/refunds")     async def refund(order_id: int, body: NewRefund, user: CurrentUser) -> dict[str, int]:         order = get_order(order_id, user)-        # BUG 1 (buggy mode): each refund is compared with the amount paid on its own.-        already = order.refunded_total if is_fixed else 0+        already = order.refunded_total         if already + body.amount > order.paid:             raise HTTPException(400, "refund exceeds amount paid")         order.refunds.append(body.amount)

In this run the search first broke the rule with paid 50 and refunded 60. The shrinker tried shorter sequences, found that all 4 steps are needed, and cut the values down to 1. The fresh search in this recorded run used a smaller budget than the CLI's default.

A fix counts only if four checks pass, and all four are run by the engine, not judged by an AI:

1. Exact replay. The counterexample's steps are replayed on the fixed app, and the rule must hold in every replay.
2. Your project's tests. The fix must not break what already passed.
3. The generated regression test. It failed before the fix and must pass now.
4. A fresh search with a new seed. No approved rule may break. In the CLI the default budget is 20,000 sequences or 120 seconds, whichever comes first.

When a check fails, Roook goes back to the diagnosis with the new evidence, up to 3 times, and then reports honestly that the fix is not verified. Only a verified fix is committed to a rook/fix-* branch.

Every counterexample is saved as rook/counterexamples/cx_NNN.json, numbered from cx_001. It holds everything needed to replay the sequence exactly, and Roook never overwrites one that exists.

version

The file format, 1.

cx_id

The counterexample's id, such as cx_001. It is also the file name.

rule

The broken rule as it was when found: id, text, kind, scope, when and check.

steps

The minimal sequence. Each step has its action, actor and the exact params, plus refs: which earlier captured value each reference used. Steps sent at the same time are grouped under parallel.

violated_at_step

The step after which the rule was false, counted from 0.

observed

The values the engine read from your app at that point. Very large or deeply nested values are cut, and the cut is marked.

expected

The rule's check expression: what must be true.

reproduced

How many replays broke the rule, such as 10/10.

flaky

True when some replays broke the rule and others did not.

seed

The search seed the sequence was found with.

model_hash

A hash of the rook.yaml model it was found with.

created_at

When it was saved.

Three commands work on a saved counterexample, against an app you started yourself. None of them calls IBM Bob.

rook explain cx_001
rook replay cx_001 --base-url http://127.0.0.1:8000
rook verify cx_001 --base-url http://127.0.0.1:8000

rook explain

Prints the rule, the minimal steps, the step where the rule broke, the observed values and the replay count. It needs no running app.

rook replay

Runs the exact steps against your app, 10 times unless you pass rook replay cx_001 --base-url http://127.0.0.1:8000 --times 3. Exit code 1 while the rule is still broken, 0 when it held in every replay, 2 when the replay proves nothing or the arguments are wrong.

rook verify

Runs two of the four checks on your app: the exact replay and a fresh search (2,000 sequences or 60 seconds by default; change them with rook verify cx_001 --base-url http://127.0.0.1:8000 --sequences 20000 --seconds 120). Exit code 0 when both pass. Your project's tests and the regression test are not run by this command: they run inside the sandbox during rook run.

• The counterexample is an id, looked up in rook/counterexamples/ of the current folder, or a path to its .json file. Pass rook explain cx_001 --repo ~/.rook/workspaces/<run-id> to look in another folder, such as the workspace of a run on a local folder.
• The model is read from rook/rook.yaml in the same folder, or from the file you name: rook explain cx_001 --model ./rook/rook.yaml.
• The app address must be a loopback address on your machine, such as http://127.0.0.1:8000. Anything else is refused.
• Values the model reads from the environment come from variables named ROOK_ENV_ plus the name, such as ROOK_ENV_ADMIN_PASSWORD.

In the web app, replaying a counterexample and downloading its test are not built yet.