Introduction

F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C, WASM, or ASM code. This enables verifying the functional correctness and security of realistic applications. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives.

F*'s type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs.

F* is written entirely in F*, and bootstraps via OCaml. It is open source and under active development on GitHub. A detailed description of the current F* variant is available in a series of POPL and ICFP papers (2016, 2017, 2018, 2019, and 2020). You can learn more about F* by following the online tutorial and reading our papers. Materials from recent talks are also available below.

Community: Please use the GitHub Discussions list to ask questions about F*, learn about announcements, etc. Although we have only recently started using GitHub Discussions, we hope it will become the primary way to engage with the F* community and also an archive of questions & answers that are of general interest.
The F* developers and many users interact on this Slack forum---you should be able to join 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 monthly F* users and developers meeting is open to all---we hope to see you there!

Download

F* is open source, distributed under the Apache 2.0 license. It is developed in the open and the source is hosted on GitHub. Binary packages are also available for multiple platforms.
You can check out our latest releases on GitHub.

This is the easiest way to get F* quickly running on your machine, but if the binary package you use is old you might be missing out on new features and bug fixes. We also provide experimental automatic weekly builds and of course you can also build F* from source yourself.

F* Tutorial

Click the image below to start the online tutorial version of the F* book. The book is also available as a PDF.

Low* tutorial

We also have a Low* tutorial that covers Low*, a low-level subset of F*. The tutorial also explains how to use the KaRaMeL tool to compile Low* to C.

Support

For documentation on F* please refer to the tutorial and the GitHub wiki.

F* is a state-of-the-art research project under active development; as such, it contains a number of known bugs. If you encounter a problem with F*, we encourage you to report it to the GitHub issue tracker. Please understand that we may not have the necessary manpower to address new feature requests - as an open source project, we welcome your contributions to help improve F*.

Users can chat about F* or ask questions on the F* Zulip instance. (Zulip is a good open source alternative to Slack)

The fstar-club mailing list is dedicated to F* users. Here is where various F* announcements are made to the general public (e.g. for releases, new papers, etc) and where users can ask questions, ask for help, discuss, provide feedback, announce jobs requiring at least 10 years of F* experience, etc. List archives are public, but only members can post. Join here!

People

F* is a joint project between Microsoft Research, Inria, and the community at large.

Current team

Danel Ahman (University of Ljubljana)
Cezar-Constantin Andrici (MPI-SP)
Benjamin Beurdouche (Inria Paris)
Karthikeyan Bhargavan (Inria Paris)
Jay Bosamiya (Carnegie Mellon University)
Antoine Delignat-Lavaud (MSR Cambridge)
Victor Dumitrescu (Nomadic Labs)
Cédric Fournet (MSR Cambridge)
Aymeric Fromherz (Carnegie Mellon University)
Chris Hawblitzel (MSR Redmond)
Cătălin Hriţcu (MPI-SP)
Markulf Kohlweiss (University of Edinburgh)
Kenji Maillard (Inria)

Asher Manning (Zen Protocol)
Guido Martínez (CIFASIS-CONICET Rosario)
Denis Merigoux (Inria Paris)
Bryan Parno (Carnegie Mellon University)
Zoe Paraskevopoulou (Princeton University)
Clément Pit-Claudel (MIT)
Jonathan Protzenko (MSR Redmond)
Tahina Ramananandro (MSR Redmond)
Aseem Rastogi (MSR Bangalore)
Nikhil Swamy (MSR Redmond)
Théo Winterhalter (MPI-SP)
Christoph M. Wintersteiger (MSR Cambridge)
Santiago Zanella-Béguelin (MSR Cambridge)

Past contributors

Alejandro Aguirre (IMDEA)
Abhishek Anand (Cornell)
Gilles Barthe (IMDEA)
Gavin Bierman (MSR Cambridge)
Barry Bond (MSR Redmond)
Tej Chajed (MIT)
Pierre-Evariste Dagand (CNRS and LIP6)
Juan Chen (MSR Redmond)
Simon Forest (ENS Paris)
Benjamin Grégoire (Inria Sophia-Antipolis)
Armaël Guéneau (Inria Paris and ENS Lyon)
Samin Ishtiaq (MSR Cambridge)
Chantal Keller (Université Paris-Sud)

