Verifpal verifies the security of cryptographic protocols. It is written for practitioners and students. A passing query means the search found no attack within its stated bounds. It is not a proof.
- Workbench: run Verifpal in your browser
- Install: macOS, Windows, Linux, or from source with
cargo build --release - Editor extensions: Visual Studio Code, Neovim, Zed
- Analysis reports: HTML, JSON and LaTeX output
- Quickstart
- Introduction
- Modeling a protocol
- Writing security queries
- How analysis works and its search limits
- Command line
- Language reference
- Protocol studies: Signal, Scuttlebutt, post-quantum
- Comparison with ProVerif and Tamarin
- From Toy to Instrument: Seven Years of Verifpal (paper)
- Citing Verifpal
- Community and events
- Contributing and security policy
Verifpal is free software under the GNU General Public License, version 3.
© Copyright 2019-2026 Nadim Kobeissi. “Verifpal” and the “Verifpal” logo/mascot are registered trademarks of Nadim Kobeissi.