Fiat-Crypto
A system that synthesizes correct-by-construction, formally verified code for cryptographic primitives, extracting the result to OCaml, Rust, and Go.
Fiat-Crypto synthesizes cryptographic primitive code that is correct by construction, using the Coq (Rocq) proof assistant to formally verify the generated implementations. It targets finite-field and elliptic-curve arithmetic used by cryptographic libraries, producing code that can be checked against a specification rather than trusted by inspection alone.
The project builds with Coq and the Rocq standard library, plus OCaml libraries for code extraction, and it publishes the generated code as a Rust crate and a Go package. Building the full project from source can take over an hour.
Synthesis can also be tried directly in a browser through a WebAssembly build compiled with js_of_ocaml.