mlsanityData to 7 Oct 2026

DafnyBench: A Benchmark for Formal Software Verification

arXiv 2406.08467 ↗First posted 12 Jun 2024cs.SE cs.AI cs.LGcited by 54

Not on the map. Why?

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.

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

Builds on

14 of 32 references.

References · 14

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  3. 2021Program Synthesis with Large Language Modelscited by 3,509
  4. 2023Sparks of Artificial General Intelligence: Early experiments with GPT-4cited by 2,579
  5. 2024LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Codecited by 1,906
  6. 2021Measuring Coding Challenge Competence With APPScited by 879
  7. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  8. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  9. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  10. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  11. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  12. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
2 more
  1. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  2. 2021Extracting functional programs from Coq, in Coqcited by 1

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 4; 2025: 21; 2026: 29.

54 papers.

Sort:

By area:

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  2. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  3. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 31
  4. 2025VERINA: Benchmarking Verifiable Code Generationcited by 30
  5. 2025CLEVER: A Curated Benchmark for Formally Verified Code Generationcited by 27
  6. 2025AI Agentic Programming: A Survey of Techniques, Challenges, and Opportunitiescited by 26
  7. 2025Frontier AI's Impact on the Cybersecurity Landscapecited by 21
  8. 2025Proving the Coding Interview: A Benchmark for Formally Verified Code Generationcited by 18
  9. 2025GSM-Infinite: How Do Your LLMs Behave over Infinitely Increasing Context Length and Reasoning Complexity?cited by 16
  10. 2025A benchmark for vericoding: formally verified program synthesiscited by 16
  11. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 11
  12. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 11
38 more
  1. 2024dafny-annotator: AI-Assisted Verification of Dafny Programscited by 8
  2. 2025OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verificationcited by 8
  3. 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Codecited by 7
  4. 2025Dafny as Verification-Aware Intermediate Language for Code Generationcited by 6
  5. 2025Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verificationcited by 6
  6. 2026VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Leancited by 6
  7. 2026SEVerA: Verified Synthesis of Self-Evolving Agentscited by 6
  8. 2025Agentic Verification of Software Systemscited by 5
  9. 2025Towards Repository-Level Program Verification with Large Language Modelscited by 4
  10. 2026Neural Theorem Proving for Verification Conditions: A Real-World Benchmarkcited by 4
  11. 2025A Case Study on the Effectiveness of LLMs in Verification with Proof Assistantscited by 3
  12. 2025Inferring multiple helper Dafny assertions with LLMscited by 3
  13. 2026ConvexBench: Can LLMs Recognize Convex Functions?cited by 3
  14. 2026Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systemscited by 3
  15. 2025Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarcitycited by 2
  16. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  17. 2026Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Inductioncited by 2
  18. 2026Spec-Harness: Measuring and Improving Behavioral Adequacy of LLM-Synthesized Formal Specificationscited by 2
  19. 2026CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generationcited by 2
  20. 2026Certified Program Synthesis with a Multi-Modal Verifiercited by 2
  21. 2025Towards Automated Formal Verification of Backend Systems with LLMscited by 1
  22. 2025Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learningcited by 1
  23. 2025The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guaranteecited by 1
  24. 2026Perish or Flourish? A Holistic Evaluation of Large Language Models for Code Generation in Functional Programmingcited by 1
  25. 2026VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generationcited by 1
  26. 2026AxDafny: Agentic Verified Code Generation in Dafnycited by 1
  27. 2026Formal Disco: Scalable Open-Ended Generation of Formally Verified Programscited by 1
  28. 2026P3: Joint Program-and-Proof Planning for Verified Code Generationcited by 1
  29. 2026Vero: Can AI Agents Build Formally Verified Software Repositories?cited by 1
  30. 2026Toward an Agentic Infused Software Ecosystemcited by 0
  31. 2026From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verificationcited by 0
  32. 2026VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generationcited by 0
  33. 2026Automating Formal Verification with Agent-Guided Tree Searchcited by 0
  34. 2026FVSpec: Real-World Property-Based Tests as Lean Challengescited by 0
  35. 2026Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiabilitycited by 0
  36. 2026TLA+-Bench: An Execution-Grounded Benchmark and Dataset for Natural-Language to TLA Specification Generationcited by 0
  37. 2026VeriSkill: A Self-Evolution Framework for Program Verification Skillscited by 0
  38. 2026SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programscited by 0

50 most cited of 54 All 54 (JSON)