Topic 21 — Formal Methods & Verification

Testing (topic 16) finds bugs you imagined; formal methods find the ones you didn’t. This topic covers the three tools that actually get used in databases — TLA+ (model checking protocols), e-graphs (equality saturation for optimizers), SMT (Z3) — plus Lean 4 for the proof end of the spectrum.

                 what it checks         effort    used by
  fuzz/PBT (16)  behaviors you generate  hours    everyone
  TLA+ / TLC     ALL behaviors of a      days     AWS, MongoDB,
                 finite model                     CockroachDB
  SMT (Z3)       one logical formula     mins     query verifiers
                 (validity/satisfiab.)            (Cosette), symex
  Lean 4 proof   the actual theorem,     weeks    seL4-style kernels,
                 unbounded                        mathlib

graph LR
    SAT["SAT solver<br/>(CDCL)"] --> SMT["SMT = SAT + theories<br/>DPLL(T), Z3"]
    SMT --> EM["e-matching over an<br/>e-graph (congruence closure)"]
    EM -.same data structure.-> EGG["egg: equality saturation<br/>(rewrite ALL ways, then pick)"]
    EGG --> OPT["query optimizers<br/>M21 rewrite stage"]
    TLA["TLA+ spec"] --> TLC["TLC model checker<br/>(BFS over states)"]
    TLC --> PROTO["replication / MVCC<br/>protocol checking"]
    LEAN["Lean 4"] --> PROOF["machine-checked proof<br/>(unbounded, forever)"]

The problem, measured (bench lane 1, provided — runs today)

cargo run --release --bin eqsat_bench — a hand-ordered rewriter on the canonical trap expression (a*2)/2, then on random trees:

-- the ordering trap: (a*2)/2 --
hand: cost 5 (1 firing, 11.9 µs) — Div(Shl(Var("a"), Num(1)), Num(2))

-- random exprs, 20 seeds per depth --
depth   in cost   hand cost   hand µs   firings
    4        31          21       4.3         4
    6       127          90      17.3        15
    8       511         355     102.1        61
   10      2047        1390     420.7       248

The answer to (a*2)/2 is a. The hand-ordered rewriter returns (a << 1) / 2, cost 5, and stops. It is not buggy and it did not run out of rules — it applied a locally excellent rewrite (*2 → <<1, a real strength reduction) which destroyed the syntactic shape that the cancellation rule was waiting for. One firing, then a local optimum, forever.

That is the entire motivation for equality saturation, and it is why the sweep matters too: hand rewriting only removes about 32% of the cost at every depth (2047 → 1390 at depth 10), consistently, because the same class of ordering accident keeps happening. An e-graph does not choose an order — it keeps all the equivalent forms and extracts the cheapest at the end, which is why the egg column exists and why “phase ordering” is a compiler problem with a data structure for an answer rather than a heuristic for one.

1. E-graphs: the data structure

