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.

F* Tutorial

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


Past contributors


Papers

24 results
2023
[24] ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER (, , , , ), In Certified Programs and Proofs, . [bibtex] [pdf]
[23] FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores (, , , , , , , ), In Certified Programs and Proofs, . [bibtex] [pdf]
2022
[22] Provably-Safe Multilingual Software Sandboxing using WebAssembly (, , ), In Proceedings of the USENIX Security Symposium, . [bibtex] [pdf]
[21] Hardening Attack Surfaces with Formally Proven Binary Format Parsers (, , , , , , , , , ), 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, . [bibtex] [pdf]
2021
[20] Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (, , , , , , ), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), . [bibtex] [pdf]
[19] DICE*: A Formally Verified Implementation of DICE Measured Boot (, , , , ), In 30th Usenix Security Symposium, . [bibtex] [pdf]
[18] Programming and Proving with Indexed Effects (, , , , ), . [bibtex] [pdf]
[17] A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer (, , , , , , , , ), In Proceedings of the IEEE Symposium on Security and Privacy, . [bibtex] [pdf]
2020
[16] SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs (, , , , , ), In 25th ACM SIGPLAN International Conference on Functional Programming (ICFP), . [bibtex] [pdf]
[15] Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language (, , , , ), In Proceedings of the Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), . [bibtex] [pdf]
2019
[14] Dijkstra Monads for All (, , , , , , ), In 24th ACM SIGPLAN International Conference on Functional Programming (ICFP), . (To Appear) [bibtex] [pdf]
[13] The Next 700 Relational Program Logics (, , , ), arXiv:1907.05244, . [bibtex] [pdf]
[12] Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (, , , , , , , , , , , , ), In 28th European Symposium on Programming (ESOP), Springer, . [bibtex] [pdf] [doi]
[11] Formally Verified Cryptographic Web Applications in WebAssembly (, , , ), In 2019 IEEE Symposium on Security and Privacy (SP), . [bibtex] [pdf] [doi]
[10] Wys*: A DSL for Verified Secure Multi-party Computations (, , ), In 8th International Conference on Principles of Security and Trust (POST) (Flemming Nielson, David Sands, eds.), Springer, volume 11426, . [bibtex] [pdf] [doi]
[9] A Verified, Efficient Embedding of a Verifiable Assembly Language (, , , , , ), In PACMPL, . [bibtex] [pdf]
2018
[8] Recalling a Witness: Foundations and Applications of Monotonic State (, , , , , ), In PACMPL, volume 2, . [bibtex] [pdf]
[7] A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations (, , , , , , , , , ), In The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, . [bibtex] [pdf]
2017
[6] Verified Low-Level Programming Embedded in F* (, , , , , , , , , , ), In PACMPL, volume 1, . [bibtex] [pdf] [doi]
[5] Everest: Towards a Verified, Drop-in Replacement of HTTPS (, , , , , , , , , , , , , , , , , , , , , ), In 2nd Summit on Advances in Programming Languages, . [bibtex] [pdf]
[4] Dijkstra Monads for Free (, , , , , , , ), In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), ACM, . [bibtex] [pdf] [doi]
2016
[3] Towards a Provably Correct Encoding from F* to SMT (), Inria Internship Report, . [bibtex] [pdf]
[2] Dependent Types and Multi-Monadic Effects in F* (, , , , , , , , , , , ), In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM, . [bibtex] [pdf]
2013
[1] Verifying Higher-order Programs with the Dijkstra Monad (, , , , ), In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, . [bibtex] [pdf]

Talks