F* (pronounced F star) is an ML-like functional programming language aimed at program verification. Its type system includes polymorphism, 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 manual proofs. Programs written in F* can be translated to OCaml, F#, or C for execution.

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 one. 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 including the underlying cryptographic primitives. Moreover, while F* is extracted to OCaml by default, we are devising a subset of F* that can be compiled to C for efficiency.

Previous versions of F* could also be translated to JavaScript. We have used these previous versions 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.

Download

The sources of F* are hosted on GitHub. Binary packages are available for multiple platforms.