Verified cryptographic implementations: Jasmin, hax, Cryptol/SAW, Fiat-Crypto, HACL*, CryptoLine, Kani compared
================================================================================

Frameworks that prove properties of the code that ships: functional correctness against a specification, memory safety, and constant-time behaviour, for C, Rust, assembly and generated field arithmetic. This is where post-quantum verification happens in practice: ML-KEM and ML-DSA implementations in libjade, libcrux, AWS-LC, mlkem-native and Apple corecrypto all carry machine-checked proofs from tools in this category.

Jasmin and libjade: Formosa Crypto — ML-KEM (incl. AVX2), ML-DSA, X-Wing, Keccak / SHA-3, X25519, x86-64 assembly — Verified compiler from a low-level language to assembly; correctness proved in EasyCrypt; constant-time checked — Active (Jasmin 2026.03.2 released July 2026)
hax: Cryspen — Rust, libcrux ML-KEM and ML-DSA, Protocol models (ProVerif) — Translation of a large Rust subset into proof assistants; properties proved on the extracted model — Active; Lean backend under development with EF funding
Cryptol and SAW: Galois — C / LLVM, Java, x86-64, AWS-LC and s2n, BLST, Soroban (Formal Verso) — Executable specifications in Cryptol; SAW proves implementations equivalent via SMT and symbolic simulation — Active (SAW 1.4, Cryptol 3.4 in 2025)
Fiat-Crypto: MIT PLV — Finite-field arithmetic, Curve25519, P-256, Custom primes — Correct-by-construction code generation from Rocq proofs — Active, mature; deployed in BoringSSL and Go
HACL*, Vale and EverCrypt: Project Everest (Inria Prosecco, Microsoft Research, CMU) — C and assembly primitives, Firefox NSS, Linux kernel, mbedTLS, WireGuard — Verified C extracted from F* (HACL*) and verified assembly (Vale), unified in EverCrypt — Maintained; post-quantum work moved to libcrux/hax
Aeneas: Inria (Son Ho) and AeneasVerif — Rust, Plonky3 and RISC Zero code (2026 pipeline paper) — Functional translation of Rust into pure models for Lean, F* or Rocq — Active
Kani: AWS — Rust, Rust standard library verification challenge, AWS Rust libraries — Bounded model checking (CBMC backend) for panics, memory safety and user assertions — Active
CBMC: Diffblue, AWS and community — C, mlkem-native, s2n — Bounded model checking for memory safety and assertions — Active, mature
CryptoLine: Academia Sinica (Bow-Yaw Wang) — Bignum and NTT assembly, OpenSSL, BoringSSL, wolfSSL, PQC NTTs — Algebraic and range reasoning on straight-line arithmetic code — Active research
Verus: CMU, Microsoft and community — Rust (systems and some cryptographic code) — Ghost specifications and SMT-discharged proofs in Rust itself — Active
How to choose: High-speed assembly for a primitive with a matching EasyCrypt proof: **Jasmin** and **libjade**. | Production Rust that must stay readable: **hax** (to F*, Rocq, Lean, ProVerif) or **Aeneas** (to Lean), with **Kani** for panic and memory-safety proofs on the rest. | Hand-optimised C or assembly against a reference: **Cryptol and SAW**, **CryptoLine** for bignum and NTT arithmetic, **CBMC** for memory safety. | Field arithmetic for a new curve or field: **Fiat-Crypto** generates it with a proof. | A whole verified library rather than a proof of your own code: HACL* / EverCrypt or **libcrux**.

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