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 sys...