Formal verification catches what SWE-bench tests miss: a quarter to a half of test-passing patches admit counterexamples

arXiv·high signalXBlueskyLinkedInCopy link

SWE-Proof (arXiv 2609.21190, 18 Sep) applies a pipeline called Benchproofer to SWE-bench Verified, turning 500 real issues into formally verified tasks by writing a specification for the new code, axiomatizing the existing functions it calls, and admitting an instance only after mechanical and adversarial gates agree. Across two frontier models, a quarter to a half of patches that pass the held-out tests admit counterexamples, and a correct formal specification lifts resolution from 85% to 95% for Opus 4.8. The catch is that models cannot write the specifications themselves: those that must gain nothing over an unaided baseline, only 62% of their specifications pass the audit, and specification faithfulness fails on 89% of unresolved instances against 47% of resolved ones.