Tackling Concurrency Bugs with TLA+

on YouTube ↗30m

" summary

Specifies a bank transfer system with math not code, models it in TLA+ (PlusCal for authoring) and runs the TLC checker from the TLA+ Toolbox to exhaustively explore schedules. The model enumerates combinatorics — 100 initial states and 24 orderings (2,400 behaviors) — finds an interleaving that violates a no‑overdraft invariant, and validates fixes (transactional or architectural) before coding. Also catches real bugs in app installer and deployment models and documents designs compactly.

AI-written summary · about

" chapters (13)

1. 0:00Introduction
2. 0:37Housekeeping Notes
3. 2:27Concurrency
4. 5:43Tools
5. 6:05Unit Tests
6. 7:18Static Typing
7. 8:15Purity
8. 13:35Invariants
9. 14:31Coding
10. 22:20Demo Itis
11. 23:11App Sinker
12. 24:50Documentation
13. 26:01Finding Bugs

" related talks

• 24mTLA+: Your Secret Weapon Against Concurrency HellFrederic G. Marand · SREday London 2025 Q3
• 01h 12mDistributed systems showdown — TLA + vs real codeJack Vanlightly · Hydra 2021
• 22meXtreme Modelling in PracticeJesse Davis, Max Hirschhorn, Judah Schvimer · TLA+ Community Event 2020
• 23mKayfabe: Model-based program testing with TLCStar Dorminey · TLA+ Community Event 2020
• 30mModel-based testing with TLA+ and ApalacheIgor Konnov, Andrey Kupriyanov · TLA+ Community Event 2020
• 14mModel-guided Fuzzing of Distributed SystemsRupak Majumdar, Ege Berkay Gulcan, Burcu Kulahcioglu Ozkan, Srinidhi Nagendra · OOPSLA 2025
• 05mLT: Proof Driven DevelopmentGideon Keith-Stanley · ElixirConf US 2026
• 37mContracts For Getting More Programs Less WrongRob Simmons · Strange Loop 2018