nw-tlaplus-verification

TLA+ / Formal Verification

When and how to use TLA+ for design verification. Complements PBT (which verifies implementation).

Decision Tree: When to Use TLA+ vs PBT vs Both

Is the risk in the DESIGN or the IMPLEMENTATION?
  |
  +-- Design risk (protocol correctness, distributed coordination, concurrency)
  |     -> Does the system involve concurrent or distributed state?
  |       Yes -> Use TLA+ for design verification
  |              Then use PBT to verify implementation matches design
  |       No  -> PBT alone is likely sufficient
  |
  +-- Implementation risk (edge cases, serialization, data transforms)
  |     -> Use PBT alone
  |
  +-- Both
        -> TLA+ validates design, PBT validates implementation

Use TLA+ When:

• Design bug would cause data loss or significant customer impact
• System involves concurrent or distributed state manipulation
• Subtle interactions between components are hard to reason about informally
• Informal reasoning or testing has already failed to prevent bugs

Skip TLA+ When:

• Simple CRUD with straightforward business logic
• UI/UX behavior
• Performance optimization (TLA+ models correctness, not performance)
• Design is well-understood; risk is only in implementation bugs
• Rapid prototyping where design changes frequently

TLA+ in 60 Seconds

TLA+ describes what a system should do, not how. A specification consists of:

• Variables: State components
• Init: Valid starting states
• Next: How system transitions between states
• Invariants: Conditions that must hold in every reachable state

TLC model checker exhaustively explores all reachable states within bounded model. If invariant violated, TLC provides counterexample trace -- shortest path from initial state to violation.

PlusCal as Entry Point

PlusCal is imperative-looking language transpiling to TLA+. Most programmers find it easier to learn first.

(* --algorithm Transfer
variables accounts = [a |-> 100, b |-> 100];

process Transfer \in 1..2
variables from, to, amount;
begin
  Pick:
    from := "a"; to := "b"; amount := 50;
  Check:
    if accounts[from] >= amount then
      Debit:
        accounts[from] := accounts[from] - amount;
      Credit:
        accounts[to] := accounts[to] + amount;
    end if;
end process;
end algorithm; *)

\* Invariant: total money is conserved
MoneyConserved == accounts["a"] + accounts["b"] = 200