Fiat-Crypto: crypto code that is generated from a proof, not written by hand

A compiler for field arithmetic, parameterised on the command line

The repository describes itself as a project for synthesizing correct-by-construction code for cryptographic primitives, and the mechanism is a compiler rather than a library.

The Coq development builds binary compilers that generate code using some implementation strategy. The parameters, the modulus, the hardware multiplication input bitwidth and so on, are specified on the command line of the compiler, and the generated C code is written to standard output.

That design has a practical consequence that is easy to miss. The generator is not tied to a particular curve. One binary serves all of them, and the curve is a parameter. The README shows the pattern with two invocations, one generating 64-bit code for the 2 to the power of 255 minus 19 curve and one generating 32-bit code for the same field, and then the same idea applied to a NIST P-256 field with the word-by-word Montgomery strategy:

    ./fiat_crypto word-by-word-montgomery 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c # 3

The trailing operation names on the command line are the requested primitives, things like carry multiplication, carry squaring, addition, subtraction, selection, and conversion to and from bytes. So the invocation reads as a specification of what arithmetic you want over what field, and the output is a C file you can read, compile and audit.

This is the point of the project. A hand-written field arithmetic routine is code nobody wants to review line by line, and a generated one comes with a proof about the properties that matter, which is what correct by construction means in practice.

The implementation strategy is the real interface

The binary is called fiat_crypto and it takes the strategy as its first argument, and the list of strategies in the README is the closest thing the project has to an API documentation.

There are six: saturated Solinas, unsaturated Solinas, word-by-word Montgomery, Dettman multiplication, Solinas reduction and base conversion.

The distinction that matters most in practice is the difference between the two Solinas variants and Montgomery. Solinas reduction is the technique of writing a field element in a redundant representation where the digits are allowed to exceed the base, which makes reduction cheap, and the saturated and unsaturated names distinguish two ways of handling the carries that the redundant form produces. Montgomery multiplication is the classic alternative, trading a representation change for a multiplication that needs no division, and it is the strategy behind most of the widely deployed constant-time implementations. Dettman multiplication is another multiplication approach, base conversion is for moving between representations, and there is a dedicated strategy for reduction on its own.

So choosing a strategy is choosing how your field arithmetic will work, and the README is careful that passing no arguments, or the help flag, or any invalid argument, produces a usage message rather than broken output.

The other thing the README is precise about is that the compiler binaries exist in two flavours. The OCaml extraction produces one binary and the Haskell extraction produces another, and there are separate make targets for each as well as a combined one, plus a target that builds only the unified OCaml compiler. The build time saving from that last one is why the README mentions it separately, since a full build is measured in hours rather than minutes.

Building it is a research project, not an install

The requirements are a good summary of what kind of project this is.

You need Coq 9.0 or later, with the Rocq standard library 9.1 or later, including the OCaml libraries. If you install Coq from the Ubuntu packages you also need the OCaml development library for Coq. In some cases, such as installing through Homebrew on a Mac, you may also need the OCaml findlib tool. The extracted OCaml code for the standalone binaries requires OCaml 4.08 or later, and generating the JSON code through the Makefile also requires jq.

The README then gives a package manager table, which is the most useful part of the requirements for a new user. On Debian and Ubuntu the packages are Coq, the findlib tool, the Coq OCaml development library and jq. On macOS with Homebrew they are Coq, findlib, coreutils and jq. On Arch they are Coq, findlib, ocaml-zarith and jq, and the Alpine row adds OCaml, make and the edge testing repository, because the package versions in the main repository are not new enough.

The build itself is a clone with submodules, and the README is explicit that the submodules matter:

git clone --recursive https://github.com/mit-plv/fiat-crypto.git

If you forgot the recursive flag, you run the submodule update command from inside the repository. Then you run make, and the README tells you to look at the continuous integration to see how long that should take, saying that at the time of the last update it was about an hour and ten minutes for a parallel make with two jobs. If you only want the command line binaries, you can save some time with a single target:

make standalone-unified-ocaml

There is a separate target for the C files of popular curves, which end up in a directory in the tree, and one for the OCaml compiler binaries alone, one for the Haskell ones, and one for both.

The outputs cover more languages than the name suggests

