Dafny is a programming language with a program verifier. As you type in your program, the verifier constantly looks over your shoulders and flags any errors. Dafny is currently spread across 3 sites:
- This site, including
- sources
- binary downloads for Windows, Mac, GNU/Linux, and FreeBSD
- the issue tracker (old issues are on codeplex)
- the wiki, including frequently asked questions
- The Rise4fun site, including a tutorial, where you can verify Dafny programs in your web browser.
Community
You can ask questions about Dafny on Stack Overflow or participate in general discussion on Dafny's .
Try Dafny
The easiest way to get started with Dafny is to use rise4fun, where you can write and verify Dafny programs without having install anything. On rise4fun, you will also find the online Dafny tutorial.
It is also easy to install Dafny on your own machine in VS Code, which gives you a much better user experience than in the web browser.
Setup
See installation instructions on the wiki
and instructions for installing the Dafny mode for Emacs.
Read more
Here are some ways to get started with Dafny:
- 4-part course on the Basics of specification and verification of code:
- Lecture 0: Pre- and postconditions (19:08)
- Lecture 1: Invariants (20:56)
- Lecture 2: Binary search (21:14)
- Lecture 3: Dutch National Flag algorithm (20:33)
- New overview article: Accessible Software Verification with Dafny, IEEE Software, Nov/Dec 2017
- Online tutorial, focusing mostly on simple imperative programs
- 3-page tutorial notes with examples (ICSE 2013)
- Dafny Quick Reference
- Language reference for the Dafny type system, which also describes available expressions for each type
- Cheatsheet: basic Dafny syntax on two pages
- Dafny Reference Manual [html] [pdf]
- Dafny Power User
- Videos at Verification Corner
The language itself draws pieces of influence from:
- Euclid (from the mindset of a designing a language whose programs are to be verified),
- Eiffel (like the built-in contract features),
- CLU (like its iterators, and inspiration for the out-parameter syntax),
- Java, C#, and Scala (like the classes and traits, and syntax for functions),
- ML (like the module system, and its functions and inductive datatypes), and
- Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).
External contributions
- Haskell-to-Dafny translator, by Duncan White
- Vim-loves-Dafny mode for vim, by Michael Lowell Roberts
- Boogie-Friends Emacs mode
Contributors
To enforce some basic style conventions, we've adopted pre-commit. We're
using their default hooks. When you clone
Dafny, install pre-commit as per the instructions.
For example, on OSX you do
$ brew install pre-commit
Then run
$ pre-commit install
This will install pre-commit hooks in your .git/hooks directory.
Code of Conduct
This project has adopted the Microsoft Open Source Code of Conduct. For more information see the Code of Conduct FAQ or contact opencode@microsoft.com with any additional questions or comments.
License
Dafny itself is licensed under the MIT license. (See LICENSE.txt in the root directory for details.) The subdirectory third_party contains third party material; see NOTICES.txt for more details.