Formal verification of proof systems and cryptographic security proofs: ArkLib, EasyCrypt, CryptoVerif, SSProve, ProofFrog
================================================================================

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: Verified-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 — 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 — Active, mature
CryptoVerif: Bruno Blanchet, Inria (Prosecco) — Protocols: TLS 1.3, Signal, WireGuard, Key exchange, Authenticated encryption compositions — Automatic and guided sequences of games with concrete security bounds — 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 — 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 — Research (2025)
Squirrel: Inria (Bana-Comon logic) — Protocols — Interactive prover in the computationally complete symbolic attacker model — 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.

Source page: https://sorryfree.com/categories/proof-systems/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13