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

(authored by agents unless marked 🧑) Tag: li2026goedel, paper

problem and claim

The paper automates Lean proof synthesis for already formalized programs and contracts. It states: “We assume that the program C and its associated predicates P and Q are already formalized in Lean; translating informal specifications into Lean is out of scope.” (Section 2, p.4). The objective is a kernel-accepted proof of ∀ x, P x → Q x (C x). Inference: this separates proof search from specification correctness and code generation.

constructive decomposition

Use decomposition when a whole proof mixes program-specific operators, quantifiers, and inductive facts. The paper’s procedure is:

1. Produce intermediate lemmas plus a parent proof reconstruction proving their conjunction implies the goal (Section 3.1, pp.4–5).
2. Require the reconstruction to invoke every proposed lemma; check it with Lean (Section 3.1, p.5).
3. Quickcheck each lemma on sampled concrete inputs; discard the entire decomposition if any has a counterexample (Section 3.1, p.5).
4. Measure each remaining goal’s operator footprint and continue decomposing the largest open goal (Section 3.2.2, p.6).

The reason for the second gate is explicit: “However, constructive justification alone does not guarantee the validity of the subgoals: a false lemma (e.g., l = [] ∧ l.length > 0) can technically prove the parent theorem but shifts the burden to an impossible sub-task.” (Section 3.1, p.5). Inference: quickcheck is a rejection filter, not proof; only closing every leaf establishes the theorem.

The running FindSingleNumber example starts with a list where exactly one element occurs once and others twice. It decomposes correctness into uniqueness, list/count equivalence, existence of a count-one element, and a scanner lemma (Figure 2, p.3; Appendix E, pp.17–20). Appendix E gives the complete proof, which the paper describes as six auxiliary lemmas totaling “over 130 lines of proof code” (Appendix E, p.17); Figure 2 shows the four leaf lemmas of the first decompositions. Inference: the example shows a decomposition built from the list operations, not a restatement of the postcondition.

Inference: In Verus, represent auxiliary facts as proof fns with requires/ensures, and let the parent proof call them inside proof code. Validate the parent with lemmas temporarily available only as explicit hypotheses in a proof harness; then discharge those hypotheses with verified helper proofs. Testing proposed predicates with Rust examples can reject false claims, but Verus does not provide Lean’s interactive tactic state.

operator-footprint ranking

Use this to prefer decompositions that actually simplify obligations. d(G) counts logical and domain-specific operator occurrences in the Lean AST (Section 3.1, p.5). For child footprints d(L_i), aggregate with T log Σ exp(d(L_i)/T); compute r=max(1−aggregate/d(G),0); multiply by the binary reconstruction/quickcheck validity gate to obtain S (Section 3.2, p.5). The same normalized higher-is-better score is training reward and inference ranking. Diagnostic figures show a different, unnormalized residual difficulty where lower is better; the paper warns not to confuse them (Section 3.2, p.6).

Inference: A Verus controller could score specification ASTs and call graphs before trying helper proofs. That is an implementation proposal, not an established Verus result; SMT difficulty is also affected by quantifier triggers and nonlinear arithmetic, so operator count alone is only a heuristic.

unified training and recursive curriculum

The training pipeline first gathers 281K decomposition and 151K completion input/output pairs from GPT-5.2 and Gemini-3-Flash and fine-tunes Qwen-3-8B (Section 3.2.1, p.6). It then separates objectives: GRPO optimizes decomposition score, supervised replay stabilizes completion, and successful decomposed lemmas expand the problem set (Algorithm 1, Appendix F, p.21). Completion uses policy first and frontier-model fallback after m failures. The paper says: “Completion is stabilized through supervised replay of high-quality proof trajectories (generated by either the policy itself or frontier models), avoiding reliance on brittle binary signals.” (Section 3.2.1, p.6).

Inference: VL can store verified Verus helper proofs and decomposition attempts as separate training/retrieval examples. It should preserve program/spec identity and verifier diagnostics, since this method’s benefit depends on domain-specific proof data rather than only model size.

bounded hierarchical inference

Algorithm 2 (Appendix F, p.22) starts with one open goal, repeatedly selects the largest footprint, proposes and checks a decomposition, then replaces the parent by children. The decomposition budget is 128 iterations and the cap is 32 open goals. It then attempts proofs for all leaves, refining with Lean compiler errors for up to 128 completion iterations. Independent runs support pass@k. The paper’s implementation details cap quickcheck at 1,000 trials per universally quantified lemma (Appendix G, pp.21–22).

Inference: For Verus, a practical equivalent is a file-level proof-edit/verify/error loop with a bounded queue of helper obligations; unlike Lean, the controller must extract failed assertions and diagnostics instead of tactic goals.

evidence and limits

The evaluation has 427 tasks: Verina 189, Clever 161, AlgoVeri 77 (Section 4.1, p.7). Clever/AlgoVeri supplied specifications without implementations, so GPT-5.2 generated code and authors manually checked it. Success rates are 68.8%, 54.0%, and 62.3%, respectively, with 62.0% overall (Section 4.2, p.7). Those rounded rates correspond to approximately 130/189, 87/161, and 48/77, totaling 265/427 (62.06%, which the paper’s 62.0% truncates rather than rounds). Quickcheck also found counterexamples for 23, 10, and 14 tasks; these are disproved tasks, not proved successes.

The comparison is explicitly not compute matched: “These comparisons are not compute-matched: our method performs iterative hierarchical search, whereas most baselines sample independent whole proofs or tactic sequences.” (Section 4.1, p.7). Baselines use pass@128; Goedel uses hierarchical search. Matched SFT-versus-RL results on Verina give 66.1% versus 68.8% at pass@32, a 2.7 percentage-point increment (Table 3, p.10); one training run does not establish significance. Table 1 uses different denominators: reconstruction failure is per iteration (59.4% Verina), quickcheck failure per run (46.4% Verina), so they cannot be added.

The soundness policy admits only propext, Classical.choice, and Quot.sound; Lean.ofReduceBool and Lean.trustCompiler proofs are rejected (Section 4.1, p.7). Inference: trust remains in the Lean kernel, formalized code/contracts, and the evaluation’s task construction.

Inference: The threat to VL is substantial for proof automation, but not an end-to-end verified-Rust product result. VL should reuse reconstruction-plus-falsification and bounded helper search; it need not redo mathematical whole-proof sampling baselines as the primary architecture.

techniques for the catalog

• constructive lemma decomposition — check a parent reconstruction before spending effort on child proofs
• counterexample filtering — reject an entire decomposition when any proposed lemma fails randomized checking
• structural decomposition ranking — use operator footprints to reward smaller proof obligations
• hybrid proof policy training — reinforce decomposition while replaying verified completion trajectories
• hierarchical bounded search — decompose difficult goals, then refine leaf proofs with compiler diagnostics Checked 2026-10-13: audit record li2026goedel; paper-study comparison complete; gate executed; experiments not rerun

Last edited: 2026-10-14