Dafny

Dafny is a programming language inspired by Euclid, Eiffel, CLU, Java, C#, ML and Coq. It features pre- and post-conditions, along with loop variants and invariants. Limited support is provided for object-oriented programming. It's free and open-source, released under MIT License.

Among its list of features are generic classes, inductive data types, dynamic allocation, along with implicit dynamic frames (derivative from separation logic). The language is primarily being used in teaching formal specification and verification. It's also typically used in contests for verifying software.

Because it builds on the Boogie intermediate language, it uses Z3, which is included in the downloaded package. After unzipping the archive, you can run "dafny /help" to view a list of supported commands.

For instance, you can pick the Dafny prelude file  (/dprelude:<file>), print the Dafny program after resolving it (/rprint:<file>), specify the filename and location for the output .cs, .dll or .exe files (/out:<file>), ignore include directives (/noIncludes) and external attributes (/noExterns), as well as allow the implicit class called "_default" to contain fields, instance methods and functions (/allowGlobals).

Boogie options are available too, like allowing only parsing (/noResolve) or only parsing and resolving (/noTypeCheck). Additional commands can be used for inference, debugging and general tracking, CIVL, verification-condition generation and splitting, and so on.