Pith. sign in

REVIEW 3 major objections 5 minor 48 references

Vero: Can AI Agents Build Formally Verified Software Repositories?

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

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

Pith's one-line read Vero is the first repository-level benchmark for joint code-and-proof synthesis, and the strongest agent fully solves only 27 of 43 instances.

desk verdict Vero is a genuinely new, carefully built repository-level benchmark for verified code generation, and the exact solve counts matter less than the reproducible measurement and the honest audit trail. read the letter →

arxiv 2608.13522 v1 pith:CJ6EAXBJ submitted 2026-08-13 cs.LG cs.AIcs.LOcs.PLcs.SE

Zhe Ye , Hantao Lou , Yuechun Sun , Peiyang Song , Zhengxu Yan , Timothe Kasriel , Qingyang Zhang , Kaiyu Yang
show 3 more authors
Soonho Kong Jingxuan He Dawn Song
This is my paper · ORCID
classification cs.LGcs.AIcs.LOcs.PLcs.SE
keywords verifiedcodegenerationformalverificationLean4AIcodingagentsrepository-levelbenchmarkproofsynthesisimplementationaudit
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

Vero is a benchmark that asks AI coding agents to produce an entire Lean 4 repository from fixed API signatures and manually written specifications, rather than a single function or a supplied implementation. The paper's central claim is that this joint implementation-and-proof task is the right unit of measurement for trustworthy AI-generated software, and that current agents are not ready for it: the strongest configuration fully solves 27 of 43 instances in code-and-proof mode, and 10 instances resist all eight configurations. The authors show that the bottleneck is not local proof skill, since the best agent passes about 87% of individual specifications, but repository-scale organization—discovering shared invariants and building reusable lemma libraries. To keep benchmark defects from masquerading as agent failures, Vero includes a formal audit route that accepts machine-checked negative evidence and uses it to repair specifications.

What carries the argument

The central mechanism is the RepoImpl interface structure: every API signature is a field of one structure and each specification is a predicate over that structure, not over a fixed function. Because the proof target can be swapped from the reference implementation to the agent's own code, the same instance supports both task modes and the audit path. The formal audit mechanism accepts three forms of machine-checked negative evidence—an unsatisfiable individual specification, a reference implementation that violates a specification, and inconsistent specification sets—and routes them to curator repair, which during development surfaced 38 adjudicated defects across 9 instances.

What would settle it

Have an independent team rewrite the specifications for a random sample of instances straight from the upstream documentation and tests, then rerun the strongest agent; if many previously unsolved repositories flip to solved (or solved ones flip to unsolved), the measured capability gap is partly an artifact of specification wording. A sharper check: for the ten instances that resist all eight configurations, provide a human-written lemma library for the missing shared invariants and see whether the same agents then close the repositories; if they do not, the bottleneck is not organization but something else.

Watch

Extended reading notes

Core claim

Vero claims to be the first repository-level benchmark that evaluates agents on jointly synthesizing implementations and machine-checked Lean 4 proofs. Each of its 43 instances is a multi-module project frozen around a fixed interface structure: all API implementations are fields of a single RepoImpl structure, and every one of the 2,705 specifications is a proposition parameterized over that structure. This makes proof-only and code-and-proof modes two instances of the same format, and it lets the audit mechanism switch the proof target to a formal counterexample. Empirically, agents pass most specifications in isolation but rarely finish a repository: full solves require cross-module invariants and helper lemma libraries, and the ten unsolved repositories mark the current frontier.

Load-bearing premise

The benchmark's conclusions stand on the assumption that the 2,705 manually curated Lean 4 specifications faithfully encode what the upstream programs are supposed to do; the audit mechanism can certify formal satisfiability, but it cannot certify that a satisfiable specification is the right one.

Editorial extensions

