F*: A general-purpose proof-oriented programming language

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

I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.

Would this language be useful for implementing compilers and formally proving things about them?

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?

Would this language be useful for implementing compilers and formally proving things about them?

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?

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

I'm the opposite: when landing in a programming language site I want to know the user case the authors had in mind, the memory model, the type system, the compilation targets, the data layout, the control structures, and only at the end just check that the syntax is not indentation based.

To borrow your video game analogy. F* is the dwarf fortress of programming languages. Screenshots are only going to confuse anyone who isn't ready to take a significant mental journey.

> Clicked like 5 pages and never found 1 code example.

But I clicked one (1) link to the online book and found a thousand?

just click the screenshot

Thank you ! I just had the absolute same experience and was about to write a similar comment - take my upvote instead !

That’s because syntax is the least interesting part of F*.

I clicked on 2 links on the main page in the Learn F* section...

I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.

What do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?

To borrow your video game analogy. F* is the dwarf fortress of programming languages. Screenshots are only going to confuse anyone who isn't ready to take a significant mental journey.

Thank you ! I just had the absolute same experience and was about to write a similar comment - take my upvote instead !

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

just click the screenshot

Takes you to an empty editor with still no code examples

I guess it's a bit popular right now

    * Error 17 at Welcome.fst(24,0-28,30):
      - Could not start SMT solver process.
      - Command: ‘/home/site/wwwroot/fstar/bin/z3’
      - Exception:
          Unix.Unix_error(Unix.ENOENT, "create_process", "/home/site/wwwroot/fstar/bin/z3")
    
    1 error was reported (see above)

> https://fstar-lang.org/tutorial/

FYI: The link to this tutorial is unluckily a little bit obscured on the F* website: Go to

> https://fstar-lang.org/index.html#learn (1)

and click on the image below the text "You probably want to read it while trying out examples and exercises in your browser by clicking the image below.".

In the section of (1) also the PDF version is linked:

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

> Clicked like 5 pages and never found 1 code example.

But I clicked one (1) link to the online book and found a thousand?

Should be on the home page of any programming language site.

What do you mean "express calling"? You mean calling the former C versions of the functions not yet ported, while asserting their behavior?

I guess it's a bit popular right now

    * Error 17 at Welcome.fst(24,0-28,30):
      - Could not start SMT solver process.
      - Command: ‘/home/site/wwwroot/fstar/bin/z3’
      - Exception:
          Unix.Unix_error(Unix.ENOENT, "create_process", "/home/site/wwwroot/fstar/bin/z3")
    
    1 error was reported (see above)

Takes you to an empty editor with still no code examples

That’s because syntax is the least interesting part of F*.

Then why are we all so interested?

Examples provide more than syntax. It's the semantics that we care about most.

I clicked on 2 links on the main page in the Learn F* section...

So I'm very seriously considering making my language indentation based. You're saying you wouldn't like that?

> https://fstar-lang.org/tutorial/

FYI: The link to this tutorial is unluckily a little bit obscured on the F* website: Go to

> https://fstar-lang.org/index.html#learn (1)

and click on the image below the text "You probably want to read it while trying out examples and exercises in your browser by clicking the image below.".

In the section of (1) also the PDF version is linked:

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

Should be on the home page of any programming language site.

For what it's worth, I love the semantics of many indentation based languages (F# for example) but really dislike editing them. Visually scanning is much easier with braces (imo) and it's much easier to navigate braced languages when using a vim-like editor

No indeed I'm not a fan. I find it brittle and arbitrary for data values especially; that also makes automatic code generation and edition harder, for no good reason. But that's not an important consideration either way.

I don't mind indentation based languages. I used to hate them, but they've grown on me after using python, Haskell, Idris, Agda, etc. And I ended up making my own language indentation based (it is similar to Idris).

That said, it is hard-mode:

- You'll have to figure out how to parse it.

- If you want editor support, it's a pain to get tree-sitter to handle it.

- You may not be able to pull off editor operations like "rename" without implementing a pretty printer (a rename might affect indentation).

I think it is helpful for crude error recovery. On parse error, my language will simply skip to the next column 0 token and parse another declaration.

I did not do this (hindsight), but I would recommend arranging the grammar so you only get indented blocks in cases where the previous line ends in a keyword that introduces it. I think python has a trailing `:` every time indentation is introduced, and Elm does this too - in statements like `let` you need a newline after the `let` to get the multi-declaration version. (This addresses the rename issue.)

I think this falls under "[wanting] to know the user case the authors had in mind"

I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

I still don't see any code examples!

But I do see the editor to try it.

I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.

It matters a lot how the syntax looks IMO and seeing how, say, an API is scaffolded, helps understand a lot about the language in one glance

Edit: Page 18 of the PDF. That's the first time I found what the code looks like, thanks for sharing!

Is there actually any difference when it's just one (1) link away? Are most of us seriously this busy that we cannot spend even half a minute on this?

That said, it is hard-mode:

- You'll have to figure out how to parse it.

- If you want editor support, it's a pain to get tree-sitter to handle it.

- You may not be able to pull off editor operations like "rename" without implementing a pretty printer (a rename might affect indentation).

