The Dafny Programming Language and Static Verifier

In this talk, I will give an overview of Dafny, a verification-aware programming language that is currently maintained by my colleagues and me at Amazon Web Services.

Dafny is a full-grown language with support for common programming concepts such as inductive datatypes, lambda expressions, and classes. It can be compiled to C#, Java, Javascript, Python, and Go, making integration with existing workflow possible.

At the same time, Dafny offers an extensive toolbox for mathematical proofs about programs, including quantifiers, (co-)induction, and the ability to use and prove lemmas. Programs can be annotated in the style of Hoare-Logic, with pre-and post-conditions, loop-invariants, as well as termination and read/write framing specifications. Proofs can be verified instantaneously, through compilation to the Boogie intermediate language, which uses the Z3 SMT-solver to discharge proof obligations.

After an initial formal introduction, I’ll give a live-demo of Dafny. I’ll then review some of its publicly known use-cases at Amazon and highlight its potential for supporting your own research.