All frameworks, by category
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.
ZK circuit verification
Frameworks that prove or check that a zero-knowledge circuit (R1CS, PLONKish, AIR, Circom, Noir, Halo2, Cairo) does what its specification says. Proof-assistant frameworks (Clean, zkLean, Halva, sp1-lean, Garden, Lampe) produce machine-checked soundness and sometimes completeness theorems; SMT and static tools (Picus, CIVER, Circomspect, zkFuzz) find underconstrained signals automatically but do not prove absence of bugs. Category guide →
| Framework | Targets | Approach | Access | Status |
|---|---|---|---|---|
| CleanzkSecurity (hosted under Verified-zkEVM) | AIR · PLONK · R1CS · zkVM chips · Plonky3-style tables | Embedded Lean 4 DSL; proof assistant; soundness and completeness theorems per gadget, composed without re-proving | Open source (MIT) | Active, funded by an Ethereum Foundation Verified zkEVM grant |
| sp1-leanSuccinct, with Nethermind | SP1 Hypercube · RISC-V (RV64) chips · AIR | Lean 4 on Clean; chip constraints proved sound against the Sail RISC-V model | Open source (MIT / Apache-2.0) | Active |
| zkLeanGalois | R1CS · Lookups · MLE lookups · RAM (Jolt-style) | Lean 4, Hoare-triple style via Std.Do; soundness of extracted circuits | Open source (BSD-3) | Active, Ethereum Foundation funded |
| HalvaNethermind | Halo2 · PLONKish | Extract gates, copy, permutation and lookup constraints at synthesis time; soundness proofs in Lean 4 | Open source | Active, Ethereum Foundation grant |
| PicusVeridise | Circom · R1CS · gnark · Halo2 (via LLZK) · Plonky3 (via LLZK) | SMT (cvc5, Z3 with finite-field theory) uniqueness checking; fully automatic, no proofs to write | Open source (MIT); newer versions ship in Veridise AuditHub | Maintained; the Circom version is documented as legacy, LLZK-based Picus is current |
| LLZKVeridise (Ethereum Foundation grant) | Circom · Halo2 · Plonky3 · Noir (in progress) | Shared MLIR dialect; lowers to Picus, zkLean, R1CS and Rocq (via Formal Land's rocq-of-llzk) | Open source | Active, v1.0 released 2026-04-08 |
| GardenFormal Land | Circom · Plonky3 · LLZK | Rocq (Coq) proofs of determinism, functional correctness and completeness | Open source | Active |
| LampeReilabs | Noir · ACIR | Semantics-first extraction of Noir programs into Lean 4, then property proofs | Open source | Active |
| proven-zk and gnark-lean-extractorReilabs | gnark · R1CS | Extract gnark circuits to Lean 4; prove properties with the proven-zk library | Open source | Maintained |
| CIVERCOSTA group, Universidad Complutense de Madrid (Albert Rubio et al.) | Circom 2.1.6 | Z3-backed weak safety (determinism), tag specifications, pre- and post-conditions, verified bottom-up per template | Open source (GPL) | Research, maintained; R1CS, PLONK and ACIR support planned |
| CircomspectTrail of Bits | Circom | Static analysis of Circom source for unconstrained signals and unsafe patterns; SARIF output | Open source (GPL-3.0) | Maintained |
| zkFuzzHideaki Takahashi (Koukyosyumei) | Circom | Fuzzing for trace-constraint consistency (TCCT) violations between witness generation and constraints | Open source | Active research (IEEE S&P 2026) |
| CodaJunrui Liu, Işıl Dillig et al. (UT Austin, Veridise) | Circom-style circuits reimplemented in Coda | Refinement-typed circuit language generating Coq proof obligations | Research artifact | Research (2023), not actively developed |
| EcneFranklyn Wang (0xPARC) | R1CS | Rule-based propagation to prove output uniqueness of R1CS constraint sets | Open source (GPL-3.0) | Low activity research tool |
| NAVePedro Antonino, Namrata Jain | Noir · ACIR | cvc5 with finite-field SMT-LIB theories | Research | Research (January 2026) |
| Verified Cairo AIR (Stone and S-two)StarkWare with Jeremy Avigad and Yoav Seginer | Cairo VM AIR · Stone · S-two | Lean 4 proofs that AIR satisfiability implies a correct Cairo execution; Sierra-to-CASM building blocks | Open source | Active (paper June 2026); in-house at StarkWare, not a service |
Proof systems and computational proofs
Frameworks for machine-checking the cryptographic argument itself: knowledge soundness of a polynomial IOP, the security reduction of a KEM, or the game-hopping proof in a paper. These work in the computational model, where the adversary is a probabilistic polynomial-time algorithm and security is a concrete bound, and they are the only tools on this index that verify the proof system rather than the circuit inside it. Category guide →
| Framework | Targets | Approach | Access | Status |
|---|---|---|---|---|
| ArkLibVerified-zkEVM (Quang Dao et al., Ethereum Foundation) | Interactive oracle reductions · Sum-check · Polynomial commitments · FRI / STIR / WHIR · Fiat-Shamir · BCS | Lean 4 with VCV-io for probabilistic reasoning; completeness and soundness of proof-system components | Open source | Active; Nethermind maintains an ArkLibFri fork |
| EasyCryptFormosa 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 | Interactive prover for game-based, code-based security proofs over probabilistic programs; paired with Jasmin for verified implementations | Open source | Active, mature |
| CryptoVerifBruno Blanchet, Inria (Prosecco) | Protocols: TLS 1.3, Signal, WireGuard · Key exchange · Authenticated encryption compositions | Automatic and guided sequences of games with concrete security bounds | Open source | Active, mature |
| SSProveAarhus University, MPI-SP and others | Primitives and protocols in the computational model | Rocq framework for state-separating proofs; hax backend available | Open source | Active research |
| ProofFrogRoss Evans, Douglas Stebila (University of Waterloo) | Game-based security proofs (papers) | Custom language (FrogLang) and checker for game transitions; MCP server for AI assistants | Open source | Research (2025) |
| SquirrelInria (Bana-Comon logic) | Protocols | Interactive prover in the computationally complete symbolic attacker model | Open source | Active research |
Symbolic protocol analysis
Automatic analyzers that model a protocol with perfect (Dolev-Yao) cryptography and search for attacks over unbounded sessions: authentication failures, key-compromise impersonation, downgrade, replay and unknown-key-share. Tamarin and ProVerif are the standard tools; Verifpal trades expressiveness for approachability; DY* embeds the analysis in F* for executable code. Category guide →
| Framework | Targets | Approach | Access | Status |
|---|---|---|---|---|
| TamarinETH Zürich, CISPA, University of Oxford | TLS 1.3 · 5G AKA · WPA2 · Noise · EMV · Messaging protocols | Symbolic (Dolev-Yao) analysis over unbounded sessions with user-guided lemmas | Open source | Active, mature |
| ProVerifBruno Blanchet, Inria (Prosecco) | Protocols · hax models extracted from Rust | Symbolic analysis of applied pi-calculus models, unbounded sessions, largely automatic | Open source | Active, mature |
| VerifpalSymbolic Software (Nadim Kobeissi) | Protocols | Symbolic analysis with an intentionally simple modelling language | Open source | Maintained |
| DY*Inria, CISPA, University of Stuttgart | Protocol implementations in F* (Signal, ACME) | Dolev-Yao reasoning inside the F* proof assistant, over executable protocol code | Open source | Research, active |
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. Category guide →
| 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 |
Proof assistants and general verifiers
The foundations underneath the specialised frameworks: interactive proof assistants (Lean 4, Rocq, Isabelle/HOL, F*, ACL2), a semantics framework (K), and SMT-based verifiers for smart contracts (Certora Prover, Halmos, hevm). Choosing one fixes the ecosystem, the available libraries, the hiring pool and, increasingly, which AI proving tools can help. Category guide →
| Framework | Targets | Approach | Access | Status |
|---|---|---|---|---|
| Lean 4 and MathlibLean FRO and the Mathlib community | Clean · zkLean · Halva · ArkLib · sp1-lean · Lampe · EvmYul · Cairo AIR proofs | Interactive theorem prover with a small trusted kernel, a large mathematics library and a growing AI-prover ecosystem | Open source (Apache-2.0) | Active |
| Rocq (formerly Coq)Inria and the Rocq community | Fiat-Crypto · SSProve · Garden · rocq-of-rust · rocq-of-solidity | Interactive theorem prover based on the calculus of inductive constructions | Open source (LGPL) | Active |
| Isabelle/HOLTU München and University of Cambridge | C and ARM64 via AutoCorres2 · Apple corecrypto | Higher-order logic with strong automation; refinement via AutoCorres2 | Open source (BSD) | Active |
| F*Microsoft Research and Inria | HACL* · hax (main backend) · DY* · libcrux | Dependently typed effectful programming with SMT automation; extraction to C and OCaml | Open source (Apache-2.0) | Active |
| ACL2 (R1CS and PFCS books)ACL2 community (Kestrel Institute) | R1CS · Prime-field constraint systems · acl2-jolt | First-order logic with strong automation; R1CS and PFCS libraries; acl2-jolt for Jolt circuits | Open source (BSD) | Mature, niche |
| K framework and KEVMRuntime Verification | EVM (KEVM) · zkevm-harness · Lean backend for K | Rewriting-based semantics from which interpreters, symbolic executors and provers are derived | Open source | Active, mature |
| Certora ProverCertora | Solidity · Vyper · Solana (Rust) · Move · Soroban | Rule-based specification (CVL) discharged by SMT over bytecode | Open source (2025) | Active |
Challenges and programs
Live venues where verified artifacts are produced competitively or under a coordinated program: zk.golf (cheapest circuit with a Lean proof of soundness and completeness), better.codes (raise a Lean-checked soundness bound for Reed-Solomon proximity), and the Ethereum Foundation's Verified zkEVM program that funds most of the frameworks on this index. Category guide →
| Framework | Targets | Approach | Access | Status |
|---|---|---|---|---|
| zk.golfzkSecurity | R1CS over BN254 · GF(2) hash compression track · Clean circuits | Fixed Lean interface and specification per challenge; submissions are Clean circuits plus kernel-checked proofs; score = allocations + constraints | Open challenge; challenges repository public | Active (launched 2026-07-02) |
| better.codesEthereum Foundation Formal Verification team, Yukon and zkSecurity | koalaIRS12 proximity problem · FRI / STIR / WHIR soundness · Lean 4 | A formalised open problem from the Proximity Prize; solvers point AI agents at improving the machine-checked lower bound; every submission is kernel-checked and promoted proofs are credited | Open challenge; program terms on the site | Active (launched 2026-08-20) |
| Verified zkEVM programEthereum Foundation | Clean · zkLean · Halva · ArkLib · LLZK · Sail RISC-V Lean · KEVM equivalence · hax Lean backend | Grants and coordination for a formally verified, bug-free zk(E)VM stack, targeted for 2027 | Program; individual projects are open source | Active |