https://www.fstar-lang.org/F* is a new higher order, effectful programming language (like ML) designed with program verification in mind. Its type system is based on a core that resembles System Fω (hence the name), but is extended with dependent types, refined monadic effects, refinement types, and higher kinds. Together, these features allow expressing precise and compact specifications for programs, including functional correctness properties. The F* type-checker aims to prove that programs meet their specifications using an automated theorem prover (usually Z3) behind the scenes to discharge proof obligations. Programs written in F* can be translated to OCaml, F#, or JavaScript for execution.
We have used F* in a number of projects, ranging from verifying implementations of cryptographic constructions and protocols, implementations of web browser extensions, formalizing the semantics of other languages (including JavaScript and a compiler from a subset of F* to JavaScript, and TS*, a secure subset of TypeScript), and even certifying the correctness of the core of F* type-checker itself.
The latest version of F* is written entirely in F*, and bootstraps in OCaml and F#. It is open source and under active development on GitHub. A detailed description of this new F* version is available in a recent draft. You can learn more about F* by following the online tutorial.