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/