Designing Distributed Systems with TLA+
summary
TLA+ is a specification language plus a model checker that finds deep concurrency bugs before code lands: a queued-worker ETL model surfaces an ambiguous create/delete race, a 16-step failure trace, and a stuttering/crash counterexample that appears in ~30 seconds; fixing requires making message-handling explicit, adding fair workers and a cleaner process to remove orphan content. Companies like AWS and Azure use TLA+; small changes get rechecked in about five minutes against invariants such as no orphan content.
AI-written summary · about
chapters (8)
- 0:00Start
- 1:00Distributed System
- 19:29Process Message Code
- 19:58Create
- 22:50What happened?
- 24:11PARAMS
- 28:01Companies using TLA
- 28:54Conclusions
related talks
43mTowards Language Support for Distributed Systems
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
48mFault Tolerance on the Cheap Making Systems That Probably Won't Fall Over
14mFormal specifications for Microservices -
20mBuilding Reliable LLM Systems
01h 02mTools for simplified large scale systems
34mThe Holy Grail of Systems Analysis: from What to Where to Why
36mGeographically Distributed Prallel Databases - A Reality!