TLA+ Formal Verification

Verify system designs and algorithm correctness by exhaustively checking every reachable state.

When to use

Concurrent systems (the classic use case)

• Concurrent actors sharing mutable state (offline queues, sync engines, caches)
• Distributed systems (client-server sync, multi-device, event sourcing)
• Multi-agent orchestration (swarm agents, parallel worktree operations)
• Any system where "it works in my test" is insufficient because interleavings matter

Algorithm invariant checking (the underrated use case)

• Pure functions with complex input spaces (recursive traversals, tree walkers, parsers)
• Functions with multiple code paths that must produce consistent results
• Algorithms where "for all possible inputs, property X must hold"
• Migration/transformation logic where data must never be lost or corrupted
• Any code where you suspect a subtle edge case but can't enumerate all inputs by hand