# Dafny: Statically Verifying Functional Correctness

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Dec 2014.

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

- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation](https://mlsanity.com/paper/2605.01394/) (2026)

## Abstract (arXiv)

This report presents the Dafny language and verifier, with a focus on describing the main features of the language, including pre- and postconditions, assertions, loop invariants, termination metrics, quantifiers, predicates and frames. Examples of Dafny code are provided to illustrate the use of each feature, and an overview of how Dafny translates programming code into a mathematical proof of functional verification is presented. The report also includes references to useful resources on Dafny, with mentions of related works in the domain of specification languages.