Veil

Multi-Modal Verification of Distributed Protocols

Veil is a foundational framework for specifying, testing, and proving safety properties of state transition systems, built using Lean.

GitHubPlayground Zulip

One Framework, Many Capabilities

Image

Specify

Write protocol models in an expressive domain-specific language. The language guides you to write specifications that admit fully automated proofs, but you can use Lean's full power when needed.

Image

Find Bugs

Find bugs in seconds with both concrete and symbolic model checking. Visualise execution traces and counterexamples directly in the Lean InfoView.

Image

Discover Properties

Interactively discover inductive invariants with Veil's powerful counterexample to induction (CTI) generator.

Image

Verify

Prove safety properties with push-button automation. When default automation isn't enough, use Lean's full tactic language to finish the job.

See It in Action

import Veil

veil module Ring

type node
instantiate tot : TotalOrder node
instantiate btwn : Between node

open Between TotalOrder

relation leader : node → Bool
relation pending : node → node → Bool

#gen_state

after_init {
  leader N := false
  pending M N := false
}

ghost relation isNext (n : node) (next : node) :=
  ∀ Z, n ≠ next ∧ ((Z ≠ n ∧ Z ≠ next) → btw n next Z)

action send (n next : node) {
  require isNext n next
  pending n next := true
}

action recv (sender n next : node) {
  require isNext n next
  require pending sender n
  pending sender n := false
  if (sender = n) then
    leader n := true
  else
    if (le n sender) then
      pending sender next := true
}

safety [single_leader] leader N ∧ leader M → N = M
invariant [leader_greatest] leader L → le N L
invariant [self_msg_greatest] pending L L → le N L

#gen_spec

#model_check { node := Fin 7 }

sat trace {
  any 3 actions
  assert (∃ l, leader l)
}

unsat trace {
  any 5 actions
  assert (∃ n₁ n₂, n₁ ≠ n₂ ∧ leader n₁ ∧ leader n₂)
}

#check_invariants

end Ring

Integrated IDE Experience

Explore counterexample traces, discover invariants, and debug protocols directly in VS Code — all powered by Lean's Language Server.

Image

Try It Online

Write and verify protocols directly in your browser. No installation required.

Launch Playground