Ensuring the correctness of LLM‑generated code is a core challenge for modern software engineering. Existing agentic code‑generation benchmarks rely on held‑out test suites, which are inherently incomplete and increasingly vulnerable to memorization. Formal verification avoids both issues, yet prior work only covers standalone tasks whose specifications are provided as input, and cannot handle real issues that span large repositories and express intent in vague natural language. We introduce the Benchproofer pipeline, which turns a coding task with a known correct patch into a formally verifiable one: it writes a specification for the new code, summarizes the existing functions it calls with axioms, and admits an instance only after both mechanical and adversarial gates agree. Applying it to SWE‑bench Verified yields SWE‑Proof, a collection of 500 real issues whose correctness is formally verified rather than merely tested, and it can be extended to SWE‑bench Pro. Across two frontier models, verification catches errors missed by tests: roughly a quarter to a half of test‑passing patches admit counterexamples, structured natural‑language specifications do not fix this, while a correct formal specification lifts Opus 4.8’s resolution rate from 85% to 95%. Writing the specification is the hard part: models that must generate their own specifications gain nothing over an unaided baseline, and only 62% of their specifications pass our audit. The dominant failure mode is faithfulness—a specification that constrains part of the required behavior while leaving the rest free. Specification quality still correlates with outcome, failing on 89% of unresolved instances versus 47% of resolved ones, making faithful specification synthesis a concrete open problem.
Review