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

P3: Joint Program-and-Proof Planning for Verified Code Generation

Summary

This paper introduces P3, a novel LLM-based agentic workflow for verified code generation, which jointly plans both the program and its proof before elaborating either artifact. The authors argue that the de facto sequential program-then-proof pipeline is both ineffective and inefficient because a program generated without anticipating its proof can be structurally difficult to verify, leading to brittle repair loops. Inspired by Dijkstra's principle that programs and their correctness arguments should be developed hand in hand, P3 first derives a unified program-and-proof plan from the specification, then elaborates the implementation and proof scaffold under this shared plan. The paper also introduces Lean4Commit0, a new repository-derived, library-level benchmark for evaluating verified code generation in realistic settings.

Problem with Existing Approach

The paper identifies a fundamental limitation in the standard workflow: "The input to verified code generation is a formal specification σ = (P, Q) for a target function... Given σ, the goal is to construct two artifacts: a program π implementing the function, and a certificate κ from which a verifier can establish that, on every input satisfying P, running π terminates and returns an output satisfying Q. However, existing verified-code-generation pipelines often follow a sequential program-then-proof schedule: the LLM first commits to a concrete implementation, after which a separate proving stage... is invoked to discharge the resulting proof obligations. This creates a problem because an implementation generated without anticipating its proof may lack the invariant or induction structure needed for a clean correctness argument. In such cases, local repair is unlikely to recover a proof-friendly structure that was never planned."

The paper illustrates this with a listMax example, showing that two implementations computing the same value induce very different proof obligations. Version (A) using structural recursion admits an induction that mirrors the postcondition, while Version (B) using an accumulator fold is in fact substantially harder to verify against the stated specification because a proof cannot proceed directly from the original postcondition; it must first generalize to an accumulator invariant. The paper concludes: The failure mode is therefore structural: the sequential schedule commits the implementation before identifying the proof structure most natural for the specification, often leading to wasted certificate search.

P3 Methodology

P3 operates in two stages: Planning and Elaboration. In the planning stage, P3 proposes candidate plans based on σ and selects a plan ρ containing a program sketch aligned with a compatible proof sketch. A plan ρ records four commitments: "(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."

The planning agent validates candidate plans at the sketch level, checking that "the program sketch must meet the task instructions, including any algorithmic constraints; the proof sketch must explain why the chosen decomposition preserves the bridging predicate and why that predicate entails Q; and any nontrivial strengthening of Q needed by the proof must be named as an auxiliary lemma rather than left implicit." The compact procedure involves proposing candidates, rejecting those with violations, selecting the one with the smallest anticipated proof burden, and elaborating under that plan, returning to planning if elaboration requires unplanned elements.

In the elaboration stage, "the agent writes an implementation whose control structure follows the decomposition fixed by ρ... For proofs, the agent writes a certificate scaffold with the same shape: the target theorem, the auxiliary lemma statements named by the plan, and the top-level proof structure that invokes the planned induction, case analysis, or lemma applications. Proof completion becomes a local elaboration problem rather than an unconstrained proof search problem."

The plan also provides structured feedback: "An elaboration-level failure is one whose error localizes under the current plan... The agent repairs the localized artifact while keeping the rest of the plan and the other side of the pair intact. A plan-level failure is signaled when repeated local repairs cannot close the obligations under ρ... In that case the agent retreats to planning, revises ρ, and only then re-elaborates the program and certificate against the new plan."

Lean4Commit0 Benchmark

The paper introduces Lean4Commit0, a benchmark built from 108 real-world open-source libraries spanning four mainstream ecosystems: Python, Rust, C/C++, and Java. It contains 511 implementation placeholders and 519 theorem placeholders. The benchmark extends beyond single-function tasks to include relational specifications that connect multiple API calls. For example, in the Fabric library (Python SSH deployment), after setting key k to value v, a subsequent lookup of k returns some v; and if the same key is set at a lower level and then a higher level, get returns the higher-precedence value.

The benchmark uses a three-stage specification quality pipeline: "a reference-satisfaction check verifies that the behavior of the original implementation is consistent with the Lean specification; a mutation-rejection check tests whether the specification rejects behavior-changing mutants; an LLM review flags specifications that are trivial or irrelevant. The quality score is defined as Quality(σ) = 0.5 · Mutation(σ) + 0.5 · Review(σ), and tasks are admitted only if reference satisfaction is complete and the aggregate score is at least 80%." The mean quality score across the benchmark is 90.7%.

Experimental Results

The paper evaluates P3 on Verina (189 tasks), AlgoVeri (77 tasks), and Lean4Commit0 (108 tasks) using four frontier LLM backends: Codex-GPT-5.5, Gemini-3-Pro, Claude-Sonnet-4.6, and Claude-Opus-4.7. The main results show that P3 attains the best solve rate on every (benchmark, model) cell, with the absolute gain over the stronger baseline (∆) ranging from +4.6 to +11.2 percentage points. Specifically, on Verina, gains range from +5.2 to +11.2 points; on AlgoVeri, from +5.2 to +7.8 points; and on Lean4Commit0, from +4.6 to +5.5 points.

A targeted ablation comparing P3 with P LAN-S EQ (implementation-only planning) shows joint program-and-proof planning improves solve rate by 3.3–8.3 points. The paper notes that "P LAN-S EQ helps on Verina and AlgoVeri but hurts on Lean4Commit0, where independently reasonable API implementations may be difficult to connect under a relational theorem unless they are planned against their shared proof obligations."

On efficiency, P3 reduces per-task cost by 3.0–39.6% and wall-clock time by 3.1–37.2% relative to the better baseline on the difficult subset of tasks. The paper attributes much of the baseline's cost to full-restart repair: after local repairs fail under the committed program, the agent rewrites both artifacts.

A case study on left-leaning red-black-tree deletion shows that "S EQ's structural route reaches 6,344 lines without closing, while rebuild closes in 1,176 lines only after inheriting redundant invariants. P3 compares both sketches, recognizes that rebuild reduces the value-set goal to list permutation, and closes it in 1,105 lines and about 34 minutes."

Conclusion

The paper concludes that "Committing to implementation structure before proof structure induces brittle repair loops; P3 instead fixes a shared decomposition, bridging predicate, and auxiliary lemmas before elaboration, routing feedback to local repair or explicit replanning. Lean4Commit0 complements this workflow with repository-derived, library-level tasks, relational API specifications, and a uniform quality pipeline, moving verified generation toward correctness arguments planned with the code rather than recovered after the fact."

Improvements to AI Systems:

1. Joint Planning Architecture: Implement a dual-planning module that generates program sketches and proof sketches simultaneously from a specification, rather than sequentially. The AI system can now reason about proof feasibility before committing to implementation details, avoiding structural mismatches that cause repair loops.

2. Sketch-Level Validation: Add a validation layer that checks program-proof compatibility at the sketch level—verifying that the recursion structure, branch decomposition, and induction scheme align with the postcondition before any code is written. The system can reject incompatible plans early and propose alternatives.

3. Plan-Level vs. Elaboration-Level Error Routing: Build a hierarchical error-handling mechanism that classifies failures as either local (fixable within the current plan) or structural (requiring replanning). The system can now avoid wasteful full-restart repairs by distinguishing between syntax/type errors and proof-structure incompatibilities.

4. Auxiliary Lemma Pre-Declaration: Incorporate a step where the system explicitly names and states any strengthening of the specification (e.g., accumulator invariants, generalized induction hypotheses) as auxiliary lemmas during planning. This forces the system to anticipate proof obligations that aren't directly derivable from the postcondition.

5. Proof-Burden Cost Model: Add a scoring function that estimates the anticipated proof complexity of each candidate plan (e.g., number of induction steps, required lemmas, generalization depth). The system can now select the plan with minimal proof burden, not just the most syntactically natural implementation.

6. Relational Specification Handling: Extend the system's planning to handle multi-API relational contracts (e.g., set-then-get consistency, precedence rules across calls). The system can now generate plans that coordinate proof obligations across multiple function calls, rather than treating each function in isolation.

7. Repository-Aware Planning: Integrate library-level context (existing lemmas, data structures, API patterns) into the planning phase. The system can now reuse known proof patterns and library functions that align with the specification, reducing the need for novel proof construction.

8. Feedback-Driven Replanning Trigger: Implement a threshold-based mechanism that detects when repeated local repairs fail under a plan (e.g., after N failed attempts on the same proof obligation). The system can automatically retreat to replanning, revising the decomposition or bridging predicate, rather than persisting in a doomed repair loop.

9. Cost-Efficiency Optimization: Use the joint planning approach to reduce token consumption and wall-clock time by avoiding full-restart repair cycles. The system can now allocate compute resources more efficiently, focusing effort on plan validation and local elaboration rather than repeated global rewrites.

10. Benchmark-Driven Quality Filtering: Incorporate a three-stage specification quality pipeline (reference-satisfaction, mutation-rejection, LLM review) into the system's training or evaluation loop. The system can now be trained or fine-tuned on specifications that are guaranteed non-trivial and behavior-sensitive, improving its ability to handle realistic, complex verification tasks.

Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction. The de facto workflow decouples the two halves of the problem: first synthesize a program, then attempt to prove it correct. We observe that this sequential pipeline can be both ineffective and inefficient in practice. A program generated without anticipating its proof can be subtly incorrect or structurally difficult to verify, forcing the LLM into brittle repair loops that alternate between patching the code and patching the proof. Inspired by Dijkstra's view that a program and its correctness argument should be developed hand in hand, we propose P cubed, an LLM-based agentic workflow that first derives a unified program-and-proof plan from the specification, then elaborates the implementation and proof scaffold under this shared plan. To evaluate verified code generation in realistic settings, we further introduce Lean4Commit0, a repository-derived, library-level benchmark built by extracting core APIs from real-world software repositories and translating their requirements, including relational specifications across APIs, into Lean tasks. Using four frontier LLM backends, we evaluate P cubed on Verina, AlgoVeri, and our Lean4Commit0 benchmark, where it achieves the highest solve rate in every benchmark--model setting. Compared with the stronger baseline, it improves solve rates by 4.6--11.2 percentage points and reduces per-task API cost by up to roughly 40% and wall-clock time by up to roughly 37% on the difficult subset of each benchmark. A targeted ablation further shows gains of 3.3--8.3 points over implementation-only planning, isolating the benefit of planning the program and proof jointly.