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

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

paper identity and scope

P^3 studies verified code generation in Lean 4: an LLM must emit an executable program and a machine-checkable proof for a formal pre/post specification. The paper’s central claim is that committing to code before deciding its proof structure causes wasted repair. P^3 first chooses a shared plan for code and proof, then elaborates both under that plan. The paper also introduces Lean4Commit0, a benchmark made from APIs in 108 real repositories, with relational properties across APIs. Evidence is from one run per task/model/method, four closed LLM backends, and Lean 4.28.0. The work is about Lean; Appendix C gives a short Verus sketch (quoted below), and the detailed mappings to Verus in this study are my inference. An earlier human-notes study, p3_joint_planning_20260813.md, already records the main comparison and product positioning. This study adds the paper’s step-by-step plan and elaboration procedures, the listMax proof-shape example, exact benchmark quality formula and denominators, restart rates, and a concrete Verus mapping for each technique.

The paper models a specification as σ=(P,Q), where P is an input precondition and Q relates inputs to outputs. A solution consists of program π and certificate κ accepted by a verifier. The paper explicitly places Verus in the same problem family: “In SMT-based systems, such as Dafny [16], F⋆ [17], and Verus [18], κ is a collection of program annotations whose verification conditions are discharged by an SMT solver.” (section 2, page 3). In Lean, κ is a proof term/tactic script checked by the kernel. Appendix C adds one Verus sketch: in Verus, a shared plan would pair Rust control and data structures with pre/postconditions, loop invariants, decreases clauses, ghost state, and SMT-facing auxiliary lemmas, and it says this transfer is plausible but not empirically established. The finer mapping to Verus annotations and ghost proof code checked through generated SMT obligations in this study is my inference.

technique 1: joint program-and-proof planning

What it is. Before writing implementation or proof, P^3 constructs plan ρ with four commitments: the contract and algorithmic instruction; program decomposition (recursion variable, branches, representation, helpers, termination); concrete library functions and lemmas; and proof obligations (bridging predicate, induction/cases, auxiliary lemmas). The plan is a lightweight shared structural sketch, not full Lean code. The paper states: “A plan ρ records four commitments that the program and proof must later realize: (i) the formal contract and any algorithmic or asymptotic instruction; (ii) the program decomposition, including the recursion variable, branch structure, data representation, auxiliary routines, and termination measure; (iii) the concrete library functions and existing lemmas on which elaboration will rely; and (iv) the proof obligations, including the bridging predicate, induction or case structure, and statements of auxiliary lemmas.” (section 3.1, page 4).

When to use it. Use this whenever multiple implementations satisfy the same postcondition but expose very different proof obligations, or when complexity/algorithm instructions constrain the implementation. It is especially useful for loops, folds, recursive data structures, and relational API tasks. It is not a license to weaken or alter a specification.

How to do it.

1. Read σ and any hard algorithm/complexity instruction. Restate them without changing pre/postconditions.
2. Propose several candidate plans. For each, state decomposition, intended invariant/bridging predicate, induction or case split, termination measure, and named library lemmas.
3. Reject a candidate if its sketch violates instructions, does not preserve the bridging predicate, or cannot entail Q.
4. Select a surviving plan exposing the smallest anticipated proof burden and freeze those structural choices.
5. Elaborate code and proof only according to that plan. If a new algorithm, invariant, or structural lemma is required, classify this as plan failure and replan rather than silently changing code.

The paper’s compact procedure is directly operational: “1. Propose candidate plans from σ, each containing all four commitments above. 2. Reject a candidate if its program sketch violates the instruction, its decomposition does not preserve the bridging predicate, or the predicate does not entail Q. 3. Select a surviving candidate whose decomposition exposes the smallest anticipated proof burden, and freeze its structural commitments as ρ. 4. Elaborate (π, κ) under ρ; repair local errors in place, but return to Step 1 if elaboration requires an unplanned algorithm, invariant, or structural lemma.” (section 3.1, page 4).

