mlsanityData to 14 Oct 2026

A benchmark for vericoding: formally verified program synthesis

arXiv 2509.22908 ↗First posted 26 Sep 2025cs.SE cs.LG cs.PLcited by 20

Not on the map. Why?

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

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

19 of 49 references.

References · 19

  1. 2019Sentence-BERT: Sentence Embeddings using Siamese BERT-Networkscited by 9,170
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  3. 2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,373
  4. 2017Billion-scale similarity search with GPUscited by 2,497
  5. 2022Competition-Level Code Generation with AlphaCodecited by 1,462
  6. 2021Measuring Coding Challenge Competence With APPScited by 902
  7. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  8. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  9. 2023AI Control: Improving Safety Despite Intentional Subversioncited by 229
  10. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  11. 2024HumanEval-XL: A Multilingual Code Generation Benchmark for Cross-lingual Natural Language Generalizationcited by 86
  12. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 57
7 more
  1. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 49
  2. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 35
  3. 2025VERINA: Benchmarking Verifiable Code Generationcited by 34
  4. 2025Measuring the environmental impact of delivering AI at Google Scalecited by 32
  5. 2025CLEVER: A Curated Benchmark for Formally Verified Code Generationcited by 29
  6. 2025Proving the Coding Interview: A Benchmark for Formally Verified Code Generationcited by 19
  7. 2025VerifyThisBench: Generating Code, Specifications, and Proofs All at Oncecited by 9

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 2; 2026: 18.

20 papers.

Sort:

By area:

  1. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 12
  2. 2026VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generationcited by 3
  3. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  4. 2026P3: Joint Program-and-Proof Planning for Verified Code Generationcited by 2
  5. 2026Vero: Can AI Agents Build Formally Verified Software Repositories?cited by 2
  6. 2026Automating Formal Verification with Reinforcement Learning and Recursive Inferencecited by 1
  7. 2025BRIDGE: Building Representations In Domain Guided Program Synthesiscited by 0
  8. 2026Teaching LLMs Program Semantics via Symbolic Execution Tracescited by 0
  9. 2026Viverra: Text-to-Code with Guaranteescited by 0
  10. 2026Automating Formal Verification with Agent-Guided Tree Searchcited by 0
  11. 2026FVSpec: Real-World Property-Based Tests as Lean Challengescited by 0
  12. 2026Neuro-Symbolic Reasoning for Vulnerability Detectioncited by 0
8 more
  1. 2026Case study: solving P-99 with LPTP and an LLMcited by 0
  2. 2026An AI Approach to Verified Production Cryptographic Librariescited by 0
  3. 2026SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programscited by 0
  4. 2026COUNTERMEM: World-Model Verified Counter-Factual Memory for Language Agentscited by 0
  5. 2026FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verificationcited by 0
  6. 2026Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generationcited by 0
  7. 2026TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agentscited by 0
  8. 2026claimcheck: Measuring and Improving Specification Faithfulnesscited by 0