P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation
2026-08-10 • Artificial Intelligence
Artificial IntelligenceProgramming Languages
AI summaryⓘ
The authors address the challenge of generating computer programs that are correct by design using large language models (LLMs). They point out that creating a program first and then proving its correctness separately can cause errors and inefficiencies. To fix this, they propose a method called P³, which plans both the program and its proof together from the start, making the process smoother and more reliable. They also introduce a new benchmark, Lean4Commit0, based on real software code to test their approach. Their experiments show that P³ performs better and faster than previous methods in proving program correctness.
large language modelverified code generationformal specificationproof assistantprogram synthesisproof planningLean4benchmarkcorrectness proofsoftware verification
Authors
Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li, Kaiyu Yang
Abstract
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^3$, 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^3$ 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.