Dafny
Programming with specifications and verification
What it does
Dafny incorporates specifications such as preconditions and postconditions into its language, uses a static verifier, and can compile programs to other development languages.
When to use it
For algorithms with explicit correctness conditions, use invariant and method-specification examples to describe loops and their intended results.