If this is right

  • Because roughly 87% per-specification pass rates leave most repositories unfinished, full-repository verification should be scored as an all-or-nothing property rather than by partial coverage.
  • Reusable helper lemmas carry most of the proof text in completed repositories, so agent designs that explicitly plan shared lemma libraries should be the next target for improvement.
  • Implementation freedom helps only the strongest agents; weaker configurations spend their budget on the extra implementation obligation and finish fewer repositories, so code-and-proof and proof-only measure different capabilities.
  • Without the formal audit mechanism, the 38 latent specification defects found during curation would have been misattributed to agent failures, so benchmark quality depends on formal negative evidence.
  • Ten instances and 219 specifications resist every tested configuration, giving a concrete, inspectable frontier for future work.

Reading between the lines

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

  • A natural next step is to add complexity specifications, since agents already trade asymptotic efficiency for provability when the proof obligation is the binding constraint.
  • The audit mechanism should run continuously after release: stronger future agents will keep producing negative proofs that expose new latent benchmark errors, so the benchmark and the agents can improve together.
  • The observed pattern that agents freeze their implementations early and then grind on proofs suggests a testable design change: an agent that revisits its definitions after repeated failures on a bridging lemma would likely close more hard repositories.
  • Porting Vero to another proof assistant would test whether the gap between per-specification and per-repository success rates is about repository organization generally or about Lean specifically.
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. This paper introduces Vero, a repository-level benchmark for verified code generation in Lean 4, constructed from 43 instances translated from Dafny, Verus, Coq, and Python repositories, with 743 scored APIs and 2,705 scored specifications. The benchmark supports both proof-only and code-and-proof evaluation modes, includes an anti-cheating grader and a formal audit mechanism that accepts machine-checked negative evidence about specifications, and is evaluated with four frontier coding-agent configurations. The authors report that the strongest configuration fully solves only 27 of 43 instances in code-and-proof mode and 25 in proof-only mode, that 10 instances resist all eight evaluated configurations, and that successful runs depend on building reusable lemma libraries rather than local proof skill.

Significance. If the benchmark specifications are semantically faithful, Vero is a valuable contribution to the verified-code-generation literature: it is the first benchmark, to my knowledge, to require joint implementation and proof synthesis at repository scale, and it does so in a multi-language, multi-domain setting. The paper's strengths include its detailed anti-cheating layers with concrete attack examples, the formal audit mechanism with human-adjudicated case studies, per-instance pass counts in the appendix, and the authors' willingness to manually inspect substitutions and failure artifacts. The main scientific value as evidence about agent verification capability, however, rests on the semantic fidelity of 2,705 manually curated specifications, which is also the point of greatest residual risk.

major comments (3)
  1. [§3.3, §3.5, §5, Appendix F] The paper's central interpretation that the 10 'resists all configurations' instances and the 27-of-43 ceiling reflect a gap in agents' verification capability presupposes that every one of the 2,705 specifications is semantically faithful to the upstream repository and satisfiable by the reference implementation. Appendix F directly documents that this presupposition failed 38 times across 9 instances, including a directly contradictory pair on verdict and false length assumptions on verified_bitmasks, all of which survived type-checking and manual review. Section 5 concedes that the audit certifies formal satisfiability but not semantic correctness, and the benchmark deliberately contains no Lean ground-truth proofs as a contamination safeguard, so there is no positive machine-checked certificate that the remaining specifications hold of the reference implementations. A false or unsatisfiable residual specification would make a proof-only instance unsolvable by construction and a code-and-proof instance nearly so, inflating both the 'resists all configurations' count and the 27/43 ceiling. I request an additional validation artifact: for every instance, a curator-written sanity proof in a branch not exposed to agents that each specification holds of the reference implementation, or, failing that, a quantitative residual-risk analysis reporting how many of the 2,705 specifications were formally audited and with what outcome.
  2. [§4.2, Appendix G, Appendix H.4] The claim that code-and-proof mode measures repository-scale verified software generation is weakened by implementation substitution, which the paper itself documents. In Appendix G, the munkres Hungarian-algorithm reference is replaced by a 164-line permutation enumeration by three agents, and in Appendix H.4 sortedcontainers' O(log n) bisection is replaced by an O(n) linear scan; across five audited pairs the agents close 250 specifications in code-and-proof versus 201 in proof-only. These are behaviorally correct with respect to the scored specifications but are not faithful reconstructions of the upstream repositories, and the missing cost behavior is explicitly a gap in the metric. The paper should separate 'faithful' full solves from 'substituted' full solves in all headline numbers and either add complexity specifications to the benchmark or state clearly that the benchmark deliberately measures specification satisfaction rather than repository reconstruction.
  3. [§4.1, Figure 3, Table 4] All reported full-solve counts are based on a single run of each configuration per instance. LLM-agent outcomes are stochastic, and full solve is a Boolean decision, so the point estimates 27, 25, 8, and 2, and the exact ordering of configurations, may not be stable. The 'frontier-resistant' claim depends on these counts. Please add at least three repeated runs for the strongest configuration on a subset of instances, or a small multi-run study for all configurations, and report the spread; alternatively, explicitly qualify the headline counts as single-sample observations, since the per-instance pass-count table alone does not provide this information.
