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.

F* Tutorial

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.

Community


Please use GitHub Discussions to ask questions about F*, learn about announcements, etc.

We also have a mailing list, which has very low traffic. You can subscribe at fstar-mailing-list.

The F* developers and many users interact on this Slack forum---you should be able to join the forum automatically by clicking here, but if that doesn't work,please ask for access on this thread.

There is also a public forum on Zulip.

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

Semantics and 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.

Applications in Systems

Applications in Parsing

Applications in Programming, Program Proof, and Program Analysis

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.