F*'s type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs.
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 the current F* variant is available in a series of POPL papers (2016, 2017, and 2018). You can learn more about F* by following the online tutorial and reading our papers. Materials from recent talks are also available below. And to keep up to date with the latest news on F* you can read our blog.