Dafny: a verification-aware language that checks your code as you type

What Dafny is for, and who ends up using it

Testing samples a program's behaviour; it does not cover the space between samples. Dafny attacks that gap by making the specification part of the program and having a verifier check, ahead of execution, that every path satisfies it. The README describes the tool as a "verification-ready programming language" whose verifier "constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications."

The audience is narrower than a general-purpose language's. It fits people who already write pre- and post-conditions in their head, or in comments that nothing enforces: authors of algorithms with subtle invariants, compiler and protocol engineers, and researchers who need proofs that survive a reviewer. The README points to a four-part lecture course covering pre- and postconditions, invariants, binary search and the Dutch National Flag algorithm, which is a fair sketch of the intended difficulty curve. If you have never written a loop invariant, the first hour will be uncomfortable and the second hour will be the point.

How verification works: specifications, SMT solving and the Boogie layer

A Dafny file mixes executable code with specification clauses. Pre- and post-conditions, termination conditions, loop invariants and read/write specifications are all part of the language, alongside unbounded and bounded quantifiers and calculational proofs. The verifier consumes those clauses and asks whether every execution path can violate them.

The repository layout shows what sits underneath. Source/Dafny.sln builds the compiler and parser, and the Makefile carries a separate target for Boogie:

make boogie

That target builds boogie/Binaries/Boogie.exe from Source/Boogie.sln in Release configuration. Boogie is the intermediate verification language that turns Dafny's proof obligations into queries for an SMT solver. This is why verification feels immediate in an editor and why it can also stall: the solver is doing real work on every keystroke, and a loop invariant that is almost right produces a counterexample rather than a pass. The README's own framing, that verification is "an integral part of development", is a design commitment, not a marketing line. You are expected to iterate on specifications the way you iterate on code.

Dafny also generates itself. The Makefile's dfy-to-cs target runs Source/DafnyCore/DafnyGeneratedFromDafny.sh, and dfy-to-cs-noverify passes --no-verify to that script. Parts of the compiler are written in Dafny and translated to C#. That is a strong signal about the language's maturity, and also a warning: if you modify the core, you may need to regenerate C# from Dafny sources before the build reflects your change.

Installing Dafny and running a first file

The README gives two routes. The easier one is the Visual Studio Code extension, which is what the "Try Dafny" section recommends first, followed by the online tutorial. The second is the Dafny CLI, installed from the binary downloads page on GitHub, which covers Windows, macOS, GNU/Linux and FreeBSD. Installation instructions live in the wiki's INSTALL page rather than in the repository README, so expect to follow a link before you have a working binary.

Once the CLI is on your path, you write Dafny source in a file and verify it. The README's own starting point is the tutorial at dafny-lang.github.io/dafny/OnlineTutorial/guide, which walks through simple imperative programs with pre- and postconditions, loop invariants and termination conditions. Work through that before writing anything of your own, because the syntax for specification clauses is not guessable from the surrounding code.

To build the toolchain from source rather than downloading a binary, the Makefile's default target builds the solution, which includes the parser:

make exe

That runs dotnet build Source/Dafny.sln. When it finishes, the compiler and verifier are built from the checked-out sources. Verification is then an iterative loop: edit the file, let the verifier report errors and counterexamples, adjust the specifications, repeat. That loop, edit then re-verify, is the whole workflow.

To produce runnable code, Dafny compiles to C#, Go, Python, Java or JavaScript. The README says "more to come", so treat the target list as current rather than fixed. Compilation is the step that lets verified logic sit inside an existing service instead of replacing it.

Where Dafny will fight you

Verification is not free and it is not automatic in the way type inference is. An invariant that is true but too weak will fail, and the counterexample the verifier shows may not explain why. The README's own emphasis on loop invariants, termination conditions and calculational proofs is a list of the things you will spend time on. Budget for proof engineering, not just programming.

The toolchain is heavier than a single binary. Building from source goes through dotnet build Source/Dafny.sln, and the verification backend is a separate Boogie build. The nightly release listed in the repository carries a date-based tag, and the most recent numbered release is v4.11.0 from 2025-08-25, with v4.10.0 before it in February 2025. Pinning a numbered release rather than a nightly is the safer default for a build you intend to reproduce.

