Language models help formally verify real software fixes accurately
SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
Machine LearningArtificial IntelligenceSoftware Engineering
Summary
Ensuring that code generated by AI models works correctly is a big challenge because simple testing can miss errors or copy memorized code. The authors created Benchproofer, a system that turns typical code fixes into problems that can be formally checked with proofs, making sure the fixes really work as intended. They tested it on 500 real software issues and found that many fixes passing tests actually had errors caught by formal verification. Writing the precise formal specifications remains difficult and is a key challenge to solve.
What this means in practice
- •For software engineering teams: Use formal verification with Benchproofer to ensure real-world code patches are truly correct, beyond relying on incomplete test suites.
- •For automated code generation developers: Improve AI code generation tools by integrating formal verification to catch errors test suites overlook during code fixes.
Authors
George Ma, Benjamin Mikek, Haoyu Li, Ferhat Erata, Yuhao Zhang, Zeren Shui, Behrooz Omidvar Tehrani, Jun Huan, Murali Krishna Ramanathan, Somayeh Sojoudi, Hao Zhou, Anoop Deoras
Abstract
Ensuring the correctness of LLM-generated code is a core challenge for modern software engineering. Benchmarks for agentic code generation check correctness with held-out test suites, which are inherently incomplete and increasingly susceptible to memorization. Formal verification avoids both problems, but existing work covers only standalone tasks whose specifications are given as input, not real issues, which touch large repositories and state intent in vague natural language. We present Benchproofer, a pipeline that turns a coding task with a known correct patch into a formally verified one: it writes a specification for the new code, summarizes the existing functions that code calls with axioms, and admits an instance only after mechanical and adversarial gates agree. Applying it to SWE-bench Verified yields SWE-Proof, 500 real issues whose correctness is formally verified rather than tested, and it extends to SWE-bench Pro. Across two frontier models, verification catches what tests miss: a quarter to a half of test-passing patches admit counterexamples, which a structured natural-language specification does not fix, while a correct formal one lifts resolution from 85% to 95% for Opus 4.8. Writing that specification is the hard part: models that must write their own gain nothing over an unaided baseline, and only 62% of their specifications pass our audit. The usual failure is faithfulness, a specification that constrains part of the required behavior and leaves the rest free. Specification quality still tracks the outcome, failing on 89% of unresolved instances against 47% of resolved ones, making faithful specification synthesis a concrete open problem.