# DafnyPro: LLM-Assisted Automated Verification for Dafny Programs

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Jan 2026.

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

- [SEVerA: Verified Synthesis of Self-Evolving Agents](https://mlsanity.com/paper/2603.25111/) (2026)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [ExVerus: Verus Proof Repair via Counterexample Reasoning](https://mlsanity.com/paper/2603.25810/) (2026)
- [Certified Program Synthesis with a Multi-Modal Verifier](https://mlsanity.com/paper/2604.16584/) (2026)
- [From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification](https://mlsanity.com/paper/2604.22601/) (2026)
- [Combining Mechanical and Agentic Specification Inference for Move](https://mlsanity.com/paper/2605.10005/) (2026)
- [Natural Language based Specification and Verification](https://mlsanity.com/paper/2605.11315/) (2026)
- [An Empirical Study of LLM-Generated Specifications for VeriFast](https://mlsanity.com/paper/2606.26490/) (2026)
- [Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification](https://mlsanity.com/paper/2607.10291/) (2026)
- [Specula: Scaling formal specifications for autonomous model checking of system code](https://mlsanity.com/paper/2607.25333/) (2026)
- [Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification](https://mlsanity.com/paper/2609.34886/) (2026)

## Abstract (arXiv)

We present DafnyPro, an inference-time framework that enhances LLMs for generating verification annotations in Dafny. DafnyPro comprises three key components: a diff-checker that prevents modifications to base program logic, a pruner that removes unnecessary invariants, and a hint-augmentation system that retrieves and applies predefined, problem-independent proof strategies. We evaluate DafnyPro using Claude Sonnet 3.5 and 3.7 on four benchmarks: Clover, MBPP-Dafny, HumanEval-Dafny, and DafnyBench, achieving consistent performance gains in all cases. Notably, on DafnyBench, the most challenging benchmark, Claude Sonnet 3.5 enhanced with DafnyPro achieves 86% correct proofs, a 16 pp improvement over the base model. We also fine-tune two Qwen models on training data derived from verification attempts by larger models enhanced with DafnyPro. Our 7B and 14B models achieve 68% and 70% correct proofs on DafnyBench, respectively, demonstrating that smaller models can maintain high verification accuracy.