On: Verified Programming in F*: A Tutorial

[mmoskal]

F* primary aim is correctness - think something between Coq/LEAN/Isabelle and OCaml/F#. It uses a dependent type system to verify deep functional properties of programs (say that qsort actually sorts, or that a tree is balanced and implements a mathematical map).

Typically such languages are more academic than F*.

[wolfspider → mmoskal]

I would also say take a look at Bosque it is also from the same camp as F* but much simpler to use Z3 with.