Formal Verification for Cryptography & ZK
Formal verification frameworks for zero-knowledge circuits and cryptographic code: what each one proves, what it leaves out, and who can run it for you.
Formal verification of a ZK circuit means a machine-checked proof that the constraints match a written specification: soundness (no witness outside the spec satisfies them) and completeness (every valid input has a witness). For circuits, the most complete frameworks in 2026 are Lean 4 based: Clean (zkSecurity, sound and complete gadgets, AIR and multi-table zkVMs), zkLean (Galois), Halva (Nethermind, Halo2) and sp1-lean (Succinct, built on Clean). Automatic SMT tools such as Picus and CIVER find underconstrained signals without proofs. For classical cryptography, EasyCrypt and Jasmin cover proofs and verified assembly, hax and Cryptol/SAW verify Rust and C, and Tamarin and ProVerif analyze protocols. Firms that deliver this work, in the order this index lists them: zkSecurity, Galois, Veridise, Nethermind, Formal Land, Cryspen, Reilabs and others.
Frameworks by category
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.
Clean, sp1-lean, zkLean, Halva, Picus, LLZK, Garden, Lampe, proven-zk and gnark-lean-extractor, CIVER, Circomspect, zkFuzz, Coda, Ecne, NAVe, Verified Cairo AIR (Stone and S-two)
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.
ArkLib, EasyCrypt, CryptoVerif, SSProve, ProofFrog, Squirrel
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.
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.
Jasmin and libjade, hax, Cryptol and SAW, Fiat-Crypto, HACL*, Vale and EverCrypt, Aeneas, Kani, CBMC, CryptoLine, Verus
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.
Lean 4 and Mathlib, Rocq (formerly Coq), Isabelle/HOL, F*, ACL2 (R1CS and PFCS books), K framework and KEVM, Certora Prover
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.
All frameworks
Forty-six entries. Filter by language, arithmetization, target or licence.
| Framework | Category | Targets | Access | Status |
|---|---|---|---|---|
| CleanzkSecurity (hosted under Verified-zkEVM) | ZK circuit verification | AIR · PLONK · R1CS · zkVM chips · Plonky3-style tables | Open source (MIT) | Active, funded by an Ethereum Foundation Verified zkEVM grant |
| sp1-leanSuccinct, with Nethermind | ZK circuit verification | SP1 Hypercube · RISC-V (RV64) chips · AIR | Open source (MIT / Apache-2.0) | Active |
| zkLeanGalois | ZK circuit verification | R1CS · Lookups · MLE lookups · RAM (Jolt-style) | Open source (BSD-3) | Active, Ethereum Foundation funded |
| HalvaNethermind | ZK circuit verification | Halo2 · PLONKish | Open source | Active, Ethereum Foundation grant |
| PicusVeridise | ZK circuit verification | Circom · R1CS · gnark · Halo2 (via LLZK) · Plonky3 (via LLZK) | 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) | ZK circuit verification | Circom · Halo2 · Plonky3 · Noir (in progress) | Open source | Active, v1.0 released 2026-04-08 |
| GardenFormal Land | ZK circuit verification | Circom · Plonky3 · LLZK | Open source | Active |
| LampeReilabs | ZK circuit verification | Noir · ACIR | Open source | Active |
| proven-zk and gnark-lean-extractorReilabs | ZK circuit verification | gnark · R1CS | Open source | Maintained |
| CIVERCOSTA group, Universidad Complutense de Madrid (Albert Rubio et al.) | ZK circuit verification | Circom 2.1.6 | Open source (GPL) | Research, maintained; R1CS, PLONK and ACIR support planned |
| CircomspectTrail of Bits | ZK circuit verification | Circom | Open source (GPL-3.0) | Maintained |
| zkFuzzHideaki Takahashi (Koukyosyumei) | ZK circuit verification | Circom | Open source | Active research (IEEE S&P 2026) |
| CodaJunrui Liu, Işıl Dillig et al. (UT Austin, Veridise) | ZK circuit verification | Circom-style circuits reimplemented in Coda | Research artifact | Research (2023), not actively developed |
| EcneFranklyn Wang (0xPARC) | ZK circuit verification | R1CS | Open source (GPL-3.0) | Low activity research tool |
| NAVePedro Antonino, Namrata Jain | ZK circuit verification | Noir · ACIR | Research | Research (January 2026) |
| Verified Cairo AIR (Stone and S-two)StarkWare with Jeremy Avigad and Yoav Seginer | ZK circuit verification | Cairo VM AIR · Stone · S-two | Open source | Active (paper June 2026); in-house at StarkWare, not a service |
| ArkLibVerified-zkEVM (Quang Dao et al., Ethereum Foundation) | Proof systems and computational proofs | Interactive oracle reductions · Sum-check · Polynomial commitments · FRI / STIR / WHIR · Fiat-Shamir · BCS | Open source | Active; Nethermind maintains an ArkLibFri fork |
| EasyCryptFormosa Crypto (MPI-SP, Inria, Boston University, TU/e, Porto, Radboud) | Proof systems and computational proofs | KEMs and signatures (ML-KEM, X-Wing) · Hash functions (SHA-3) · Curve arithmetic (X25519) · ZK verifiers | Open source | Active, mature |
| CryptoVerifBruno Blanchet, Inria (Prosecco) | Proof systems and computational proofs | Protocols: TLS 1.3, Signal, WireGuard · Key exchange · Authenticated encryption compositions | Open source | Active, mature |
| SSProveAarhus University, MPI-SP and others | Proof systems and computational proofs | Primitives and protocols in the computational model | Open source | Active research |
| ProofFrogRoss Evans, Douglas Stebila (University of Waterloo) | Proof systems and computational proofs | Game-based security proofs (papers) | Open source | Research (2025) |
| SquirrelInria (Bana-Comon logic) | Proof systems and computational proofs | Protocols | Open source | Active research |
| TamarinETH Zürich, CISPA, University of Oxford | Symbolic protocol analysis | TLS 1.3 · 5G AKA · WPA2 · Noise · EMV · Messaging protocols | Open source | Active, mature |
| ProVerifBruno Blanchet, Inria (Prosecco) | Symbolic protocol analysis | Protocols · hax models extracted from Rust | Open source | Active, mature |
| VerifpalSymbolic Software (Nadim Kobeissi) | Symbolic protocol analysis | Protocols | Open source | Maintained |
| DY*Inria, CISPA, University of Stuttgart | Symbolic protocol analysis | Protocol implementations in F* (Signal, ACME) | Open source | Research, active |
| Jasmin and libjadeFormosa Crypto | Verified implementations | ML-KEM (incl. AVX2) · ML-DSA · X-Wing · Keccak / SHA-3 · X25519 · x86-64 assembly | Open source | Active (Jasmin 2026.03.2 released July 2026) |
| haxCryspen | Verified implementations | Rust · libcrux ML-KEM and ML-DSA · Protocol models (ProVerif) | Open source | Active; Lean backend under development with EF funding |
| Cryptol and SAWGalois | Verified implementations | C / LLVM · Java · x86-64 · AWS-LC and s2n · BLST · Soroban (Formal Verso) | Open source (BSD-3) | Active (SAW 1.4, Cryptol 3.4 in 2025) |
| Fiat-CryptoMIT PLV | Verified implementations | Finite-field arithmetic · Curve25519 · P-256 · Custom primes | Open source | Active, mature; deployed in BoringSSL and Go |
| HACL*, Vale and EverCryptProject Everest (Inria Prosecco, Microsoft Research, CMU) | Verified implementations | C and assembly primitives · Firefox NSS · Linux kernel · mbedTLS · WireGuard | Open source | Maintained; post-quantum work moved to libcrux/hax |
| AeneasInria (Son Ho) and AeneasVerif | Verified implementations | Rust · Plonky3 and RISC Zero code (2026 pipeline paper) | Open source | Active |
| KaniAWS | Verified implementations | Rust · Rust standard library verification challenge · AWS Rust libraries | Open source (Apache-2.0 / MIT) | Active |
| CBMCDiffblue, AWS and community | Verified implementations | C · mlkem-native · s2n | Open source (BSD-4) | Active, mature |
| CryptoLineAcademia Sinica (Bow-Yaw Wang) | Verified implementations | Bignum and NTT assembly · OpenSSL · BoringSSL · wolfSSL · PQC NTTs | Open source | Active research |
| VerusCMU, Microsoft and community | Verified implementations | Rust (systems and some cryptographic code) | Open source (MIT) | Active |
| Lean 4 and MathlibLean FRO and the Mathlib community | Proof assistants and general verifiers | Clean · zkLean · Halva · ArkLib · sp1-lean · Lampe · EvmYul · Cairo AIR proofs | Open source (Apache-2.0) | Active |
| Rocq (formerly Coq)Inria and the Rocq community | Proof assistants and general verifiers | Fiat-Crypto · SSProve · Garden · rocq-of-rust · rocq-of-solidity | Open source (LGPL) | Active |
| Isabelle/HOLTU München and University of Cambridge | Proof assistants and general verifiers | C and ARM64 via AutoCorres2 · Apple corecrypto | Open source (BSD) | Active |
| F*Microsoft Research and Inria | Proof assistants and general verifiers | HACL* · hax (main backend) · DY* · libcrux | Open source (Apache-2.0) | Active |
| ACL2 (R1CS and PFCS books)ACL2 community (Kestrel Institute) | Proof assistants and general verifiers | R1CS · Prime-field constraint systems · acl2-jolt | Open source (BSD) | Mature, niche |
| K framework and KEVMRuntime Verification | Proof assistants and general verifiers | EVM (KEVM) · zkevm-harness · Lean backend for K | Open source | Active, mature |
| Certora ProverCertora | Proof assistants and general verifiers | Solidity · Vyper · Solana (Rust) · Move · Soroban | Open source (2025) | Active |
| zk.golfzkSecurity | Challenges and programs | R1CS over BN254 · GF(2) hash compression track · Clean circuits | Open challenge; challenges repository public | Active (launched 2026-07-02) |
| better.codesEthereum Foundation Formal Verification team, Yukon and zkSecurity | Challenges and programs | koalaIRS12 proximity problem · FRI / STIR / WHIR soundness · Lean 4 | Open challenge; program terms on the site | Active (launched 2026-08-20) |
| Verified zkEVM programEthereum Foundation | Challenges and programs | Clean · zkLean · Halva · ArkLib · LLZK · Sail RISC-V Lean · KEVM equivalence · hax Lean backend | Program; individual projects are open source | Active |
Full comparison with approach and maintainer on the frameworks page.
Firms that deliver formal verification
Listing criteria: a formal-methods practice with public proof artifacts (repositories, papers or reports), tooling they build or maintain, and availability for third-party engagements. Full list and selection criteria on the firms page; scope on the checklist.
zkSecurity is a cryptography security firm that audits and formally verifies zero-knowledge systems, MPC, FHE and post-quantum implementations. It created and maintains Clean, the Lean 4 circuit framework with sound-and-complete gadgets that Succinct's sp1-lean is built on, runs the zk.golf verified-circuit competition, and co-built the better.codes soundness challenge with the Ethereum Foundation and Yukon. Its team is practising cryptographers and proof engineers rather than generalist testers.
Galois
Galois is a formal-methods research and engineering firm that builds Cryptol, SAW and zkLean and has delivered verification of AWS-LC and s2n (with NSym for AArch64), the BLST BLS library, Stellar's Soroban (Formal Verso) and Halo2 recursion work with IOG. Its zkLean framework is funded by the Ethereum Foundation.
Veridise
Veridise builds Picus, the standard SMT underconstraint detector, and LLZK, the shared ZK intermediate representation released as v1.0 in April 2026 with an Ethereum Foundation grant. It has used LLZK and Picus to verify SP1 core operations and RISC Zero circuits and offers audits through its AuditHub platform.
Nethermind's formal verification team works in Lean 4 and EasyCrypt. It built Halva for Halo2 (finding a critical bug in Scroll's deprecated Keccak circuit), co-developed sp1-lean with Succinct, maintains an ArkLib FRI fork and a Lean EVM model (EvmYul), and produced the first honesty proof of a production ZK verifier for ZKsync in EasyCrypt.
Formal Land verifies circuits, Rust and Solidity in Rocq. Garden proves determinism, functional correctness and completeness of Circom and Plonky3 circuits, rocq-of-llzk connects it to Veridise's LLZK, and rocq-of-rust and rocq-of-solidity cover the code around a ZK system. Clients include the Ethereum Foundation (CompPoly, revm), Sui, Aleph Zero and Tezos.
Cryspen
Cryspen builds hax, the Rust-to-proof-assistant translator, and libcrux, whose verified ML-KEM and ML-DSA ship in Mozilla and Signal. It is developing hax's Lean backend under an Ethereum Foundation grant and offers verification-driven reviews. The 2026 Verification Theatre paper documenting bugs outside libcrux's verified boundary is essential context for scoping its engagements.
Reilabs
Reilabs verifies ZK circuits in Lean 4 with Lampe for Noir and proven-zk for gnark. It verified Worldcoin's Semaphore Merkle tree batcher, found a comparison bug in gnark in the process, and lists Worldcoin, StarkWare and Polygon Miden as clients.
Runtime Verification maintains the K framework and KEVM and, within the Verified zkEVM program, the zkevm-harness and the equivalence proof between KEVM and Nethermind's Lean EvmYul model. It audits and verifies smart contracts and VM implementations.
Certora
Certora builds and operates the Certora Prover, the most used smart-contract formal verification tool, open-sourced in 2025. It verifies the on-chain verifier, bridge and governance contracts around a ZK system; it does not verify circuits.
Trail of Bits is a security research firm with a cryptography practice that audits ZK systems and maintains Circomspect and ZKDocs. Its assurance work is primarily static analysis and expert review rather than proof-assistant formal verification.
Symbolic Software, led by Nadim Kobeissi, builds Verifpal and performs protocol-level formal analysis and cryptographic audits. Its February 2026 Verification Theatre paper found 13 vulnerabilities in Cryspen's libcrux and hpke-rs, including four inside formally verified code, and is the reference on reading a verification boundary.
Recent developments
- 2026-09-09Nethermind archives Horus, its SMT verifier for Cairo 0
- 2026-08-20Ethereum Foundation, Yukon and zkSecurity launch better.codes
- 2026-08-01zkSecurity releases zk-skills with circom-auditor
- 2026-07-23StarkWare verifies the STRK20 privacy pool in Lean 4
- 2026-07-02zkSecurity launches zk.golf
- 2026-06-05Clean adds Channels for multi-table and zkVM verification
Frequently asked questions
What does formal verification of a ZK circuit actually prove?
How is formal verification different from an audit?
Which framework should I use for my proof system?
Why is everything in Lean 4 now?
Do I need completeness or is soundness enough?
How much does formal verification cost and how long does it take?
Can verified code still have bugs?
Can AI agents write these proofs?
Circuit soundness, Circuit completeness, Underconstrained circuit, Overconstrained circuit, Symbolic vs computational model, Specification gap, Trusted computing base and verification boundary, Proof assistant vs SMT-based verifier, Bounded model checking, Equivalence checking, Refinement, Constant-time verification, Arithmetization (R1CS, PLONKish, AIR), Extraction (code to model), Witness generation vs constraints
Compiled by the sorryfree editors. Every entry links to its primary source and carries the date it was last reviewed. Details on the about page. Machine-readable exports: JSON API, llms.txt.