CryptoVerif
Direct answerCryptoVerif automates game-hopping proofs in the computational model, producing concrete security bounds for protocols. It has been applied to TLS 1.3, Signal and WireGuard and is the computational counterpart to ProVerif.
- Maintainer
- Bruno Blanchet, Inria (Prosecco)
- Website
- https://bblanche.gitlabpages.inria.fr/CryptoVerif/
- Category
- Proof systems and computational proofs
- Targets
- Protocols: TLS 1.3, Signal, WireGuardKey exchangeAuthenticated encryption compositions
- Approach
- Automatic and guided sequences of games with concrete security bounds
- Access
- Open source
- Status (2026-09-13)
- Active, mature
What CryptoVerif does
Where EasyCrypt is interactive and expressive, CryptoVerif is more automatic and best on protocol compositions. Many analyses run both a symbolic (ProVerif or Tamarin) and a computational (CryptoVerif) model of the same protocol.
Where it is strong
- Automation reduces proof effort.
- Concrete bounds, not just yes/no.
- Long record on major protocols.
Limits and caveats
- Less flexible than EasyCrypt for novel primitives.
- Modelling effort still significant.
- Small user community.
When to choose it
Choose CryptoVerif for protocol-level computational guarantees, especially hybrid post-quantum handshakes.
Who works with CryptoVerif
No firm on this index lists CryptoVerif as a core tool yet; the firms below cover the same problem class.
Top-listed for proof-system verification work: zkSecurity
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
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
Related frameworks in Proof systems and computational proofs
ArkLib, EasyCrypt, SSProve, ProofFrog, Squirrel.