This repository provides an introductory tutorial to the use of F*, a proof-oriented programming language, for generating verified implementations of cryptographic functions.
This work was carried out by an MSc mathematics student during an internship with the company.
The worked example is the Extended Euclidean Algorithm (EEA) — a simple algorithm grounded in elementary number theory that underpins many cryptographic primitives (e.g., modular multiplicative inverses for RSA).
Roughly, the verified code generation process can be summed up as follows:
- Specify the algorithm in
F*along with expected pre/post-conditions - Prove termination and correctness w.r.t. the post-conditions assisted by the built-in SMT solver
- Automatically extract verified executable code in the OCaml programming language from the EEA specification.
- Run the generated code.
This folder hosts:
- A compilation guide that explains how to set up the toolchain (F*, OCaml, Dune) and run the verified EEA implementation.
- The source code of the EEA specifications in F*.