A proof that the change did only what you asked. Or the input that breaks it, with the line to fix. Same change, same verdict, every time.
{
"unit": "applyAll",
"verdict": "WITNESS",
"input": 17,
"floor": -1,
"parent": { "posted": 1 },
"candidate": { "posted": 0 },
"where": "candidate.ts:15 <= where the parent had <",
"replay": "node langs/ts/check.mjs --seed 3 --n 60"
}Against the published reader, same 184 instances, same judge.
Recordings against the strongest reader, on 43 defects that passed review.
Each separated by an input lean found. None proved equal.
Proved or executed, across 36 repositories.
One repository we operate. A reviewer reads about ten a day.
The gate reads neither the change text nor any statement by its producer. It runs both versions and compares them.
917 changes in 13 days in one repository. The agent's account of a change never enters the verdict.
A gate in CI. Run it advisory first: one comment per pull request, updated on every push. Then block on WITNESS.
The benchmark ships with every judge verdict and both judge logs. A new language merges when it passes the conformance suite.
Each instrument compares two versions of the system and refuses on evidence. lean reports the strongest verdict the evidence supports.
The system runs under a fixed stimulus set before and after the change. A difference outside the selected scope is refused.
lean proves the candidate equal to the parent for every input and every world. A component finite by its types is explored to the end.
continue became a filter and a map. Equal_statement: true, 5 verified, 0 errors.For every artifact that is not a function, a predicate declared outside the change compares the two versions.
An input on which the two versions differ. lean draws it itself, and names the source line on each side.
<= where the parent had <.No difference found within a stated bound, and it says so. A bounded pass never becomes a proof. ASK names the construct.
Two builds on the same screens: pixels, layout and the accessibility tree. lean names the state where two renders differ.
The official pipeline, unchanged judge, three rounds. Both entries counted over the 184 instances both scored.
| Entry | Precision | Recall | F1 | Comments |
|---|---|---|---|---|
| DA + leanreader, gate, lean | 34.09+6.37 | 29.47−0.96 | 31.61+2.59 | 1,059−367 |
| Open Code Reviewthe published reader | 27.72 | 30.43 | 29.02 | 1,426 |
Percent, mean of three judge rounds. The readers ran on different models: ours on claude-opus-5-5 with a claude-opus-4-8 filter, the floor on claude-opus-4-6. A same-model run is scheduled. 12 of 196 instances unscored: 11 commits GitHub no longer serves, 1 reader failure.
Lane B needs only Node 24. Python 3 and Dafny 4 run the proof lane; without them lane A reports ASK.
The checkout holds the pairs the runs below use.
$ git clone https://github.com/NexusGPT/lean && cd lean
Parent, candidate, unit name. lean picks the lanes and draws the input.
$ node langs/ts/check.mjs --parent langs/ts/tests/pairs/readme_ledger/parent.ts --candidate langs/ts/tests/pairs/readme_ledger/candidate.ts --unit applyAll --no-project --n 60 --seed 3 --out ledger.json $ jq -c '.witness | {input, floor: .args[3], parent: .parent.outcome.returned.posted, candidate: .candidate.outcome.returned.posted}' ledger.json {"input":17,"floor":-1,"parent":1,"candidate":0}
Every click order from every prop assignment, to the end of its state space.
$ node langs/ts/check.mjs --parent langs/ts/tests/pairs/finite_components/parent.tsx --candidate langs/ts/tests/pairs/finite_components/candidate.tsx --unit Toggle --no-project --n 60 --out toggle.json PASS-decided -> toggle.json # every click order from every prop assignment, decided: 8 state pairs over 2 assignment(s)
docker build -t lean:local .An acceptance gate that reads neither the change text nor any statement by its producer.