Specifying Distributed Systems with TLA+ Workshop
summary
Workshop teaches TLA+ from the ground up, uses TLA+ Toolbox and the TLC model checker to write formal specs of distributed algorithms (examples: Paxos and Two Phase Commit), runs the model checker to produce counterexamples, and shows concrete bugs found — two surprising protocol bugs cited — plus how to constrain state space and visualize traces with dot. The exercises specify initial/next-state formulas, run short models to catch safety and liveness issues, and the later parts of the six‑hour workshop are unavailable due to camera malfunction.
AI-written summary · about
chapters (16)
- 0:00Intro
- 10:38TLA Toolbox
- 18:30Workshop Introduction
- 24:58Workshop Presentation
- 25:42Formal Methods
- 26:40Everything is Broken
- 26:50Premium Car
- 28:10Unintended Acceleration
- 29:35Software
- 31:14Dont deploy on Friday
- 34:00Too complex
- 34:28Testing
- 34:57Example
- 43:07Summary
- 48:38Leslie Lamport
- 51:32What is TLA
related talks
24mKubernetes Operators: Safety First Through Model Checkers
23mNew Pattern for Sailing Multi-host LLM Inference
40mHow Terraform’s simple graph concepts deploy complex infrastructure as code
37mRoad to a self-healing infrastructure with HolmesGPT and a private LLM
42mConsensus Algorithms in Distributed Systems (Theory and Practice)
10mLightning Talk: LLM-Driven Applications: Intro to LLM Agents in Kubernetes
01h 01mTaming Infrastructure Workflow at Scale
14mReasoning Operators: Bringing LLM Logic Into Kubernetes Control Loops