F* is an ML-like programming language aimed at program verification. At its core is a type system based on dependent types, refinement types and Hoare-style logics for user-defined monadic effects. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving, user provided proof terms, as well as interactive proofs using tactics.

This tutorial provides a general introduction to F* followed by a focus on Low*, a subset of F* that extracts to C code for efficient, low-level programming. The examples we present are drawn from Project Everest, an ongoing effort using F* and Low* to verify and deploy secure components in the HTTPS ecosystem, including protocols such TLS and the cryptographic algorithms that underlie it