When a coding agent’s patch passes every test in the repository, the ticket gets closed. This paper rebuilt 500 real issues so that correctness is decided by a machine-checked proof against a written specification instead of by the test suite — and the same patches, all of which passed all hidden tests, stopped holding up. Resolution fell from 85.0% to 58.2% for the stronger model and from 81.2% to 33.4% for the other. Hand a model the correct specification and it gets back to 96%; ask it to write its own and it gains nothing at all.
Every agentic coding benchmark, and almost every internal one, defines “resolved” the same way: apply the model’s patch, run the repository’s tests, count the issues where the previously failing tests now pass and nothing else broke. That definition is doing quiet work. It says the tests encode what the fix was supposed to do. The authors took 500 issues that had already been scored that way and re-decided them against a formal specification and a machine-checked proof, and a large slice of the resolved column did not survive.
Flip the audit on. Then put your own backlog through it.
The gap is not a model quality story. Both models wrote patches that satisfied every test the maintainers had written, and on plenty of instances those patches were genuinely right. The measurement is what changed: 26.8 points of the stronger model’s tally and 47.8 points of the weaker one’s were patches that passed everything and still admitted a concrete input on which they differ from the reference fix. Nothing in the pipeline could have told you which ones.
The reason a passing suite is weak evidence is not sloppiness, it is arithmetic. A test fixes one input and checks one output. A specification is a statement about all inputs — a precondition and a postcondition the implementation has to satisfy everywhere — and a verifier either produces a proof or hands back the input where it breaks. If a patch is wrong on a thin slice of the input space, the suite catches it only if someone happened to write a case that lands in that slice.
Widen the broken slice, add test cases, and watch how much sampling it takes to be confident.
This is where the paper’s concrete failures live. Step through three shapes of patch that pass a reasonable suite and still differ from the reference fix.
The obvious objection to all of this is that formal specifications are hand-written by experts and there are 500 issues. The paper’s answer is a pipeline — Benchproofer — that drafts the artefacts with an agent and then refuses to admit any instance until a battery of independent gates agree. The agent doing the drafting sees the ground-truth patch, the buggy code and the test lists; the models being evaluated later never do.
Step through the stages. The gate list below lights up as the instance reaches them.
Three backends carry the proofs, and the paper keeps them separate on purpose: Nagini verifies a statically typed subset of Python through a solver, Velvet is a small imperative language checked inside a proof assistant, and the third route discharges obligations with proofs the agent writes itself. An instance that only passes under one backend is a fact about that tool. Results that hold across all three are a fact about the patch.
Once correctness is decided by proof, the experiment splits cleanly. Give the model a verifier tool and let it write its own specification to check against, and nothing happens — resolution moves between −1.0 and +0.6 points against the plain baseline. Give it the gold specification and the same model resolves around 94–96% of issues. The tool was never the bottleneck; knowing what “correct” means was.
So the interesting question becomes what is wrong with the specifications the models write. The paper audits every synthesised specification against five properties, and one failure mode dominates every other by a factor of three to ten: faithfulness — a specification that constrains part of the required behaviour and leaves the rest free. It is not that the models write false statements. They write true statements that are too weak, which is exactly what a thin test suite is.
And the two halves join up. Across the instances the models failed to resolve, 89% of their self-written specifications also failed the audit; across the ones they resolved, 47% did. Whatever makes a model able to fix an issue is close to whatever makes it able to say what fixing it would mean.
Nobody is putting a proof assistant in front of their agent’s pull requests this quarter. The transferable part is cheaper: the paper shows that the gap between “tests pass” and “behaviour is right” is large, measurable, and closed by writing down the property rather than by buying a better model. A property-based check — one statement, quantified over generated inputs — is the version of this you can ship today, and it sits in the same slot in the loop.
Set how thin your acceptance checks are, then add the cheap oracles one at a time.
The numbers in that panel are illustrative — they follow the paper’s shape, not its measurements. What is not illustrative is the ordering it encodes: a second model reviewing the diff is the weakest of the three oracles, because it shares the first model’s idea of what the issue asked for. The differential check and the property check are cheaper and they disagree with the patch for reasons the patch’s author cannot talk them out of.