# A benchmark for vericoding: formally verified program synthesis

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

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 49 references that are in the map.
- First posted on arXiv 26 Sep 2025.

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

- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Billion-scale similarity search with GPUs](https://mlsanity.com/paper/1702.08734/) (2017)
- [Competition-Level Code Generation with AlphaCode](https://mlsanity.com/paper/2203.07814/) (2022)
- [Measuring Coding Challenge Competence With APPS](https://mlsanity.com/paper/2105.09938/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [AI Control: Improving Safety Despite Intentional Subversion](https://mlsanity.com/paper/2312.06942/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [HumanEval-XL: A Multilingual Code Generation Benchmark for Cross-lingual Natural Language Generalization](https://mlsanity.com/paper/2402.16694/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Measuring the environmental impact of delivering AI at Google Scale](https://mlsanity.com/paper/2508.15734/) (2025)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [Proving the Coding Interview: A Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2502.05714/) (2025)
- [VerifyThisBench: Generating Code, Specifications, and Proofs All at Once](https://mlsanity.com/paper/2505.19271/) (2025)

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

- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)
- [MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification](https://mlsanity.com/paper/2512.10187/) (2025)
- [P3: Joint Program-and-Proof Planning for Verified Code Generation](https://mlsanity.com/paper/2608.09277/) (2026)
- [Vero: Can AI Agents Build Formally Verified Software Repositories?](https://mlsanity.com/paper/2608.13522/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [BRIDGE: Building Representations In Domain Guided Program Synthesis](https://mlsanity.com/paper/2511.21104/) (2025)
- [Teaching LLMs Program Semantics via Symbolic Execution Traces](https://mlsanity.com/paper/2605.06184/) (2026)
- [Viverra: Text-to-Code with Guarantees](https://mlsanity.com/paper/2605.14972/) (2026)
- [Automating Formal Verification with Agent-Guided Tree Search](https://mlsanity.com/paper/2605.27485/) (2026)
- [FVSpec: Real-World Property-Based Tests as Lean Challenges](https://mlsanity.com/paper/2606.01008/) (2026)
- [Neuro-Symbolic Reasoning for Vulnerability Detection](https://mlsanity.com/paper/2607.03963/) (2026)
- [Case study: solving P-99 with LPTP and an LLM](https://mlsanity.com/paper/2607.21196/) (2026)
- [An AI Approach to Verified Production Cryptographic Libraries](https://mlsanity.com/paper/2608.00965/) (2026)
- [SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs](https://mlsanity.com/paper/2608.29841/) (2026)
- [COUNTERMEM: World-Model Verified Counter-Factual Memory for Language Agents](https://mlsanity.com/paper/2609.31874/) (2026)
- [FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification](https://mlsanity.com/paper/2610.00885/) (2026)
- [Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation](https://mlsanity.com/paper/2610.10604/) (2026)
- [TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents](https://mlsanity.com/paper/2610.14923/) (2026)
- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)

## Abstract (arXiv)

We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications - in contrast to vibe coding, which generates potentially buggy code from a natural language description. Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean. Of these, 6,174 are new unseen problems. We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs. Adding natural-language descriptions does not significantly improve performance. We also find that LLM progress has improved progress on pure Dafny verification from 68% to 96% over the past year. The benchmark and vericoding results are shared at https://github.com/Beneficial-AI-Foundation/vericoding-benchmark