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.

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 DSL
  • ActionTheory.lean: meta-theory of action DSL with the soundness proof
  • ActionLang.lean: implementation of action DSL expansion
  • SpecLang.lean: implementation of protocol declaration commands
• SMT/: tactics for interactions with SMT
• Tactic/: auxiliary tactics for proof automation

Case Studies implemented in Examples/

• FO/: non-EPR protocols
• IvyBench/: benchmarks translated from Ivy
• Rabia/: Rabia protocol
• StellarConsensus/: Stellar Consensus Protocol
• SuzukiKasami/: Suzuki Kasami protocol

Build

1. Install Python. The latest version of Python can be downloaded from here.

2. Install Lean. Detailed instructions on Lean installations can be found here.

3. Install Z3.

   • For Ubuntu run

     sudo apt update
     sudo apt install z3

   • For Mac

     brew install z3

4. Install 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 On Ubuntu/MacOS

     echo 'export PATH=$HOME/.local/bin:$PATH' >> ~/.bashrc
     source ~/.bashrc

     For Zsh

     echo 'export PATH=$HOME/.local/bin:$PATH' >> ~/.zshrc
     source ~/.zshrc

5. 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

Evaluation

After installing Veil's dependencies, you can run Veil on all benchmarks and generate a graph using the eval/run_eval.py script. This script accepts the following parameters:

• Input file name or directory: for a file name, it runs Veil on that file and prints the time taken split into simplification time, translation time and solving time. For a directory, run Veil on all files in the directory recursively.
• --repeat N (optional, default 1) - run Veil the specified number of times and report an average result.
• --output-file <filename> (optional) - if set and the input is a directory, output a graph showing Veil's run times to the specified file. The file extension may be pdf or png.

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:

1. 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.
2. Run the container with docker run -dt --platform=linux/amd64 <image-id>.
3. On your host computer, install the Dev Containers VS Code plugin.
4. Connect to the Docker container with the Dev Containers: Attach to Running Container... action from the Command Palette (Ctrl/Cmd + Shift + P).
5. On the container, install the Lean 4 VS Code plugin. This needs to be done once per container.
6. Initially, Veil will be placed in /root/veil. You can move it, or open that folder directly from VS Code.
7. 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.

Getting Started

To build Veil run lake build. This will build the whole project with tests in Tests/ but without case studies. To build case studies run lake build Examples.