TLA+ / Formal 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: