Introduction
F* (pronounced F star) is a general-purpose proof-oriented
programming language, supporting both purely functional and
effectful programming. It combines the expressive power of dependent
types with proof automation based on SMT solving and tactic-based
interactive theorem proving.
F* programs compile, by default, to OCaml. Various fragments of F*
can also be extracted to F#, to C or Wasm by a tool
called KaRaMeL,
or to assembly using
the Vale
toolchain. F* is implemented in F* and bootstrapped using OCaml.
F* is open source on GitHub and is under
active development by Microsoft Research,
Inria, and by the community.
Download
F* is distributed under the Apache 2.0 license.
Binaries for Windows, Linux, and Mac OS X are posted regularly on the releases page on GitHub.
You can also install F* from OPAM, Docker, Nix, or build it from sources, by following the instructions here.
Learn F*
An online
book Proof-oriented
Programming In F* is being written and regular updates are
posted online. You probably want to read it while trying out
examples and exercises in your browser by clicking the image below.
Low*
We also have a
tutorial that covers Low*, a low-level subset of F*, which can be compiled to C by KaRaMeL.
Course Material
F* courses are often taught at various seasonal schools. Lectures and course materials for some of them are
also a useful resource.
-
Embedding Proof-oriented Programming Languages in F*)
-
Formal Verification with F* and Meta-F*
-
Verifying Low-Level Code for Correctness and Security
-
Program Verification with F*
Uses
F* is used in several projects in both industrial and academic settings.
We list a few of them here. If you are using F* in your project, please
let us know by writing to the fstar-mailing-list.
Project Everest
Project Everest is an umbrella project that develops high-assurance
secure communication software in F*. A big part of the development of F* has been motivated by the scenarios
that Project Everest targets. Several offshoots from Project Everest continue as their own projects, including
some of those listed below.
HACL*, ValeCrypt, and EverCrypt
HACL* is a library of high-assurance cryptographic primitives, written in F* and extracted to C.
ValeCrypt provides formally proven implementations of cryptographic primitives in Vale,
a framework for verified assembly language programming embedded in F*.
EverCrypt combines them into a single cryptographic provider.
Code from these projects is now used in production in several projects,
including Mozilla Firefox,
the Linux kernel,
Python,
mbedTLS, the Tezos blockchain,
the ElectionGuard electronic voting SDK, and the Wireguard VPN.
EverParse
EverParse is a parser generator for binary formats that produces C code extracted from formally proven F*.
Parsers from EverParse are used in production in several projects, including in Windows Hyper-V,
where every network packet passing through the Azure cloud platform is parsed and validated first by code generated by EverParse. EverParse is also used in other
production settings, including ebpf-for-windows.
Research
F* is an active topic of research, both in the programming languages and formal methods community,
as well as from an application perspective in the security and systems communities.
We list a few of them below, with full citations to these papers available here.
If you would like your paper included in this list, please contact fstar-maintainers@googlegroups.com.
The Design of F* and its DSLs
Semantics and Effects
- Verifying
Higher-order Programs with the Dijkstra Monad (PLDI
2013), which introduces the concept of the Dijkstra monad,
a core feature of F*'s system of effects.
- Dijkstra
Monads for Free (POPL 2017), which shows how to
automatically derive Dijkstra monads for a class of
computational monads using a continuation-passing
transformation
- A Monadic
Framework for Relational Verification: Applied to Information
Security, Program Equivalence, and Optimizations (CPP
2018), which builds on the Dijkstra Monads for Free work to
construct a framework for proving properties that relate
multiple programs or program executions.
- Dijkstra Monads
for All (ICFP 2019), which generalizes the notion of a
Dijkstra monad and shows how to systematically relate
computational and specificational monads via monad morphisms.
- Recalling a
Witness: Foundations and Applications of Monotonic
State (POPL 2018), which describes the design of a
program logic for reasoning about programs whose state
evolves monotonically, e.g., where the state is an
append-only log. This logic underpins both Low* and
Steel.
- SteelCore:
An Extensible Concurrent Separation Logic for Effectful
Dependently Typed Programs (ICFP 2020), which describes
the SteelCore concurrent separation logic, the basis of the
Steel DSL.
Applications in Security and Cryptography
Many papers applying F* in security and cryptography can be
found in
the Project
Everest bibliography. We mention a few prominent ones here
as well as other applications not related to Project Everest.
- WYS*: A DSL for
Verified Secure Multi-party Computations (POST 2017),
which describes the WYS* language, a domain-specific language
for writing verified mixed-mode secure multi-party
computations.
- Implementing
and Proving the TLS 1.3 Record Layer(S&P 2017), which
describes a verified implementaion of the TLS-1.3 record layer
in Low*.
- HACL*: A
Verified Modern Cryptographic Library (CCS 2017), which
describes HACL*, a verified cryptographic library
implemented in Low*.
- Formally
Verified Cryptographic Web Applications in WebAssembly
(S&P 2019), which develops LibSignal*, an implementation
of the Signal protocol in F* using HACL*, compiled to Wasm
by KaRaMeL.
- EverCrypt:
A Fast, Verified, Cross-Platform Cryptographic
Provider (S&P 2020), a crypto provider combining C and
assembly code from HACL* and Vale, as well as some
applications built on top of it, including a verified
high-performance Merkle tree that was used in an initial
version of Microsoft Azure CCF.
- HACL×N:
Verified Generic SIMD Crypto (for all your favorite
platforms) (CCS 2020), which metaprograms vectorized
versions of cryptographic primitives, enabling a
"write-once, get vectorized versions for free" style.
- A
Security Model and Fully Verified Implementation for the IETF
QUIC Record Layer (S&P 2021), a verified implementation of
the QUIC record layer in Low* combined with the protocol logic
implemented in Dafny.
- DICE*:
A Formally Verified Implementation of DICE Measured Boot
(USENIX Security 2021), which proves the correctness &
security of the DICE measured boot protocol for
micro-controllers, implemented in Low*, using EverCrypt and
EverParse.
- DY*:
A Modular Symbolic Verification Framework for Executable
Cryptographic Protocol Code (Euro S&P 2021), a framework
for type-based symbolic security analysis of cryptographic
protocol implementations developed in F*.
- A
Tutorial-Style Introduction to DY* (LNCS 2021), which is, yes,
a tutorial-style introduction to DY*.
- An
In-Depth Symbolic Security Analysis of the ACME
Standard (CCS 2021), which proves the security of a
model of the ACME certificate issuance and management
protocol using DY*.
- Noise*:
A Library of Verified High-Performance Secure Channel Protocol
Implementations (S&P 2022), which metaprograms provably
secure implementations for a family of secure channel
protocols.
- TreeSync:
Authenticated Group Management for Messaging Layer
Security (USENIX Security 2023), a reference
implementation of MLS in F*, proven secure using the DY*
framework.
Applications in Systems
Applications in Parsing
Applications in Programming, Program Proof, and Program Analysis
- Verified
Compilation of Space-Efficient Reversible Circuits (CAV
2018), which presents ReVerC, a compiler for reversible
circuits proven correct in F*.
-
Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
(VSTTE 2020), which develops verified transformations
for assembly programs in the Vale framework.
- Statically
verified refinements for multiparty protocols (OOPSLA
2020), which presents Session*, a session-typed programming
language for multiparty protocols, formalized in F*.
- Verified
Functional Programming of an Abstract Interpreter (SAS
2021), which develops an abstract interpretation framework for
an imperative language with a very compact proof of soundness
developed in F*.
- Catala:
a programming language for the law (ICFP 2021), where
core parts of the compiler are formalized and proven correct
in F*.
- Verification of
a Merkle Patricia Tree Library Using F*, which ports a
Merkle tree library from OCaml to F*, finds and fixes a bug,
and eventually proves it correct.
- Certified
mergeable replicated data types (PLDI 2022), which
presents PEEPUL, a framework in which to build replicated data
types for use in distributed programming, formalized in
F*.
- Aeneas:
Rust verification by functional translation (ICFP
2022), which translates Rust into pure F* enabling
functional correctness proofs.
- Q*:
Implementing Quantum Separation Logic in F* (PlanQC 2022),
which adapts the SteelCore separation logic for use with a
quantum programming language.
Papers about an older version of F*
The first paper to introduce a system called F* was in
2011. Although the current version of F* was redesigned and
implemented in 2015, we include some of these older papers here
for completeness.
