Veil Framework

This example demonstrates the formalization and verification of the Stellar Consensus Protocol (SCP) within the Veil framework. The implementation is adapted from the original SCP proofs (originally in Ivy and Isabelle/HOL) and provides two layers of modeling:

1. Concrete System Model: A higher-order model where concepts like quorums have explicit definitions involving sets and quantifications.
2. Abstract Model: A first-order logic abstraction where system properties (e.g., node_properties and quorum_properties) are stated as axioms.

The verification goal is to prove that the concrete model satisfies the abstract model's properties.

The signature of a transition system is defined by three types of components. Components can be mutable (default) or immutable (part of the background theory).

• Individuals: Single values of a type. Use immutable for constants.
• Relations: Predicates over types. Important: Declare relations as Bool-valued (not Prop-valued) to ensure the state is executable for the model checker.
• Functions: Total functions from domain to codomain. Use immutable for fixed mappings like topology.

individual leader : List node           -- mutable
immutable individual maxRound : round   -- immutable

relation leader : node -> Bool          -- mutable relation

function currentRound : node -> Nat    -- function
immutable function nextNode : node -> node

When writing your own Veil specifications, follow these project conventions:

• Naming: Use PascalCase for file names (e.g., TwoPhaseCommit.lean).
• Module Declaration: Each file must declare a veil module that matches the file name.
• Imports: Each file should import only Veil.

The SCP example is organized into two primary Lean files:

• SCPTheory.lean: Contains the concrete system model. This file is adapted from the Isabelle/HOL specification and defines the detailed mechanics of the protocol.
• SCP.lean: Contains the abstract model (adapted from the Ivy specification) and the bridge proof. It includes the proof showing that the concrete model satisfies the abstract properties defined in the first-order logic abstraction.

A Veil module defines a state transition system, including its background theory and state. Every module must start with import Veil, begin with veil module <Name>, and end with end <Name>.

import Veil

veil module Ring
-- module contents go here
end Ring

Veil provides a variety of protocol specifications organized by their source or modeling style. Use these to learn different modeling patterns:

• Tutorials: Best for beginners. Includes Ring.lean (syntax and commands) and FloodSet.lean (full multi-modal workflow: modeling $\rightarrow$ testing $\rightarrow$ interactive proof). The POPL26/ subfolder demonstrates different type encodings (decidable, finite, natural numbers).
• Ivy: Uses Ivy-style first-order encodings with uninterpreted types and relations.
• TLA: Translations of TLA+ specifications using concrete types, structures, and lists.
• Synchronous: Models synchronous consensus protocols with time-bounded rounds and crash-fault tolerance.
• Puzzles: State machine models of recreational puzzles, useful for practicing with the Veil model checker.

Use #model_check to exhaustively enumerate reachable states in a finite instance. The first argument instantiates parameters (types/params), and the second provides concrete values for the theory (immutable components).

For non-exhaustive testing, use #simulate to perform random walks on the state graph.

// Exhaustive model checking
#model_check { node := Fin 4 } { nextNode := fun n => n + 1 }

// Random simulation
#simulate { node := Fin 3 } {} (numTraces := 2000) (maxSteps := 500) (seed := 42)

Symbolic Bounded Model Checking explores behaviors up to a bounded number of steps using SMT. It checks all instantiations of parameters at once.

• sat trace: Finds an execution reaching a specific state or satisfying an assertion. Use an empty trace sat trace { } to check if assumptions are satisfiable.
• unsat trace: Proves that no execution of a given shape reaches a specific state.

// Find a satisfiable trace
sat trace { 
  any 3 actions
  assert (∃ l, leader l)
}

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

You can learn the Veil DSL and its verification workflows through two primary walkthrough specifications located in the Examples/Tutorial directory:

• Ring Leader Election (Ring.lean): Introduces Veil's syntax and core commands like #check_invariants, #model_check, and handling sat/unsat trace results.
• FloodSet Protocol (FloodSet.lean): A complete multi-modal workflow covering modeling, testing via concrete and symbolic model checking, counterexample-driven invariant discovery, and interactive Lean proofs.

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

Veil examples are managed using lake. You can build the entire examples suite or target a specific specification file for checking.

# Build all examples
lake build Examples

# Build and check a single example
lake lean Examples/Tutorial/Ring.lean