minor comments (5)
  1. [§2, reference [29]] The text credits CoqStoq to reference [29], but the reference list entry [29] is 'Rango: Adaptive retrieval-augmented proving...' by Thompson et al.; please check whether this is the intended citation or add the missing CoqStoq reference.
  2. [§3.5, Eq. (3)] The notation overloads S as both a set and a proposition (for example, '∀ S∈S′' and later 'S(impl)' appear in the same formula); using lower-case letters for individual propositions would make the condition clearer.
  3. [Figure 3(c) caption] The caption 'Exact full-solve matrix' is not self-explanatory; clarify what the rows and columns represent and what the entries 0×, 1×, 2×, and ≥3× mean.
  4. [Appendix H.1, deposit_sc proof block] The proof of the auxiliary conjunction appears to be cut off after 'induction t ...' with empty lines; please include the complete proof or an explicit ellipsis.
  5. [Table 4, dedekind_reals rows] The dedekind_reals rows show 0/82 in every cell; even if the instance is intended as a hard case, the main text should explicitly state whether the audit found any specification defects there, since a uniform 0 across all configurations is exactly the pattern a false or unsatisfiable specification would produce.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: Vero reports direct empirical measurements from a fixed benchmark and grading harness, with no fitted-input prediction loop or load-bearing self-citation.

full rationale

Vero is a benchmark and evaluation paper rather than a derivation chain: the central claims are the measured solve counts (e.g., 27/43 in code-and-proof) obtained by running fixed agent configurations against a frozen Lean 4 scaffold and grading with an independent rebuild, axiom allowlist, and declaration screening. No parameter is fitted to a subset of results and then renamed as a prediction; the benchmark specifications and reference implementations are manually curated and the audit mechanism's negative certificates are machine-checked by Lean and adjudicated by human curators. The same class of agents can propose audit certificates, but acceptance requires a formal Lean proof plus human review against upstream sources, so the audit is not circular. Self-citations such as VERINA and LeanDojo appear only in related-work positioning and are not load-bearing for Vero's results. The acknowledged limitation that the audit cannot certify semantic correctness of specifications is a validity caveat about benchmark fidelity, not a circularity in the paper's argument.

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

The central claims are empirical, so the ledger records benchmark-validity assumptions the results rest on rather than fitted parameters. No free parameters or invented entities are present.