Verus form (inference). A Verus plan should list the Rust function contract (requires, ensures), required complexity/algorithm, ownership/data representation, loop or recursion decomposition, decreases measure, and all planned invariants. Its proof side should name assert, assert forall, broadcast proof fn, lemma, and ghost-state facts needed to connect loop state to the postcondition. Candidate plans can compare a vector traversal with an iterator fold, or an in-place tree update with a rebuild, before Rust annotations are written. The plan must reserve the exact mutable borrows and ghost snapshots needed by the chosen representation; a Lean proof term cannot simply be copied to Verus. SMT failures after implementation are local only if the planned invariant is sufficient; missing invariant means replan.

Evidence and limitations. P^3 reports 3.3–8.3 percentage-point gains over implementation-only planning in an ablation (Table 3). In 189 Verina traces with Claude Opus, 131/141 successes (92.9%) retained the first plan; only 4/48 failures (8.3%) were attributed to inadequate planning. This does not establish that plans predict proof burden perfectly: the paper calls retention only a proxy. A plan can be wrong, and closed-source model behavior and single runs limit reproducibility.

technique 2: plan-gated elaboration and local repair

What it is. After freezing ρ, P^3 emits concrete code and a proof scaffold matching the planned structure. Proof leaves may initially be local gaps; Lean diagnostics then drive completion. The key is that local repair cannot redesign the algorithm. “For programs, the agent writes an implementation whose control structure follows the decomposition fixed by ρ: the recursive argument, case split, collection combinator, or auxiliary routine is not chosen again during coding.” (section 3.2, page 5).

How to do it.

1. Instantiate the planned recursion/cases/combinator and all named helper statements.
2. Emit the proof’s top-level induction/case structure and bridging predicate, leaving only local leaves unresolved.
3. Run the verifier and inspect localized goals/errors through Lean LSP/MCP feedback.
4. Fill a leaf or small auxiliary lemma while preserving ρ and the other artifact.
5. If repeated local repairs fail, or diagnostics show an unplanned invariant/algorithm is necessary, retreat to planning and create a new ρ (the paper does not fix a count; Appendix E allows refining the current plan once or twice, then discarding it); then regenerate both artifacts.

Verus form (inference). Generate Rust and proof scaffolding together: write the function body and loop skeleton plus requires/ensures, invariant, and decreases clauses from ρ. Run verus; repair an arithmetic assertion, trigger, or quantifier locally while preserving control flow. Use ghost variables and helper lemma functions as the planned scaffold. A solver error that reveals an absent relational invariant should trigger re-planning, not ad hoc mutation of the body. Verus’s SMT feedback is less interactive than Lean’s tactic goals, so diagnostics may be coarser; this is an engineering adaptation, not a result shown by the paper.

Evidence. The mechanism is supported by lower full-restart rates (Table 6). For Verina, P^3 rates are 11.7%, 7.8%, 5.3%, and 8.5% for Codex, Gemini, Sonnet, Opus versus sequential 28.6%, 24.7%, 18.5%, and 24.9%. On AlgoVeri, P^3 rates are 11.2%, 7.0%, 5.8%, and 9.1% versus 34.9%, 32.2%, 23.2%, and 33.6%. The denominator is all 189 Verina or 77 AlgoVeri runs per backend. The paper attributes savings to avoiding full rewrites after local repair fails. Lean remains the trusted final checker; the model, planner, prompts, and API are outside the trusted base. On Lean4Commit0 (n=108 per backend), P^3 full-restart rates are 1.7%, 1.6%, 1.2%, and 2.2% for Codex, Gemini, Sonnet, and Opus, versus sequential rates 4.3%, 4.9%, 4.4%, and 5.2%.

technique 3: choose proof-friendly decomposition using listMax

What it is. The paper’s running example computes the maximum of a non-empty integer list under a specification requiring membership and an upper bound. Structural recursion (A) mirrors the postcondition; an accumulator fold (B) is shorter but requires a generalized invariant. The exact fold invariant is: “lemma foldl_max_gen (init : Int) (ys : List Int) : ys.foldl max init ∈ init :: ys ∧ ∀ z ∈ init :: ys, z ≤ ys.foldl max init” (section 2, page 3).

How to apply it. For each candidate implementation, derive a sufficient bridging predicate that makes one recursive step compositional. For structural recursion, split [x] and x::y::t; apply the tail induction hypothesis and prove membership/upper bound with max. For a fold, generalize over arbitrary accumulator init, prove the invariant by induction on ys, then specialize init to xs.head! for a non-empty input. Record this stronger predicate in ρ before coding; otherwise proof search discovers it late and may discard code.

