Welcome to TLA-La-Land (or An Introduction to Software Verification)
summary
Introduces the TLA+ formal specification language and model-checking to design and verify distributed systems, addressing hard problems like message ordering and exactly-once delivery in microservices. Shows how to express system designs and desired properties as invariants (abstracting low-level details) and uses a practical example to demonstrate detecting design errors and getting started with software verification.
AI-written summary · about
chapters (9)
- 0:00Formal methods intro
- 4:56Writing specs
- 10:35TLA+ action logic
- 14:28Traffic light model
- 23:13TLC model checker
- 28:09Safety and liveness
- 34:50Avoiding stuttering
- 37:15Distributed queue example
- 41:10Conclusion & Q&A
related talks
01h 13mDesigning distributed systems with TLA+
34mTLA+ at Microsoft to build planetary-scale systems
38mThe Verification of a Distributed System
48mThe Verification of a Distributed System
01h 11mWorkshop: TLA+ in action (Part 2)
01h 12mWorkshop: TLA+ in action (Part 4)
15mTLC: Temporal Logic of Distributed Components
41mDesigning software with complex configurations