Verifpal: Software

Get Verifpal

Verifpal runs on Windows, macOS and Linux. Select an operating system for installation instructions. Packages and binaries are available on the releases page.

macOS

Homebrew — recommended


							brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
							

							brew install --cask verifpal

If you installed Verifpal as a Homebrew formula, run brew uninstall verifpal before installing the cask. Use brew upgrade for future updates.

Direct download

Download the darwin_arm64 archive for Apple silicon from the releases page. Move the binary to a directory on your PATH.

Windows

winget — recommended

winget is included with Windows 10 and 11.


							winget install SymbolicSoftware.Verifpal

Scoop


							scoop bucket add verifpal https://github.com/symbolicsoft/verifpal.git
							

							scoop install verifpal

Direct download

Download the windows_amd64 archive from the releases page. Move verifpal.exe to a directory on your PATH.

Linux

Your distribution’s package — recommended

Download the package for your distribution from the releases page and install it with the corresponding command. Replace amd64 with arm64 on ARM systems.


							# 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


							brew tap verifpal.com/source https://github.com/symbolicsoft/verifpal
							

							brew install --cask verifpal

Homebrew installs casks on Linux since version 4.6.16, on both amd64 and arm64. Check yours with brew --version and run brew update if it is older. Use brew upgrade for future updates.

Direct download

Download the linux_amd64 or linux_arm64 archive from the releases page. Move the binary to a directory on your PATH.

From source — any system

Install the Rust toolchain, then use Cargo to install the published crate or build a clone of the source repository.


						# Install the published crate:
						

						cargo install verifpal
						

						# Build a repository clone:
						

						cargo build --release

All archives and packages include manual pages, shell completions for bash, zsh and fish, and example models.

Editor support

Official extensions are available for Visual Studio Code, Neovim and Zed. A short video demonstrates the Visual Studio Code extension.

Visual Studio Code

Syntax highlighting, live query analysis and protocol diagrams.

Neovim

Inline verification diagnostics, formatting and hover documentation.

Zed

Live diagnostics and attacker analysis through Verifpal’s language server.

Analysis reports

See an example report

By default, Verifpal writes verification results to the terminal. --format html writes a self-contained HTML report with a protocol sequence diagram, highlighted model source, and a diagram and trace for each attack. The report has no external assets.


				verifpal verify signal.vp --format html > report.html

--format tex writes a standalone LaTeX report with a message-sequence chart, query results, a keyed diagram and numbered trace for each attack, and the model source as an appendix. Terms are typeset as mathematics. BEGIN/END markers surround each figure, and all macros are defined in one preamble so figures can be copied into another document. View the compiled example.


				verifpal verify signal.vp --format tex > report.tex
				

				tectonic report.tex

Scientific background

Read the paper

The latest Verifpal research paper formalizes the language and analysis, including soundness and termination results.

Verifpal builds on work by Prof. Bruno Blanchet, the author of ProVerif. This does not imply his endorsement of Verifpal.