# DafnyBench: A Benchmark for Formal Software Verification

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

## Key facts

- Cited by 57 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 32 references that are in the map.
- First posted on arXiv 12 Jun 2024.

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

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Sparks of Artificial General Intelligence: Early experiments with GPT-4](https://mlsanity.com/paper/2303.12712/) (2023)
- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [Measuring Coding Challenge Competence With APPS](https://mlsanity.com/paper/2105.09938/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Extracting functional programs from Coq, in Coq](https://mlsanity.com/paper/2108.02995/) (2021)

## Built on by (most cited first, 30 of 57)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [AI Agentic Programming: A Survey of Techniques, Challenges, and Opportunities](https://mlsanity.com/paper/2508.11126/) (2025)
- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [A benchmark for vericoding: formally verified program synthesis](https://mlsanity.com/paper/2509.22908/) (2025)
- [Proving the Coding Interview: A Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2502.05714/) (2025)
- [GSM-Infinite: How Do Your LLMs Behave over Infinitely Increasing Context Length and Reasoning Complexity?](https://mlsanity.com/paper/2502.05252/) (2025)
- [VeruSAGE: A Study of Agent-Based Verification for Rust Systems](https://mlsanity.com/paper/2512.18436/) (2025)
- [AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms](https://mlsanity.com/paper/2602.09464/) (2026)
- [dafny-annotator: AI-Assisted Verification of Dafny Programs](https://mlsanity.com/paper/2411.15143/) (2024)
- [OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification](https://mlsanity.com/paper/2504.20964/) (2025)
- [VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean](https://mlsanity.com/paper/2602.18307/) (2026)
- [SEVerA: Verified Synthesis of Self-Evolving Agents](https://mlsanity.com/paper/2603.25111/) (2026)
- [VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code](https://mlsanity.com/paper/2510.06296/) (2025)
- [Dafny as Verification-Aware Intermediate Language for Code Generation](https://mlsanity.com/paper/2501.06283/) (2025)
- [Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification](https://mlsanity.com/paper/2509.23061/) (2025)
- [Agentic Verification of Software Systems](https://mlsanity.com/paper/2511.17330/) (2025)
- [Towards Repository-Level Program Verification with Large Language Models](https://mlsanity.com/paper/2509.25197/) (2025)
- [Inferring multiple helper Dafny assertions with LLMs](https://mlsanity.com/paper/2511.00125/) (2025)
- [Neural Theorem Proving for Verification Conditions: A Real-World Benchmark](https://mlsanity.com/paper/2601.18944/) (2026)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants](https://mlsanity.com/paper/2508.18587/) (2025)
- [ConvexBench: Can LLMs Recognize Convex Functions?](https://mlsanity.com/paper/2602.01075/) (2026)
- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)
- [Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcity](https://mlsanity.com/paper/2502.11901/) (2025)
- [MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification](https://mlsanity.com/paper/2512.10187/) (2025)

## Abstract (arXiv)

We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPT-4 and Claude 3 to auto-generate enough hints for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and hints. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.