F* (pronounced ‘F star’) is a proof-oriented programming language, general-purpose, that combines dependent types with proof automation via SMT and interactive tactics. It supports both purely functional and effectful programming.
According to the official website fstar-lang.org, programs in F* compile by default to OCaml, but can also be extracted to F#, C, or Wasm using the KaRaMeL tool, or to assembly via the Vale toolchain. The language is implemented in F* and bootstrapped with OCaml.
F* is open source, distributed under the Apache 2.0 license, and available on GitHub. Binaries for Windows, Linux, and Mac OS X are published regularly on the releases page. It can also be installed via OPAM, Docker, Nix, or compiled from source.
Development is active, led by Microsoft Research, Inria, and the community. An online book called ‘Proof-oriented Programming In F*’ is in progress, with regular updates, and there is a tutorial for Low*, a low-level subset that can be compiled to C via KaRaMeL.
F* is used in industrial and academic projects. The Project Everest is an umbrella that develops high-assurance secure communication software in F*. Several subprojects were born from it, such as HACL*, ValeCrypt, and EverCrypt.
HACL* is a library of high-assurance cryptographic primitives, written in F* and extracted to C. ValeCrypt provides formally verified implementations in Vale, a framework for verified assembly language embedded in F*. EverCrypt combines both into a single cryptographic provider.
Code from these projects is in production in various places, including Mozilla Firefox, the Linux kernel, Python, mbedTLS, the Tezos blockchain, the ElectionGuard electronic voting SDK, and the Wireguard VPN.
EverParse is a parser generator for binary formats that produces formally verified C code extracted from F*. EverParse parsers are used in production in Windows Hyper-V, where every network packet passing through the Azure platform is parsed and validated by code generated by EverParse. It is also used in ebpf-for-windows.
Research in F* is active in the programming languages and formal methods communities, as well as applications in security and systems. One of the central concepts is the Dijkstra monad, introduced in 2013 at PLDI, which allows verifying higher-order programs. Later works, such as ‘Dijkstra Monads for Free’ (POPL 2017) and ‘Dijkstra Monads for All’ (ICFP 2019), generalized and automated this approach.
Other milestones include the concurrent separation logic SteelCore (ICFP 2020), basis of the Steel DSL, and PulseCore (PLDI 2025), an impredicative concurrent separation logic that underpins the Pulse language, embedded in F* for proof-oriented programming.
In the security area, F* was used to verify the TLS 1.3 record layer (S&P 2017), the HACL* cryptographic library (CCS 2017), the Signal protocol via LibSignal* compiled to Wasm (S&P 2019), and the EverCrypt provider (S&P 2020).
There are also verified implementations of the QUIC record layer (S&P 2021), the DICE measured boot protocol (USENIX Security 2021), and the ACME standard (CCS 2021). The DY* framework allows symbolic analysis of executable cryptographic protocols.
F* stands out as a mature tool for formal verification, with real adoption in critical infrastructures. Its open source nature and collaborative development between Microsoft Research, Inria, and the community reinforce the role of open source as a democratic counterpoint to closed solutions.
For those who want to learn, the online book and course materials at seasonal schools are valuable resources. The language continues to evolve, with new research and applications constantly emerging.