PV4 Dafnychecks user-specified annotations and languages' rules for a Dafny program

Application domain/field

Type of tool

Auto-active verifier/Deductive verifier

Expected input

Program and specifications


Dafny language

Expected output

Errors if the program violates a rule of the language or if the program violates the specification.


Dafny is an SMT-based automatic program verifier. It can be used to prove functional correctness of programs. It does not require any user interaction with the solver, but the user does need to write specifications. Dafny will report errors if the program may violate a rule of the language (e.g. index bounds error) or if the program violates the specification (e.g. postcondition not established). Dafny will translate the given program (and specifications) into the verification language Boogie. Boogie will generate verification conditions based on the program, which are passed to an SMT solver (specifically Z3). Dafny is used to describe both the verifier and the language that it uses. Specifications are written in the form of preconditions, postconditions, invariants, ghost code, frame conditions, and more.


License: MIT license There is a VSCode plugin for Dafny: Repository Visual Studio Marketplace


Related papers

Last publication date


Related tools

Other auto-active verifiers (i.e. verifiers where the user has no interaction with the solver): Spec#, Frama-C, SPARK, AutoProof.

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.