Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

Zenan Li; Ziran Yang; Deyuan He; Haoyu Zhao; Andrew Zhao; Shange Tang; Kaiyu Yang; Aarti Gupta

cs.SEMar 18, 2026

Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification

Authors: Zenan Li, Ziran Yang, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, +2 more

Organizations: ETH Zürich · Princeton Language and Intelligence · Department of Computer Science, Princeton University · Apodex

Abstract

Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness. Formally verifying that implementations satisfy specifications requires constructing machine-checkable proofs, a task that remains beyond current automation. We propose a hierarchical proof search framework for automated code verification in Lean~4 that decomposes complex verification goals into structurally simpler subgoals before attempting tactic-level proving. Central to our approach is a principled decomposition score that combines constructive justification with structural effectiveness. The same score serves as both the training reward and the inference-time ranking criterion, aligning optimization and deployment. We train Goedel Code Prover, a single unified policy for both decomposition and completion, through supervised initialization followed by hybrid reinforcement learning, where a continuous decomposition reward supports planning exploration while supervised replay stabilizes proof generation. On three Lean-based code verification benchmarks comprising 427 tasks, our 8B-parameter model achieves a 62.0% prove success rate, a 2.6 improvement over the strongest baseline under the reported inference settings. We further observe consistent inference-time scaling: success rates improve monotonically with search iterations and sampling budget, while whole-proof baselines plateau within the evaluated budgets.

Figures & tables

Panel of Figure 2 — Figure 2: Overview. Stage 1: The goal is recursively decomposed into simpler sub-lemmas; the score $S$ ranks candidates by validity and structural reduction in operator footprint $d(\cdot)$ . Stage 2: Leaf lemmas are proved via iterative tactic generation with Lean 4 compiler feedback. The score serves as both training reward and inference-time ranking criterion.

Figure 3: Percentage of solved problems by baselines and our framework across three benchmarks. Baselines are evaluated with parallel generation under a Pass@128 budget; our method operates under a search-based inference setting using Göedel-Code-Prover-8B. Our framework outperforms all baselines by a substantial margin across every benchmark.

Figure 4: Prove success rate vs. completion iterations under different pass@

k

budgets.

Figure 5: Unnormalized decomposition score vs. prove rate on Verina. Lower raw scores indicate simpler decompositions and separate instances proved within the evaluated budget from those left unsolved (AUROC = 0.903).

Table 5

Model	Pass@1	Pass@10	Pass@20	Pass@32
SFT only	26.9	44.9	53.9	66.1
SFT + RL	29.1	46.0	57.1	68.8
Difference	+2.2	+1.1	+3.2	+2.7

Table 3: Matched-budget comparison of the SFT-only policy and the policy after RL on Verina. Entries are prove success rates (%).

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Figure 6 — Figure 6: Prompt template for the decomposition stage. The model receives the target theorem name and the full Lean formalization, and produces a reasoning trace followed by helper lemmas and a proof of the main theorem.

Panel of Figure 7 — Figure 7: Prompt template for the completion stage. The model receives the current code, the target goal state, and responds with SEARCH/REPLACE diffs that fill in proof bodies.

Decomposition	Completion	Verina
—	GPT-OSS-120B	20.1
—	Gemini-3-Flash	19.6
GPT-OSS-120B	GPT-OSS-120B	44.9
GPT-5.2-Pro	Gemini-3-Flash	54.4

Appendix

Table 4: Verina results (%) when instantiating the framework with off-the-shelf models without fine-tuning.

Threshold	Verina	Clever	AlgoVeri	Total
$\geq 50$ chars	7	5	1	13/427
$\geq 100$ chars	3	0	0	3/427
$\geq 200$ chars	0	0	0	0/427

Appendix

Table 5: Benchmark tasks whose implementation shares a contiguous substring with a training implementation.

