# Towards AI-Assisted Synthesis of Verified Dafny Methods

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

## Key facts

- Cited by 58 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 1 Feb 2024.

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

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (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)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming](https://mlsanity.com/paper/2405.01787/) (2024)
- [Proving the Coding Interview: A Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2502.05714/) (2025)
- [RL Is Neither a Panacea Nor a Mirage: Understanding Supervised vs. Reinforcement Learning Fine-Tuning for LLMs](https://mlsanity.com/paper/2508.16546/) (2025)
- [Propose, Solve, Verify: Self-Play Through Formal Verification](https://mlsanity.com/paper/2512.18160/) (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)
- [Laurel: Unblocking Automated Verification with Large Language Models](https://mlsanity.com/paper/2405.16792/) (2024)
- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [ProofWright: Towards Agentic Formal Verification of CUDA](https://mlsanity.com/paper/2511.12294/) (2025)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification](https://mlsanity.com/paper/2504.20964/) (2025)
- [New Solutions on LLM Acceleration, Optimization, and Application](https://mlsanity.com/paper/2406.10903/) (2024)
- [VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code](https://mlsanity.com/paper/2510.06296/) (2025)
- [Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages](https://mlsanity.com/paper/2406.03636/) (2024)
- [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)
- [RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation](https://mlsanity.com/paper/2502.05344/) (2025)
- [The Hitchhiker's Guide to Program Analysis, Part II: Deep Thoughts by LLMs](https://mlsanity.com/paper/2504.11711/) (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)
- [Can LLMs Enable Verification in Mainstream Programming?](https://mlsanity.com/paper/2503.14183/) (2025)
- [AutoReSpec: A Framework for Generating Specification using Large Language Models](https://mlsanity.com/paper/2604.03758/) (2026)
- [VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation](https://mlsanity.com/paper/2605.08553/) (2026)

## Abstract (arXiv)

Large language models show great promise in many domains, including programming. A promise is easy to make but hard to keep, and language models often fail to keep their promises, generating erroneous code. A promising avenue to keep models honest is to incorporate formal verification: generating programs' specifications as well as code so that the code can be proved correct with respect to the specifications. Unfortunately, existing large language models show a severe lack of proficiency in verified programming. In this paper, we demonstrate how to improve two pretrained models' proficiency in the Dafny verification-aware language. Using 178 problems from the MBPP dataset, we prompt two contemporary models (GPT-4 and PaLM-2) to synthesize Dafny methods. We use three different types of prompts: a direct Contextless prompt; a Signature prompt that includes a method signature and test cases, and a Chain of Thought (CoT) prompt that decomposes the problem into steps and includes retrieval augmentation generated example problems and solutions. Our results show that GPT-4 performs better than PaLM-2 on these tasks and that both models perform best with the retrieval augmentation generated CoT prompt. GPT-4 was able to generate verified, human-evaluated, Dafny methods for 58% of the problems, however, GPT-4 managed only 19% of the problems with the Contextless prompt, and even fewer (10%) for the Signature prompt. We are thus able to contribute 153 verified Dafny solutions to MBPP problems, 50 that we wrote manually, and 103 synthesized by GPT-4. Our results demonstrate that the benefits of formal program verification are now within reach of code generating large language models...