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

arXiv: https://arxiv.org/abs/2608.09277 · HTML: https://mlsanity.com/paper/2608.09277/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 47 references that are in the map.
- First posted on arXiv 10 Aug 2026.

## Builds on (most cited first, 29 of 29)

- [A Survey on Large Language Models for Code Generation](https://mlsanity.com/paper/2406.00515/) (2024)
- [Plan-and-Solve Prompting: Improving Zero-Shot Chain-of-Thought Reasoning by Large Language Models](https://mlsanity.com/paper/2305.04091/) (2023)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Large Language Model-Based Agents for Software Engineering: A Survey](https://mlsanity.com/paper/2409.02977/) (2024)
- [Self-planning Code Generation with Large Language Models](https://mlsanity.com/paper/2303.06689/) (2023)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [A Survey on Code Generation with LLM-based Agents](https://mlsanity.com/paper/2508.00083/) (2025)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [Commit0: Library Generation from Scratch](https://mlsanity.com/paper/2412.01769/) (2024)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [Program Synthesis from Polymorphic Refinement Types](https://mlsanity.com/paper/1510.08419/) (2015)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [Proving the Coding Interview: A Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2502.05714/) (2025)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification](https://mlsanity.com/paper/2603.19329/) (2026)
- [CSLib: The Lean Computer Science Library](https://mlsanity.com/paper/2602.04846/) (2026)
- [Growing Mathlib: maintenance of a large scale mathematical library](https://mlsanity.com/paper/2508.21593/) (2025)
- [Learning to Disprove: Formal Counterexample Generation with Large Language Models](https://mlsanity.com/paper/2603.19514/) (2026)
- [Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs](https://mlsanity.com/paper/2606.17981/) (2026)
- [WybeCoder: Verified Imperative Code Generation](https://mlsanity.com/paper/2603.29088/) (2026)
- [ExVerus: Verus Proof Repair via Counterexample Reasoning](https://mlsanity.com/paper/2603.25810/) (2026)
- [Neuro-Symbolic Proof Generation for Scaling Systems Software Verification](https://mlsanity.com/paper/2603.19715/) (2026)

## Built on by (most cited first, 2 of 2)

- [LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs](https://mlsanity.com/paper/2610.08246/) (2026)
- [Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification](https://mlsanity.com/paper/2610.09681/) (2026)

## Abstract (arXiv)

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 P3, 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 P3 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.