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 in INSTALL.md.
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 in this bibliography.
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.
- PulseCore:
A Dependently Typed Stratified Separation Logic, a
foundational, axiom-free concurrent separation logic
shallowly embedded in F*, supporting dynamic invariants and
higher-order ghost state in a predicative
setting---PulseCore is the basis of the Pulse 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.
- Modularity,
Code Specialization, and Zero-Cost Abstractions for Program
Verification (ICFP 2023), which describes
proof-engineering techniques used in HACL* for generic
implementations of cryptographic constructions that can be
specialized repeatedly to many concrete implementations in
C. The techniques used here led to the adoption of verified
cryptographic code into the libraries of the Python
programming language.
- Verifying
Indistinguishability of Privacy-Preserving Protocols
(OOPSLA 2023), which provides a library called Waldo in F*
that enables proofs of indistinguishability over traces of
communication in networking protocols.
- Comparse:
Provably Secure Formats for Cryptographic Protocols (CCS
2023), which provides a parsing library for data formats that
are appropriate for use with symbolic protocol
analyzers. Comparse provides bit-level precise accounting of
formats allowing the DY* protocol analysis framework to reason
about concrete messages and identify protocol flaws that it
previously would have missed.
Applications in Systems
- Provably-Safe
Multilingual Software Sandboxing using WebAssembly (USENIX
2022), which describes a verified implementation of a sandbox
for WebAssembly modules in Low* and Rust.
- FastVer:
Making Data Integrity a Commodity (SIGMOD 2021), which
formalizes a protocol for data integrity monitoring in F*.
- FastVer2:
A Provably Correct Monitor for Concurrent, Key-Value
Stores (CPP 2022), which proves the correctness of a
low-level, concurrent implementation of the FastVer protocol
in Steel.
- Pipit on the
Post: Proving Pre- and Post-Conditions of Reactive Systems (ECOOP
2024), which embeds a reactive language in F* and uses it to verify
some control systems that execute in real time.
- StarMalloc: Verifying a
Modern, Hardened Memory Allocator (SPLASH 2024), a
security-oriented, concurrent memory allocator that can be used as a
drop-in replacement in real-world projects, verified in Steel.
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.
- Pipit:
Reactive Systems in F* (Extended Abstract) (TyDe 2023),
which describes a embedded DSL for verifying reactive systems.
- Securing
Verified IO Programs Against Unverified Code in F*
(POPL 2024), which presents SCIO*, a formally secure
compilation framework for statically verified programs
performing input-output (IO).
AI-assisted Programming
Miscellaneous
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.
