Dafny is a programming language with builtin specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs.
The Dafny programming language is designed to support the static verification of programs. It is imperative, sequential, supports generic classes, dynamic allocation, and inductive datatypes, and builds in specification constructs. The specifications include pre and postconditions, frame specifications (read and write sets), and termination metrics.
To further support specifications, the language also offers updatable ghost variables, recursive functions, and types like sets and sequences. Specifications and ghost constructs are used only during verification; the compiler omits them from the executable code.
The Dafny verifier is run as part of the compiler. As such, a programmer interacts with it much in the same way as with the static type checker—when the tool produces errors, the programmer responds by changing the program’s type declarations, specifications, and statements.
The easiest way to try out Dafny is in your web browser at rise4fun. Once you get a bit more serious, you may prefer to download to run it on your machine. Although Dafny can be run from the command line (on Windows or other platforms), the preferred way to run it is in Microsoft Visual Studio 2010, where the Dafny verifier runs in the background while the programmer is editing the program.
The Dafny verifier is powered by Boogie and Z3.
From verified programs, the Dafny compiler produces code (.dll or .exe) for the .NET platform. However, the facilities for interfacing with other .NET code are minimal.
The source code for Dafny is available.

Learn more
To become a user of Dafny, follow the Dafny tutorial online.
You can also see Dafny in action in some episodes of Verification Corner.
To learn more about the features of Dafny, the Dafny Quick Reference may be for you.
The following paper presents the salient features of Dafny, along with the SchorrWaite algorithm written in Dafny. If you’re scientifically or technically inclined, this is the one to read and cite:
K. Rustan M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR16, volume 6355 of LNCS, pages 348370. Springer, 2010. [PDF] [slides from the conference presentation]
To dig deeper into the technology behind Dafny, the following lecture notes from the Marktoberdorf 2008 summer school describe the encoding of Dafny into Boogie 2:
K. Rustan M. Leino. Specification and verification of objectoriented software. In Engineering Methods and Tools for Software Safety and Security, volume 22 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 231266. IOS Press, 2009. [PDF] [slides from the lectures]

Dafny Quick Reference
This page illustrates many of the most common language features in Dafny. In order to get you started more quickly, the descriptions here are simplified–this page is not the language reference. For example, this pages does not go into modules, iterators, or refinement, which you won’t need until you write larger or more advanced programs in Dafny.
Programs
At the top level, a Dafny program (stored as a file with extension .dfy) is a set of declarations. The declarations introduce types, methods, and functions, where the order of introduction is irrelevant. These userdefined types include classes and inductive datatypes. The classes themselves also contain a set of declarations, introducing fields, methods, and functions. If the program contains a parameterless method called Main, then execution of the compiled program starts there, but it is not necessary to have a main method to do verification.
Comments start with // and go to the end of the line, or start with /* and end with */ and can be nested.
Fields
In a class, a field x of some type T is declared as:
var x: T
Unlike for local variables and bound variables, the type is required and will not be inferred. The field can be declared to be a ghost field by preceding the declaration with the keyword ghost. Dafny’s types include bool for booleans, int for mathematical (that is, unbounded) integers, string for strings, userdefined classes and inductive datatypes, set for a finite mathematical (immutable) set of T values (where T is a type), and seq for a mathematical (immutable) sequence of T values. In addition, there are array types (which are like predefined “class” types) of one and more dimensions, written array, array2, array3, …. The type object is a supertype of all class types, that is, an object denotes any reference, including null. Another useful type is nat, which denotes a subrange of int, namely the nonnegative integers.
Methods
A method declaration (either at the top level or inside a class) has the form:
method M(a: A, b: B, c: C) returns (x: X, y: Y, z: Y)requires Premodifies Frameensures Postdecreases Rank{Body}
where a, b, c are the method’s inparameters, x, y, z are the method’s outparameters, Pre is a boolean expression denoting the method’s precondition, Frame denotes a set of objects whose fields may be updated by the method, Post is a boolean expression denoting the method’s postcondition, Rank is the method’s variant function, and Body is a statement that implements the method. Frame can be a list of expressions, each of which is a set of objects or a single object, the latter standing for the singleton set consisting of that one object. The method’s frame is the union of these sets, plus the set of objects allocated by the method body. For example, if c and d are parameters of a class type C, then
modifies {c, d}
modifies {c} + {d}
modifies c, {d}
modifies c, d
all mean the same thing.
If omitted, the pre and postconditions default to true and the frame defaults to the empty set. The variant function is a list of expressions, denoting the unending lexicographic tuple consisting of the given expressions followed implicitly by “top” elements. If omitted, Dafny will guess a variant function for the method, namely the lexicographic tuple that starts with the list of the method’s inparameters.
A method can be declared as ghost by preceding the declaration with the keyword ghost. By default, a method in a class has an implicit receiver parameter, this. This parameter can be removed by preceding the method declaration with the keyword static. A static method M in a class C can be invoked by C.M(…).
In a class, a method can be declared to be a constructor method by replacing the keyword method with the keyword constructor. A constructor can only be called at the time an object is allocated (see objectcreation examples below), and for a class that contains one or more constructors, object creation must be done in conjunction with a call to a constructor. Ordinarily, a method has a name, of course, but a class is allowed to have one constructor without a name–an anonymous constructor–like this:
constructor (n: int)modifies this{Body}
Often, ghost methods are used as lemmas. This can be made clearer in the program text by declaring the method with lemma instead of ghost method.
Here is an example method that takes 3 integers as inparameters and returns these in 3 outparameters in sorted order:
method Sort(a: int b: int, c: int) returns (x: int, y: int, z: int)ensures x <= y <= z && multiset{a, b, c} == multiset{x, y, z}{x, y, z := a, b, c;if z < y {y, z := z, y;}if y < x {x, y := y, x;}if z < y {y, z := z, y;}}
Functions
A function declaration (either at the top level or inside a class) has the form:
function F(a: A, b: B, c: C): Trequires Prereads Frameensures Postdecreases Rank{Body}
where a, b, c are the method’s parameters, T is the type of the function’s result, Pre is a boolean expression denoting the function’s precondition, Frame denotes a set of objects whose fields the function body may depend on, Post is a boolean expression denoting the function’s postcondition, Rank is the function’s variant function, and Body is an expression that defines the function. The precondition allows a function to be partial, that is, the precondition says when the function is defined (and Dafny will verify that every use of the function meets the precondition). The postcondition is usually not needed, since the body of the function gives the full definition. However, the postcondition can be a convenient place to declare properties of the function that may require an inductive proof to establish. For example:
function Factorial(n: int): intrequires 0 <= nensures 1 <= Factorial(n){if n == 0 then 1 else Factorial(n1) * n}
says that the result of Factorial is always positive, which Dafny verifies inductively from the function body. To refer to the function’s result in the postcondition, use the function itself, as shown in the example.
By default, a function is ghost, and cannot be called from nonghost code. To make it nonghost, replace the keyword function with the two keywords function method. A function that returns a boolean can be declared with the keyword predicate (and then eliding the colon and return type).
By default, a function in a class has an implicit receiver parameter, this. This parameter can be removed by preceding the function declaration with the keyword static. A static function F in a class C can be invoked by F.M(…). This can give a convenient way to declare a number of helper functions in a separate class.
Classes
A class is defined as follows:
class C {// member declarations go here}
where the members of the class (fields, methods, and functions) are defined (as described above) inside the curly braces.
Datatypes
An inductive datatype is a type whose values are created using a fixed set of constructors. A datatype Tree with constructors Leaf and Node is declared as follows:
datatype Tree = Leaf  Node(Tree, int, Tree)
The constructors are separated by vertical bars. Parameterless constructors need not use parentheses, as is shown here for Leaf.
For each constructor Ct, the datatype implicitly declares a boolean member Ct?, which returns true for those values that have been constructed using Ct. For example, after the code snippet:
var t0 := Leaf;var t1 := Node(t0, 5, t0);
the expression t1.Node? evaluates to true and t0.Node? evaluates to false. Two datatype values are equal if they have been created using the same constructor and the same parameters to that constructor. Therefore, for parameterless constructors like Leaf, t.Leaf? gives the same result as t == Leaf.
A constructor can optionally declare a destructor for any of its parameters, which is done by introducing a name for the parameter. For example, if Tree were declared as:
datatype Tree = Leaf  Node(left: Tree, data: int, right: Tree)
then t1.data == 5 and t1.left == t0 hold after the code snippet above.
Generics
Dafny supports type parameters. That is, any class, inductive datatype, method, and function can have type parameters. These are declared in angle brackets after the name of what is being declared. For example:
class MyMultiset { /*…*/ }datatype Tree = Leaf  Node(Tree, T, Tree)method Find(key: T, collection: Tree) { /*…*/ }function IfThenElse(b: bool, x: T, y: T): T { /*…*/ }
Statements
Here are examples of the most common statements in Dafny.
var LocalVariables := ExprList;Lvalues := ExprList;assert BoolExpr;print ExprList;
if BoolExpr0 {Stmts0} else if BoolExpr1 {Stmts1} else {Stmts2}
while BoolExprinvariant Invmodifies Framedecreases Rank{Stmts}
match Expr {case Empty => Stmts0case Node(l, d, r) => Stmts1}
break;return;
The var statement introduces local variables (which are not allowed to shadow other variables declared inside the same set of most tightly enclosing curly braces). Each variable can optionally be followed by :T for any type T, which explicitly gives the preceding variable the type T (rather than being inferred). The ExprList with initial values is optional. To declare the variables as ghost variables, precede the declaration with the keyword ghost.
The assignment statement assigns each righthand side in ExprList to the corresponding lefthand side in Lvalues. These assignments are performed in parallel (more to the point, all necessary reads occur before the writes), so the lefthand sides must denote distinct Lvalues. Each righthand side can be an expression or an object creation of one of the following forms:
new Tnew T.Init(ExprList)new T(ExprList)new T[SizeExpr]new T[SizeExpr0, SizeExpr1]
The first form allocates an object of type T. The second form additionally invokes an initialization method or constructor on the newly allocated object. The third form shows how the syntax differs from the second form when the constructor called is anonymous. The other forms show examples of array allocations, in particular a one and a twodimensional array of T values, respectively.
The entire righthand side of an assignment can also be a method call, in which case the lefthand sides are the actual outparameters (omitting the := if there are no outparameters).
The assert statement claims that the given expression evaluates to true (which is checked by the verifier).
The print statement outputs to standard output the values of the given print expressions. Characters in strings can be escaped; for example, of interest for the print statement is that n denotes a newline character inside a string.
The if statement is the usual one. The example shows stringing together alternatives using else if. The else branch is optional, as usual.
The while statement is the usual loop, where the invariant declaration gives a loop invariant, the modifies clause restricts the modification frame of the loop, and the decreases clause introduces a variant function for the loop. By default, the loop invariant is true, the modification frame is the same as in the enclosing context (usually the modifies clause of the enclosing method), and the variant function is guessed from the loop guard.
The match statement evaluates the source Expr, an expression whose type is an inductive datatype, and then executes the case corresponding to which constructor was used to create the source datatype value, binding the constructor parameters to the given names. If they are not needed to mark the end of the match statement, then the curly braces that surround the cases can be elided.
The break statement can be used to exit loops, and the return statement can be used to exit a method.
Expressions
The expressions in Dafny are quite similar to those in Javalike languages. Here are some noteworthy differences.
In addition to the shortcircuiting boolean operators && (and) and  (or), Dafny has a shortcircuiting implication operator ==> and an ifandonlyif operator . As suggested by their widths, has lower binding power than ==>, which in turn has lower binding power than && and .
Dafny comparison expressions can be chaining, which means that comparisons “in the same direction” can be strung together. For example,
0 <= i < j <= a.Length == N
has the same meaning as:
0 <= i && i < j && j <= a.Length && a.Length == N
Note that boolean equality can be expressed using both == and . There are two differences between these. First, == has a higher binding power than . Second, == is chaining while is associative. That is, a == b == c is the same as a == b && b == c, whereas a b c is the same as a (b c), which is also the same as (a b) c.
Operations on integers are the usual ones, except that / (integer division) and % (integer modulo) follow the Euclidean definition, which means that % always results in a nonnegative number. (Hence, when the first argument to / or % is negative, the result is different than what you get in C, Java, or C#, see http://en.wikipedia.org/wiki/Modulo_operation.)
Dafny expressions include universal and existential quantifiers, which have the form:
forall x :: Expr
and likewise for exists, where x is a bound variable (which can be declared with an explicit type, as in x: T) and Expr is a boolean expression.
Operations on sets include + (union), * (intersection), and – (set difference), as well as the set comparison operators < (proper subset), and >=, and !! (disjointness). The expression x in S says that x is a member of set S, and x !in S is a convenient way of writing !(x in S). To make a set from some elements, enclose them in curly braces. For example, {x,y} is the set consisting of x and y (which is a singleton set if x == y), {x} is the singleton set containing x, and {} is the empty set.
Operations on sequences include + (concatenation) and the comparison operators < (proper prefix) and <= (prefix). Membership can be checked like for sets: x in S and x !in S. The length of a sequence S is denoted S, and the elements of such a sequence have indices from 0 to less than S. The expression S[j] denotes the element at index j of sequence S. The expression S[m..n], where 0 <= m <= n <= S, returns a sequence whose elements are the nm elements of S starting at index m (that is, from S[m], S[m+1], … up to but not including S[n]). The expression S[m..] (often called “drop m”) is the same as S[m..S], that is, it returns the sequence whose elements are all but the first m elements of S. The expression S[..n] (often called “take n”) is the same as S[0..n], that is, it returns the sequence that consists of the first n elements of S. If j is a valid index into sequence S, then the expression S[j := x] is the sequence that is like S except that it has x at index j. Finally, to make a sequence from some elements, enclose them in square brackets. For example, [x,y] is the sequence consisting of the two elements x and y such that [x,y][0] == x and [x,y][1] == y, [x] is the singleton sequence whose only element is x, and [] is the empty sequence.
The ifthenelse expression has the form:
if BoolExpr then Expr0 else Else1
where Expr0 and Expr1 are any expressions of the same type. Unlike the if statement, the ifthenelse expression uses the then keyword, and must include an explicit else branch.
The match expression is analogous to the match statement and has the form:
match Expr {case Empty => Expr0case Node(l, d, r) => Expr1}
The curly braces can be used to mark the end of the match expression, but most commonly this is not needed and the curly braces can then be elided.

Dafny was a popular tool among the teams at the VSTTE 2012 program verification competition. It was also used at the COST Verification Competition 2011, as part of the FoVeOOS conference. And it was used in the VSComp 2010 competition at VSTTE 2010, from which a report was published:
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, and Benjamin Weiss. The 1st Verified Software Competition: Experience Report. In FM 2011: Formal Methods – 17th International Symposium on Formal Methods, volume 6664 of LNCS, pages 154168. Springer, 2011. [PDF]
(which won Best Paper Award at FM 2011). You can find Dafny solutions to the problem sets of these competitions under the Test directory of the Dafny sources.
Dafny has also been used to solve various verification benchmark challenges. At the Verified Software: Tools, Techniques, and Experiments (VSTTE 2008) conference, Weide et al. presented some verification benchmarks to facilitate the comparison between different specification languages and verifiers. This paper describes Dafny programs for those benchmarks:
K. Rustan M. Leino and Rosemary Monahan. Dafny meets the Verification Benchmarks Challenge. In VSTTE 2010, volume 6217 of LNCS, pages 112126. Springer, 2010. [PDF]
Dafny has also been used to solve some of the VACID0 verification benchmarks:
K. Rustan M. Leino and Michał Moskal. VACID0: Verification of Ample Correctness of Invariants of Datastructures, Edition 0. Tools and Experiments workshop at VSTTE 2010. [PDF]

Dafny is being used in teaching. Here’s a partial list of universities that are or have been using Dafny in some capacity in lectures and class work:

Caltech, Rajeev Joshi (CS 116)

Lomonosov Moscow State University, Eugene Kornykhin

Kansas State University, Torben Amtoft

Imperial College London, Sophia Drossopoulou and Will Sonnex

NUI Maynooth, Rosemary Monahan

ETH Zurich, Peter Müller

University of Washington, Ethan Jackson; Emina Torlak

University of Iowa, Cesare Tinelli

Koç University, Serdar Taşıran

Rice University, Swarat Chaudhuri (COMP 507)

UNSW, Carroll Morgan

University of Toronto, Azadeh Farzan

Princeton, Andrew Appel

CMU, Jonathan Aldrich

Chalmers Technical University, Moa Johansson

Eindhoven Technical University, Kees Huizing

Ohio State University, Bruce Weide

Clemson University, Murali Sitaraman

FCT Universidade Nova de Lisboa, Luis Caires

University of the Basque Country, Paqui Lucio

University of Southampton, Michael Butler
 University of Twente, Marieke Huisman
 Yale, Ruzica Piskac
 SUNY Stony Brook, Annie Liu
 University of Edinburgh, Ian Stark (APL14)
 Lübeck University of Applied Sciences, Andreas Schaefer
 UniBw München, Birgit Elbl and Lothar Schmitz
 IIT Madras, Ganesan Ramalingam
 Clarkson University, Christopher Lynch
 Tel Aviv University, Mooly Sagiv
 University of Utah, Zvonimir Rakamaric
 Memorial University, Theodore Norvell
 University of California, Santa Cruz, Cormac Flanagan
 Trinity College Dublin, Vasileios Koutavas
 Farhad Mehta, HSR Hochschule für Technik Rapperswil
and tutorials and summer schools:
 Summer School Marktoberdorf, 2008 and 2011
 LASER Summer School, 2011
 Summer School on Logic and TheoremProving in Programming Languages, Eugene, OR, 2008
 Tutorial, KTH, Stockholm, 2012
 Invited tutorial, VSTTE 2012
 Tutorial, HILT 2012
 Tutorial, ICSE 2013
If you are, or have been, teaching using Dafny, Rustan Leino would love to know of your experience. And if you want a mention on these lists, please let him know.


 Try Dafny in your browser
 Download Dafny
 Contribute to Dafny source
 Dafny online tutorial
People
People
Chris Hawblitzel
Senior Researcher
Jay Lorch
Senior Principal Researcher
Michal Moskal
Principal Research Software Development Engineer
Nikhil Swamy
Senior Principal Researcher