F* is a language in the tradition of ML equipped with dependent types, monadic effects, refinement types and a weakest precondition calculus. Together, these features enable the F* programmer to prove functional correctness using a combination of automation via SMT solving and manual program proofs.

In the context of the greater Everest project, we are using F* to prove, build and deploy miTLS, a verified, efficient implementation of the Transport Layer Security (TLS) 1.3 protocol.

This extended abstract presents our work in progress. We are currently focusing our efforts on proving the memory safety and functional correctness of Elliptic Curve Cryptography (ECC) primitives, and on extracting this code to C. ECC primitives are a good candidate: they are modeled after the reference implementations in C. Therefore, they only exercise an imperative, first-order subset of F* that lends itself well to an efficient extraction to C.