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 POPL 2016 paper and a POPL 2017 paper. You can learn more about F* by following the online tutorial. Materials from recent talks are available below. Read our blog to keep up to date with the latest news on F*.
The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and elliptic curve cryptography. Moreover, while F* is extracted to OCaml by default, we are devising a subset of F* that can be compiled to C for efficiciency.