The repository tree is where the scope of the project becomes visible, because the top level is a list of output targets rather than a list of source directories.

There is a directory for the generated C, one for Rust, one for Go, one for Java, one for Zig, one for JSON, one for HTML and one for AMD64 assembly. Alongside them are the Bedrock 2 directory for a different verification backbone, a coqprime directory, a rupicola directory, a rewriter directory and an inversion directory, which are the pieces of the proof and tooling that sit around the code generator.

The per-language directories exist because the extraction is not one target but several. The Makefile shows special handling for the files that are not compiled through the standard Coq makefile, namely the OCaml extraction, the JavaScript of OCaml extraction, the Haskell extraction and the generated performance test files, and there is a separate directory for the extraction of JavaScript through the js of OCaml compiler, which is what makes the web version of the synthesis possible.

Two other build systems are present. There are build files for coqprime and for the rewriter in the Bazel style, and there is a set of composed, cached and config makefiles at the top level, so the build can be assembled in different ways for different consumers.

The languages are the practical headline. A team that writes Rust, Go or Java can get field arithmetic in their own language with a proof behind it, rather than a C file with a wrapper, and that is a large part of why the project exists.

The honest notes in the repository are the most interesting files

Several files at the top level have titles that read like an engineer's diary, and they are worth more than another paragraph of feature description.

There is a document on crypto defects, one on BoringSSL notes, and one called folk wisdom, and the names alone tell you that this is a project that has looked hard at what goes wrong in hand-written cryptographic code and written down what it learned. The BoringSSL notes in particular are the kind of document that tells you the project is aimed at people who intend to use the output in a real, audited stack rather than in a demo.

There is also a primes file and an output tests directory, which is the mechanism for checking that the generated code does what the proof says. Generated code is only useful if someone checks it, and a directory of output tests next to the generators is the sign that the project does.

The release history is slow and deliberate, with v0.1.4 in May 2024, v0.1.5 in June 2025 and v0.1.6 in October 2025, and the last push on 2026-10-19. Version zero point one for a project of this size is not a warning sign, it is a statement about what the artefact is: a research tool whose output you generate yourself, not a package with a stable release contract.

The licence picture needs a moment. The repository listing records the licence as a custom one that GitHub cannot classify and points at the licence file, while the tree itself contains separate Apache, BSD 1-Clause and MIT licence files, which usually means the output is offered under several terms. Which one applies to which artefact is exactly the question the licence file should answer, and it is worth reading before the generated code lands in a product.

Continuous integration across six platforms, and a browser version

The badge row at the top of the README is a good summary of how the project is validated, and it is unusually broad.

There are continuous integration workflows for Coq on Docker, on Debian, on Alpine, on Arch Linux, on Windows and on macOS, plus a separate workflow for the opam package. Six operating system and distribution combinations for a proof development is a heavy requirement, and it is a signal about the audience: the people using this are the ones who build cryptographic primitives for a living and need to know the extraction works on the platform they ship.

The second badge row points at the other ways the project is consumed. There is a release badge, a Zulip stream for discussion, a badge for the Rust crate and a badge for the Go reference documentation. So the generated code is not trapped in the Coq development. There is a published crate and a documented Go package, and the project has a community space of its own rather than only an issue tracker.

Then there is the part that makes the project explorable without a Coq installation. You can try out the synthesis on the web, and the README notes that this is supported by compilation through the js of OCaml compiler. That is a small piece of engineering with a large practical payoff, because the alternative for a newcomer is an hour of build before you can see anything work.

So the shape of the project is a verified development with several extraction targets, several output languages, a broad continuous integration matrix, and a browser front end that lets you try it in a minute.

Editorial conclusion

Adopt Fiat-Crypto if you are implementing a curve or a field arithmetic routine and want the implementation to come with a proof of its properties rather than a test suite, since that is the whole premise of the project. Do not adopt it if you need a library you can add to a build this afternoon, because the build needs a recent Rocq installation, OCaml, submodules and about an hour of machine time. Before you start, decide which output language you need and which implementation strategy fits your field, and check the licence question, because the repository listing records a custom licence while the tree contains separate Apache, BSD and MIT licence files.

Frequently asked questions

Official sources

1. Issues
2. mit-plv/fiat-crypto on GitHub
3. Project website
4. README
5. Releases