# dafny-annotator: AI-Assisted Verification of Dafny Programs

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 17 references that are in the map.
- First posted on arXiv 5 Nov 2024.

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

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [STaR: Bootstrapping Reasoning With Reasoning](https://mlsanity.com/paper/2203.14465/) (2022)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [Proof Automation with Large Language Models](https://mlsanity.com/paper/2409.14274/) (2024)
- [miniCodeProps: a Minimal Benchmark for Proving Code Properties](https://mlsanity.com/paper/2406.11915/) (2024)

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

- [VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus](https://mlsanity.com/paper/2510.25015/) (2025)
- [Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verification](https://mlsanity.com/paper/2509.23061/) (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)
- [Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning](https://mlsanity.com/paper/2509.06239/) (2025)
- [An Empirical Study of LLM-Generated Specifications for VeriFast](https://mlsanity.com/paper/2606.26490/) (2026)
- [Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability](https://mlsanity.com/paper/2607.09366/) (2026)
- [Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification](https://mlsanity.com/paper/2607.10291/) (2026)

## Abstract (arXiv)

Formal verification has the potential to drastically reduce software bugs, but its high additional cost has hindered large-scale adoption. While Dafny presents a promise to significantly reduce the effort to write verified programs, users are often required to provide logical annotations to aid the verifier. Here, we explore using a combination of Large Language Models and search to build dafny-annotator: a tool that adds logical annotations to a Dafny method until the verifier can prove it correct. On a test set from the DafnyBench collection of programs, greedy search guided by LLaMa 3.1 8B successfully annotates only 15.7% of the methods. Since this data-driven approach is hindered by the lack of large-scale training data, we propose a method for open-ended synthesis of new Dafny programs in a flexible pipeline where LLMs formulate high-level ideas, implement them, and incrementally propose changes to existing programs, which Dafny validates. This gives us a synthetic dataset, DafnySynth, which we use to augment DafnyBench for training. Fine-tuning on both datasets boosts LLaMa 8B's success rate to 50.6% -- significantly better than the base model, or training on either dataset alone. Our results suggest a path towards capable AI assistants for languages that don't yet have large-scale human-generated examples. In turn, such assistants might reduce friction for users and ultimately drive adoption.