TLA+ at Microsoft to build planetary-scale systems
summary
Microsoft uses TLA+ to specify and validate concrete designs for Cosmos DB and a global AI scheduler, producing five consistency levels formally specified and implemented, and a Consistency Checker Service that tracks transaction histories so the launched Cosmos SLA reports no consistency violations. TLA+ models include Chandy‑Lamport plus two custom snapshot algorithms to compare tradeoffs without coding, saving months of engineering. The practice also guides hiring, embeds specs in wikis, and ties formal models to incident fixes and customer-facing SLAs.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 4:07Outline
- 5:17Cosmos Database
- 6:41Requirements
- 12:08System overview
- 16:05Consistency levels
- 20:15Debugging
- 29:29Applying TLA
- 30:51Team wiki
- 31:23TLA spec
- 32:20SLAs
- 33:05Summary
related talks
01h 13mDesigning distributed systems with TLA+
42mWelcome to TLA-La-Land (or An Introduction to Software Verification)
31mTurning an Incident Report into a Design Issue with TLA+
41mDesigning software with complex configurations
24mErla+: Translating TLA+ Models into Executable Actor-Based Implementations
01h 13mWorkshop: TLA+ in action (Part 3)
01h 12mWorkshop: TLA+ in action (Part 4)
18mSmart Casual Verification of the Confidential Consortium Framework