Proof assistants and general verifiers
In 2026 the ZK ecosystem has largely settled on Lean 4: Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, proven-zk, Nethermind's EVM model and StarkWare's Cairo proofs are all Lean. Rocq remains strong for implementation verification (Fiat-Crypto, Formal Land's rocq-of-rust and Garden, SSProve), Isabelle appears in Apple's corecrypto proofs, F* underpins HACL* and hax, and ACL2 has a mature but niche prime-field constraint library.
Smart-contract verifiers are listed here because ZK verifiers deploy on-chain. Certora Prover, Halmos and hevm check the Solidity or bytecode around a verifier contract; none of them verifies the circuit.
Frameworks in this category
| 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 |
How to choose
- New ZK verification project in 2026: Lean 4. The libraries, the funded projects and the AI provers are there.
- Rust implementation verification with a Rocq team, or reuse of Fiat-Crypto: Rocq.
- C and ARM64 code with a refinement-style methodology: Isabelle/HOL with AutoCorres2, as Apple did.
- Executable semantics that both runs and proves (EVM, zkVM ISAs): the K framework.
- On-chain verifier contract properties: Certora Prover for full rule-based verification, Halmos or hevm for bounded symbolic checks.
Firms that do this work
zkSecurity, Galois, Veridise, Nethermind (Formal Verification team), Formal Land, Cryspen, Reilabs, Runtime Verification, Certora, Trail of Bits, Symbolic Software
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Other categories
ZK circuit verification, Proof systems and computational proofs, Symbolic protocol analysis, Verified implementations, Challenges and programs