Verus form (inference). A recursive Rust list_max can use a decreases list length and postcondition directly. An iterative fold needs a loop invariant quantified over the accumulator: accumulator is in the processed prefix and bounds every processed element; the final result then implies membership and upper bound over the whole slice. Express the accumulator fact with invariant and ghost sequence snapshots, and prove a helper lemma for max. Verus cannot use Lean’s theorem syntax or List.foldl; use Rust slices/Vec and integer ordering while preserving the same logical strengthening.

Evidence/failure. The example is fully checked in Lean (Appendix D), but it is illustrative rather than a benchmark aggregate. Version B’s universal init is an implementation-induced obligation, and, inference, a planner that optimizes only line count may choose it accidentally. The example demonstrates why proof-friendly structure can conflict with idiomatic or efficient code; P^3 does not claim one decomposition is universally best.

technique 4: repository and relational specification quality gates

What it is. Lean4Commit0 converts 108 public libraries (65 Python, 17 Rust, 15 C/C++, 11 Java) into 108 tasks with 511 code placeholders and 519 theorem placeholders. Tasks include relational theorems connecting multiple APIs, such as setting a configuration value then querying it or checking precedence between two updates. This tests whether plans coordinate several implementations against shared proof obligations.

How to build/use it.

1. Extract core user-facing APIs and encode each as a Lean signature, postcondition, and correctness theorem.
2. Add relational specifications whenever semantics spans calls.
3. Check every reference input/output pair against the Lean spec (hard admissibility).
4. Mutate executable reference implementations; require behavior-changing mutants to be rejected.
5. Have an LLM review for trivial, tautological, duplicate, or irrelevant specs.
6. Admit only complete reference satisfaction and Quality = 0.5·Mutation + 0.5·Review >= 80%, where Review is the normalized 1–5 score.

Verus form (inference). A comparable corpus would package Rust APIs with requires/ensures and relational lemmas over sequential calls. Run reference tests through a Rust shim, mutate implementation behavior, and verify that the contract rejects mutants. This tests specification adequacy separately from proof-generation ability. Verus’s ownership and state model would require relational ghost snapshots or abstract state, so Lean’s direct value-level encoding is not enough.

Evidence. Table 1 reports 1,030 placeholders total, 98.6% mutation rejection, 82.7% review, and 90.7% mean quality; all 108 libraries clear the 80% threshold. Solve rates still range only 9–22% on Lean4Commit0, showing that relational library tasks remain difficult despite the gate. The authors warn that tests may miss intent and an accepted artifact is correct only relative to its shipped specification.

technique 5: explicit phase and quality gates

What it is. Appendix E turns the workflow into six gated phases: understand the specification and enumerate every code/proof hole; co-derive a plan; obtain an external PASS-PLAN verdict; emit code and proof sketches with only intended sorry leaves; fill tactic details; and run mechanical and instruction-compliance quality gates. Specifications are read-only, and only standard axioms are allowed.

How to use it. Require a plan file with restated contract, algorithmic idea, library support, and proof-obligation sketch before editing code. Run an independent plan verifier; on FAIL revise the plan. Compile the code sketch before filling proof leaves. At the end run a mechanical checker for sorries, compilation, and axioms, then an instruction checker over the code region. A failed instruction check sends the agent back to planning rather than allowing an in-place algorithm swap. This external phase gate is distinct from Lean kernel checking and is an orchestration control.

Verus form (inference). Make an equivalent plan artifact mandatory before Rust edits; gate it with a separate reviewer or script, then run Verus compilation/SMT checks and an algorithm-compliance check. Keep contract text immutable and reject unauthorized axioms or assume-like escapes. The paper supplies no Verus implementation, so gate names and exact tooling are adaptation proposals.

Evidence and limits. The appendix documents the six phases and final gates, but does not report a separate ablation of each gate. Their value is process containment: they make silent algorithm switching and proof-hole delivery mechanically detectable, while final semantic adequacy still depends on the specification.

measured results, trust, and product threat

