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
```

**Labels** define atomicity boundaries. Everything between two labels executes atomically. Concurrency interleavings happen at label boundaries.

PlusCal limitation: can't express all TLA+ patterns (complex fairness, some non-determinism forms). Start with PlusCal, switch to raw TLA+ when needed.

## TLC Model Checker Workflow

1. Write spec in PlusCal or TLA+
2. Configure model: concrete values for constants, invariants to check
3. Run TLC: exhaustive breadth-first exploration of all reachable states
4. If violation found: TLC provides counterexample trace (shortest path to violation)
5. Fix design, re-check
6. Gradually increase model parameters (more nodes, more messages)

### Model Configuration (.cfg file)

```
SPECIFICATION Spec
CONSTANT
  Nodes = {n1, n2, n3}
  MaxMessages = 4
INVARIANT
  MoneyConserved
  NoDoubleDelivery
```

### Managing State Space Explosion

State space grows O(constants^variables). 3 nodes = ~1,000 states; 4 nodes = ~100,000. Most bugs manifest with 2-3 nodes.

Mitigation:
- Start with 2-3 nodes, low bounds (most bugs manifest with small configs)
- Use symmetry reduction for interchangeable elements
- Use state constraints to limit exploration
- Use simulation mode (`-simulate`) for large models (random sampling instead of exhaustive)

## Common Modeling Patterns

### Message Passing
Network as set of in-flight messages. Send adds to set, receive removes. Unreliable network: messages removed without receipt (loss) or kept after receipt (duplication).

### Shared Memory
Variables represent memory locations. Locks modeled as variables indicating holding process.

### Failures
Node crash: non-deterministic removal from active set. Volatile state lost, persistent retained. Restart: rejoin with fresh volatile state.

### Leader Election
Nodes propose, vote, become leader when majority achieved. Safety: at most one leader per term.

### Transactions
Two-phase commit: resource managers prepare, transaction manager commits when all prepared. Safety: no partial commits.

## Safety and Liveness

**Safety** ("nothing bad happens"): Expressed as invariants. Violated by finite counterexample trace. Example: "Two processes never hold the same lock."

**Liveness** ("something good eventually happens"): Requires fairness assumptions. Cannot be violated by finite prefix. Example: "Every request eventually gets a response."

Start with safety. Add liveness after safety established.

## The TLA+ to PBT Pipeline

Key integration point between formal verification and testing:

1. **TLA+ specification**: Identify invariants, safety properties, state machine transitions
2. **Model check with TLC**: Verify design correctness
3. **Implementation phase**: Code the verified design
4. **PBT phase**: Translate TLA+ invariants into PBT properties

Properties discovered during TLA+ become PBT test oracles:
- TLA+ invariant "total money conserved" becomes `assert sum(all_accounts) == initial_total`
- TLA+ safety "no double-delivery" becomes stateful PBT postcondition
- TLA+ state machine transitions map to stateful PBT commands

TLA+ invariants are exhaustive. PBT samples. If TLA+ proves A, B, and C, your PBT must check all three.

### What Each Catches

| TLA+ Catches (Design) | PBT Catches (Implementation) |
|----------------------|----------------------------|
| Protocol deadlocks | Off-by-one errors |
| Consistency violations under failure | Incorrect serialization |
| Missing error handling paths | Memory management issues |
| Race conditions in algorithms | Edge cases in data transforms |

Neither catches: performance bugs | usability issues | integration with external systems.

## Tooling

- **VS Code extension** (`alygin.vscode-tlaplus`): Primary IDE. Syntax highlighting, model checking, counterexample visualization. Requires Java 11+.
- **TLA+ Toolbox**: Original Eclipse-based IDE. Still functional but VS Code preferred.
- **Command-line TLC**: `java -jar tla2tools.jar -config Spec.cfg Spec.tla`
- **Apalache**: Symbolic model checker using SMT (Z3). Use when TLC hits state explosion (>10M states).
- **Community Modules**: Reusable TLA+ modules (FinSets, Sequences, Bags, Json, TLCExt).

## Real-World Adoption

- **AWS**: DynamoDB, S3, EBS -- found subtle bugs in every system, including potential data loss. Engineers learned TLA+ in 2-3 weeks.
- **Azure Cosmos DB**: All five consistency levels formally specified. Specs open-sourced.
- **Elasticsearch**: Replication, cluster coordination, shard allocation. Models open-sourced.
- **MongoDB, CockroachDB, Kafka**: Protocol verification.

## Iterative Development Approach

1. Start with 2 processes, 1 message type
2. Add failure modes (crash, restart, message loss)
3. Add more processes (verify N-participant scaling)
4. Add liveness properties (verify progress under fairness)
5. Add optimizations (verify optimized paths maintain correctness)