Theorem class	Cases	$r>0$	Representative examples (reduction ratio)
Hoare-style program correctness (CSLib)	14	9	otp_ciphertextDist_eq_uniform (0.872), mergeSort_sorted (0.502), toNAFinAcc_language_eq (0.492), Shamir privacy (0.154), and pred_correct for SKI (0.112)
Type-safety theorems (CSLib)	3	0	STLC/Fsub preservation and progress statements
Structural and categorical theorems (CSLib)	5	0	LTS composition, Turing-machine composition, $\omega$ -regular complement, CLL $\eta$ -expansion, and infinite Ramsey
Pure mathematics (Mathlib)	10	0	Lagrange, Beatty, Hensel, Siegel, Kronecker, Shortlex, Lucas–Lehmer, and related theorems

Appendix

Table 6: Behavior of the operator-footprint reduction ratio on human-written decompositions. The ratio is informative primarily for Hoare-style program-correctness statements, its intended setting.

Statistics	Verina	Clever	AlgoVeri	Total
Lemma count (mean)	17.02	12.13	8.48	14.38
Lemma count (std)	11.79	10.57	10.97	11.97
Proof length (mean)	167.11	137.78	129.87	154.28
Proof length (std)	108.50	97.79	83.03	103.11

Appendix

Table 7: Statistics of proved problems: mean and standard deviation of lemma count and proof length (lines of code).

Figure 8: Residual operator-footprint ratio

\bar{d}/d(G)

vs. iterations across three benchmarks. Lower values indicate more aggressive goal simplification and therefore a higher reduction ratio

r

Figure 9: Inference scaling curves (pass@k) of two baseline verifiers, BFS-Prover-V2-32B and Göedel-Prover-V2-32B, on the three evaluation benchmarks. The x-axis denotes the number of sampled proof attempts

k

, and the y-axis shows the percentage of problems solved.

Figure 10: Unnormalized decomposition score vs. prove rate on training data. As on Verina, lower raw scores are associated with higher prove rates.

Figure 11: Unnormalized decomposition-score distribution before training across benchmarks. Lower values are better.

Figure 12: Unnormalized decomposition-score distribution after training across benchmarks. Lower values are better.

Explore similar work

WybeCoder: Verified Imperative Code Generation
Mar 31, 2026Fabian Gloeckle, Mantas Baksys, Darius Feher +5Formal Verification Code Generation
FAIR, Meta · CERMICS, ENPC, Institut Polytechnique de Paris, CNRS · Computer Lab, University of Cambridge +3
P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation
Aug 10, 2026Zenan Li, Ziran Yang, Peiyang Song +2Code Generation Formal Verification
1Apodex · 2Princeton University · 3Caltech +1
Automating Formal Verification with Agent-Guided Tree Search
May 26, 2026Leo YaoCode Generation LLM-Based Program Synthesis
Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology

Mar 31, 2026J/K move · Enter open · S save

WybeCoder: Verified Imperative Code Generation

Fabian Gloeckle, Mantas Baksys, Darius Feher, Kunhao Zheng+4

FAIR, Meta · CERMICS, ENPC, Institut Polytechnique de Paris, CNRS · Computer Lab, University of Cambridge+3

Formal Verification Code Generation LLM-Based Program Synthesis Interactive Theorem Proving

Open paper AskPDF arXiv

Recent progress in large language models (LLMs) has substantially advanced automatic code generation and formal theorem proving, yet software verification has not seen comparable gains. To address this gap, we propose WybeCoder, an agentic code verification framework that enables prove-as-you-generate development, in which code, invariants, and proofs co-evolve. WybeCoder builds on a recent framework that combines automatic verification condition generation and SMT solving with interactive proofs in Lean. To enable systematic evaluation, we translate two benchmarks for functional verification in Lean, Verina and Clever, into equivalent imperative code specifications. On complex algorithms such as Heapsort, we observe consistent performance improvements as we scale our approach, synthesizing dozens of valid invariants and dispatching dozens of subgoals, ultimately producing hundreds of lines of verified code and overcoming plateaus reported in previous work. Our best system solves 74% of Verina tasks and 62% of Clever tasks at moderate compute budgets, substantially surpassing previous evaluations and paving the way for the automated construction of large-scale datasets of verified imperative code.

Abstract

Explore similar work

WybeCoder: Verified Imperative Code Generation

P3^{3}3: Joint Program-and-Proof Planning for Verified Code Generation

Automating Formal Verification with Agent-Guided Tree Search

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation