An Interactive Proof Mode for Dafny

News

August 1st, 2025: The project is now officially funded by a generous Amazon Research Award.

About

Dafny is a programming language that enables program specification and verification. The compiler includes a verifier that checks and ensures that the program meets its specification.

The verifier is not fully automatic: it relies on additional annotations that must be supplied by the programmer, such as invariants or helper assertions, to check the implementation against the specification. The annotations constitute the program proof and they must be supplied in the source code.

We are working towards an interactive proof mode for Dafny, similar on the surface to the Rocq prover or to the Why3 interactive proof mode, which will allow the programmer to construct proofs interactively.