# 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.

Website: http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf