Pith. sign in

REVIEW 3 major objections 5 minor 56 references

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

T0 review · 3 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims that a joint program-and-proof plan raises verified-code-generation solve rates by 4.6–11.2 percentage points across all tested models and benchmarks.

desk verdict Solid empirical paper on joint program-and-proof planning for verified code generation, but the headline gains depend on an unmeasured LLM judge for instruction compliance; worth sending to review with a request to validate that judge. read the letter →

arxiv 2608.09277 v1 pith:QT62LQ6F submitted 2026-08-10 cs.AI cs.PL

Zenan Li , Ziran Yang , Peiyang Song , Zhaoyu Li , Kaiyu Yang This is my paper · ORCID
classification cs.AIcs.PL MSC 68Q60
keywords verifiedcodegenerationLean4LLMagentsprogram-and-proofplanningformalverificationrelationalspecificationsbenchmarkconstruction
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper targets verified code generation, where an LLM must output both a program and a machine-checked proof in Lean 4. It argues that the usual schedule—write the program first, prove it later—fails structurally, because a committed implementation may force a proof shape that was never planned, sending agents into expensive repair loops. P3 instead has the agent first settle a shared plan that fixes the program decomposition, the library lemmas it will use, and the proof obligations including any auxiliary invariant, and only then elaborate both artifacts against that plan. On Verina, AlgoVeri, and a new repository-derived benchmark, Lean4Commit0, P3 posts the highest solve rate in every benchmark-and-model cell, with gains of 4.6–11.2 points over the stronger baseline and 3.3–8.3 points over implementation-only planning, while cutting cost and time on hard tasks by up to roughly 40% and 37%.

What carries the argument

The load-bearing object is the shared plan, a small structured document with four commitments: the formal contract plus any algorithmic instruction; the program decomposition (recursion variable, branches, data representation, termination measure); the concrete library functions and lemmas; and the proof obligations (bridging predicate, induction or case structure, auxiliary lemma statements). It acts as a single point of retreat: elaboration-level failures are repaired in place under the plan, while plan-level failures trigger an explicit return to planning. The plan is lightweight because it is a sketch, not a Lean term, so the agent can compare alternative structural routes before either artifact is written.

What would settle it

Select a random sample of accepted solutions on Verina and AlgoVeri, run each with size-doubled inputs, and compare the observed complexity against the natural-language instruction; if a substantial fraction of judge-approved solutions violate the stated complexity, the solve-rate gap is partly an artifact of the instruction judge rather than of planning.

Watch

Extended reading notes

Core claim

The central discovery is that proof structure is a selection criterion for program structure, not an afterthought. P3 introduces a two-stage agentic workflow: a planning stage proposes and validates a plan that pairs a program sketch with a proof sketch—fixing the recursion or case-split decomposition, the library functions, the bridging predicate, and the auxiliary lemmas—and an elaboration stage writes Lean code and proof scaffolds under that frozen plan, repairing locally when possible and retreating to replanning only when the plan itself cannot carry the proof. The listMax example shows why ordering matters: an accumulator-fold implementation is fine as code but forces proof of a universal fold invariant, while structural recursion lets the postcondition itself serve as the bridging predicate. The authors claim the plan makes the cost of such structural choices visible before any code is committed, and their experiments support that claim across four frontier LLM backends and three benchmarks.

Load-bearing premise

Measured success depends on an LLM judge's verdict that the produced code follows natural-language algorithmic or complexity instructions; a lenient or noisy judge would inflate the reported solve-rate gains even though Lean's kernel objectively checks the formal proof.

Editorial extensions

