Formal verification frameworks for ZK circuits and cryptography, compared
=========================================================================

Every framework on this index in one place, grouped by what it verifies: ZK circuits, proof systems and computational proofs, symbolic protocol analysis, verified implementations, general proof assistants, and challenge platforms. Each row links to a page with the exact properties proved, the circuit or code model, the maintainer, and its limits.

Clean: ZK circuit verification — zkSecurity (hosted under Verified-zkEVM) — AIR, PLONK, R1CS, zkVM chips, Plonky3-style tables — Active, funded by an Ethereum Foundation Verified zkEVM grant
sp1-lean: ZK circuit verification — Succinct, with Nethermind — SP1 Hypercube, RISC-V (RV64) chips, AIR — Active
zkLean: ZK circuit verification — Galois — R1CS, Lookups, MLE lookups, RAM (Jolt-style) — Active, Ethereum Foundation funded
Halva: ZK circuit verification — Nethermind — Halo2, PLONKish — Active, Ethereum Foundation grant
Picus: ZK circuit verification — Veridise — Circom, R1CS, gnark, Halo2 (via LLZK), Plonky3 (via LLZK) — Maintained; the Circom version is documented as legacy, LLZK-based Picus is current
LLZK: ZK circuit verification — Veridise (Ethereum Foundation grant) — Circom, Halo2, Plonky3, Noir (in progress) — Active, v1.0 released 2026-04-08
Garden: ZK circuit verification — Formal Land — Circom, Plonky3, LLZK — Active
Lampe: ZK circuit verification — Reilabs — Noir, ACIR — Active
proven-zk and gnark-lean-extractor: ZK circuit verification — Reilabs — gnark, R1CS — Maintained
CIVER: ZK circuit verification — COSTA group, Universidad Complutense de Madrid (Albert Rubio et al.) — Circom 2.1.6 — Research, maintained; R1CS, PLONK and ACIR support planned
Circomspect: ZK circuit verification — Trail of Bits — Circom — Maintained
zkFuzz: ZK circuit verification — Hideaki Takahashi (Koukyosyumei) — Circom — Active research (IEEE S&P 2026)
Coda: ZK circuit verification — Junrui Liu, Işıl Dillig et al. (UT Austin, Veridise) — Circom-style circuits reimplemented in Coda — Research (2023), not actively developed
Ecne: ZK circuit verification — Franklyn Wang (0xPARC) — R1CS — Low activity research tool
NAVe: ZK circuit verification — Pedro Antonino, Namrata Jain — Noir, ACIR — Research (January 2026)
Verified Cairo AIR (Stone and S-two): ZK circuit verification — StarkWare with Jeremy Avigad and Yoav Seginer — Cairo VM AIR, Stone, S-two — 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) — Interactive oracle reductions, Sum-check, Polynomial commitments, FRI / STIR / WHIR, Fiat-Shamir, BCS — Active; Nethermind maintains an ArkLibFri fork
EasyCrypt: Proof systems and computational proofs — Formosa Crypto (MPI-SP, Inria, Boston University, TU/e, Porto, Radboud) — KEMs and signatures (ML-KEM, X-Wing), Hash functions (SHA-3), Curve arithmetic (X25519), ZK verifiers — Active, mature
CryptoVerif: Proof systems and computational proofs — Bruno Blanchet, Inria (Prosecco) — Protocols: TLS 1.3, Signal, WireGuard, Key exchange, Authenticated encryption compositions — Active, mature
SSProve: Proof systems and computational proofs — Aarhus University, MPI-SP and others — Primitives and protocols in the computational model — Active research
ProofFrog: Proof systems and computational proofs — Ross Evans, Douglas Stebila (University of Waterloo) — Game-based security proofs (papers) — Research (2025)
Squirrel: Proof systems and computational proofs — Inria (Bana-Comon logic) — Protocols — Active research
Tamarin: Symbolic protocol analysis — ETH Zürich, CISPA, University of Oxford — TLS 1.3, 5G AKA, WPA2, Noise, EMV, Messaging protocols — Active, mature
ProVerif: Symbolic protocol analysis — Bruno Blanchet, Inria (Prosecco) — Protocols, hax models extracted from Rust — Active, mature
Verifpal: Symbolic protocol analysis — Symbolic Software (Nadim Kobeissi) — Protocols — Maintained
DY*: Symbolic protocol analysis — Inria, CISPA, University of Stuttgart — Protocol implementations in F* (Signal, ACME) — Research, active
Jasmin and libjade: Verified implementations — Formosa Crypto — ML-KEM (incl. AVX2), ML-DSA, X-Wing, Keccak / SHA-3, X25519, x86-64 assembly — Active (Jasmin 2026.03.2 released July 2026)
hax: Verified implementations — Cryspen — Rust, libcrux ML-KEM and ML-DSA, Protocol models (ProVerif) — Active; Lean backend under development with EF funding
Cryptol and SAW: Verified implementations — Galois — C / LLVM, Java, x86-64, AWS-LC and s2n, BLST, Soroban (Formal Verso) — Active (SAW 1.4, Cryptol 3.4 in 2025)
Fiat-Crypto: Verified implementations — MIT PLV — Finite-field arithmetic, Curve25519, P-256, Custom primes — Active, mature; deployed in BoringSSL and Go
HACL*, Vale and EverCrypt: Verified implementations — Project Everest (Inria Prosecco, Microsoft Research, CMU) — C and assembly primitives, Firefox NSS, Linux kernel, mbedTLS, WireGuard — Maintained; post-quantum work moved to libcrux/hax
Aeneas: Verified implementations — Inria (Son Ho) and AeneasVerif — Rust, Plonky3 and RISC Zero code (2026 pipeline paper) — Active
Kani: Verified implementations — AWS — Rust, Rust standard library verification challenge, AWS Rust libraries — Active
CBMC: Verified implementations — Diffblue, AWS and community — C, mlkem-native, s2n — Active, mature
CryptoLine: Verified implementations — Academia Sinica (Bow-Yaw Wang) — Bignum and NTT assembly, OpenSSL, BoringSSL, wolfSSL, PQC NTTs — Active research
Verus: Verified implementations — CMU, Microsoft and community — Rust (systems and some cryptographic code) — Active
Lean 4 and Mathlib: Proof assistants and general verifiers — Lean FRO and the Mathlib community — Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, EvmYul, Cairo AIR proofs — Active
Rocq (formerly Coq): Proof assistants and general verifiers — Inria and the Rocq community — Fiat-Crypto, SSProve, Garden, rocq-of-rust, rocq-of-solidity — Active
Isabelle/HOL: Proof assistants and general verifiers — TU München and University of Cambridge — C and ARM64 via AutoCorres2, Apple corecrypto — Active
F*: Proof assistants and general verifiers — Microsoft Research and Inria — HACL*, hax (main backend), DY*, libcrux — Active
ACL2 (R1CS and PFCS books): Proof assistants and general verifiers — ACL2 community (Kestrel Institute) — R1CS, Prime-field constraint systems, acl2-jolt — Mature, niche
K framework and KEVM: Proof assistants and general verifiers — Runtime Verification — EVM (KEVM), zkevm-harness, Lean backend for K — Active, mature
Certora Prover: Proof assistants and general verifiers — Certora — Solidity, Vyper, Solana (Rust), Move, Soroban — Active
zk.golf: Challenges and programs — zkSecurity — R1CS over BN254, GF(2) hash compression track, Clean circuits — Active (launched 2026-07-02)
better.codes: Challenges and programs — Ethereum Foundation Formal Verification team, Yukon and zkSecurity — koalaIRS12 proximity problem, FRI / STIR / WHIR soundness, Lean 4 — Active (launched 2026-08-20)
Verified zkEVM program: Challenges and programs — Ethereum Foundation — Clean, zkLean, Halva, ArkLib, LLZK, Sail RISC-V Lean, KEVM equivalence, hax Lean backend — Active

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