Monday's arxiv list had the usual crop of new benchmarks, and I nearly scrolled past another one built on SWE-bench Verified. This one doesn't add tasks. It puts machine-checked proofs behind the 500 that already exist, then counts how many "resolved" patches survive. Fewer than the leaderboard says. It also puts the core idea of spec-driven development to a real test, and the answer cuts both ways. My thesis: the leverage is in the spec, and agents can't yet write a faithful one.
What it does#
SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs? by George Ma, Benjamin Mikek, Haoyu Li and colleagues at UC Berkeley, Georgia Tech, UIUC and AWS AI Labs introduces Benchproofer. It's a pipeline that takes a coding task with a known-good patch and turns it into a formally verified one. Verified code generation isn't new, but earlier work stuck to small standalone exercises where someone hands the model a formal spec. Real issues live in large repos and state their intent in vague prose. Benchproofer copes by modeling only the new or changed code. Every unchanged function that code calls gets summarized as axioms, and those axioms are fuzzed against the real function. An instance is admitted only after it clears two kinds of gates. The mechanical ones check that the reference implementation verifies, that the pre-fix code fails, and that mutants fail. In the adversarial ones, LLM auditors try to break the spec with concrete counterexamples.
The result covers all 500 SWE-bench Verified instances under three verification tools: Nagini for Python, Velvet (a Lean-based language) and plain Lean. It also carries over to 242 of the 266 Python tasks in SWE-bench Pro. The authors then run Claude Opus 4.8 and GPT-5.5 through a grid of settings in one SWE-agent-style scaffold with the same prompts and budgets. The settings vary what the agent is given: a verifier tool, the edit locations, the ground-truth spec, or an instruction to write its own. As a non-formal control, each spec also comes as structured natural-language requirements in EARS, the notation many spec-driven tools use. That's 53,500 agent episodes in total.
The key result#
Start with the baseline. By the official tests, Opus 4.8 resolves 85.0% of instances and GPT-5.5 resolves 81.2%. The authors then aim an adversarial auditor at every passing patch. Its job is to write a new test that fails on the agent's patch and passes on the ground-truth one. Tests that check behavior the issue never required are thrown out. After that audit, Opus falls to 58.2% and GPT-5.5 to 33.4%. A quarter to a half of test-passing patches are still wrong. In one setting where each violation was confirmed mechanically against the formal ground truth, 29.0% of Opus's resolved patches and 50.3% of GPT-5.5's had one. Now the other half of the story. Give the agent the correct formal spec plus a verifier, and resolution rises from 85.0% to 95.1% for Opus and from 81.2% to 94.7% for GPT-5.5, averaged over the three tools. Most of that isn't just the spec revealing where to edit: against giving the edit locations alone, the spec still adds 6.9 and 7.7 points. Ask the agent to write the spec itself and the gain disappears. The best of six settings beats the baseline by 0.6 points. Only about 62% of self-written specs pass the audit. The main failure is faithfulness: the spec is correct about the functions it models but models too few of them.
Why it matters#
If your agent loop treats "tests pass" as done, and every Claude Code setup I've built does, this paper puts a number on how often that's a false positive. That's on well-curated tasks, too. You don't need Lean to act on it. The audit is a pattern you can copy tomorrow: once the tests go green, spawn a sub-agent whose only job is to write a test the patch fails. Give it the issue text, not the implementer's reasoning, so it isn't anchored on the same assumptions. Count a failure only if the test checks something the issue actually requires, which is the audit's own rule against invented requirements. It's cheap next to a bad merge. It also changes what "done" means, from "passed the tests I happened to have" to "survived an adversary."
The spec findings matter even more for spec-driven development. The good news: a correct spec is worth about ten points on a benchmark where frontier models already sit in the mid-80s. The bad news: the agent can't produce that spec on its own. Prompting "write a spec, then implement against it" buys nothing, because the spec quietly leaves part of the behavior unconstrained and the code then verifies against the part that's left. EARS doesn't rescue it either. With a structured natural-language spec, tests pass even more often. But 17.8 points of Opus's pass rate and 46.0 of GPT-5.5's are patches that still differ from the correct fix. Structure without a checker is just formatting. So in a spec-driven workflow, the human review of the spec is the step that matters, and the question needs to change. Not "is each requirement right?", because models mostly get that part right, but "what behavior did this spec leave out?" Then back each requirement with something a machine checks: a property test, a contract, a type. One more detail: when told to both formalize and patch, Opus edits the repo before its spec verifies in about three quarters of episodes. GPT-5.5 formalizes first about two thirds of the time. Outcomes barely differ. So don't build hooks that force the spec to come first. Put that effort into checking what the spec covers.
The caveats#
Two models, one research scaffold. Neither Claude Code nor Codex CLI was in the loop, and production harnesses with their own habits around running tests could move these numbers.
The headline audit is run by LLMs. It has safeguards: it can only lower grades, it throws out invented requirements, and one setting confirms it mechanically at 29–50%. It's still evidence, not proof, and "behaves differently from the reference patch" is a stricter bar than "wrong for users."
The 95% is a ceiling. The ground-truth specs were written with the gold patch in hand and then attacked with hundreds of millions of executions of real repository code. Nobody gets a spec like that for free on an ordinary ticket.
Python only, and the axioms describe the unchanged code only loosely. 24 SWE-bench Pro tasks (renames, signature changes, side effects) couldn't be modeled. A release is promised but not linked yet.
The takeaway#
I'm filing SWE-Proof under "the oracle problem finally has a number." Green tests are a minimum bar, not proof the patch is right. In spec-driven development, what matters is whether the spec is faithful, not what format it's written in. Here's what I'm changing: my agent loops get a counterexample sub-agent that runs after the tests pass, and my spec reviews now start with one question. What did we leave unconstrained?