If this is right

  • If P3's claim holds, agents that plan code and proof jointly should dominate sequential pipelines on any benchmark where proof structure is sensitive to implementation choice.
  • The reported gains imply that planning overhead is small enough for joint planning to beat pure implementation planning on textbook tasks and to be essential on library-level relational tasks.
  • Lean4Commit0-style quality gating—reference satisfaction, mutation rejection, and LLM review—gives a floor for reading future solve rates on repository-derived tasks.
  • The cost and time reductions on difficult tasks imply that the plan-first workflow avoids most full-restart repairs.
  • Because Lean accepts only kernel-checked artifacts, every solved task carries a genuine machine-checked correctness guarantee relative to its shipped specification.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the same co-derivation discipline is ported to SMT-backed verifiers such as Dafny or Verus, the plan would pair loop invariants, decreases clauses, and ghost state with the program structure; the paper's own limitation section calls this transfer plausible but unverified.
  • The reliance on an LLM instruction judge means raw solve rates should be read as the conjunction of two checks; a direct comparison of the judge's verdicts against human judgments of algorithmic compliance would tighten the measurement.
  • A testable extension would vary the plan schema, such as omitting the bridging-predicate or library-support fields, and measure whether gains concentrate on tasks whose specifications share relational structure; the current ablation hints that implementation-only planning can hurt on such tasks.
  • The paper's single-run protocol means the reported gaps of 4–11 points could partly reflect sampling noise; repeated runs on a subset of tasks would bound that uncertainty.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes P3, an LLM agentic workflow for verified code generation in Lean 4 that first produces a joint program-and-proof plan and then elaborates both artifacts under that plan, in contrast to the usual program-then-proof schedule. It also introduces Lean4Commit0, a repository-derived benchmark of 108 libraries with relational specifications, and evaluates P3 against plain and program-then-proof baselines on Verina, AlgoVeri, and Lean4Commit0 using four LLM backends. The reported headline result is that P3 achieves the highest solve rate in all 12 benchmark-model cells, with gains of 4.6--11.2 percentage points over the stronger baseline, and reduces cost and wall-clock time on a difficult subset. The formal part of the solve criterion is Lean kernel acceptance, but the solve rate additionally requires that the implementation satisfy a natural-language algorithmic instruction, a condition judged by an LLM subagent whose reliability is not validated.

Significance. If the central claim holds, the paper makes a useful conceptual contribution: it gives evidence that planning the program and proof together, rather than committing to code first, improves both effectiveness and efficiency in LLM-based verified code generation. The introduction of Lean4Commit0 is a genuine benchmark contribution, with a documented specification-quality pipeline, relational cross-API specifications, and repository-derived tasks that go beyond textbook single-function benchmarks. The evaluation is broad in coverage (three benchmarks, four backends, an ablation, and trace-level analysis), and the formal success signal is machine-checked by the Lean kernel, which is an objective check for the formal component. The main weakness is that the informal component of the solve criterion -- instruction compliance -- is assessed by an unvalidated LLM judge, and all configurations are run only once, so the magnitude and robustness of the reported gains are not yet established.

