Distributed systems showdown — TLA + vs real code
summary
Built a minimalist BookKeeper-style distributed log both as a TLA+ model and as a Java Maelstrom/Jepsen prototype; TLA+ uses two specs (~300 and ~1,000 lines) and TLC explores millions of states and found the defect in ~20s by producing an exact error trace, while the Java model (52 files, ~6,000 LOC, single‑threaded event loop, many CompletableFutures) requires local invariants that crash the node to surface bugs and only reproduces that same bug via Maelstrom after days of stochastic runs.
AI-written summary · about
chapters (19)
- 0:00Start
- 7:54What Properties Should Our Models Have
- 9:16Tla Plus Is a Specification Language
- 11:01What Is a State
- 12:15Safety Properties
- 13:02Liveness
- 14:32Maelstrom
- 23:13State Enumeration versus Simulation
- 26:21Segmented Log
- 31:15Segment Life Cycle
- 35:06Single Threaded Event Loop
- 38:22Invariants
- 41:30Model Checking Wins and Fails
- 42:29Error Trace
- 49:48Final Thoughts
- 51:39Challenges
- 52:25Battle in the State Space
- 59:03What's Next
- 1:07:09Pitfalls
related talks
01h 13mDesigning distributed systems with TLA+
24mTLA+: Your Secret Weapon Against Concurrency Hell
30mTackling Concurrency Bugs with TLA+
43mWeeks of Debugging Can Save You Hours of TLA+
41mDesigning software with complex configurations
22meXtreme Modelling in Practice
38mEverything about distributed systems is terrible
24mErla+: Translating TLA+ Models into Executable Actor-Based Implementations