Workshop: TLA+ in action (Part 1)
summary
Workshop builds a TLA+ specification of Safra’s EWD998 termination detector, iterates from a token-free counter to the token+count version, and exercises the toolchain: Gitpod TLA+ IDE and the TLC model checker. Early runs yield 16 then ~80k states; for N=6 TLC generates ~14 million states (260k distinct, diameter 19) until a pending<3 constraint bounds unbounded counters. Demonstrates catching off‑by‑one and design gaps, refining the spec until termination detection holds for small N.
AI-written summary · about
chapters (11)
- 0:00Introduction and setup
- 5:32Workshop format and theory
- 10:43What is TLA+ and use cases
- 15:43The algorithm problem
- 17:38Developing the solution
- 22:29Specifying the solution
- 27:16Writing the TLA+ spec
- 35:23Defining system actions
- 40:57Initial state and structure
- 47:06The next-state relation
- 56:49Model checking and breaks
related talks
41mDesigning software with complex configurations
01h 13mDesigning distributed systems with TLA+
32mTLA + specification of PCR parallel programming pattern
15mTLC: Temporal Logic of Distributed Components
43mWeeks of Debugging Can Save You Hours of TLA+
31mTurning an Incident Report into a Design Issue with TLA+
42mWelcome to TLA-La-Land (or An Introduction to Software Verification)
18mSmart Casual Verification of the Confidential Consortium Framework