major comments (3)
  1. [§5.1, Table 2, Appendix E Phase 6] The solve-rate claim rests on an LLM judge whose reliability is never measured. A task is counted as solved only if the solution "satisfies the instruction and passes Lean's checker" (Section 5.1), and the instruction-compliance check is performed by the subagent lean-verifier-instruction, which reads the code region and judges whether it meets the algorithmic intent (Appendix E, Phase 6). No human agreement study, calibration, false-positive analysis, or error analysis is reported for this judge, and each configuration is run once. Since the claimed gains are 4.6--11.2 percentage points, which on Verina (n=189) is roughly 9--21 tasks, a judge bias or leniency of that size would erase the headline result. This concern is method-correlated rather than merely shared across cells: P3 restates the instruction verbatim in its plan and emits plan-documented code, which may systematically influence the same LLM judge even when the output is no more compliant than a baseline's. I would need a validation of this judge -- for example, an independent human annotation of instruction compliance on a stratified sample of accepted and rejected solutions, with reported agreement and a per-cell false-positive rate -- before the Table 2 deltas can be taken at face value.
  2. [§5.1, Appendix C, Table 2] The statistical basis for the central claim is a single run per (task, model, method) configuration. The paper acknowledges this in Appendix C, but the acknowledgment does not address the fact that the reported gaps are small relative to the expected stochastic variance of LLM agents. For example, a 5.2-point gain on Verina corresponds to about 10 tasks out of 189; with a single run, the 95% binomial confidence interval for a single method's solve rate is already about ±7 points, so the difference between two methods is not statistically distinguishable on a per-cell basis. The consistency across all 12 cells is suggestive, but it does not replace variance estimation because all cells share the same pipeline and the same unvalidated judge. I recommend reporting confidence intervals over tasks (e.g., bootstrap or exact binomial intervals), and ideally running a repeated-seed experiment on a representative subset to estimate within-task stochasticity. Without this, the headline "P3 attains the best solve rate on every cell" should be weakened or supported with variance-aware analysis.
  3. [§5.2, Appendix J, Table 5] The efficiency comparison on the "difficult subset" is defined as the top 25% of tasks ranked by mean cost across the three methods (Section 5.2, Appendix J). This selection is not independent of the methods being compared: because P3 is cheaper on many tasks, the mean cost used for selection is pulled down by P3 itself, which can exclude tasks where P3 is expensive and include tasks where the baselines are expensive. This creates a selection bias that can inflate the reported cost and time reductions (up to 39.6% and 37.2%). The efficiency claim would be more convincing if the difficult subset were defined by a method-independent criterion -- for example, tasks that all methods fail to solve within a time limit, or tasks selected by a fixed feature such as length or formal-spec complexity -- or if the analysis were repeated on the full set with appropriate conditioning. As written, the efficiency result is confounded by the selection rule.
minor comments (5)
  1. [§1, Figure 1] Figure 1 is visually clear, but the caption would benefit from stating explicitly that the plan is produced before either the program or proof is elaborated; the current abstract already says this, so the figure caption is just a presentation issue.
  2. [§4.2, Table 1] The quality score Quality(σ) = 0.5·Mutation + 0.5·Review is presented without a justification for the equal weighting; a brief sentence explaining why the two components are weighted equally would improve reproducibility and interpretability.
  3. [§5.1] The phrase "we augment each task with a natural-language instruction specifying the expected algorithmic strategy or asymptotic complexity" would benefit from listing where these instructions are released and how they were authored; the Figshare link is given, but not an explicit pointer to the instruction files.
  4. [Appendix I] The plan-retention analysis is informative, but the sentence "retention is only a proxy for proof-burden prediction accuracy" is important and could be moved earlier in the appendix to frame the numbers correctly.
  5. [Appendix E] The skill description says "Self-review is not a gate" and delegates the plan gate to lean_plan_verify or lean-verifier-plan, but the appendix does not describe how these plan-gate subagents are validated; a short note on their reliability would be useful given that the paper's core claim is about planning quality.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: P3's headline solve-rate gains are empirically measured against Verina, AlgoVeri, and the new Lean4Commit0 benchmark; self-citations are present but not load-bearing.

full rationale

