RefactorProof: LLM Proofs Break After Code Refactoring

Verifiable code generation benchmarks usually check a proof against a single fixed implementation. The authors of RefactorProof wanted to know what happens if the implementation is rewritten while its behavior stays the same. From the 185 VERINA tasks that compile in their pinned environment, they built 458 Lean-certified variants. The specification and the proof being checked did not change by a single byte. The result: on structural refactorings, proofs fail verification en masse. For VERINA reference proofs, the survival rate (task-normalized structural PSR) is 4.3%. For specialized LLM provers, it is 13.3–26.8%.

How the brittleness test works

The idea is simple and brutal. A formal proof is tied to the specific text of a program: names, the order of definitions, the structure of expressions. If a developer extracts a function, changes how a computation is shaped, or renames a variable, nothing changes logically, yet the Lean proof may stop building. Refactoring happens constantly in real development, so whether a proof survives an edit is a practical question.

VERINA provides reference proofs for only 46 tasks, and all of them come from the basic split. For this reason, the authors base their main model-versus-reference comparisons on 21–25 short non-recursive tasks, chosen so that every participant stands on the same ground. This is a narrow sample, and the scale of the conclusions should be read with that in mind.

Machines are brittle, but humans are more so

The unexpected twist is that model-generated proofs turned out to be more robust than the reference ones. On comparable tasks, the overall share of unchanged proofs that survive is higher for the models than for the VERINA artifacts. The 95% confidence intervals for all three models do not include zero.

• DeepSeek-Prover-V2-7B: +15.6 points over the reference
• Goedel-Prover-V2-32B: +18.8 points
• Goedel-Prover-V2-8B: +20.3 points

The ordering holds when T1 variants, which every proof survives, are excluded; when results are aggregated with balance across refactoring families; and under alternative, practically applicable rules for selecting a valid proof. The likely reason is that the reference proofs are written for a specific code shape and tightly coupled to it, while models more often produce more straightforward proofs that depend less on construction details. This is a hypothesis; the authors do not prove such a mechanism.

Broken doesn't mean expensive to fix

The paper's main caveat concerns the cost of a breakage. Predefined single-identifier edits fix 51 of 54 eligible structural failures of reference proofs and 58 of 85 eligible failures of model proofs. So most of the "brittleness" disappears with a cheap edit, and for the reference proofs almost everything gets fixed. For the models the picture is worse: about 68% versus 94%.

RefactorProof therefore measures only the stability of an unchanged proof under refactoring. It does not assess the cost of maintaining a proof after it breaks, and the authors say so explicitly.

Key study parameters

• Benchmark: RefactorProof, derived from VERINA
• Source tasks: 185 (compile in the pinned Lean environment)
• Certified variants: 458
• VERINA reference proofs: 46 tasks, basic split only
• Comparable sample: 21–25 short non-recursive tasks
• Structural PSR of reference proofs: 4.3%
• Structural PSR of specialized provers: 13.3–26.8%
• Models tested: DeepSeek-Prover-V2-7B, Goedel-Prover-V2-32B, Goedel-Prover-V2-8B
• Repair by editing a single identifier: 51/54 for reference proofs, 58/85 for models
• Venue: NeurIPS 2026 Workshop on AI for Verifiable Coding; categories cs.AI, cs.LO, cs.SE

What to change in practice

Teams building "LLM writes the code and the proof, Lean checks" pipelines get a clear signal: checking against a single fixed implementation overstates reliability. Add refactored variants of the program to CI and run the proof against them. If a proof fails, try cheap automatic identifier edits first; according to the paper, they resolve a significant share of cases. When evaluating prover models, look not only at the share of tasks solved but also at whether proofs survive code changes. The takeaway for benchmark authors is just as direct: measure both stability and repair cost. RefactorProof does not yet include the second metric.