assumptions (4)
  • standard math Lean 4's kernel checks are the ground truth for proof correctness.
    The benchmark and the grader compile instances with Lean v4.29.1; the paper relies on kernel checking to validate agent proofs and audit certificates.
  • domain assumption The curated specifications faithfully represent upstream behavior.
    Track 2 specifications are written by the authors from docs and tests, and Track 1 are translations of existing formalizations. Section 5 notes that this cannot be guaranteed by the audit mechanism.
  • domain assumption The anti-cheating layers prevent all reward hacking.
    Three layers are described in Appendix D, but the paper notes that the dijkstar attack was found only during development, so the guarantee is empirical rather than formal.
  • domain assumption The evaluated models have not memorized the novel Lean formalizations.
    The contamination argument in Section 3.4 assumes no public Lean ground truth exists for the translated instances, which is plausible but not machine-checkable.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Vero: Can AI Agents Build Formally Verified Software Repositories?." pith.science (2026). https://pith.science/paper/CJ6EAXBJ

@misc{pith2026260813522,
  author       = {Pith},
  title        = {Pith review of: Vero: Can AI Agents Build Formally Verified Software Repositories?},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CJ6EAXBJ}},
  note         = {Machine review of arXiv:2608.13522}
}
read the original abstract

AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.

Figures

Figures reproduced from arXiv: 2608.13522 by the authors.

Figure 1
Figure 1. Vero’s end-to-end construction and evaluation workflow. Human-gated curation converts real-world Python and formal-language repositories into Lean 4 benchmark instances with fixed definitions, API signatures, specifications, and reference implementations. Agents are evaluated in proof-only or code-and-proof mode and scored by an independent grader, while the formal audit route returns machine-checked evidence of ben… view at source ↗
Figure 2
Figure 2. Excerpt from a Vero example illustrating a benchmark instance. Frozen content like API signatures and specifications are provided by the curator. The agent fills in the body of canonical (in code-and-proof mode) and the proof obligation marked sorry (in both mode). 3.2 Task and Evaluation Vero supports two task modes that differ in which obligations the agent must discharge. In both modes, we evaluate whether the ag… view at source ↗
Figure 3
Figure 3. Agent performance on Vero. (a,b) Cumulative full solves, out of 43, over the 90-minute budget in code-and-proof and proof-only; diamonds mark each configuration’s median runtime. (c) Which configurations fully solve each instance in each mode. GPT-5.5 (xhigh) leads both modes, but Vero remains frontier-resistant. GPT-5.5 (xhigh) fully solves 27 of 43 instances in code-and-proof and 25 in proof-only, ahead of Claude … view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: Full-repository outcomes and artifact sizes by task mode. (a) Paired full-solve outcomes across the two modes for each of the 172 instance–agent pairs. (b–d) Implementation lines, proof lines, and their ratio at the end of each of the 344 runs, split by mode and by whe…
Figure 5
Figure 5. Figure 5: Proof structure in the 82 full solves. A helper is a theorem the agent writes to support its specification proofs. (a) How many specifications share one helper. (b) Share of proof lines that live in helpers. (c) Pass rates in the other seven runs, grouped by each speci…
Figure 6
Figure 6. Figure 6: Agents fix implementations early and grow proofs until the deadline. Columns are agent configurations. Top row shows authored proof lines over time in both modes; bottom row shows authored implementation lines in code-and-proof. Thin lines are per-repository trajectori…
Figure 7
Figure 7. Figure 7: Where failures remain at the end of a run. (a) Repositories grouped by the share of their specifications still failing. (b) Breakdown of remaining specifications by failure reason. (c) Number of GPT-5.5 (xhigh) repositories with at most x failing specifications. when p…
Figure 8
Figure 8. Figure 8: Which specifications fail. (a) Failure rate by semantic type, equalized across repositories. (b) How often each type appears among the 262 unfinished evaluations. (c) Within-repository failure￾rate differences for four statement features. Diamonds and whiskers show agg…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