The central claim—that joint program-and-proof planning improves verified-code-generation solve rates—is established by direct measurement on external benchmarks (Verina, AlgoVeri) and on the newly introduced Lean4Commit0 benchmark. No equation in the paper fits a parameter and then redeclares that fit as a prediction; P3 is an agent workflow, and its reported deltas in Table 2 are observed solve-rate differences, not derived quantities. The self-citations that appear (Goedel-Code-Prover [10], AlgoVeri [15], Learning to Disprove [25]) are used as benchmarks, baselines in related work, or component tools; none of these citations supplies the paper's central conclusion. Lean4Commit0 is authored by the same team, but its construction pipeline (reference satisfaction, mutation rejection, LLM review) is independent of the P3 method, and the method's effectiveness is also measured on the pre-existing Verina and AlgoVeri suites. The paper's solve criterion does rely on an LLM judge ('lean-verifier-instruction', Appendix E Phase 6) for the non-formal algorithmic-instruction part, and the paper acknowledges this limitation; however, this is a measurement-validity concern rather than a circular derivation, since the judge is not an input from which the reported gains are algebraically forced. The paper is also transparent about single runs and lack of significance testing. Under the defined circularity patterns, no step exhibits a self-definitional reduction, a fitted input renamed as prediction, a load-bearing self-citation chain, or a uniqueness theorem imported from the authors' prior work. The score of 2 reflects the presence of several same-group citations and an in-house benchmark, while the central empirical comparison retains independent content.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The measurement claims rest on benchmarks, budgets, and judges chosen by the authors. No mathematical derivation is involved, so the ledger records design choices and domain assumptions rather than fitted theory parameters.

free parameters (4)
  • Quality admission threshold = 80%
    Lean4Commit0 admits a task only if its aggregate quality score reaches this threshold; the value is chosen by the authors, not derived.
  • Quality score weights = 0.5 * Mutation + 0.5 * Review
    The two quality components are combined with equal weights chosen by hand.
  • Per-task API budget = 30.0 USD and 180 minutes
    Budgets are fixed across methods and affect both solve rates and the relative efficiency comparison.
  • Difficult subset fraction = top 25% by mean cost
    Efficiency savings are reported on the subset of tasks ranked highest by mean cost across the three methods; this post-hoc selection can exaggerate the gains.
assumptions (5)
  • domain assumption Lean 4 kernel acceptance correctly establishes that the generated program satisfies the formal specification.
    The solve-rate metric treats Lean acceptance as ground truth for the formal part (Section 2 and Section 5.1).
  • domain assumption The lean-verifier-instruction judge reliably decides whether an implementation meets the added algorithmic or complexity instruction.
    A task counts as solved only if an LLM judge passes it (Appendix E Phase 6); the reliability of this judge is not measured.
  • ad hoc to paper The natural-language algorithmic instructions added to Verina and AlgoVeri preserve the original tasks and are applied fairly to all methods.
    Verina and AlgoVeri are augmented with instructions they did not originally contain (Section 5.1), changing the evaluation protocol.
  • domain assumption Lean4Commit0 specifications adequately capture intended library behavior via reference satisfaction and mutation rejection.
    Specification adequacy cannot be checked directly; the quality pipeline is a proxy (Section 4.2).
  • domain assumption Closed-source LLM backends are treated as stable enough that one run per configuration estimates method performance.
    Single-run execution without variance estimation assumes sample noise does not dominate the reported differences (Appendix C).

how reviews work

0 comments
Cite this review

Pith. "Pith review of P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation." pith.science (2026). https://pith.science/paper/QT62LQ6F

@misc{pith2026260809277,
  author       = {Pith},
  title        = {Pith review of: P$^3$: Joint Program-and-Proof Planning for Verified Code Generation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QT62LQ6F}},
  note         = {Machine review of arXiv:2608.09277}
}
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.

Figures

Figures reproduced from arXiv: 2608.09277 by the authors.

Figure 1
Figure 1. Our proposed framework. Top: the program-then-proof pipeline commits to an implemen￾tation before the proof’s structure is known, so the two artifacts only meet at verification time and mismatches trigger coupled code/proof repair. Bottom: our workflow first settles a shared structural plan, then elaborates the program and proof scaffold against the same plan, so that consistency holds by construction rather than be… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

