F* – Microsoft's programming language with a superset of features over F#

After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code.