Verified implementations
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.
A verified specification is not a verified deployment. Implementation-level tools connect the two, either by generating code from a proof (Fiat-Crypto, Jasmin), by proving hand-written code equivalent to a spec (Cryptol/SAW, CryptoLine, HACL*), or by extracting a model from production Rust into a prover (hax, Aeneas). Bounded model checkers (Kani, CBMC) sit at the cheaper end: they prove memory safety and absence of panics within loop bounds, with no specification needed.
Two lessons from 2026 shape how to read this category. Verified code has shipped at scale (Firefox, Linux, Go, BoringSSL, Signal, AWS). And verification has a boundary: the February 2026 Verification Theatre paper documented 13 vulnerabilities in verified libraries, four inside code covered by proofs, all caused by properties that were never specified. Ask every implementation-verification vendor to state the boundary.
Frameworks in this category
| Framework | Targets | Approach | Access | Status |
|---|---|---|---|---|
| Jasmin and libjadeFormosa 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 | Open source | Active (Jasmin 2026.03.2 released July 2026) |
| haxCryspen | 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 | Open source | Active; Lean backend under development with EF funding |
| Cryptol and SAWGalois | 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 | Open source (BSD-3) | Active (SAW 1.4, Cryptol 3.4 in 2025) |
| Fiat-CryptoMIT PLV | Finite-field arithmetic · Curve25519 · P-256 · Custom primes | Correct-by-construction code generation from Rocq proofs | Open source | Active, mature; deployed in BoringSSL and Go |
| HACL*, Vale and EverCryptProject 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 | Open source | Maintained; post-quantum work moved to libcrux/hax |
| AeneasInria (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 | Open source | Active |
| KaniAWS | Rust · Rust standard library verification challenge · AWS Rust libraries | Bounded model checking (CBMC backend) for panics, memory safety and user assertions | Open source (Apache-2.0 / MIT) | Active |
| CBMCDiffblue, AWS and community | C · mlkem-native · s2n | Bounded model checking for memory safety and assertions | Open source (BSD-4) | Active, mature |
| CryptoLineAcademia Sinica (Bow-Yaw Wang) | Bignum and NTT assembly · OpenSSL · BoringSSL · wolfSSL · PQC NTTs | Algebraic and range reasoning on straight-line arithmetic code | Open source | Active research |
| VerusCMU, Microsoft and community | Rust (systems and some cryptographic code) | Ghost specifications and SMT-discharged proofs in Rust itself | Open source (MIT) | 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.
Firms that do this work
zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile Website ↗
Other categories
ZK circuit verification, Proof systems and computational proofs, Symbolic protocol analysis, Proof assistants and general verifiers, Challenges and programs