56 extracted references · 31 canonical work pages

  1. [1]

    Large language model-based agents for software engineering: A survey.ACM Transactions on Software Engineering and Methodology, 2024

    Junwei Liu, Kaixin Wang, Yixuan Chen, Xin Peng, Zhenpeng Chen, Lingming Zhang, and Yiling Lou. Large language model-based agents for software engineering: A survey.ACM Transactions on Software Engineering and Methodology, 2024

    2024

  2. [2]

    A survey on code generation with llm-based agents.arXiv preprint arXiv:2508.00083, 2025

    Yihong Dong, Xue Jiang, Jiaru Qian, Tian Wang, Kechi Zhang, Zhi Jin, and Ge Li. A survey on code generation with llm-based agents.arXiv preprint arXiv:2508.00083, 2025

    arXiv 2025

  3. [3]

    A survey on large language models for code generation.ACM Transactions on Software Engineering and Methodology, 35 (2):1–72, 2026

    Juyong Jiang, Fan Wang, Jiasi Shen, Sungju Kim, and Sunghun Kim. A survey on large language models for code generation.ACM Transactions on Software Engineering and Methodology, 35 (2):1–72, 2026

    2026

  4. [4]

    The lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. InInternational Conference on Automated Deduction, pages 625–635. Springer, 2021

    2021

  5. [5]

    Growing mathlib: maintenance of a large scale mathematical library

    Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Roth- gang, and Damiano Testa. Growing mathlib: maintenance of a large scale mathematical library. InInternational Conference on Intelligent Computer Mathematics, pages 51–70. Springer, 2025

    2025

  6. [6]

    Cslib: The lean computer science library.arXiv preprint arXiv:2602.04846, 2026

    Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, and Sorrachai Yingchareonthawornchai. Cslib: The lean computer science library.arXiv preprint arXiv:2602.04846, 2026

    arXiv 2026

  7. [7]

    Verina: Benchmarking verifiable code generation.arXiv preprint arXiv:2505.23135, 2025

    Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, and Dawn Song. Verina: Benchmarking verifiable code generation.arXiv preprint arXiv:2505.23135, 2025

    arXiv 2025

  8. [8]

    Proving the coding interview: A benchmark for formally verified code generation

    Quinn Dougherty and Ronak Mehta. Proving the coding interview: A benchmark for formally verified code generation. In2025 IEEE/ACM International Workshop on Large Language Models for Code (LLM4Code), pages 72–79. IEEE, 2025

    2025

