Model checking and formal proof

Deep dive

How it works

Parts:

• model — initial states plus a transition relation (processes, shared variables, messages, failures), in TLA+, Promela, SMV or code
• property — safety invariant (bad state never reached) or temporal formula (LTL/CTL) for liveness
• visited set — hash set of expanded states, with a parent link per state for the trace
• frontier — queue (breadth-first) or stack (depth-first) of states to expand
• engine — explicit-state search, BDD, SAT/SMT unrolling, or proof assistant

Explicit-state operations:

1. Seed. Put the initial states in the visited set and the frontier.
2. Expand. Pop a state; compute one successor per enabled transition.
3. Check. Test the invariant, and deadlock (no transition enabled, not a legal end state).
4. Dedupe. An unvisited successor is stored with its parent and queued.
5. Stop. On a violation, follow the parent links back: that is the counterexample. An empty frontier proves the property for the model.

Liveness:

• LTL speaks about every run: G !(cs0 && cs1) (always), G (try0 -> F cs0) (a request is eventually served), plus X next, U until. CTL quantifies over paths: AG (all paths, always), EF (some path, eventually), e.g. AG EF reset.
• A liveness violation is a lasso: a path into a cycle that never reaches the goal. Finding it needs cycle detection (nested DFS, strongly connected components), not one bad state.
• Without fairness a scheduler may never run a process. Assume weak fairness (a continuously enabled step eventually happens) or strong fairness (a step enabled infinitely often happens).

Beyond explicit states:

• Reductions. Symmetry: states equal up to permuting identical processes keep one canonical form (TLC symmetry sets). Partial-order: skip interleavings of independent steps (Spin).
• Symbolic. Hold state sets as binary decision diagrams, step whole sets (NuSMV).
• Bounded. Unroll k steps and ask a SAT or SMT solver for Init(s0) and T(s0,s1) and ... and not P(si). Satisfiable: counterexample. Unsatisfiable: no bug within k steps (CBMC, Kani, Apalache).
• Deductive. Prove the invariant inductive: true initially, preserved by every step. Done in proof assistants (Isabelle/HOL, Rocq, Lean) or verifiers that send obligations to SMT solvers (Dafny, Why3, Frama-C, SPARK).

 model + property --> engine --+--> explicit: BFS/DFS, visited set --> "ok, N states" | trace
                               +--> symbolic: BDD image steps ------> "ok" | trace
                               +--> bounded: unroll k, SAT/SMT ------> "no bug <= k" | model
                               +--> proof: invariant + obligations --> proved | open goal

Code

Breadth-first checker for two processes entering a critical section: naive test-then-set (breaks mutual exclusion), set-flag-first (safe, deadlocks), Peterson's algorithm (correct).

use std::collections::{HashMap, VecDeque};

#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum Proto { Naive, FlagFirst, Peterson }

// pc: 0 idle, 1-2 entry steps, 3 critical section, 4 exit
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub struct State { pc: [u8; 2], flag: [bool; 2], turn: usize }

const INIT: State = State { pc: [0; 2], flag: [false; 2], turn: 0 };

/// Successor when process `i` steps; None = blocked.
fn step(p: Proto, s: State, i: usize) -> Option<State> {
    let (j, mut n) = (1 - i, s);
    n.pc[i] = match (p, s.pc[i]) {
        (Proto::Naive, 0) => if s.flag[j] { return None } else { 1 },  // test ...
        (Proto::Naive, 1) => { n.flag[i] = true; 3 }                   // ... then set: not atomic
        (Proto::FlagFirst, 0) => { n.flag[i] = true; 1 }
        (Proto::FlagFirst, 1) => if s.flag[j] { return None } else { 3 },
        (Proto::Peterson, 0) => { n.flag[i] = true; 1 }
        (Proto::Peterson, 1) => { n.turn = j; 2 }                      // give way
        (Proto::Peterson, 2) => if !s.flag[j] || s.turn == i { 3 } else { return None },
        (_, 3) => 4,
        (_, 4) => { n.flag[i] = false; 0 }
        _ => unreachable!(),
    };
    Some(n)
}

#[derive(Debug, PartialEq)]
pub enum Verdict {
    Ok { states: usize },
    MutexViolated(Vec<(usize, State)>), // (process that moved, state after)
    Deadlock(Vec<(usize, State)>),
}

