F*: A Proof-Oriented General-Purpose Programming Language
Original: F*: A general-purpose proof-oriented programming language
Why This Matters
F* demonstrates that formally verified, proof-oriented code can reach large-scale production systems across cloud, OS, and security infrastructure.
F* (F star) is an open-source, general-purpose proof-oriented programming language developed by Microsoft Research and Inria. It combines dependent types with SMT-based proof automation, compiles to OCaml by default, and is distributed under the Apache 2.0 license for Windows, Linux, and macOS.
F* (pronounced 'F star') is a general-purpose proof-oriented programming language that supports both purely functional and effectful programming. It integrates dependent types with SMT-based proof automation and interactive tactic-based theorem proving. By default, F* programs compile to OCaml, but various subsets can also target F#, C, WebAssembly via the KaRaMeL tool, or assembly via the Vale toolchain. F* is self-hosted—implemented in F* and bootstrapped using OCaml—and is open source on GitHub under the Apache 2.0 license, actively developed by Microsoft Research, Inria, and the broader community.
Notably, F* powers several high-assurance production systems. The HACL* cryptographic library, extracted from F* to C, is deployed in Mozilla Firefox, the Linux kernel, Python, mbedTLS, the Tezos blockchain, ElectionGuard, and WireGuard VPN. EverParse, a formally verified binary format parser generator written in F*, is used in Windows Hyper-V to parse every network packet traversing the Azure cloud platform. The umbrella Project Everest coordinates development of high-assurance secure communication software using F*. Learning resources include an online book 'Proof-Oriented Programming in F*,' Low* tutorials, and course materials from multiple academic summer schools.