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.
A verified circuit is only as good as the proof system that compiles it. Sum-check, FRI, STIR and WHIR, Fiat-Shamir transforms and polynomial commitment schemes all carry pen-and-paper soundness proofs that have historically contained errors. Two families of tools address this. ArkLib formalizes interactive oracle reductions and their composition in Lean 4, targeting the SNARK components the Ethereum Foundation cares about. EasyCrypt, CryptoVerif and SSProve are general computational provers, used for KEMs, signatures, TLS and, in one production case, a ZK verifier's honesty proof.
Expect these projects to be slower and more research-shaped than circuit verification. The payoff is that they close the gap between a verified circuit and a verified system, which is why the Ethereum Foundation's 2025 zkEVM security roadmap requires a formal soundness argument for recursion by the end of 2026.
Frameworks in this category
| 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 |
How to choose
- Verifying a SNARK component (sum-check, FRI/STIR/WHIR, polynomial commitments, Fiat-Shamir): ArkLib, in Lean 4, with VCV-io for probabilistic reasoning.
- Proving a primitive or protocol secure in the computational model with a team that already writes game-based proofs: EasyCrypt (paired with Jasmin for verified code) or SSProve in Rocq.
- Automating a game sequence for a protocol like TLS, Signal or WireGuard: CryptoVerif.
- Checking that a paper's game-hopping proof is well-formed: ProofFrog.
- Proving a soundness bound for a Reed-Solomon proximity problem: the better.codes challenge is the live venue, with Lean-checked submissions.
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, Symbolic protocol analysis, Verified implementations, Proof assistants and general verifiers, Challenges and programs