F*: A General-Purpose Proof-Oriented Programming Language
Overview
F* is a general-purpose proof-oriented programming language that supports both purely functional and effectful programming through dependent types, SMT solving, and tactic-based interactive theorem proving.
The language is implemented in F* and bootstrapped using OCaml. Its core design relies on dependent types to express rich specifications, while proof automation is provided by SMT solvers and an interactive tactic language. F* programs can be written in a functional style or with effects such as state, exceptions, or concurrency, and the same language is used to write both programs and their correctness proofs.
Compilation Targets
F* programs are compiled by default to OCaml, with additional extraction paths to F#, C, WebAssembly, and verified assembly via KaRaMeL and Vale.
By default, the F* compiler emits OCaml code that can be linked with the OCaml runtime. The KaRaMeL tool extracts subsets of F* (including Low*) to C or to WebAssembly. The Vale toolchain extracts low-level F* fragments to assembly language, enabling verification of performance‑critical code. These extraction mechanisms allow the same source to target multiple back‑ends while preserving functional correctness guarantees.
Installation and Distribution
F* is released under the Apache 2.0 license and provides binaries for Windows, Linux, and macOS on GitHub releases, plus OPAM, Docker, Nix, and source builds.
Users can download pre‑built binaries from the F* releases page on GitHub. Alternative installation methods include OPAM packages, Docker images, Nix expressions, or building from source following the instructions in INSTALL.md. All distribution channels are maintained by the F* development team at Microsoft Research, Inria, and the community.
Learning Resources
The primary learning material for F* is an online book titled Proof-oriented Programming In F*, supplemented by a Low* tutorial and various course materials from seasonal schools.
The book Proof-oriented Programming In F* is regularly updated and available as a PDF on the F* website. An accompanying tutorial page provides a snapshot and exercises that can be tried in the browser. A separate tutorial covers Low*, the low‑level subset of F* that compiles to C via KaRaMeL. Course materials from events such as the Oregon Programming Language Summer School (2019, 2021), ECI 2019, and EUTypes Summer School 2018 are also published online, containing lecture notes, slides, and code examples.
Low* Subset
Low* is a low-level subset of F* that can be compiled to C by KaRaMeL, enabling verified systems programming.
Low* restricts F* to a fragment suitable for systems code, providing direct control over memory layout and inline assembly while retaining the language’s dependent type system. Code written in Low* can be proved correct in F* and then extracted to efficient C, making it appropriate for developing verified cryptographic primitives, parsers, and OS components.
Community and Support
The F* community uses GitHub Discussions, a public Zulip forum, a low‑traffic mailing list, and monthly PoP Up Seminars for communication and support.
Questions and announcements are handled in the GitHub Discussions forum. A public Zulip chat (fstar.zulipchat.com) serves as the main real‑time discussion venue. A Google Groups mailing list exists for low‑traffic announcements. The F* PoP Up Seminar, a user and developer meeting, is held irregularly but aims for a monthly cadence. Maintainers can be reached at fstar-maintainers@googlegroups.com.
Industrial and Academic Uses
F* is used in several high‑assurance projects, most notably Project Everest, which produces verified cryptographic libraries and parsers deployed in Firefox, the Linux kernel, Python, mbedTLS, Tezos, ElectionGuard, Wireguard, Windows Hyper‑V, and ebpf‑for‑windows.
Project Everest develops HACL* (a verified cryptographic library), ValeCrypt (verified assembly cryptography), and EverCrypt (a combined provider). EverParse generates verified parsers for binary formats. These artifacts have been integrated into production software: Firefox uses HACL* for TLS, the Linux kernel includes HACL* curve25519 code, Python’s cryptography library incorporates HACL*, mbedTLS bundles EverCrypt, Tezos switched to HACL*, ElectionGuard relies on EverCrypt, Wireguard uses HACL* for cryptographic operations, Windows Hyper‑V employs EverParse‑generated parsers for network packets, and the ebpf‑for‑windows project uses EverParse for eBPF program loading.
Research Foundations
Research on F* spans language design, semantics and effects, security and cryptography, systems, parsing, programming and program analysis, and AI‑assisted programming, with numerous peer‑reviewed papers cited in the project bibliography.
Key works include the POPL 2016 paper "Dependent Types and Multi-monadic Effects in F*" describing the core language, the ICFP 2017 paper "Verified Low-level Programming Embedded in F*" introducing Low*, the POPL 2019 paper "A Verified, Efficient Embedding of a Verifiable Assembly Language" presenting Vale, and the ESOP 2019 paper "Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms" describing the metaprogramming system. Additional papers cover Dijkstra monads, Steel and SteelCore concurrent separation logics, USSL and PulseCore, and various application‑specific verifications in cryptography, systems, parsing, and programming language implementation.
Applications in Security and Cryptography
F* has been applied to verify cryptographic protocols and implementations, including TLS 1.3, QUIC, Signal, post‑quantum TLS, and various authenticated encryption constructions.
Notable verified artifacts include the TLS‑1.3 record layer (S&P 2017), HACL* (CCS 2017), EverCrypt (S&P 2020), HACL×N (CCS 2020), the QUIC record layer (S&P 2021), DICE measured boot (USENIX Security 2021), DY* framework for symbolic protocol analysis (Euro S&P 2021), Noise* library for secure channel protocols (S&P 2022), TreeSync for MLS (USENIX Security 2023), and Comparse for protocol‑aware parsing (CCS 2023). Recent work also proves Rust TLS‑1.3 implementations via translation to F* (CCS 2025).
Applications in Systems
F* is used to verify memory allocators, sandboxing, data integrity monitors, and concurrent key‑value stores.
Examples include a provably‑safe WebAssembly sandbox (USENIX 2022), FastVer and FastVer2 for data integrity monitoring (SIGMOD 2021, CPP 2022), Pipit for reactive real‑time systems (ECOOP 2024), and StarMalloc, a hardened concurrent memory allocator verified in Steel (SPLASH 2024).
Applications in Parsing
F* drives verified parser generators like EverParse and ASN1* that produce provably correct C parsers for binary formats such as CBOR, CDDL, COSE, and ASN.1 DER.
EverParse was introduced in USENIX Security 2019 and later used to harden Hyper‑V packet parsers (PLDI 2022). ASN1* provides verified ASN.1 DER parsing (CPP 2022). Recent work formalizes CBOR, CDDL, and COSE in F* and develops provably correct parsers and formatters in Pulse (CCS 2025).
Applications in Programming, Program Proof, and Program Analysis
F* supports verified compilation of reversible circuits, session‑typed multiparty protocols, abstract interpreters, domain‑specific languages for law, and verification of Rust and OCaml code.
Notable results include a verified compiler for reversible circuits (CAV 2018), Session* for multiparty protocols (OOPSLA 2020), an abstract interpretation framework verified in F* (SAS 2021), the Catala language for law with verified compiler parts (ICFP 2021), verification of a Merkle Patricia tree (arXiv 2021), Aeneas translating Rust to F* for functional correctness (ICFP 2022), Q* adapting SteelCore for quantum separation logic (PlanQC 2022), SecIO* and SecRef* for secure interaction with unverified code (POPL 2024, ICFP 2025), and a mechanically verified garbage collector for OCaml verified in F* and Low* (JAR 2025).
AI-Assisted Programming Efforts
Recent work explores neural synthesis and AI agents to automate F* program and proof generation, as well as to derive binary format specifications from natural language.
The ICSE 2025 paper "Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming" curates a large F* code corpus to train models for program and proof synthesis. The arXiv paper "3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers" develops agents that turn RFCs and examples into format specifications usable with EverParse.
Community Feedback on Hacker News
Comments on the Hacker News post highlighted desires for more visible syntax examples, inquired about industrial adoption, and discussed the language’s suitability for compiler verification and low‑level programming.
"Clicked like 5 pages and never found 1 code example. Idk why languages don't have their syntax in a sandbox front-and-center on the home page. It's like a video game site with zero screenshots or videos (also rampant). New programming languages I want 2 things: 1. What does the syntax look like 2. Why would I use this language Talk about the proof logic, show the syntax, thank you" – @cyanregiment
"I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language." – @pvsnp
"https://fstar-lang.org/tutorial/" – @LelouBil
"I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages. Is this used in the industry ? And for what kind of software ?" – @LelouBil
"Guess responsive stylesheets can't be implemented without side effects..." – @boutell
"Would this language be useful for implementing compilers and formally proving things about them?" – @3lambda
"Looks very very interesting and exciting! Key question: is anyone using it anger and has experience to share?" – @_doctor_love
"F* seems to be a collection of like five different languages and proof systems. Honestly I never figured it out. Does it get basic stuff like subtraction and u8 right, unlike Lean?" – @IshKebab
"- stupid question: why dont we have a programming language that looks like typed python but runs much faster than c++, zig and rust" – @vivzkestrel