F*

A Multi-Paradigm programming language created by Microsoft. Can be used as a Theorem Prover. Allows precise functional correctness though type checking programs with SMT Solvers.