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* sits at the intersection of 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* represents a significant step toward making formal verification 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* is part of a generation of languages reshaping the boundary between programming and proof.