ProVerif: Automatic symbolic analysis in the applied pi-calculus
================================================================

ProVerif 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: Protocols, hax models extracted from Rust
Approach: Symbolic analysis of applied pi-calculus models, unbounded sessions, largely automatic
Access: Open source
Status: Active, mature
Strengths: High automation. | hax backend from Rust. | Decades of published models.
Limits: Weaker on global mutable state. | Symbolic model only. | May not terminate on some models.
Firms using it: Cryspen, Symbolic Software
Sources: https://bblanche.gitlabpages.inria.fr/proverif/

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