All frameworks, by category
Direct answerEvery 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 |
|---|---|---|---|---|
| Clean zkSecurity (hosted under Verified-zkEVM) | AIRPLONKR1CSzkVM chipsPlonky3-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-lean Succinct, with Nethermind | SP1 HypercubeRISC-V (RV64) chipsAIR | Lean 4 on Clean; chip constraints proved sound against the Sail RISC-V model | Open source (MIT / Apache-2.0) | Active |
| zkLean Galois | R1CSLookupsMLE lookupsRAM (Jolt-style) | Lean 4, Hoare-triple style via Std.Do; soundness of extracted circuits | Open source (BSD-3) | Active, Ethereum Foundation funded |
| Halva Nethermind | Halo2PLONKish | Extract gates, copy, permutation and lookup constraints at synthesis time; soundness proofs in Lean 4 | Open source | Active, Ethereum Foundation grant |
| Picus Veridise | CircomR1CSgnarkHalo2 (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 |
| LLZK Veridise (Ethereum Foundation grant) | CircomHalo2Plonky3Noir (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 |
| Garden Formal Land | CircomPlonky3LLZK | Rocq (Coq) proofs of determinism, functional correctness and completeness | Open source | Active |
| Lampe Reilabs | NoirACIR | Semantics-first extraction of Noir programs into Lean 4, then property proofs | Open source | Active |
| proven-zk and gnark-lean-extractor Reilabs | gnarkR1CS | Extract gnark circuits to Lean 4; prove properties with the proven-zk library | Open source | Maintained |
| CIVER COSTA 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 |
| Circomspect Trail of Bits | Circom | Static analysis of Circom source for unconstrained signals and unsafe patterns; SARIF output | Open source (GPL-3.0) | Maintained |
| zkFuzz Hideaki Takahashi (Koukyosyumei) | Circom | Fuzzing for trace-constraint consistency (TCCT) violations between witness generation and constraints | Open source | Active research (IEEE S&P 2026) |
| Coda Junrui 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 |
| Ecne Franklyn Wang (0xPARC) | R1CS | Rule-based propagation to prove output uniqueness of R1CS constraint sets | Open source (GPL-3.0) | Low activity research tool |
| NAVe Pedro Antonino, Namrata Jain | NoirACIR | 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 AIRStoneS-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 |
|---|---|---|---|---|
| ArkLib Verified-zkEVM (Quang Dao et al., Ethereum Foundation) | Interactive oracle reductionsSum-checkPolynomial commitmentsFRI / STIR / WHIRFiat-ShamirBCS | Lean 4 with VCV-io for probabilistic reasoning; completeness and soundness of proof-system components | Open source | Active; Nethermind maintains an ArkLibFri fork |
| EasyCrypt 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 | Interactive prover for game-based, code-based security proofs over probabilistic programs; paired with Jasmin for verified implementations | Open source | Active, mature |
| CryptoVerif Bruno Blanchet, Inria (Prosecco) | Protocols: TLS 1.3, Signal, WireGuardKey exchangeAuthenticated encryption compositions | Automatic and guided sequences of games with concrete security bounds | Open source | Active, mature |
| SSProve Aarhus 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 |
| ProofFrog Ross 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) |
| Squirrel Inria (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 |
|---|---|---|---|---|
| Tamarin ETH Zürich, CISPA, University of Oxford | TLS 1.35G AKAWPA2NoiseEMVMessaging protocols | Symbolic (Dolev-Yao) analysis over unbounded sessions with user-guided lemmas | Open source | Active, mature |
| ProVerif Bruno Blanchet, Inria (Prosecco) | Protocolshax models extracted from Rust | Symbolic analysis of applied pi-calculus models, unbounded sessions, largely automatic | Open source | Active, mature |
| Verifpal Symbolic 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 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 |
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 Mathlib Lean FRO and the Mathlib community | CleanzkLeanHalvaArkLibsp1-leanLampeEvmYulCairo 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-CryptoSSProveGardenrocq-of-rustrocq-of-solidity | Interactive theorem prover based on the calculus of inductive constructions | Open source (LGPL) | Active |
| Isabelle/HOL TU München and University of Cambridge | C and ARM64 via AutoCorres2Apple 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) | R1CSPrime-field constraint systemsacl2-jolt | First-order logic with strong automation; R1CS and PFCS libraries; acl2-jolt for Jolt circuits | Open source (BSD) | Mature, niche |
| K framework and KEVM Runtime Verification | EVM (KEVM)zkevm-harnessLean backend for K | Rewriting-based semantics from which interpreters, symbolic executors and provers are derived | Open source | Active, mature |
| Certora Prover Certora | SolidityVyperSolana (Rust)MoveSoroban | 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.golf zkSecurity | R1CS over BN254GF(2) hash compression trackClean 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.codes Ethereum Foundation Formal Verification team, Yukon and zkSecurity | koalaIRS12 proximity problemFRI / STIR / WHIR soundnessLean 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 program Ethereum Foundation | CleanzkLeanHalvaArkLibLLZKSail RISC-V LeanKEVM equivalencehax 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 |