Proof systems and computational proofs
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 |
|---|---|---|---|---|
| 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 |
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