48 extracted references · 31 canonical work pages

  1. [1]

    Agent skills

    Anthropic. Agent skills. https://platform.claude.com/docs/en/agents-and-tools/ agent-skills/overview, 2026. Accessed: 2026-05-02

    work page 2026

  2. [2]

    Program synthesis with large language models.arXiv preprint arXiv:2108.07732, 2021

    Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, et al. Program synthesis with large language models.arXiv preprint arXiv:2108.07732, 2021

    arXiv 2021

  3. [3]

    PhD thesis, Inria, 1997

    Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al.The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997

    work page 1997

  4. [4]

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

    Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emil- ian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, et al. A benchmark for vericoding: formally verified program synthesis.arXiv preprint arXiv:2509.22908, 2025

    arXiv 2025

  5. [5]

    Evaluating large language models trained on code.arXiv preprint arXiv:2107.03374, 2021

    Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained on code.arXiv preprint arXiv:2107.03374, 2021

    arXiv 2021

  6. [6]

    The Lean theorem prover (system description)

    Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). InInternational Conference on Automated Deduction (CADE), 2015

    work page 2015

  7. [7]

    Verifythis- bench: Generating code, specifications, and proofs all at once.arXiv preprint arXiv:2505.19271, 2025

    Xun Deng, Sicheng Zhong, Barı¸ s Bayazıt, Andreas Veneris, Fan Long, and Xujie Si. Verifythis- bench: Generating code, specifications, and proofs all at once.arXiv preprint arXiv:2505.19271, 2025

    arXiv 2025

  8. [8]

    Proving the coding interview: A benchmark for formally verified code generation.arXiv preprint arXiv:2502.05714, 2025

    Quinn Dougherty and Ronak Mehta. Proving the coding interview: A benchmark for formally verified code generation.arXiv preprint arXiv:2502.05714, 2025

    arXiv 2025

