SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
George Ma, Benjamin Mikek, Haoyu Li, Ferhat Erata, Yuhao Zhang, Yuhao Zhang, Zeren Shui, Behrooz Omidvar Tehrani, et al.
cs.LG · cs.AI · cs.SE
Quick verdict
Claims first formally verified SWE-bench benchmark; rigorous multi-gate construction, but LLM-judged audits and a single model temper the headline findings.
Summary
The paper introduces Benchproofer, a pipeline that converts coding tasks with known-correct patches into formally verified benchmark instances, and releases SWE-Proof: all 500 SWE-bench Verified issues plus 266 Python SWE-bench Pro issues, each carrying a formal specification, axioms summarizing unchanged callees, a verifying reference implementation, and machine-checked proofs under three backends (Nagini, Velvet, Lean), with structured-natural-language EARS as a non-formal control. Admission runs thirteen gates combining mechanical censuses — mutation testing (99.17% kill rate over 25,457 mutants), 23,482 property-test cases, roughly 187.6 million differential inputs against real repositories — with blind adversarial LLM audits. Evaluating Claude Opus 4.8 across nine settings, 26.8% of test-passing patches admit counterexamples; a supplied correct specification lifts resolution from 85.0% to 95.1% averaged over the formal backends, while structured natural-language specifications confer none of this gain. Agents writing their own specifications gain nothing: only about 56% pass the five-property audit, dominated by faithfulness failures (42.5%) — specifications that cover too little of the required behavior. Specification correctness tracks resolution (92.3% versus 50.5% audit failure). Limitations: the verify-implies-resolve guarantee rests on audited trust points rather than proof, key verdicts are LLM-adjudicated, evaluation covers a single model, and 65 Verified bundles carry documented specification-leakage relaxations.
Review complete
Assessment at a glance
5
risk flags identified
● high 0
● medium 2
● low 3
4 strengths · 4 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- Formal verification catches what tests miss: 26.8% of test-passing SWE-bench Verified patches admit counterexamples under audit (Section 4.2, Row 0 minus Row 1).
- Supplying a correct ground-truth specification lifts Claude Opus 4.8's resolution from 85.0% to 95.1% averaged over the three formal backends, while structured natural-language (EARS) specifications confer none of the gain.
- Self-constructed specifications do not help: resolution matches the unaided baseline (best backend +0.6), and only about 56% of synthesized specifications pass the five-property audit, with faithfulness failures dominating at 42.5% (Section 4.5, Table 3).
- Specification correctness tracks patch correctness: 92.3% of specifications from unresolved instances fail the audit versus 50.5% from resolved ones (Section 4.6, Table 29).
- The verify-implies-resolve guarantee is enforced by thirteen gates but ultimately rests on two audited trust points — axiom soundness and refinement fidelity — rather than proof (Sections 3.3-3.5).
Strengths
First repository-scale verification oracle for real issue-resolution tasks
SWE-Proof attaches machine-checked guarantees to all 500 SWE-bench Verified issues and 266 Python SWE-bench Pro issues across three backends (Nagini, Velvet, Lean), versus VERO's 43 hand-reformalized instances (Section C); 2,000/2,000 Verified bundles are green under all four backends (Table 4).
Evidence-heavy, attackable admission protocol
Thirteen gates (Table 11) yield exact censuses: 23,482/23,482 property-test cases receive their labeled verdicts (Table 8), 99.17% mutation kill rate over 25,457 mutants (Table 13), 187.6M differential inputs against real repositories with zero disagreements, 25.7M axiom-probe observations; successful attacks become released property-suite cases (E.3).
Clean experimental contrasts that defuse obvious confounds
Unusually honest boundary accounting
Weaknesses
Single-model evaluation on a minimal scaffold
Core metrics are LLM-adjudicated
Transliteration soft link in the guarantee chain
Statistical thinness around null claims
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
SWE-Proof (arXiv 2609.21190) makes two linked contributions. **Benchproofer** (Section 3) is a construction pipeline that turns a coding task with a known-correct patch into a formally verified one: an agent writes a specification for the changed code, unchanged callees are summarized by fuzz-validated axioms, and the instance is admitted only after thirteen mechanical and adversarial gates agree. **SWE-Proof** is the resulting benchmark: all 500 SWE-bench Verified issues plus 266 Python SWE-bench Pro issues, each with a specification, a verifying reference implementation, a pre-fix twin that must fail verification, and machine-checked proofs under Nagini, Velvet, and Lean — with a structured-natural-language EARS backend as a non-formal control (Appendix D). The central guarantee (Claim 1) is verify implies resolve: an implementation verifying against the released specification, transferred to an equivalent repository patch, resolves the issue. Evaluation claims (Section 4): 26.8% of test-passing SWE-bench Verified patches admit counterexamples; a supplied ground-truth specification lifts Claude Opus 4.8's resolution from 85.0% to 95.1% averaged over the formal backends; self-written specifications gain nothing (about 56% audit pass rate); faithfulness — specifications covering too little of the required behavioral surface — dominates failures at 42.5%; and specification quality tracks resolution (92.3% vs 50.5% audit failure, Table 29).
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 4 strengths & 4 weaknesses, analyzed in detail
- 5 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What is SWE-Proof?
A benchmark of 500 real GitHub issues (all of SWE-bench Verified, plus 266 Python tasks from SWE-bench Pro) where correctness is certified by machine-checked formal proofs instead of hidden tests. Each task ships a formal specification, axioms summarizing unchanged code, a verifying reference implementation, and a proof, built under three backends (Nagini, Velvet, Lean) plus a structured-English control.
What does the paper conclude about LLM coding agents?
Evaluating Claude Opus 4.8: about a quarter (26.8%) of patches that pass all hidden tests are actually flawed; giving the agent a correct formal specification raises resolution from 85.0% to 95.1%; but agents writing their own specification gain nothing over having none, because only about 56% of self-written specifications pass an audit — mostly they cover too little of the behavior the issue requires (faithfulness failures, 42.5%).
Why do LLMs fail to write their own formal specifications?
The dominant failure mode is faithfulness: the specification pins down the functions it models but leaves part of the required behavior unconstrained, so an implementation can verify against it and still be wrong. Covering the full behavioral surface of a fix that spans several functions is the open problem the paper identifies.
Is the SWE-Proof benchmark or code available?
The paper's reproducibility statement says both the Benchproofer pipeline and the SWE-Proof corpus will be released, including per-instance gate outcomes, property-test suites, axiom probes, and the implementation-to-patch correspondence, so third parties can re-audit every guarantee independently.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- Table 2 (the nine-setting results grid) falls in an omitted extraction section; headline numbers were recovered from the prose of Sections 4.2-4.6.
- Appendices D.4, E.3 (Table 14 tail), and F.2 are truncated; the repetition/variance details of Appendix G.4 were unavailable, limiting the statistical assessment.
- Figures 1-6 are referenced but not analyzable from text.
- Minor internal count inconsistencies noted (Table 4: 7,350 vs Table 8 sum 7,364 Pro property cases; Table 10: 187.6M vs Section E.2: 187.9M differential inputs).
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.