Verified implementations
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 libjade Formosa Crypto | ML-KEM (incl. AVX2)ML-DSAX-WingKeccak / SHA-3X25519x86-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) |
| hax Cryspen | Rustlibcrux ML-KEM and ML-DSAProtocol 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 SAW Galois | C / LLVMJavax86-64AWS-LC and s2nBLSTSoroban (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-Crypto MIT PLV | Finite-field arithmeticCurve25519P-256Custom primes | Correct-by-construction code generation from Rocq proofs | Open source | Active, mature; deployed in BoringSSL and Go |
| HACL*, Vale and EverCrypt Project Everest (Inria Prosecco, Microsoft Research, CMU) | C and assembly primitivesFirefox NSSLinux kernelmbedTLSWireGuard | Verified C extracted from F* (HACL*) and verified assembly (Vale), unified in EverCrypt | Open source | Maintained; post-quantum work moved to libcrux/hax |
| Aeneas Inria (Son Ho) and AeneasVerif | RustPlonky3 and RISC Zero code (2026 pipeline paper) | Functional translation of Rust into pure models for Lean, F* or Rocq | Open source | Active |
| Kani AWS | RustRust standard library verification challengeAWS Rust libraries | Bounded model checking (CBMC backend) for panics, memory safety and user assertions | Open source (Apache-2.0 / MIT) | Active |
| CBMC Diffblue, AWS and community | Cmlkem-natives2n | Bounded model checking for memory safety and assertions | Open source (BSD-4) | Active, mature |
| CryptoLine Academia Sinica (Bow-Yaw Wang) | Bignum and NTT assemblyOpenSSLBoringSSLwolfSSLPQC NTTs | Algebraic and range reasoning on straight-line arithmetic code | Open source | Active research |
| Verus CMU, 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