An e-graph = union-find over e-classes + hashcons (memo) + congruence closure. It stores a set of terms closed under equivalence, compactly: 2*x and x<<1 live in the same e-class, and every parent of that class automatically has both forms.

  e-class {a*2, a<<1}          union-find: id → canonical id
       /        \              hashcons:  node → e-class id
   e-class{a}  e-class{2,1<<0?}   (topic 8's hash table, again)

Three ops (egg src/egraph.rs):

• add (:970) — hashcons hit or new singleton class
• union (:1147) — union-find merge; repair is DEFERRED
• rebuild (:1416) — restore congruence invariant in one batched pass (process_unions :1346 re-canonicalizes and re-unions until fixpoint). Deferring this is egg’s headline contribution — the same amortize-the-repair move as delta matrices’ wait (topic 20) and LSM compaction (topic 4).

2. Equality saturation vs hand-ordered rules

Topic 10’s optimizer applies rules in a fixed order, destructively. Order is a silent correctness-of-outcome bug:

        (a*2)/2
  hand (ordered):  strength-reduce FIRST → (a<<1)/2 … stuck, cost 5
  egg (saturate):  keep BOTH forms; (x*y)/z→x*(y/z) still matches
                   → a*(2/2) → a*1 → a, cost 1

graph TD
    A["with_expr: seed e-graph"] --> B["match ALL rules<br/>(machine.rs VM)"]
    B --> C["apply: add + union<br/>(no destruction)"]
    C --> D["rebuild (deferred<br/>congruence repair)"]
    D --> E{"saturated? limits?<br/>run.rs StopReason"}
    E -->|no| B
    E -->|yes| F["Extractor + CostFunction<br/>pick cheapest term"]

The catch: the e-graph can blow up (assoc+comm rules alone are exponential), so Runner has node/iter/time limits — saturation is best-effort, extraction is greedy per-class. This is a search budget, the same shape as topic 10’s join-order DP cutoff.

3. TLA+ — spec the scary parts

specs/WalReplication.tla models topic 15’s WAL shipping: sequential entries, prefix logs (so a log is just a length), quorum commit, crash, longest-log failover. TLC exhaustively checks every interleaving of a 3-replica, 3-entry model:

The counterexample TLC prints is the exact PostgreSQL synchronous_commit = off data-loss story: Append → Commit (no quorum) → Crash(primary) → Failover(empty log) — committed=1, new primary has nothing. Five states. No test generator finds this guaranteed; TLC does, in under a second.

Run it: java -cp ~/repos/tla2tools.jar tlc2.TLC -deadlock WalReplication.tla (flip SyncCommit in the .cfg to see the trace).

4. Z3 — SMT in one paragraph

A SAT core with two-watch literals, lemma learning from conflict clauses, phase caching and non-chronological backtracking (TACAS’08’s own list) plus theory solvers (linear arithmetic, arrays, uninterpreted functions); quantifiers via e-matching over a congruence-closure e-graph — the same structure as egg, built for search instead of rewriting. Note what the paper does not say: it names Nelson–Oppen only as the traditional method Z3 avoids, in favour of model-based theory combination (its ref [5]), and “DPLL(T)” appears exactly once, under relevancy propagation. Z3’s modern e-graph (src/ast/euf/euf_egraph.h:22-23) mentions egg, but carefully: the worklist “is in reality inherited from the legacy SMT solver. It is claimed to have the same effect as delayed congruence table reconstruction from egg.” Databases meet Z3 in query equivalence checking (Cosette, topic 16) and symbolic execution of UDFs.

5. Lean 4 — proofs, and a runtime worth reading

Proofs are unbounded (no MaxLog=3), but cost weeks not days. Lean’s own runtime is a systems story: Counting Immutable Beans (Ullrich & de Moura, IFL 2019) reference counting with reuse tokens gives functional-but-in-place updates — an RC design directly relevant to any Rust engine tempted by Arc everywhere. Perceus is Koka’s descendant of it, and says so: its §5 is “closely based on the reference counting algorithm in the Lean theorem prover as described by Ullrich and de Moura”. M21 taste: prove one delta-matrix invariant (DP ∩ M = ∅ preserved by set/remove) in Lean, and compare with the same property as a proptest (topic 16).

Reading guides

• reading-aws-cacm15.md — Why AWS writes TLA+: exhaustively testable pseudo-code
• reading-egg-popl21.md — egg: equality saturation with deferred rebuilding
• reading-z3-tacas08.md — Z3: SAT plus theories, with an e-graph at the core
• reading-tlaplus-raft.md — A spec is a state machine: TLA+ through raft.tla
• reading-lean-perceus.md — Perceus: reference counting precise enough to reuse memory

Experiments

M21 checklist

• TLA+ spec of capstone MVCC visibility (or reuse WalReplication for the replication layer) checked by TLC in CI (a java -cp tla2tools.jar step — seconds at model scale)
• Lean proof of one delta-matrix invariant
• optional: egg-based rewrite stage in the planner, budgeted (node limit) and gated like topic 19’s JIT threshold