/// Breadth-first: the first bad state found has a shortest path.
pub fn check(p: Proto) -> Verdict {
    let mut parent: HashMap<State, Option<(State, usize)>> = HashMap::from([(INIT, None)]);
    let mut queue = VecDeque::from([INIT]);
    let trace = |parent: &HashMap<State, Option<(State, usize)>>, mut s: State| {
        let mut t = vec![];
        while let Some(&Some((prev, who))) = parent.get(&s) { t.push((who, s)); s = prev; }
        t.reverse();
        t
    };
    while let Some(s) = queue.pop_front() {
        if s.pc == [3, 3] { return Verdict::MutexViolated(trace(&parent, s)); } // invariant
        let mut moved = false;
        for i in 0..2 {
            if let Some(n) = step(p, s, i) {
                moved = true;
                parent.entry(n).or_insert_with(|| { queue.push_back(n); Some((s, i)) });
            }
        }
        if !moved { return Verdict::Deadlock(trace(&parent, s)); }
    }
    Verdict::Ok { states: parent.len() }
}

fn main() {
    match check(Proto::Naive) {
        Verdict::MutexViolated(t) => {
            assert_eq!(t.len(), 4);
            for (who, s) in &t { println!("P{who} -> {s:?}"); }
        }
        v => panic!("{v:?}"),
    }
    assert!(matches!(check(Proto::FlagFirst), Verdict::Deadlock(t) if t.len() == 2));
    assert_eq!(check(Proto::Peterson), Verdict::Ok { states: 26 });
}

Run output: the naive protocol prints a 4-step trace (both test, then both set and enter). FlagFirst deadlocks after 2 steps (both flags set, both waiting). Peterson: no violation, 26 states.

Complexity and constants

• Time O(S x T) for S reachable states with T transitions each; memory O(S). S is a product: n identical processes with k local states give up to k^n combinations.
• Bounded checking: one SAT/SMT query of size O(k x |T|), NP-hard.
• Measured on this Mac (Apple M4 Pro), release build, std HashMap (SipHash): Peterson check about 2.0 us per run (26 states, about 77 ns per state), mean of 100,000 runs.

Efficiency

• Cost: per state one hash lookup plus one insert per successor; memory-bound once the visited set outgrows cache and then RAM. The DynamoDB model ran on distributed TLC with ten EC2 instances (Newcombe et al.).
• Levers:
  • symmetry reduction — up to n! fewer states for n interchangeable processes (theory) — identical replicas
  • partial-order reduction — skips equivalent interleavings (Spin) — independent local steps
  • bitstate hashing — one bit per state, small chance of missing states (Spin README) — memory-limited searches
  • small instance — fewer states; AWS checked "sufficiently large" instances (Newcombe et al.)
• Naive → standard → state of the art:
  • hand-picked test interleavings · incomplete
  • explicit search with reductions · bounded by RAM
  • BDDs, bounded SMT, inductive invariants, proofs · unbounded, with effort

Implementation notes

• Pack states into fixed-size integers so the visited set stays small and cheap to hash. TLC keeps fingerprints (from memory).

Pitfalls

• The model is not the code: a checked Peterson says nothing about a C version lacking a memory barrier.
• Liveness unchecked: AWS's lock-free model "failed to find a liveness bug as we did not check liveness" (Newcombe et al.).
• Missing fairness gives spurious starvation; too much hides real starvation.
• Parameters too small (2 nodes) pass while the bug needs 3; coarse atomic steps hide races.
• Vacuity: a stuck model satisfies every invariant; check interesting states are reachable.
• "No bug in k steps" is not a proof.

Variants and alternatives

In production

• Cloud: Amazon modelled S3, DynamoDB, EBS and a lock manager in TLA+/PlusCal; DynamoDB's model found a data-loss bug with a 35-step shortest trace (Newcombe et al.).
• Operating systems: seL4 has machine-checked proofs of functional correctness, binary correctness and security properties (sel4.systems; Isabelle/HOL in seL4/l4v).
• Hardware: Intel reported formal verification replacing testing in Core i7 execution-engine validation (Kaivola et al.).
• Space and rail: SPARK case studies at Astrium Space Transportation and Mitsubishi Electric R&D Centre Europe (ERTS 2014); pairs with coding standards and fault-tree analysis.
• Protocols such as Raft, Multi-Paxos and two-phase commit are typical targets.

Implementations

Sources

• Newcombe et al., How Amazon Web Services Uses Formal Methods, CACM 58(4), 2015. DOI · earlier report (PDF)
• Klein et al., seL4: Formal Verification of an OS Kernel, SOSP 2009. DOI · proofs · code
• Clarke, Emerson, Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, TOPLAS 1986. DOI
• Burch, Clarke, McMillan, Dill, Symbolic model checking: 10^20 states and beyond, 1992. DOI
• Biere, Cimatti, Clarke, Zhu, Symbolic Model Checking without BDDs, TACAS 1999. DOI
• Holzmann, The model checker SPIN, IEEE TSE 1997. DOI
• Kaivola et al., Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation, CAV 2009. DOI
• AdaCore, Rail, Space, Security: Three Case Studies for SPARK 2014, 2013. blog
• Lamport, TLA+ home page. site