Benchmarks · 2026
Can a model write code a proof checker accepts?
A benchmark that strips the proof annotations from verified Dafny, asks a model to restore them, and runs the result through a real verifier behind a gate that cannot be fooled by weakening the specification.
Most code benchmarks ask whether output looks right, or whether it passes tests someone wrote. A proof checker is a harsher and more honest grader: either the obligations discharge or they do not, and there is no partial credit for plausible-looking reasoning.
The task is annotation-infill. Each problem is a verified Dafny method; the invariant, decreases and assert lines are stripped out, and the model has to restore enough of them that dafny verify succeeds.
The obvious way to cheat
A model asked to satisfy a verifier has an easier move than proving the thing: weaken what it is being asked to prove. Delete a postcondition, loosen a precondition, add assume, and the obligations discharge trivially. A naive harness records a pass.
So the gate runs before the verifier and judges soundness rather than text. The model's method body is extracted and stitched back onto our canonical header — original signature, original requires, original ensures — and that recomposed program is what gets verified.
1. TRUNCATED? stop_reason == max_tokens and output unusable
2. UNSOUND? assume · {:axiom} · {:verify false} · decreases * · assert false
3. SEMANTIC INTEGRITY body = split_method(output)
stitched = canonical_header + body
dafny verify(stitched)
4. classify
Whatever the model did to the specification is discarded. It only gets credit for proving the problem it was given.
The frontier saturates it
With that gate in place, Opus 4.8 went 210/210 — a 95% Wilson interval of [0.98, 1.00]. Six of the seven problems sit at 100% for every model and every prompt.
A saturated benchmark is a negative result about the benchmark, not a positive one about the models. The write-up says so, rather than reporting the ceiling as a finding.
The Oracle Limit
The suite saturates for a structural reason. Every problem needs a verified reference solution, because the canonical header comes from it. So the benchmark can only be as hard as the proofs I could author correctly by hand.
The real failure boundary sits above that line, in proofs too complex to cheaply write references for. Any benchmark built this way inherits the same ceiling. If you are about to build one, that is the constraint to design around.
Where feedback helps, and where it does not
The extension loop hands verifier errors back to the model and lets it retry. The split is sharp: fluency failures repair, reasoning failures do not.
If the model had the right idea and expressed it wrongly, the error message is enough. If it had the wrong idea, showing it the error again does not supply the right one. That distinction is the useful output of the project: it tells you which failures an agentic loop can be expected to absorb.