Tomer Libal (MSR-Inria Joint Centre)
Benjamin Livshits (MSR Redmond)
Michael Hicks (University of Maryland)
Qunyan Mangus (MSR Redmond)
Gordon Plotkin (University of Edinburgh)
Michael Lowell Roberts (MSR Redmond)
Jared Roesch (University of Washington)
Cole Schlesinger (Princeton University)
Pierre-Yves Strub (École Polytechnique)
Gustavo Varo (MSR Redmond)
Jean Yang (CMU)
Peng (Perry) Wang (MIT)
Joel Weinberger (UC Berkeley)
Jean-Karim Zinzindohoué (Inria Paris)

Papers

2013
[24]	Verifying Higher-order Programs with the Dijkstra Monad (Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen and Benjamin Livshits), In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, 2013. [bibtex] [url]
2016
[23]	Dependent Types and Multi-Monadic Effects in F* (Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss and Jean-Karim Zinzindohoué), In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, 2016. [bibtex] [url]
[22]	Towards a Provably Correct Encoding from F* to SMT (Alejandro Aguirre), Inria Internship Report, 2016. [bibtex] [pdf]
2017
[21]	Dijkstra Monads for Free (Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi and Nikhil Swamy), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM, 2017. [bibtex] [url] [doi]
[20]	Everest: Towards a Verified, Drop-in Replacement of HTTPS (Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin and Jean-Karim Zinzindohoué), In 2nd Summit on Advances in Programming Languages, 2017. [bibtex] [pdf]
[19]	Verified Low-Level Programming Embedded in F* (Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet and Nikhil Swamy), In PACMPL, volume 1, 2017. [bibtex] [url] [doi]
2018
[18]	Recalling a Witness: Foundations and Applications of Monotonic State (Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi and Nikhil Swamy), In PACMPL, volume 2, 2018. [bibtex] [url]
[17]	A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations (Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi and Nikhil Swamy), In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018. [bibtex] [url]
2019
[16]	A Verified, Efficient Embedding of a Verifiable Assembly Language (Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi and Nikhil Swamy), In PACMPL, 2019. [bibtex] [pdf]
[15]	Wys*: A DSL for Verified Secure Multi-party Computations (Aseem Rastogi, Nikhil Swamy and Michael Hicks), In 8th International Conference on Principles of Security and Trust (POST) (Flemming Nielson, David Sands, eds.), Springer, volume 11426, 2019. [bibtex] [url] [doi]
[14]	Formally Verified Cryptographic Web Applications in WebAssembly (J. Protzenko, B. Beurdouche, D. Merigoux and K. Bhargavan), In 2019 IEEE Symposium on Security and Privacy (SP), 2019. [bibtex] [pdf] [doi]
[13]	Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi and Nikhil Swamy), In 28th European Symposium on Programming (ESOP), Springer, 2019. [bibtex] [url] [doi]
[12]	The Next 700 Relational Program Logics (Kenji Maillard, Catalin Hritcu, Exequiel Rivas and Antoine Van Muylder), arXiv:1907.05244, 2019. [bibtex] [url]
[11]	Dijkstra Monads for All (Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas and Éric Tanter), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019. [bibtex] [url]
2020
[10]	Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language (Bosamiya, Jay, Gibson, Sydney, Li, Yao, Parno, Bryan and Hawblitzel, Chris), In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020. [bibtex] [pdf]
[9]	SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman and Guido Martínez), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2020. [bibtex] [url]
2021
[8]	A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (Delignat-Lavaud, Antoine, Fournet, Cedric, Parno, Bryan, Protzenko, Jonathan, Ramananandro, Tahina, Bosamiya, Jay, Lallemand, Joseph, Rakotonirina, Itsaka and Zhou, Yi), In Proceedings of the IEEE Symposium on Security and Privacy, 2021. [bibtex] [pdf]
[7]	Programming and Proving with Indexed Effects (Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Tahina Ramananandro and Nikhil Swamy), 2021. [bibtex] [url]
[6]	Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux and Tahina Ramananandro), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2021. [bibtex] [url]
[5]	DICE*: A Formally Verified Implementation of DICE Measured Boot (Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani and Aditya V. Thakur), In 30th Usenix Security Symposium, 2021. [bibtex] [url]
2022
[4]	Hardening Attack Surfaces with Formally Proven Binary Format Parsers (Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona and Arti Gupta), In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '22), June 13–17, 2022, San Diego, CA, USA, 2022. [bibtex] [pdf]
[3]	Provably-Safe Multilingual Software Sandboxing using WebAssembly (Bosamiya, Jay, Lim, Wen Shih and Parno, Bryan), In Proceedings of the USENIX Security Symposium, 2022. [bibtex] [pdf]
2023
[2]	FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores (Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno and Ravi Ramamurthy), In Certified Programs and Proofs, 2023. [bibtex] [pdf]
[1]	ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER (Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro and Nikhil Swamy), In Certified Programs and Proofs, 2023. [bibtex] [pdf]