Show all 48 references
  1. [9]

    Sloan, and Adam Chlipala

    Andres Erbsen, Jade Philipoom, Jason Gross, Robert H. Sloan, and Adam Chlipala. Simple high-level code for cryptographic arithmetic - with proofs, without compromises.2019 IEEE Symposium on Security and Privacy (SP), pages 1202–1219, 2019

    2019

  2. [10]

    Certified program synthesis with a multi-modal verifier.arXiv preprint arXiv:2604.16584, 2026

    Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey. Certified program synthesis with a multi-modal verifier.arXiv preprint arXiv:2604.16584, 2026

    2026 arXiv

  3. [11]

    CertiKOS: An extensible architecture for building certified concurrent OS kernels

    Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. InSymposium on Operating Systems Design and Implementation (OSDI), 2016

    2016

  4. [12]

    Lorch, Bryan Parno, Michael L

    Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V . Setty, and Brian Zill. Ironfleet: proving practical distributed systems correct.Proceedings of the 25th Symposium on Operating Systems Principles, 2015

    2015

  5. [13]

    Measuring coding challenge competence with APPS

    Dan Hendrycks, Steven Basart, Saurav Kadavath, Mantas Mazeika, Akul Arora, Ethan Guo, Collin Burns, Samir Puranik, Horace He, Dawn Song, et al. Measuring coding challenge competence with APPS. InNeural Information Processing Systems (NeurIPS), Datasets and Benchmarks Track, 2021

    2021

  6. [14]

    Livecodebench: Holistic and contamination free evaluation of large language models for code.arXiv preprint arXiv:2403.07974, 2024

    Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Ar- mando Solar-Lezama, Koushik Sen, and Ion Stoica. Livecodebench: Holistic and contamination free evaluation of large language models for code.arXiv preprint arXiv:2403.07974, 2024. 12

    2024 arXiv

  7. [15]

    SWE-bench: Can language models resolve real-world GitHub issues? InInternational Conference on Learning Representations (ICLR), 2024

    Carlos E Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, and Karthik R Narasimhan. SWE-bench: Can language models resolve real-world GitHub issues? InInternational Conference on Learning Representations (ICLR), 2024

    2024

  8. [16]

    seL4: Formal verification of an OS kernel

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. InSymposium on Operating sys...

    2009

  9. [17]

    Leanagent: Lifelong learning for formal theorem proving.arXiv preprint arXiv:2410.06209, 2024

    Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, and Anima Anandkumar. Leanagent: Lifelong learning for formal theorem proving.arXiv preprint arXiv:2410.06209, 2024

    2024 arXiv

  10. [18]

    Verus: Verifying rust programs using linear ghost types.Proceedings of the ACM on Programming Languages, 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, 2023

    2023

  11. [19]

    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 (LPAR), 2010

    2010

  12. [20]

    miniCodeProps: a minimal benchmark for proving code properties.arXiv preprint arXiv:2406.11915, 2024

    Evan Lohn and Sean Welleck. miniCodeProps: a minimal benchmark for proving code properties.arXiv preprint arXiv:2406.11915, 2024

    2024 arXiv

  13. [21]

    DafnyBench: A benchmark for formal software verification.Transactions on Machine Learning Research, 2025

    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.Transactions on Machine Learning Research, 2025

    2025

  14. [22]

    The Lean mathematical library

    Mathlib community. The Lean mathematical library. InCertified Programs and Proofs (CPP), 2020

    2020

  15. [23]

    HACLxN: Verified generic SIMD crypto (for all your favourite platforms)

    Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, and Santiago Zanella-Béguelin. HACLxN: Verified generic SIMD crypto (for all your favourite platforms). InProceedings of the 2020 ACM SIGSAC Conference on Com...

    2020

  16. [24]

    Can large language models verify system software? a case study using FSCQ as a benchmark

    Jianxing Qin, Alexander Du, Danfeng Zhang, Matthew Lentz, and Danyang Zhuo. Can large language models verify system software? a case study using FSCQ as a benchmark. In Proceedings of the 2025 Workshop on Hot Topics in Operating Systems, HOTOS ’25, pages 34–41. Association for...

    2025

  17. [25]

    s2n-bignum- bench: A practical benchmark for evaluating low-level code reasoning of llms.arXiv preprint arXiv:2603.14628, 2026

    Balaji Rao, John Harrison, Soonho Kong, Juneyoung Lee, and Carlo Lipizzi. s2n-bignum- bench: A practical benchmark for evaluating low-level code reasoning of llms.arXiv preprint arXiv:2603.14628, 2026

    2026 arXiv

  18. [26]

    Quantifying contamination in evaluating code generation capabilities of language models

    Martin Riddell, Ansong Ni, and Arman Cohan. Quantifying contamination in evaluating code generation capabilities of language models. InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 14116–14137, 2024

    2024

  19. [27]

    Clover: Closed-loop verifiable code generation

    Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code generation. InInternational Symposium on AI Verification, 2024

    2024

  20. [28]

    Clever: A curated benchmark for formally verified code generation.arXiv preprint arXiv:2505.13938, 2025

    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.arXiv preprint arXiv:2505.13938, 2025

    2025

  21. [29]

    Rango: Adaptive retrieval-augmented proving for automated software verification

    Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F Ferreira, Sorin Lerner, and Emily First. Rango: Adaptive retrieval-augmented proving for automated software verification. InInternational Conference on Software Engineering (ICSE), 2025

    2025

  22. [30]

    Ape-bench i: Towards file-level automated proof engineering of formal math libraries.arXiv preprint arXiv:2504.19110, 2025

    Huajian Xin, Luming Li, Xiaoran Jin, Jacques Fleuriot, and Wenda Li. Ape-bench i: Towards file-level automated proof engineering of formal math libraries.arXiv preprint arXiv:2504.19110, 2025. 13

    2025

  23. [31]

    Verisoftbench: Repository-scale formal verification benchmarks for lean.arXiv preprint arXiv:2602.18307, 2026

    Yutong Xin, Qiaochu Chen, Greg Durrett, and I¸ sil Dillig. Verisoftbench: Repository-scale formal verification benchmarks for lean.arXiv preprint arXiv:2602.18307, 2026

    2026

  24. [32]

    Autoverus: Auto- mated 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: Auto- mated proof generation for rust code.Proceedings of the ACM on Programming Languages, 9(OOPSLA2):3454–3482, 2025

    2025

  25. [33]

    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

  26. [34]

    SWE-agent: Agent-computer interfaces enable automated software engineering.arXiv preprint arXiv:2405.15793, 2024

    John Yang, Carlos E Jimenez, Alexander Wettig, Kilian Lieret, Shunyu Yao, Karthik Narasimhan, and Ofir Press. SWE-agent: Agent-computer interfaces enable automated software engineering.arXiv preprint arXiv:2405.15793, 2024

    2024 arXiv

  27. [35]

    LeanDojo: Theorem proving with retrieval-augmented language models

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. InNeural Information Processing Systems (NeurIPS), 2023

    2023

  28. [36]

    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

    2025

  29. [37]

    Veriequiv- bench: An equivalence score for ground-truth-free evaluation of formally verifiable code.arXiv preprint arXiv:2510.06296, 2025

    Lingfei Zeng, Fengdi Che, Xuhan Huang, Fei Ye, Xu Xu, Binhang Yuan, and Jie Fu. Veriequiv- bench: An equivalence score for ground-truth-free evaluation of formally verifiable code.arXiv preprint arXiv:2510.06296, 2025

    2025 arXiv

  30. [38]

    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

  31. [39]

    cp” = code-and-proof, “po

    Si Cheng Zhong and Xujie Si. Towards repository-level program verification with large language models. InProceedings of the 1st ACM SIGPLAN International Workshop on Language Models and Programming Languages, pages 27–39, 2025. 14 A Experimental Configuration A.1 Agent Harness...

    2025

  32. [40]

    Later files in the same cell shift from probing to drafting, stating a private helper and a candidate obligation proof together so that both can be checked in one compilation before either is committed to a graded slot. The agent has effectively built itself a read-eval-print ...

  33. [41]

    Those seven included spec_deposit_preserves_valid, the contract’s principal inductive invariant

    What changed relative to earlier evaluations.An earlier round of this evaluation left 7 of the 79 specifications unproven, all depending on one missing boundary-shift lemma about how Merkle-path siblings evolve when the leaf array grows by one element. Those seven included spe...

  34. [42]

    intro n v h 5simp [canonical, VestV2.btcVarintParse, h]

  35. [43]

    It has moved into a named helper

    intro h 7exact <ParseError.UnexpectedEndOfInput, 8by simp [canonical, VestV2.btcVarintParse, h]> The four-way case analysis the format actually requires has not disappeared. It has moved into a named helper. The submission’s longest proof is an 87-line bound on the parser’s co...

  36. [44]

    simp [hb] at h; rcases h with <rfl, rfl>; simp

  37. [45]

    simp [hb] at h 13by_cases hfd : b.toNat = 0xFD

  38. [46]

    SortedList7 , SortedSet7 ) and every one of them unattempted rather than rejected. The instance is a Lean port of the python-sortedcontainers library, and its reference implementation follows the Python original in using binary search over an index range: 1def bisectLeftGo (ls...

  39. [47]

    3if. . .then bisectLeftGo lst val (mid + 1) hi 4else bisectLeftGo lst val lo mid 5termination_by hi - lo Proving anything aboutbisectLeftGo requires an invariant tying thelo/hi window to the sortedness of the enclosing list, maintained across a recursion whose measure is hi - ...

  40. [48]

    7def sortOrd {a : Type} [Ord a] : List a -> List a 8| x :: xs => insertOrd x (sortOrd xs) Both definitions recurse on the list constructor, so every specification about them is provable by induction on the list with no auxiliary window invariant. The substitution costs asympto...

Pith tools

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