F*

F* (pronounced “F star”) is a general-purpose, proof-oriented programming language that combines the expressive power of dependent types with the convenience of automated SMT-based proof. Designed for writing programs whose correctness can be verified mechanically, F* brings together practical functional programming and formal methods, and it has been used to produce some of the largest verified software systems deployed in production today.

History and Origins

F* originated in research at Microsoft Research and MSR-Inria around 2011, when the first paper to bear the F* name — Secure Distributed Programming with Value-Dependent Types — appeared at ICFP. The early language was conceived as an extension of F# with refinement and value-dependent types, aimed at verifying security-critical distributed programs. A 2012 POPL paper, Self-certification: Bootstrapping Certified Typecheckers in F with Coq*, demonstrated that F*’s metatheory could be mechanized.

Beginning around 2015, the F* team — including Nikhil Swamy, Cătălin Hriţcu, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, and many collaborators across Microsoft Research, Inria, and partner universities — substantially redesigned the language. The redesigned F* introduced a richer effect system, weakest-precondition–based verification, and tight integration with the Z3 SMT solver. The 2016 ICFP paper Dependent Types and Multi-Monadic Effects in F\* described this modern incarnation, which is the basis for the language as it exists today.

Design Philosophy

F* is built around three intertwined ideas:

• Dependent types: Types may depend on values, allowing the language to express precise specifications — for example, that a function returns a sorted list of the same multiset as its input.
• Refinement types: Types can be refined by logical predicates (e.g., x:int{x >= 0}), giving programmers a lightweight way to encode invariants.
• A user-extensible effect system: Effects such as state, exceptions, divergence, and concurrency are tracked in the type system. Programmers can define their own effects and reason about them using weakest-precondition calculi.

A central design choice is to favor automation over interaction. Where proof assistants like Coq and Agda often require explicit tactic scripts, F* dispatches a large fraction of proof obligations to the Z3 SMT solver. When automation fails, programmers write proof terms or, increasingly, use F*’s interactive tactic engine (Meta-F*).

Key Features

• Compilation targets: F* extracts to OCaml by default. Subsets of the language extract to F#, and the Low\* subset extracts to portable, idiomatic C — enabling verified low-level systems code.
• Domain-specific languages: Low\* targets C-like memory models for systems and crypto code, while Steel provides concurrent separation logic for verifying concurrent and resource-managing programs.
• Self-hosted: The F* compiler is itself written in F* and bootstrapped through OCaml.
• SMT integration: Tight coupling with Z3 enables substantial proof automation.
• Meta-F\: A tactic framework for writing proofs and metaprograms in F itself.

Evolution

The language has evolved continuously since the 2015 redesign. Major directions have included the development of Low\* and the KaRaMeL (formerly KreMLin) tool that compiles it to C; the introduction of Meta-F\* for tactic-based proofs; and the Steel framework for concurrent separation logic. Releases are tagged frequently on GitHub — recent versions follow a date-based scheme such as v2026.05.03.

Current Relevance

F* is one of the most prominent proof-oriented programming languages in active production use. Through Project Everest, a multi-institution effort launched in 2016, F* has been used to build verified components of HTTPS — including miTLS (a verified TLS 1.3 implementation) and HACL\*, a verified cryptographic library.

HACL*-derived code has been deployed widely:

• Mozilla Firefox integrates HACL\* primitives in its NSS cryptographic library.
• WireGuard-related cryptographic code in the Linux kernel has reportedly drawn on HACL\*-derived implementations of Curve25519 and related primitives.
• CPython has upstreamed HACL\*-generated implementations of hash primitives such as Blake2.
• Microsoft Azure uses EverParse, an F*-generated zero-copy parser, to validate packets in its Hyper-V networking stack.

The language is developed openly on GitHub under the FStarLang/FStar repository, with active contributions from Microsoft Research, Inria, and a growing academic and industrial community.

Why It Matters

F* makes formal verification more practical for real-world systems software. By combining dependent types with SMT automation, it lets engineers verify cryptographic and security-critical code at production scale — code that ends up in browsers, operating system kernels, and cloud infrastructure used by billions of people. Together with Lean, Coq/Rocq, Idris, and Agda, F* belongs to a generation of languages that combine programming and proof.