Show all 56 references
  1. [9]

    Holden, Gabriel Synnaeve, and Peter O’Hearn

    Fabian Gloeckle, Mantas Baksys, Darius Feher, Kunhao Zheng, Amaury Hayat, Sean B. Holden, Gabriel Synnaeve, and Peter O’Hearn. Wybecoder: Verified imperative code generation.arXiv preprint arXiv:2603.29088, 2026

    2026 arXiv

  2. [10]

    Goedel-code-prover: Hierarchical proof search for open state-of-the-art code verification.arXiv preprint arXiv:2603.19329, 2026

    Zenan Li, Ziran Yang, Deyuan He, Haoyu Zhao, Andrew Zhao, Shange Tang, Kaiyu Yang, Aarti Gupta, Zhendong Su, and Chi Jin. Goedel-code-prover: Hierarchical proof search for open state-of-the-art code verification.arXiv preprint arXiv:2603.19329, 2026

    2026 arXiv

  3. [11]

    Autoverus: Automated proof generation for rust code.Proceedings of the ACM on Programming Languages, 9(OOPSLA2): 3454–3482, 2025

    Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, et al. Autoverus: Automated proof generation for rust code.Proceedings of the ACM on Programming Languages, 9(OOPSLA2): 3454–3482, 2025

    2025

  4. [12]

    Verusage: A study of agent-based verification for rust systems.arXiv preprint arXiv:2512.18436, 2025

    Chenyuan Yang, Natalie Neamtu, Chris Hawblitzel, Jacob R Lorch, and Shan Lu. Verusage: A study of agent-based verification for rust systems.arXiv preprint arXiv:2512.18436, 2025

    2025 arXiv

  5. [13]

    Exverus: Verus proof repair via counterexample reasoning.arXiv preprint arXiv:2603.25810, 2026

    Jun Yang, Yuechun Sun, Yi Wu, Rodrigo Caridad, Yongwei Yuan, Jianan Yao, Shan Lu, and Kexin Pei. Exverus: Verus proof repair via counterexample reasoning.arXiv preprint arXiv:2603.25810, 2026

    2026

  6. [14]

    Dijkstra.A Discipline of Programming

    Edsger W. Dijkstra.A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ, 1976

    1976

  7. [15]

    Algoveri: An aligned benchmark for verified code generation on classical algorithms.arXiv preprint arXiv:2602.09464, 2026

    Haoyu Zhao, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V Veeravalli, Aarti Gupta, and Sanjeev Arora. Algoveri: An aligned benchmark for verified code generation on classical algorithms.arXiv preprint arXiv:2602.09464, 2026

    2026 arXiv

  8. [16]

    Dafny: An automatic program verifier for functional correctness

    K Rustan M Leino. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning, pages 348–370. Springer, 2010. 10

    2010

  9. [17]

    Dependent types and multi-monadic effects in F ⋆

    Nikhil Swamy, C˘at˘alin Hri¸ tcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, et al. Dependent types and multi-monadic effects in F ⋆. InProceedings of the 43rd annual ACM SI...

    2016

  10. [18]

    Verus: Verifying rust programs using linear ghost types.Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286–315, 2023

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying rust programs using linear ghost types.Proceedings of the ACM on Programming Languages, 7(OOPSLA1):286–315, 2023

    2023

  11. [19]

    Springer, 2004

    Yves Bertot and Pierre Castéran.Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Springer, 2004

    2004

  12. [20]

    Paulson, and Markus Wenzel.Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 ofLecture Notes in Computer Science

    Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 ofLecture Notes in Computer Science. Springer, 2002

    2002

  13. [21]

    Clever: A curated benchmark for formally verified code generation

    Amitayush Thakur, Jasper Lee, George Tsoukalas, Meghana Sistla, Matthew Zhao, Stefan Zetzsche, Greg Durrett, Yisong Yue, and Swarat Chaudhuri. Clever: A curated benchmark for formally verified code generation. InThe Thirty-ninth Annual Conference on Neural Information Processi...

    2025

  14. [22]

    Commit0: Library generation from scratch.arXiv preprint arXiv:2412.01769, 2024

    Wenting Zhao, Nan Jiang, Celine Lee, Justin T Chiu, Claire Cardie, Matthias Gallé, and Alexan- der M Rush. Commit0: Library generation from scratch.arXiv preprint arXiv:2412.01769, 2024

    2024 arXiv

  15. [23]

    On the interplay between consistency, completeness, and correctness in requirements evolution.Information and Software technology, 45(14):993–1009, 2003

    Didar Zowghi and Vincenzo Gervasi. On the interplay between consistency, completeness, and correctness in requirements evolution.Information and Software technology, 45(14):993–1009, 2003

    2003

  16. [24]

    Empirical research on requirements quality: a systematic mapping study.Requirements Engineering, 27 (2):183–209, 2022

    Lloyd Montgomery, Davide Fucci, Abir Bouraffa, Lisa Scholz, and Walid Maalej. Empirical research on requirements quality: a systematic mapping study.Requirements Engineering, 27 (2):183–209, 2022

    2022

  17. [25]

    Learning to disprove: For- mal counterexample generation with large language models.arXiv preprint arXiv:2603.19514, 2026

    Zenan Li, Zhaoyu Li, Kaiyu Yang, Xiaoxing Ma, and Zhendong Su. Learning to disprove: For- mal counterexample generation with large language models.arXiv preprint arXiv:2603.19514, 2026

    2026

  18. [26]

    Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover, 3

    Oliver Dressler. Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover, 3

  19. [27]

    Lean 4 Skills: Theorem proving skill and workflow pack for AI coding agents, October 2025

    Cameron Freer. Lean 4 Skills: Theorem proving skill and workflow pack for AI coding agents, October 2025. URLhttps://github.com/cameronfreer/lean4-skills

    2025

  20. [28]

    George C. Necula. Proof-carrying code. InProceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106–119, 1997

    1997

  21. [29]

    Re:Form – reducing human priors in scalable formal software verification with RL in LLMs: A preliminary study on Dafny.arXiv preprint arXiv:2507.16331, 2025

    Chuanhao Yan, Fengdi Che, Xuhan Huang, Xu Xu, Xin Li, Yizhi Li, Xingwei Qu, Jingzhe Shi, Chenghua Lin, Yaodong Yang, Binhang Yuan, Hang Zhao, Yu Qiao, Bowen Zhou, and Jie Fu. Re:Form – reducing human priors in scalable formal software verification with RL in LLMs: A preliminar...

    2025 arXiv

  22. [30]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), pa...

    2023

  23. [31]

    An in-context learning agent for formal theorem-proving

    Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem-proving. InInternational Conference on Learning Representations (ICLR), 2024

    2024

  24. [32]

    Planning to hammer: Difficulty-aware decomposition for automating Rocq proofs.arXiv preprint arXiv:2606.17981, 2026

    Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, and Xiaoxing Ma. Planning to hammer: Difficulty-aware decomposition for automating Rocq proofs.arXiv preprint arXiv:2606.17981, 2026. 11

    2026 arXiv

  25. [33]

    Neuro-symbolic proof generation for scaling systems software verification

    Baoding He, Zenan Li, Wei Sun, Yuan Yao, Taolue Chen, Xiaoxing Ma, and Zhendong Su. Neuro-symbolic proof generation for scaling systems software verification. In20th USENIX Symposium on Operating Systems Design and Implementation (OSDI 26), pages 2533–2550, Seattle, W A, July ...

    2026

  26. [34]

    Jiang, Jia Deng, Stella Biderman, and Sean Welleck

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics.International Conference on Learning Representations (ICLR), 2024

    2024

  27. [35]

    DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data.arXiv preprint arXiv:2405.14333, 2024

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing theorem proving in LLMs through large-scale synthetic data.arXiv preprint arXiv:2405.14333, 2024

    2024 arXiv

  28. [36]

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.arXiv preprint arXiv:2504.21801, 2025

    2025 arXiv

  29. [37]

    Horváth, Goran Žuži´c, Erin Wieser, Anian Huang, Julian Schrittwieser, et al

    Thomas Hubert, Rishabh Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žuži´c, Erin Wieser, Anian Huang, Julian Schrittwieser, et al. Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, 2025. doi: 10.1038/s41586-025-09833-y

    2025 doi

  30. [38]

    Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor,Mathematical Aspects of Computer Science, pages 19–32. American Mathematical Society, 1967

    1967

  31. [39]

    C. A. R. Hoare. An axiomatic basis for computer programming.Communications of the ACM, 12(10):576–580, 1969

    1969

  32. [40]

    Texts and Monographs in Computer Science

    David Gries.The Science of Programming. Texts and Monographs in Computer Science. Springer, 1981

    1981

  33. [41]

    Program synthesis from polymor- phic refinement types

    Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. Program synthesis from polymor- phic refinement types. InProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 522–538, 2016

    2016

  34. [42]

    Self-planning code generation with large language models.ACM Transactions on Software Engineering and Methodology, 2024

    Xue Jiang, Yihong Dong, Lecheng Wang, Zheng Fang, Qiwei Shang, Ge Li, Zhi Jin, and Wenpin Jiao. Self-planning code generation with large language models.ACM Transactions on Software Engineering and Methodology, 2024

    2024

  35. [43]

    Plan-and-solve prompting: Improving zero-shot chain-of-thought reasoning by large language models

    Lei Wang, Wanyu Xu, Yihuai Lan, Zhiqiang Hu, Yunshi Lan, Roy Ka-Wei Lee, and Ee- Peng Lim. Plan-and-solve prompting: Improving zero-shot chain-of-thought reasoning by large language models. InProceedings of the 61st Annual Meeting of the Association for Computational Linguisti...

    2023

  36. [44]

    A benchmark for vericoding: Formally verified program synthesis.arXiv preprint arXiv:2509.22908, 2025

    Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, Miranda Zhao, Max Tan, and Max Tegmark. A benchmark for vericoding: Formally verified program synthesis.arXiv...

    2025

  37. [45]

    DafnyBench: A benchmark for formal software verification.arXiv preprint arXiv:2406.08467, 2024

    Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, and Max Tegmark. DafnyBench: A benchmark for formal software verification.arXiv preprint arXiv:2406.08467, 2024

    2024 arXiv

  38. [46]

    Z3: An efficient smt solver

    Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. InInternational conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340. Springer, 2008

    2008

  39. [47]

    cvc5: A versatile and industrial-strength smt solver

    Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, et al. cvc5: A versatile and industrial-strength smt solver. InInternational Conference on Tools and Algorithms for the Co...

    2022

  40. [49]

    - Exit: every sorry enumerated; instruction source located or confirmed absent

    Understand - Produces: classified sorry inventory (code vs proof); spec + instruction restated. - Exit: every sorry enumerated; instruction source located or confirmed absent

  41. [50]

    - Exit: plan file exists on disk; all required sections present; any locked-algorithm instruction is restated verbatim under `## Restated contract`

    Co-derive plan - Produces: <file>.plan.md with the schema's required sections. - Exit: plan file exists on disk; all required sections present; any locked-algorithm instruction is restated verbatim under `## Restated contract`. May not edit the .lean file before this artifact

  42. [51]

    - Exit: verdict is PASS-PLAN

    Plan gate - Produces: external PASS-PLAN / FAIL verdict from`lean_plan_verify`(or the`lean-verifier-plan`subagent). - Exit: verdict is PASS-PLAN. On FAIL, revise the plan file and re-run the same gate. Self-review is not a gate

  43. [52]

    `decreasing_by sorry`may stay (or be omitted if Lean auto-derives)

    Emit code sketch + proof sketch - Produces: code bodies written in full; proof bodies left as`sorry`. `decreasing_by sorry`may stay (or be omitted if Lean auto-derives). Plus stub statements for the main theorem and any auxiliary lemmas. - Exit:`lean_diagnostic_messages`report...

  44. [53]

    - Exit: no errors and no in-scope sorries

    Fill tactic details - Produces: all tactic-level sorries closed (proof sorries and any `decreasing_by sorry`-- both are tactic blocks). - Exit: no errors and no in-scope sorries

  45. [54]

    - Exit:`lean-verifier-mechanical`returns PASS-MECHANICAL and `lean-verifier-instruction`returns PASS-INSTRUCTION; act on each verdict's Action: line otherwise

    Quality gate (final) - Produces: go / no-go verdict on delivery. - Exit:`lean-verifier-mechanical`returns PASS-MECHANICAL and `lean-verifier-instruction`returns PASS-INSTRUCTION; act on each verdict's Action: line otherwise. Plan schema (Phase 2 artifact).The plan file at <fil...

  46. [55]

    Runs sorry scan, compile check, axiom check

    Mechanical gate: lean-verifier-mechanical. Runs sorry scan, compile check, axiom check. On FAIL, parent re-enters Phase 5 targeting the failing sorry / error. 16

  47. [56]

    Reads the @start code

    Instruction compliance: lean-verifier-instruction. Reads the @start code ... @end code region and judges whether the implementation satisfies the Instruction's complexity / algorithmic intent. On FAIL, parent reverts and re-enters Phase 2 with a different algorithm or stdlib p...

  48. [2025]

    URLhttps://github.com/oOo0oOo/lean-lsp-mcp

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.