Talks

Partial Evaluation, Denotational Semantics etc. in EverParse (RiSE Talk, Nov 2021)
- slides
Embedding Proof-oriented Programming Languages in F* (OPLSS 2021 Summer School)
- Online lectures at the Oregon Programming Language Summer School (2021): Lecture notes, slides, code
Proof-oriented Programming in F*
- Goldman Sachs R \& D Seminar, March 10, 2021: slides
Programming with Proofs for High-assurance Software
- PurPL: Purdue Programming Languages Seminar; August 28, 2020: video
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
- 25th ACM SIGPLAN International Conference on Functional Programming; August 28, 2020: video
The Next 700 Relational Program Logics
- ACM SIGPLAN Symposium on Principles of Programming Languages; January 23, 2020: video
Proofs of Correctness and Security for Programs that Mix C and Assembly
- Seminar at INRIA, Paris; October 9, 2019: slides
Formal Verification with F* and Meta-F*
- Lectures and tutorial at ECI 2019: Lecture notes, slides, code
Program Verification with F* course at
VTSA 2019 Summer School, 1-2 July 2019, University of Luxembourg
Verifying Low-Level Code for Correctness and Security
- Lectures at the Oregon Programming Language Summer School (2019): Lecture notes, slides, code
Verifying Imperative Programs with Functional Programming
- Keynote Talk at Trends in Functional Programming (TFP) 2019: slides
Verified Effectful Programming in F*
- Nomadic Labs Paris (Tezos): slides, video (2018-11-14)
- Keynote Talk at Trends in Functional Programming (TFP): slides (2017-06-21)
Program Verification with F* course at
2018 EUTypes Summer School, 8-12 August, 2018, Ohrid, Macedonia
Programming and Proving in F* and Low* course at
Eighth Summer School on Formal Techniques,
May 19 - May 25, 2018, Menlo College, Atherton, CA, USA
Program Verification with F* course at
EPIT 2018 Software Verification Spring School, 7-11 May, 2018, Aussois, France
What's new in F*?
- Talk at Everest Workshop: slides (2017-10-02)
Verifying Cryptographic Implementations with F* at
Computer-aided security proofs summer school. Aarhus, Denmark, October, 2017
Dijkstra Monads for Free
- Principles of Programming Languages (POPL 2017): slides (2017-01-19)
- Invited Talk at International Conference on Interactive Theorem Proving (ITP 2016): slides (2016-08-23)
Verifying Cryptographic Implementations in F*
- Course at Summer School on Models and Tools for Cryptographic Proofs, Nancy, 2017-07-10
- Course at Summer School on Computer Aided Analysis of Cryptographic Protocols, Bucharest, 2016-09-13
Dependent Types and Multi-Monadic Effects in F*
- Dagstuhl Seminar 16131 on
  Language Based Verification Tools for Functional Programs: slides (2016-03-30)
- Principles of Programming Languages (POPL 2016) (2016-01-20): video, slides
F* tutorial
- Commercial Users of Functional Programming (CUFP) (2015-09-04)
- Symposium on Principles of Programming Languages (POPL) (2015-01-13): slides
- The Joint EasyCrypt-F*-CryptoVerif School 2014 (2014-11-26 and 27): slides and other materials
Full dependency and user-defined effects in F* at ML Workshop 2015 (2015-09-03): slides, video
Dependent types, effects, and efficient verification conditions in F* at HOPE 2015 (2015-08-30): video
Type Systems for Security Verification, Lecture, Saarland University, 2015-03-16 to 27