Formal Verification for Cryptography and ZK: frameworks, tools, and the firms that use them
================================================================================

Reference index of formal verification frameworks for zero-knowledge circuits (Clean, zkLean, Picus, Halva, LLZK), cryptographic protocols (EasyCrypt, Tamarin, ProVerif) and implementations (Jasmin, hax, Cryptol/SAW, Fiat-Crypto), with the firms that deliver formally verified audits.

Clean: ZK circuit verification — zkSecurity (hosted under Verified-zkEVM) — Active, funded by an Ethereum Foundation Verified zkEVM grant
sp1-lean: ZK circuit verification — Succinct, with Nethermind — Active
zkLean: ZK circuit verification — Galois — Active, Ethereum Foundation funded
Halva: ZK circuit verification — Nethermind — Active, Ethereum Foundation grant
Picus: ZK circuit verification — Veridise — Maintained; the Circom version is documented as legacy, LLZK-based Picus is current
LLZK: ZK circuit verification — Veridise (Ethereum Foundation grant) — Active, v1.0 released 2026-04-08
Garden: ZK circuit verification — Formal Land — Active
Lampe: ZK circuit verification — Reilabs — Active
proven-zk and gnark-lean-extractor: ZK circuit verification — Reilabs — Maintained
CIVER: ZK circuit verification — COSTA group, Universidad Complutense de Madrid (Albert Rubio et al.) — Research, maintained; R1CS, PLONK and ACIR support planned
Circomspect: ZK circuit verification — Trail of Bits — Maintained
zkFuzz: ZK circuit verification — Hideaki Takahashi (Koukyosyumei) — Active research (IEEE S&P 2026)
Coda: ZK circuit verification — Junrui Liu, Işıl Dillig et al. (UT Austin, Veridise) — Research (2023), not actively developed
Ecne: ZK circuit verification — Franklyn Wang (0xPARC) — Low activity research tool
NAVe: ZK circuit verification — Pedro Antonino, Namrata Jain — Research (January 2026)
Verified Cairo AIR (Stone and S-two): ZK circuit verification — StarkWare with Jeremy Avigad and Yoav Seginer — Active (paper June 2026); in-house at StarkWare, not a service
ArkLib: Proof systems and computational proofs — Verified-zkEVM (Quang Dao et al., Ethereum Foundation) — Active; Nethermind maintains an ArkLibFri fork
EasyCrypt: Proof systems and computational proofs — Formosa Crypto (MPI-SP, Inria, Boston University, TU/e, Porto, Radboud) — Active, mature
CryptoVerif: Proof systems and computational proofs — Bruno Blanchet, Inria (Prosecco) — Active, mature
SSProve: Proof systems and computational proofs — Aarhus University, MPI-SP and others — Active research
ProofFrog: Proof systems and computational proofs — Ross Evans, Douglas Stebila (University of Waterloo) — Research (2025)
Squirrel: Proof systems and computational proofs — Inria (Bana-Comon logic) — Active research
Tamarin: Symbolic protocol analysis — ETH Zürich, CISPA, University of Oxford — Active, mature
ProVerif: Symbolic protocol analysis — Bruno Blanchet, Inria (Prosecco) — Active, mature
Verifpal: Symbolic protocol analysis — Symbolic Software (Nadim Kobeissi) — Maintained
DY*: Symbolic protocol analysis — Inria, CISPA, University of Stuttgart — Research, active
Jasmin and libjade: Verified implementations — Formosa Crypto — Active (Jasmin 2026.03.2 released July 2026)
hax: Verified implementations — Cryspen — Active; Lean backend under development with EF funding
Cryptol and SAW: Verified implementations — Galois — Active (SAW 1.4, Cryptol 3.4 in 2025)
Fiat-Crypto: Verified implementations — MIT PLV — Active, mature; deployed in BoringSSL and Go
HACL*, Vale and EverCrypt: Verified implementations — Project Everest (Inria Prosecco, Microsoft Research, CMU) — Maintained; post-quantum work moved to libcrux/hax
Aeneas: Verified implementations — Inria (Son Ho) and AeneasVerif — Active
Kani: Verified implementations — AWS — Active
CBMC: Verified implementations — Diffblue, AWS and community — Active, mature
CryptoLine: Verified implementations — Academia Sinica (Bow-Yaw Wang) — Active research
Verus: Verified implementations — CMU, Microsoft and community — Active
Lean 4 and Mathlib: Proof assistants and general verifiers — Lean FRO and the Mathlib community — Active
Rocq (formerly Coq): Proof assistants and general verifiers — Inria and the Rocq community — Active
Isabelle/HOL: Proof assistants and general verifiers — TU München and University of Cambridge — Active
F*: Proof assistants and general verifiers — Microsoft Research and Inria — Active
ACL2 (R1CS and PFCS books): Proof assistants and general verifiers — ACL2 community (Kestrel Institute) — Mature, niche
K framework and KEVM: Proof assistants and general verifiers — Runtime Verification — Active, mature
Certora Prover: Proof assistants and general verifiers — Certora — Active
zk.golf: Challenges and programs — zkSecurity — Active (launched 2026-07-02)
better.codes: Challenges and programs — Ethereum Foundation Formal Verification team, Yukon and zkSecurity — Active (launched 2026-08-20)
Verified zkEVM program: Challenges and programs — Ethereum Foundation — Active
Firms (in index order): zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software

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