Preprint
Sep 2026
SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?
This work presents Benchproofer, a pipeline that turns a coding task with a known correct patch into a formally verified one, which 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.
George Ma, Benjamin Mikek, Hao-Yu Li et al.
· 2 citations