Veil: A Framework for Automated and Interactive Verification of Transition Systems
Veil is a foundational framework for (1) specifying, (2) implementing, (3) testing, and (4) proving safety (and, in the future, liveness) properties of state transition systems, with a focus on distributed protocols.
Veil is embedded in the Lean 4 proof assistant and provides push-button verification for transition systems and their properties expressed decidable fragments of first-order logic, with the full power of a modern higher-order proof assistant for when automation falls short.
Using veil
To use veil
in your project, add the following to your
lakefile.lean
:
require "verse-lab" / "veil" @ git "main"
Or add the following to your lakefile.toml
:
[[require]]
name = "veil"
git = "https://github.com/verse-lab/veil.git"
rev = "main"
Important: if you use Veil as a library, make sure to also install
z3
, cvc5
, Python >= 3.11, and the z3-solver
, multiprocess
, and
sexpdata
Python libraries. See the Build section for detailed
instructions.
See
verse-lab/veil-usage-example
for a fully set-up example project.
Build
Veil requires Lean 4, z3
, cvc5
, Python >= 3.11, and the z3-solver
,
multiprocess
, and sexpdata
Python libraries.
To build Veil run lake build
. This will build the whole project with
tests in Tests/
but without case studies. To build the case studies
run lake build Examples
.
Detailed build instructions
-
Install Python 3 with version >= 3.11. The latest version of Python can be downloaded from here.
-
Install Lean. Detailed instructions on Lean installations can be found here. We recommend installing via
elan
. -
Install
z3
andcvc5
.-
For Ubuntu run
sudo apt update && sudo apt install z3 cvc5
-
For Mac (using Homebrew)
brew install z3 cvc5/homebrew-cvc5/cvc5
- Detailed instructions on
cvc5
installation can be found here. - If you install
cvc5
by getting the binary make sure to add it to your PATH by running:
For bash:
echo 'export PATH=$HOME/.local/bin:$PATH' >> ~/.bashrc source ~/.bashrc
For Zsh:
echo 'export PATH=$HOME/.local/bin:$PATH' >> ~/.zshrc source ~/.zshrc
- Detailed instructions on
-
-
Finally, you will need to install dependencies for our Python wrapper around the Z3 SMT solver. Run and then either:
pip3 install z3-solver multiprocess sexpdata
or (on Ubuntu)
apt-get install python3-z3 python3-multiprocess python3-sexpdata
Project Structure
The project consists of three major folders:
Veil/
: the implementation of Veil,Test/
: Veil's artificial test cases for main Veil features,Examples/
: Veil's benchmarks, consisting of realistic specifications of distributed protocols
Veil/
components
DSL/
: Veil DSLAction/Theory.lean
: meta-theory of action DSL with the soundness proofAction/Lang.lean
: implementation of action DSL expansionSpecification/Lang.lean
: implementation of protocol declaration commands
SMT/
: tactics for interaction with SMTTactic/
: auxiliary tactics for proof automation
Case Studies implemented in Examples/
FO/
: non-EPR protocolsIvyBench/
: benchmarks translated from IvyRabia/
: Rabia protocolStellarConsensus/
: Stellar Consensus ProtocolSuzukiKasami/
: Suzuki Kasami protocol
Additional resources
Docker image
We supply a script that creates a Docker image that can be used for developing and running Veil projects. This Docker image is based on x86-64 Linux, but can be used on ARM computers with any OS that can run Docker. To use it with Visual Studio Code, follow these instructions:
- Make sure Docker is running. Run
./create_docker_image.sh
. This will automatically download Veil and install most of the prerequisites on the created image. This can take up to 10 minutes. - Run the container with
docker run -dt --platform=linux/amd64 <image-id>
. - On your host computer, install the Dev Containers VS Code plugin.
- Connect to the Docker container with the
Dev Containers: Attach to Running Container...
action from the Command Palette (Ctrl/Cmd + Shift + P). - On the container, install the Lean 4 VS Code plugin. This needs to be done once per container.
- Initially, Veil will be placed in
/root/veil
. You can move it, or open that folder directly from VS Code. - Test Veil: Go to any of Veil's example files and run the
Lean 4: Server: Restart File
action from the Command Palette. This may take a while on the first run, as it has to rebuild all of Veil.