Introduction
- Introduction
- Download
- Learn
- Community
- Uses
- Research
- People
- Verifying Low-Level Code for Correctness and Security * Lectures at the Oregon Programming Language Summer School (2019): Lecture notes, slides, code Program Verification with F\ * Course at 2018 EUTypes Summer School, 8-12 August, 2018, Ohrid, Macedonia Course material
- Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (ICFP 2021), which describes the Steel language and its use of the SteelCore concurrent separation logic for proofs of imperative programs with various forms of concurrency.
- 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. USSL: A Universe-Stratified, Predicative Concurrent Separation Logica foundational, axiom-free concurrent separation logic shallowly embedded in F\, supporting dynamic invariants and higher-order ghost state in a predicative setting, by stratifying predicates according to the hierarchy of universe levels. PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs (PLDI 2025), a foundational, axiom-free concurrent separation logic shallowly embedded in F\, supporting dynamic invariants and higher-order ghost state, with impredicative invariants and later credits. PulseCore is the foundation for Pulse, an embedded language in F\* for proof-oriented programming in concurrent separation logic.
- 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. Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust (CCS 2025), which develops Bert13, an implementation of TLS-1.3 in Rust with post-quantum features, and proves it correct and secure via translation (using Hax) to a variety of prover backends, including F\, which is used to prove the Rust code panic free and to prove that the transcript formats are injective.
- 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.
- EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats (USENIX Security 2019), which describes the EverParse parser generator for parsing binary formats, producing C code.
- Hardening Attack Surfaces with Formally Proven Binary Format Parsers (PLDI 2022), which uses EverParse to harden network packet parsers in Windows Network Virtualization and Hyper-V. ASN1\: Provably Correct Non-Malleable Parsing for ASN.1 DER (CPP 2022), which formalizes the ASN.1 DER format in F\* and proves the correctness of a parser for it in EverParse. Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE (CCS 2025), which formalizes the RFCs for the CBOR binary object format and the CDDL data description language in F\, develops provably correct and secure parsers and formatters for CBOR, and a compiler for CDDL specifications, all implemented in Pulse, and applied to various applications, including the validation of COSE signed objects.
- 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). SecRef\: Securely Sharing Mutable References between Verified and Unverified Code in F\ (ICFP 2025), which presents SecRef\, a formally secure compilation framework for statically verified stateful programs. It also presents a Dijkstra Monad for Monotonic State. Automatically Verifying Replication-Aware Linearizability (OOPSLA 2025), which develops a novel fully automated technique for verifying replication-aware linearizability for Mergeable Replicated Data Types, with proofs in F\, and verified code extracted to OCaml. A Mechanically Verified Garbage Collector for OCaml (JAR 2025), which develops a verified stop-the-world mark-and-sweep GC for OCaml, verified in F\ and Low\*.
- 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers, which developsAI agents to transform mixed informal input, including natural language documents (i.e., RFCs) and example inputs into format specifications into 3D, a data format specification language used with EverParse.
- Secure Distributed Programming with Value-dependent Types (ICFP 2011), a longer version of which also appeared in JFP.
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 Valetoolchain. 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\ * Online lectures at the Oregon Programming Language Summer School (2021): Lecture notes, slides, code Formal Verification with F\ and Meta-F\* * Lectures and tutorial at ECI 2019: Lecture notes, slides, code
Community
---
Please use GitHub Discussions to ask questions about F\*, learn about announcements, etc.
Although we previously used a Slack instance, we aim to consolidate our online community on this public forum on Zulip.
We also have a mailing list, which has very low traffic. You can subscribe at fstar-mailing-list.
The F\* PoP Up Seminar, a users and developers meeting is open to all. We aim to schedule it once a month, though the schedule is irregular---we hope to see you there!
You can also contact the maintainers of F\* at fstar-maintainers@googlegroups.com.
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
Dependent Types and Multi-monadic Effects in F\ (POPL 2016) This is the canonical reference describing the F\* system. The language has evolved in significant ways since 2016, however, its core design and implementation is based on this paper. Verified Low-level Programming Embedded in F\ (ICFP 2017) which describes the Low\ fragment of F\ which is a low-level subset of F\* that can be compiled to C by KaRaMeL. A Verified, Efficient Embedding of a Verifiable Assembly Language (POPL 2019) which describes the Vale language, a verified assembly language embedded in F\. Meta-F\: Proof Automation with SMT, Tactics, and Metaprograms(ESOP 2019) which describes MetaF\, a metaprogramming system within F\ used to implement various aspects of F\*, ranging from its tactic engine to its support for typeclasses. Programming and Proving with Indexed Effects (TR 2021) which describes the design of F\'s support for user-defined effects and provides a calculus that describes the logical core of F\*.
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.
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.
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\.
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\.
AI-assisted Programming
Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming (ICSE 2025), which curates a dataset of 940KLOC of F\ code and proof and develops AI models to automate program and proof synthesis
Miscellaneous
A Theorem Proving Approach to Programming Language Semantics(ICSE-SEET 2023), which reports on experiences teaching operational, denotational, and axiomatic semantics to students using F\.
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.