I think it is helpful for crude error recovery. On parse error, my language will simply skip to the next column 0 token and parse another declaration.

Is there actually any difference when it's just one (1) link away? Are most of us seriously this busy that we cannot spend even half a minute on this?

Then why are we all so interested?

Examples provide more than syntax. It's the semantics that we care about most.

> Examples provide more than syntax. It's the semantics that we care about most.

... and this semantics is explained in a quite encompassing way in the introductory notes "Proof-Oriented Programming in F*":

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

> https://fstar-lang.org/tutorial/

I love that people hate indentation based so I show them a poorly indented C style languages codebase to see how they feel about indentation.

I think this falls under "[wanting] to know the user case the authors had in mind"

I still don't see any code examples!

But I do see the editor to try it.

I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.

It matters a lot how the syntax looks IMO and seeing how, say, an API is scaffolded, helps understand a lot about the language in one glance

Edit: Page 18 of the PDF. That's the first time I found what the code looks like, thanks for sharing!

Isn't it easy to just auto format it?

There is no "user case", it's called use case.

> I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.

Often the reason is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.

If you want a programming language that "just" enables you to write something well-understood (in particular in the area of web development) like your suggested

> "HTTP server", "hello world", "todo list app"

in a perhaps just a little bit more elegant/concise way, just look at which web development language/framework is currently fashionable on HN.

> Examples provide more than syntax. It's the semantics that we care about most.

... and this semantics is explained in a quite encompassing way in the introductory notes "Proof-Oriented Programming in F*":

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

> https://fstar-lang.org/tutorial/

Isn't it easy to just auto format it?

There is no "user case", it's called use case.

> There is no "user case", it's called use case.

Perhaps English is not a native language for zlsa?

> There is no "user case", it's called use case.

Perhaps English is not a native language for zlsa?

> I wonder why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app" that you can just click and it shows the code for how you'd make it in that language.

If you want a programming language that "just" enables you to write something well-understood (in particular in the area of web development) like your suggested

> "HTTP server", "hello world", "todo list app"

in a perhaps just a little bit more elegant/concise way, just look at which web development language/framework is currently fashionable on HN.

> just look at which web framework

See, by listing those, you can tell what it is.

I imagine the quick project showcase would be different for Swift or for Rust.

Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.

Like what kinds of things i can even think of writing with it - an implementation example

> just look at which web framework

See, by listing those, you can tell what it is.

I imagine the quick project showcase would be different for Swift or for Rust.

Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.

Like what kinds of things i can even think of writing with it - an implementation example

> I imagine the quick project showcase would be different for Swift or for Rust.

> Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.

I suggest simply having a look at the table of contents of

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

This in my opinion gives you a first rough idea for what kind of problems people are using F*.

Spoiler alert: these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].

This is exactly the reason why I wrote further above:

> Often the reason [why more languages don't have a few simple examples of: "HTTP server", "hello world", "todo list app"] is that the value that the programming language brings is thinking very differently about how to write code - the examples how to write something in it are merely the "more boring" consequences of this different way of thinking.

> I imagine the quick project showcase would be different for Swift or for Rust.

> Would be nice to have something like that for this Fstar or any language I haven’t heard of - or maybe have but never looked into so I see why people are using it.

I suggest simply having a look at the table of contents of

> https://fstar-lang.org/tutorial/proof-oriented-programming-i...

This in my opinion gives you a first rough idea for what kind of problems people are using F*.

Spoiler alert: these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].

This is exactly the reason why I wrote further above:

> these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].

Ok, what kinds of problems are they?

And ideally - what does a simple solution look like in F-star?

Set me on the path to installing the thing (ideally above the fold)

> these are not the kind of problems which are related to ["HTTP server", "hello world", "todo list app", ...].

Ok, what kinds of problems are they?

And ideally - what does a simple solution look like in F-star?

Set me on the path to installing the thing (ideally above the fold)

> Ok, what kinds of problems are they?

> And ideally - what does a simple solution look like in F-star?

RTFM

Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example.

> Set me on the path to installing the thing (ideally above the fold)

How to install this thing:

1. Read https://fstar-lang.org/index.html#download

2. Go to the GitHub page linked there: https://github.com/fstarlang/fstar/releases

3. Download F* for an operating system of your choice there.

> Ok, what kinds of problems are they?

> And ideally - what does a simple solution look like in F-star?

RTFM

Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example.

> Set me on the path to installing the thing (ideally above the fold)

How to install this thing:

1. Read https://fstar-lang.org/index.html#download

2. Go to the GitHub page linked there: https://github.com/fstarlang/fstar/releases

3. Download F* for an operating system of your choice there.

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

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

Hacker Times

Hacker Times

F*: A general-purpose proof-oriented programming language

Discussion

Discussion

Introduction

Download

Learn F*

Low*

Course Material

Community

Uses

Project Everest

HACL*, ValeCrypt, and EverCrypt

EverParse

Research

The Design of F* and its DSLs

Semantics and Effects

Applications in Security and Cryptography

Applications in Systems

Applications in Parsing

Applications in Programming, Program Proof, and Program Analysis

AI-assisted Programming

Miscellaneous

Papers about an older version of F*