verse-labveil

A verifier for automated and interactive proofs about transition systems.

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

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 in decidable fragments of first-order logic, with the full power of a modern higher-order proof assistant for when automation falls short.

Veil 2.0 Pre-Release

You are looking at a pre-release version of Veil 2.0, the upcoming major version of Veil. There are still a few bugs and rough edges. If you encounter issues, please report them to us, so we can fix them before the release. Your patience and feedback are greatly appreciated!

We provide a live environment to try out Veil 2.0, at the following URL: try.veil.dev

You can ask questions on the Veil channel on the Lean Zulip, and we will be happy to answer.

Learn Veil

The Examples/Tutorial folder contains extensively commented walkthrough specifications:

  • Examples/Tutorial/Ring.lean — the Ring Leader Election protocol, introducing Veil's syntax and its main commands (#check_invariants, #model_check, sat/unsat trace).

  • Examples/Tutorial/FloodSet.lean — a complete walkthrough of Veil's multi-modal workflow via the FloodSet synchronous crash-fault agreement protocol: modelling, testing via concrete and symbolic model checking, counterexample-driven invariant discovery, and an interactive Lean proof

These files are also available in the online playground, under the Examples button.

An explanation of the constructs of the Veil DSL can be found at docs/DSL-Reference.md.

Build

Veil requires Lean 4 and NodeJS. To install those on Linux or MacOS:

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

# Install NodeJS
curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.40.3/install.sh | bash
\. "$HOME/.nvm/nvm.sh"
nvm install 24

Then, clone Veil:

git clone https://github.com/verse-lab/veil.git

And, finally, build it:

lake exe cache get
lake build

The lake exe cache get command downloads a pre-built version of mathlib, which otherwise would take a very long time to build.

Troubleshooting

(NPM errors) If you see an error about npm, make sure it's in your PATH; the command above installs both node and npm.

(cvc5 errors) If you see an error about cvc5, run:

rm -rf .lake/packages/cvc5
lake build

There is a sporadic issue in the build process for lean-cvc5. Trying to build again often fixes the problem.