Dafny

Homepage: https://dafny.org/
Author: K. Rustan M. Leino
Paradigms: imperative, functional

Verification-aware programming language with a static program verifier; compiles to C#, Java, JavaScript, Go, and Python