ProVerif
Direct answerProVerif automatically analyses protocol models in the applied pi-calculus for secrecy, authentication and equivalence properties over unbounded sessions. It has a large model base and is a target of hax, so Rust implementations can be analysed symbolically.
- Maintainer
- Bruno Blanchet, Inria (Prosecco)
- Website
- https://bblanche.gitlabpages.inria.fr/proverif/
- Category
- Symbolic protocol analysis
- Targets
- Protocolshax models extracted from Rust
- Approach
- Symbolic analysis of applied pi-calculus models, unbounded sessions, largely automatic
- Access
- Open source
- Status (2026-09-13)
- Active, mature
What ProVerif does
ProVerif is faster and more automatic than Tamarin at the cost of expressiveness for stateful protocols. The hax backend makes it the easiest symbolic tool to attach to a Rust codebase.
Where it is strong
- High automation.
- hax backend from Rust.
- Decades of published models.
Limits and caveats
- Weaker on global mutable state.
- Symbolic model only.
- May not terminate on some models.
When to choose it
Choose ProVerif for stateless or lightly stateful protocols and for Rust code via hax.
Who works with ProVerif
Top-listed for protocol analysis 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