nw-formal-verification-tlaplus

# Formal Verification with TLA+ ## When to Recommend Formal Verification ### Decision Tree ``` Is the system distributed or concurrent? | +-- No --> Complex state machine with high failure cost? | +-- No --> NOT cost-effective. Use property-based testing. | +-- Yes --> CONSIDER TLA+ | +-- Yes --> Consensus, coordination, or distributed transactions? | +-- Yes --> RECOMMEND TLA+ | +-- No --> Could concurrency bug cause data loss or safety issues? | +-- Yes --> RECOMMEND TLA+ | +-- No --> OFFER as option ``` ### Strong Indicators (Recommend) | Domain | Why TLA+ Adds Value | Evidence | |--------|-------------------|----------| | Distributed consensus (Paxos, Raft) | Subtle interleaving bugs in leader election | Raft TLA+ spec ~400 lines, found implementation bugs | | Financial distributed transactions | Atomicity violations cause monetary loss | AWS DynamoDB replication verified | | Leader election, distributed locking | Split-brain, deadlock, stale-lock | AWS lock manager verified | | Eventual consistency / CRDTs | Convergence proofs required | TLA+ CRDT framework verifies SEC | | Safety-critical state machines | Regulatory requirements | DO-178C, CENELEC recognize formal methods | | Multi-party coordination (sagas, 2PC) | Compensation ordering, partial failure | 2PC is canonical TLA+ example | | Data replication protocols | Ordering, consistency under failure | Elasticsearch, MongoDB, Cosmos D...