Software
Get Verifpal
Release notes
Verifpal runs on Windows, macOS, Linux and FreeBSD. Pick your system below; where a package manager comes first, it is because it keeps Verifpal current on its own. Every build is on the releases page.
macOS
brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
brew install --cask verifpal
Verifpal is a cask now, not a formula. If you installed it before that change, run brew uninstall verifpal once first; afterwards brew upgrade behaves as it always did.
Take the darwin_arm64 archive for Apple silicon or darwin_amd64 for Intel from the releases page, and move the binary somewhere on your PATH. You will have to come back for updates yourself.
Windows
winget ships with Windows 10 and 11, so there is nothing to set up first.
winget install SymbolicSoftware.Verifpal
scoop bucket add verifpal https://github.com/symbolicsoft/verifpal.git
scoop install verifpal
Take the windows_amd64 archive from the releases page and put verifpal.exe somewhere on your PATH. You will have to come back for updates yourself.
Linux
Download the package for your distribution from the releases page, then install it. On an ARM machine, read arm64 for amd64 throughout.
# Debian, Ubuntu:
sudo dpkg -i verifpal_*_linux_amd64.deb
# Fedora, RHEL, openSUSE:
sudo rpm -i verifpal_*_linux_amd64.rpm
# Alpine (the packages are unsigned):
sudo apk add --allow-untrusted verifpal_*_linux_amd64.apk
# Arch:
sudo pacman -U verifpal_*_linux_amd64.pkg.tar.zst
Homebrew is macOS-only where Verifpal is concerned, so if you were using it on Linux, take a package here instead.
Take the linux_amd64 or linux_arm64 archive from the releases page, and move the binary somewhere on your PATH. You will have to come back for updates yourself.
FreeBSD
There is no FreeBSD package yet. Take the freebsd_amd64 archive from the releases page, and move the binary somewhere on your PATH.
With the Rust toolchain installed, Cargo will build Verifpal for you: either from the published crate, or from a clone of the source repository. Both compile from the same code the releases are built from, and neither updates itself.
# From crates.io, straight onto your PATH:
cargo install verifpal
# Or, in a clone of the repository:
cargo build --release
Every archive and package carries the manual pages, the shell completions for bash, zsh and fish, and the example models.
User manual
Download the PDF
The manual keeps pace with the software. It covers getting started, example models, how the analysis works underneath, and three full walkthroughs of real-world protocols. It also contains an entire manga in which Verifpal goes up against the evil Mayor N. D. Middle.
What the assurance covers
Verifpal’s syntax, semantics and analysis method are formalized, and every release since 1.0 ships with a soundness theorem behind them. When a design matters, cross-check the result against a tool such as ProVerif, which has had more than twenty years of scrutiny.
The Verifpal project maintains an extension for each editor, and a short video walks through what the Visual Studio Code one does.
Highlights syntax, runs your queries as you type, and draws the protocol as a diagram.
Puts verification diagnostics on the query lines themselves, and adds formatting and hover documentation.
Live error checking and attacker analysis, driven by the language server built into Verifpal.
Scientific background
Read the paperThe latest Verifpal research paper sets out the reasoning behind the project, including the soundness argument and the termination result.
Verifpal is inspired by two decades of work on formal verification by Prof. Bruno Blanchet, the author of ProVerif. Read that as influence, not as an endorsement of Verifpal by Prof. Blanchet.