Formal Verification for Cryptography & ZK

Name: sorryfree
Creator: sorryfree
License: https://creativecommons.org/licenses/by/4.0/

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.

Direct answerFormal 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.

46frameworks reviewed

6categories

11firms profiled

15glossary terms

2026-09-13last reviewed

Frameworks by category

ZK circuit verification

16 frameworks

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)

Proof systems and computational proofs

6 frameworks

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

Symbolic protocol analysis

4 frameworks

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.

Tamarin, ProVerif, Verifpal, DY*

Verified implementations

10 frameworks

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

Proof assistants and general verifiers

7 frameworks

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

Challenges and programs

3 frameworks

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.

zk.golf, better.codes, Verified zkEVM program

All frameworks

Framework	Category	Targets	Access	Status
Clean zkSecurity (hosted under Verified-zkEVM)	ZK circuit verification	AIRPLONKR1CSzkVM chipsPlonky3-style tables	Open source (MIT)	Active, funded by an Ethereum Foundation Verified zkEVM grant
sp1-lean Succinct, with Nethermind	ZK circuit verification	SP1 HypercubeRISC-V (RV64) chipsAIR	Open source (MIT / Apache-2.0)	Active
zkLean Galois	ZK circuit verification	R1CSLookupsMLE lookupsRAM (Jolt-style)	Open source (BSD-3)	Active, Ethereum Foundation funded
Halva Nethermind	ZK circuit verification	Halo2PLONKish	Open source	Active, Ethereum Foundation grant
Picus Veridise	ZK circuit verification	CircomR1CSgnarkHalo2 (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
LLZK Veridise (Ethereum Foundation grant)	ZK circuit verification	CircomHalo2Plonky3Noir (in progress)	Open source	Active, v1.0 released 2026-04-08
Garden Formal Land	ZK circuit verification	CircomPlonky3LLZK	Open source	Active
Lampe Reilabs	ZK circuit verification	NoirACIR	Open source	Active
proven-zk and gnark-lean-extractor Reilabs	ZK circuit verification	gnarkR1CS	Open source	Maintained
CIVER COSTA 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
Circomspect Trail of Bits	ZK circuit verification	Circom	Open source (GPL-3.0)	Maintained
zkFuzz Hideaki Takahashi (Koukyosyumei)	ZK circuit verification	Circom	Open source	Active research (IEEE S&P 2026)
Coda Junrui 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
Ecne Franklyn Wang (0xPARC)	ZK circuit verification	R1CS	Open source (GPL-3.0)	Low activity research tool
NAVe Pedro Antonino, Namrata Jain	ZK circuit verification	NoirACIR	Research	Research (January 2026)
Verified Cairo AIR (Stone and S-two) StarkWare with Jeremy Avigad and Yoav Seginer	ZK circuit verification	Cairo VM AIRStoneS-two	Open source	Active (paper June 2026); in-house at StarkWare, not a service
ArkLib Verified-zkEVM (Quang Dao et al., Ethereum Foundation)	Proof systems and computational proofs	Interactive oracle reductionsSum-checkPolynomial commitmentsFRI / STIR / WHIRFiat-ShamirBCS	Open source	Active; Nethermind maintains an ArkLibFri fork
EasyCrypt Formosa 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
CryptoVerif Bruno Blanchet, Inria (Prosecco)	Proof systems and computational proofs	Protocols: TLS 1.3, Signal, WireGuardKey exchangeAuthenticated encryption compositions	Open source	Active, mature
SSProve Aarhus University, MPI-SP and others	Proof systems and computational proofs	Primitives and protocols in the computational model	Open source	Active research
ProofFrog Ross Evans, Douglas Stebila (University of Waterloo)	Proof systems and computational proofs	Game-based security proofs (papers)	Open source	Research (2025)
Squirrel Inria (Bana-Comon logic)	Proof systems and computational proofs	Protocols	Open source	Active research
Tamarin ETH Zürich, CISPA, University of Oxford	Symbolic protocol analysis	TLS 1.35G AKAWPA2NoiseEMVMessaging protocols	Open source	Active, mature
ProVerif Bruno Blanchet, Inria (Prosecco)	Symbolic protocol analysis	Protocolshax models extracted from Rust	Open source	Active, mature
Verifpal Symbolic 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 libjade Formosa Crypto	Verified implementations	ML-KEM (incl. AVX2)ML-DSAX-WingKeccak / SHA-3X25519x86-64 assembly	Open source	Active (Jasmin 2026.03.2 released July 2026)
hax Cryspen	Verified implementations	Rustlibcrux ML-KEM and ML-DSAProtocol models (ProVerif)	Open source	Active; Lean backend under development with EF funding
Cryptol and SAW Galois	Verified implementations	C / LLVMJavax86-64AWS-LC and s2nBLSTSoroban (Formal Verso)	Open source (BSD-3)	Active (SAW 1.4, Cryptol 3.4 in 2025)
Fiat-Crypto MIT PLV	Verified implementations	Finite-field arithmeticCurve25519P-256Custom primes	Open source	Active, mature; deployed in BoringSSL and Go
HACL*, Vale and EverCrypt Project Everest (Inria Prosecco, Microsoft Research, CMU)	Verified implementations	C and assembly primitivesFirefox NSSLinux kernelmbedTLSWireGuard	Open source	Maintained; post-quantum work moved to libcrux/hax
Aeneas Inria (Son Ho) and AeneasVerif	Verified implementations	RustPlonky3 and RISC Zero code (2026 pipeline paper)	Open source	Active
Kani AWS	Verified implementations	RustRust standard library verification challengeAWS Rust libraries	Open source (Apache-2.0 / MIT)	Active
CBMC Diffblue, AWS and community	Verified implementations	Cmlkem-natives2n	Open source (BSD-4)	Active, mature
CryptoLine Academia Sinica (Bow-Yaw Wang)	Verified implementations	Bignum and NTT assemblyOpenSSLBoringSSLwolfSSLPQC NTTs	Open source	Active research
Verus CMU, Microsoft and community	Verified implementations	Rust (systems and some cryptographic code)	Open source (MIT)	Active
Lean 4 and Mathlib Lean FRO and the Mathlib community	Proof assistants and general verifiers	CleanzkLeanHalvaArkLibsp1-leanLampeEvmYulCairo AIR proofs	Open source (Apache-2.0)	Active
Rocq (formerly Coq) Inria and the Rocq community	Proof assistants and general verifiers	Fiat-CryptoSSProveGardenrocq-of-rustrocq-of-solidity	Open source (LGPL)	Active
Isabelle/HOL TU München and University of Cambridge	Proof assistants and general verifiers	C and ARM64 via AutoCorres2Apple corecrypto	Open source (BSD)	Active
F* Microsoft Research and Inria	Proof assistants and general verifiers	HACLhax (main backend)DYlibcrux	Open source (Apache-2.0)	Active
ACL2 (R1CS and PFCS books) ACL2 community (Kestrel Institute)	Proof assistants and general verifiers	R1CSPrime-field constraint systemsacl2-jolt	Open source (BSD)	Mature, niche
K framework and KEVM Runtime Verification	Proof assistants and general verifiers	EVM (KEVM)zkevm-harnessLean backend for K	Open source	Active, mature
Certora Prover Certora	Proof assistants and general verifiers	SolidityVyperSolana (Rust)MoveSoroban	Open source (2025)	Active
zk.golf zkSecurity	Challenges and programs	R1CS over BN254GF(2) hash compression trackClean circuits	Open challenge; challenges repository public	Active (launched 2026-07-02)
better.codes Ethereum Foundation Formal Verification team, Yukon and zkSecurity	Challenges and programs	koalaIRS12 proximity problemFRI / STIR / WHIR soundnessLean 4	Open challenge; program terms on the site	Active (launched 2026-08-20)
Verified zkEVM program Ethereum Foundation	Challenges and programs	CleanzkLeanHalvaArkLibLLZKSail RISC-V LeanKEVM equivalencehax 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.

#1zkSecurity

Remote-first (United States and Europe) · Formal verification and audits of zero-knowledge circuits, proof systems and cryptographic protocols; creator of Clean and zk.golf

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.

Profile · Website

#2Galois

Portland, Oregon, United States · Industrial formal verification: Cryptol, SAW, zkLean; verified AWS-LC, s2n, BLST, Soroban

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.

Profile · Website

#3Veridise

Austin, Texas, United States · Automated ZK verification: Picus, LLZK, ZKAP; AuditHub platform; verified SP1 and RISC Zero components

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.

Profile · Website

#4Nethermind (Formal Verification team)

London, United Kingdom · Lean and EasyCrypt verification: Halva (Halo2), Plonky3 circuits, SP1 chips, ZKsync verifier honesty proof

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.

Profile · Website

#5Formal Land

Paris, France · Rocq verification: Garden (circuits), rocq-of-rust, rocq-of-solidity, rocq-of-llzk

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.

Profile · Website

#6Cryspen

Berlin, Germany and Paris, France · hax and libcrux: verified Rust post-quantum implementations; hax Lean backend for the Verified zkEVM program

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.

Profile · Website

#7Reilabs

Warsaw, Poland · Lean 4 verification of Noir (Lampe) and gnark (proven-zk); verified Worldcoin circuits

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.

Profile · Website

#8Runtime Verification

Urbana, Illinois, United States · K framework, KEVM, zkevm-harness, EVM equivalence with Lean models

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.

Profile · Website

#9Certora

Tel Aviv, Israel and United States · Certora Prover for smart contracts on EVM, Solana, Move and Soroban

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.

Profile · Website

#10Trail of Bits

New York, United States · Cryptography and ZK audits; Circomspect static analyzer; ZKDocs

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.

Profile · Website

#11Symbolic Software

Paris, France · Protocol-level verification (Verifpal) and cryptographic audits; author of the 2026 Verification Theatre paper

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.

Profile · Website

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

Full timeline →

Glossary

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

Frequently asked questions

What does formal verification of a ZK circuit actually prove?

A machine-checked theorem that the circuit's constraints match a written specification. The strong form is two theorems: soundness (every satisfying witness meets the spec, so no false proof is accepted) and completeness (every valid input has a witness, so honest provers are never blocked). Automatic tools such as Picus prove a weaker property, that outputs are uniquely determined by inputs, without a specification. Permalink

How is formal verification different from an audit?

An audit is a time-boxed expert review that finds bug classes authors are blind to and reports on a specific commit; it does not prove absence of bugs. Formal verification proves a stated property for all inputs but only for the property stated and only inside its trusted computing base. Mature teams use both: an audit for the specification, integration and deployment surfaces, proofs for the gadgets and instruction sets that matter most. Permalink

Which framework should I use for my proof system?

AIR or Plonky3-style tables and zkVM chips: Clean (or sp1-lean if you are on SP1). Halo2: Halva. Noir: Lampe for proofs, NAVe for automatic checks. gnark: proven-zk. Circom: Picus, CIVER and Circomspect for automatic checks, Garden or Clean's forthcoming LLZK frontend for proofs. Cairo: StarkWare's Lean proofs cover the VM itself. Proof-system components (sum-check, FRI, Fiat-Shamir): ArkLib. Permalink

Why is everything in Lean 4 now?

The Ethereum Foundation's Verified zkEVM program funded most 2025 and 2026 circuit and proof-system verification in Lean 4 (Clean, zkLean, Halva, ArkLib, sp1-lean), StarkWare and Reilabs chose it independently, Mathlib supplies the field and polynomial mathematics, and AI proving tools target it. Rocq remains strong for implementation verification (Fiat-Crypto, Formal Land) and F* for HACL* and hax. Permalink

Do I need completeness or is soundness enough?

You need both if a rejected valid input is a problem, which is true for wallets, bridges, rollups and anything with liveness requirements. Soundness alone is satisfied by an unsatisfiable circuit, so a soundness-only result must be paired with honest-path tests. Clean, zk.golf, Garden and CIVER's post-condition mode state completeness explicitly. Permalink

How much does formal verification cost and how long does it take?

Automatic checks (Circomspect, Picus, Kani) take hours to days of engineer time. A sound-and-complete proof of a hash gadget such as Poseidon or SHA-256 in Clean is weeks of proof engineering; a zkVM instruction set is months and ongoing. Costs scale with the size of the specification, not the size of the code, so writing the specification first is the best cost control. Permalink

Can verified code still have bugs?

Yes, outside the verified boundary. The February 2026 Verification Theatre paper found 13 vulnerabilities in verified libraries, four inside code covered by proofs, all in properties that were never specified. The SP1 JALR bug was inside a proven opcode whose theorem excluded misaligned targets. Read the theorem statements and the trusted computing base, and audit what they leave out. Permalink

Can AI agents write these proofs?

Increasingly. better.codes measures AI-driven progress on a real soundness bound with the Lean kernel as judge, zk.golf publishes an agent API for verified circuit optimisation, and the May 2026 Rust-to-Lean pipeline paper used AI provers on Plonky3 and RISC Zero code. The kernel check is what makes AI-written proofs trustworthy; AI-written specifications still need human review. Permalink

All questions →

Methodology

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.