F*: A Proof-Oriented Programming Language
Introduction
Download
Learn
Community
Uses
Research
People
Introduction
F* (pronounced F star) is a general-purpose proof-oriented<br>programming language, supporting both purely functional and<br>effectful programming. It combines the expressive power of dependent<br>types with proof automation based on SMT solving and tactic-based<br>interactive theorem proving.
F* programs compile, by default, to OCaml. Various fragments of F*<br>can also be extracted to F#, to C or Wasm by a tool<br>called KaRaMeL,<br>or to assembly using<br>the Vale<br>toolchain. F* is implemented in F* and bootstrapped using OCaml.
F* is open source on GitHub and is under<br>active development by Microsoft Research,<br>Inria, and by the community.
Download
F* is distributed under the Apache 2.0 license.<br>Binaries for Windows, Linux, and Mac OS X are posted regularly on the releases page on GitHub.<br>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<br>book Proof-oriented<br>Programming In F* is being written and regular updates are<br>posted online. You probably want to read it while trying out<br>examples and exercises in your browser by clicking the image below.
Low*
We also have a<br>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<br>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,<br>8-12 August, 2018, Ohrid, Macedonia Course material
Community
Please use GitHub<br>Discussions to ask questions about F*, learn about<br>announcements, etc.
Although we previously used a Slack instance, we aim to consolidate our online community<br>on this public forum on Zulip.
We also have a mailing list, which has very low traffic. You can<br>subscribe at fstar-mailing-list.
The F* PoP Up Seminar, a<br>users and developers meeting is open to all. We aim to schedule it once a month, though<br>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.<br>We list a few of them here. If you are using F* in your project, please<br>let us know by writing to the fstar-mailing-list.
Project Everest
Project Everest is an umbrella project that develops high-assurance<br>secure communication software in F*. A big part of the development of F* has been motivated by the scenarios<br>that Project Everest targets. Several offshoots from Project Everest continue as their own projects, including<br>some of those listed below.<br>HACL*, ValeCrypt, and EverCrypt
HACL* is a library of high-assurance cryptographic primitives, written in F* and extracted to C.<br>ValeCrypt provides formally proven implementations of cryptographic primitives in Vale,<br>a framework for verified assembly language programming embedded in F*.<br>EverCrypt combines them into a single cryptographic provider.<br>Code from these projects is now used in production in several projects,<br>including Mozilla Firefox,<br>the Linux kernel,<br>Python,<br>mbedTLS, the Tezos blockchain,<br>the ElectionGuard electronic voting SDK, and the Wireguard VPN.<br>EverParse
EverParse is a parser generator for binary formats that produces C code extracted from formally proven F*.<br>Parsers from EverParse are used in production in several projects, including in Windows Hyper-V,<br>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<br>production settings, including ebpf-for-windows.
Research
F* is an active topic of research, both in the programming languages and formal methods community,<br>as well as from an application perspective in the security and systems communities.<br>We list a few of them below, with full citations to these papers available in this bibliography.<br>If you would like your paper included in this list, please contact fstar-maintainers@googlegroups.com.
The Design of F* and its DSLs
Dependent<br>Types and Multi-monadic Effects in F* (POPL 2016) This<br>is the canonical reference describing the F* system. The<br>language has evolved in significant ways since 2016,<br>however, its core design and implementation is based on<br>this paper.
Verified<br>Low-level Programming Embedded in F* (ICFP 2017) which<br>describes the Low* fragment of F* which is a low-level<br>subset of F* that can be compiled to C by...