Fiat-Crypto: Rocq-verified generation of field arithmetic
=========================================================

Fiat-Crypto generates field-arithmetic code (C, Rust, Go, Zig and more) from parameters with a Rocq proof that the output is correct. Its Curve25519 and P-256 code ships in BoringSSL and Go's standard library.

Maintainer: MIT PLV
Website: https://github.com/mit-plv/fiat-crypto
Category: Verified implementations
Targets: Finite-field arithmetic, Curve25519, P-256, Custom primes
Approach: Correct-by-construction code generation from Rocq proofs
Access: Open source
Status: Active, mature; deployed in BoringSSL and Go
Strengths: Proved generator, no per-output proof needed. | Massive deployment. | Any prime, several languages.
Limits: Field arithmetic only. | Performance below the best hand-written assembly. | No post-quantum coverage.
Firms using it: none listed
Sources: https://github.com/mit-plv/fiat-crypto

Source page: https://sorryfree.com/frameworks/fiat-crypto/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13