TLA+: Your Secret Weapon Against Concurrency Hell
summary
TLA+ models actual system states and finds concurrency bugs before code lands: Amazon credits an S3 model with catching real faults, Kafka’s replication protocol (KAFT) uncovers specification errors, and a modeled component runs in production six months without bugs while its wrapper code still fails. Uses TLC model checker for exhaustive search, Microsoft-backed symbolic model checking for larger state spaces, and the new REPL in TLA+ 1.8. Expect state-space explosion, short runs for tiny models (<1s for four states) and start small, model dependencies, and verify entry/exit code.
AI-written summary · about
chapters (9)
- 0:00Introduction and Overview
- 1:05What is TLA?
- 2:29Why Use TLA?
- 5:59How TLA Works
- 8:19Examples and Applications
- 16:59Practical Use Cases
- 19:26Tools and Resources
- 22:06Lessons Learned
- 23:25Conclusion
related talks
30mTackling Concurrency Bugs with TLA+
22meXtreme Modelling in Practice
01h 12mDistributed systems showdown — TLA + vs real code
41mDesigning software with complex configurations
23mKayfabe: Model-based program testing with TLC
28mExploring and improving the design of Abaco
39mWeeks of Debugging Can Save You Hours of TLA+
30mModel-based testing with TLA+ and Apalache