Across 12 benchmark/model cells, P^3 has the highest solve rate. Against the stronger baseline, gains are 4.6–11.2 points. Across all methods, rates span 59.3–77.2% on Verina, 31.2–48.1% on AlgoVeri, and 9.3–22.2% on Lean4Commit0 (n=189, 77, and 108 tasks respectively); P^3 alone spans 72.0–77.2%, 39.0–48.1%, and 15.7–22.2%. Difficult-subset savings are 3.0–39.6% API cost and 3.1–37.2% wall time, with subsets n=48 Verina, n=20 AlgoVeri, n=27 Lean4Commit0. Each task/model/method ran once under a $30 API budget and 180-minute limit; therefore no within-task variance or significance test is available. The difficult subset is selected by mean cost, so its savings are conditional. Inference: they may suffer selection effects. Comparison with other papers: these solve rates count tasks where a Lean agent with Lean tools (LSP/MCP) produced code and proof accepted by Lean that also satisfied an added natural-language complexity instruction (Table 2), so they are not comparable to AlgoVeri’s own 9.09% for Lean (Gemini-3 Flash, up to 15 repair rounds) or to Verina’s 4.9% one-trial ProofGen with the ground-truth code given; neither paper explains the gap, and models, agent tooling, task definition and the added instruction all differ.

The trusted evidence is Lean’s kernel acceptance of π and κ. Algorithmic-instruction compliance is a separate evaluator gate, not a kernel trust guarantee. The planner, LLM backends, prompts, benchmark extraction, reference tests, mutations, and LLM specification reviewer are not trusted to establish theorem truth. A major semantic risk is specification adequacy: vacuous or under-constrained contracts can yield formally correct but useless Rust. Appendix C says transfer to Verus is plausible but not empirically established; this is the main gap for VeruLaw. My inference is that P^3 is a medium-to-high threat to a product whose differentiator is agent-written verified Rust: it offers a general control strategy (co-design structure and proof, explicit replanning) that could raise solve rates and reduce repair cost. It does not demonstrate Rust/Verus performance, ownership-heavy code, open models, or whole systems, so it is not evidence that another system can replace VeruLaw. VL should reuse the plan schema and quality gates, then measure on Verus tasks with repeated runs and specification adequacy tests rather than assume Lean gains transfer.

Already done that VL should not redo: sequential program-then-proof repair, textbook-only benchmark claims, and single-function evaluation without relational API tasks are explicitly treated as baselines or gaps. VL should avoid presenting another planner without a Verus-specific transfer study, mutation-based contract checks, and denominator-complete cost/restart measurements.

techniques for the catalog

• joint plan ρ — enumerate contract, decomposition, library support, bridging invariant, proof cases, and auxiliary lemmas before implementation; reject plans that cannot entail the postcondition
• plan-gated elaboration — emit code and proof scaffold from the same plan, repair localized verifier goals, and replan when an unplanned invariant or algorithm is required
• proof-friendly decomposition — compare structural recursion and folds by the invariants they induce; generalize accumulator predicates before coding when needed
• relational specification QA — require reference satisfaction, mutation rejection, and non-vacuity review, with a quantitative admission threshold before benchmarking
• explicit phase gates — require read-only specifications, PASS-PLAN, mechanical checks, and instruction compliance before delivery
• restart-aware evaluation — report solve rates, costs, times, and full-restart frequencies with task denominators and single-run limitations

Audited 2026-10-12 against the paper: checked Tables 1, 2, 3, 5 and 6, the Lean4Commit0 construction counts (108 libraries, 65/17/15/11, 511 and 519 placeholders, 1,030), the Quality formula and 80% threshold, plan retention (131/141, 4/48), the four-step compact procedure and the six phases of Appendix E, the listMax example, page references and quotations, and the Verus sketches. Changed: the claim that the paper’s Verus description ends at section 2 was wrong, Appendix C gives a Verus sketch, now cited; removed an invented once limit on retreating to planning; marked two unlabelled speculations (selection effects, line-count planner) as inference; replaced the loose broadcast proof term by broadcast proof fn. Not checked: Figures and Appendix H traces beyond the text, the Lean proofs in Appendix D (not compiled), and the earlier study p3_joint_planning_20260813.md.; follow-up: added one clause saying what the solve rates measure against AlgoVeri Lean 9.09% and Verina 4.9%.

Last edited: 2026-10-13