No results found

veil

A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit issues and PRs here.

Veil: A Framework for Automated and Interactive Verification of Transition Systems

Actions status License

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"

See verse-lab/veil-usage-example for a fully set-up example project that you can use as a template.

Tutorial

The file Examples/Tutorial/Ring.lean contains a guided tour of Veil's main features. Check it out if you want to see what Veil can do!

Build

Veil requires Lean 4. We have tested Veil on macOS (arm64) and Ubuntu (x86_64). Windows with WSL2 is also supported. Native Windows support is not yet available.

To build Veil, run:

lake build

To build the case studies run:

lake build Examples
How to install Lean?

If you don't have Lean installed, we recommend installing it via elan:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:stable
Dependencies

Veil depends on z3, cvc5, and uv. You do not need to have these installed on your system, as our build system will download them automatically when you run lake build. Veil will use its own copies of these tools, and will not touch your system-wide versions.

Note that if you want to invoke Lean-Auto's auto tactic, you need to have z3 and cvc5 installed on your system and available in your PATH.

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
    • Action/Theory.lean: meta-theory of action DSL with the soundness proof
    • Action/Lang.lean: implementation of action DSL expansion
    • Specification/Lang.lean: implementation of protocol declaration commands
  • SMT/: tactics for interaction with SMT
  • Tactic/: auxiliary tactics for proof automation

Case Studies implemented in Examples/

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:

  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.