Dafny is also the wrong tool when the property you care about is not expressible as a specification over the program's own state. Liveness, timing, and the behaviour of a distributed system under message loss are not what a pre/postcondition verifier checks. The README does not claim otherwise, but it is easy to over-read "verification" as covering more than it does.

Dafny against Lean, Coq and TLA+

The comparison people search for most is Dafny versus Lean, and the difference is where the proof lives. Lean and Coq are proof assistants: you construct a term whose type is the theorem, and the kernel checks it. Dafny is an imperative programming language with a verifier attached; you write methods with contracts and the solver discharges the obligations. If your goal is a machine-checked mathematical development, a proof assistant is the natural home. If your goal is a program that runs and whose contracts hold, Dafny keeps the artifact executable, which is the property Lean and Coq do not offer for the same code.

Against TLA+, the split is state machines versus code. TLA+ specifies a system's states and transitions and is checked by a model checker over a bounded configuration; it does not compile to a running program. Dafny verifies the program itself and then compiles it. Choose TLA+ when the design is still abstract and you want to find a protocol bug before implementation; choose Dafny when the implementation exists and you want the guarantees to travel with it.

Against Verus and Why3, the difference is integration. Verus embeds verification into Rust, inheriting Rust's ownership model as part of the proof context. Why3 is a platform for connecting many provers to many languages. Dafny is a self-contained language with its own syntax, its own standard library in Source/DafnyStandardLibraries, and its own compilation targets. That self-containment is the trade: you learn a new language, and in exchange you get one tool that verifies and compiles without a foreign type system in the middle.

Building from source, releases and licence scope

If you need to modify the compiler, the Makefile is the entry point. The default target builds the solution, and the integration tests run through dotnet test:

make exe
dotnet test Source/IntegrationTests

The Makefile also exposes a filtered test target, make test name=<filter>, with build=false to skip rebuilding, and a test-dafny target for running the CLI against a single integration case. Those exist because the full integration suite is not something you run casually on every edit.

Upgrade cost is mostly a function of which release you track. Numbered releases appear at a slower cadence than the nightly, and the nightly tag changes daily. The README does not document a rollback procedure, and the repository's RELEASE_NOTES.md is where breaking changes would be recorded, so read it before moving a verified codebase across a major version. Verification failures after an upgrade are more likely to come from changed solver heuristics than from changed syntax.

On licensing, the README states that Dafny itself is MIT, with details in LICENSE.txt at the root. It also states that Source/DafnyCore/Coco contains third-party material under its own LICENSE.txt. The repository's license field is reported as NOASSERTION, which is consistent with a root licence that does not describe every subdirectory. If you redistribute Dafny or embed it in a product, read both files rather than assuming the root MIT text covers the whole tree. This is a description of what the files say, not legal advice.

What to check on your own code before you commit

The failure mode that surprises people is a specification that verifies but does not say what they meant. A postcondition can be satisfied by a function that returns the wrong answer for inputs your precondition excludes, and the verifier will happily accept it because you told it those inputs do not occur. Write the precondition you actually need, then test the compiled output against a few concrete cases to confirm the two agree.

The second thing to check is whether your proofs survive a version bump. Because the solver does the work, a change in heuristics can turn a passing file into a failing one without any edit on your side. Keep the Dafny version pinned in your build and re-run verification as an explicit step rather than assuming it still holds.

The third is audience. A verified codebase is only as good as the people who can read the invariants. If nobody on the team can explain why a loop invariant is inductive, the proof is a liability the first time someone has to change the loop.

Editorial conclusion

Adopt Dafny when the cost of a missed edge case exceeds the cost of writing loop invariants and termination arguments: protocol state machines, index arithmetic, parsers, anything where a test suite samples a space you need covered. Do not adopt it as a general-purpose replacement for your application language, and do not expect the verifier to accept a program whose invariants you have not worked out. Before committing, install the VS Code extension, run the online tutorial's binary search example, and check whether the automatic induction heuristics discharge your own loop or leave you writing manual lemmas. Then read Source/DafnyCore/Coco/LICENSE.txt, because the MIT licence on the repository root does not cover that subdirectory.

Frequently asked questions

Official sources

1. dafny-lang/dafny on GitHub
2. Issues
3. Project website
4. README
5. Releases