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*.

• 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.

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.

• USSL: A Universe-Stratified, Predicative Concurrent 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, 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.

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.

• 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.

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

• 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.

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).

• 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*.

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

• 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.

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.

• Secure Distributed Programming with Value-dependent Types (ICFP 2011), a longer version of which also appeared in JFP.

• Self-certification: bootstrapping certified typecheckers in F* with Coq (POPL 2012), which certifies the correctness of the F* typechecker by programming it in F* itself and bootstrapping the process by checking about 7GB of proof using Coq in about 24 machine-days of compute time.

• Fully abstract compilation to JavaScript (POPL 2013), which models a subset of JavaScript in F* and develops a secure compiler from an ML-like language to JavaScript.

• Gradual typing embedded securely in JavaScript (POPL 2014), which develops a source-to-source compiler for JavaScript with defensive checks to ensure the soundness of gradual typing in adversarial contexts, proven corrent in F*.

• Probabilistic relational verification for cryptographic implementations (POPL 2014), which develops RF*, a relational dialect of the language useful for proving security properties like noninterference and for game-based cryptographic proofs.