Notes from Leslie Lamport’s video Introduction to TLA+.
What is TLA+?
A language for high-level modeling of critical parts of digital systems. It was created for concurrent and distributed systems and can help find design errors before writing code.
Its tools include:
- TLC: the model checker.
- TLAPS: the TLA+ proof system.
- TLA+ Toolbox: an IDE for writing specifications and running the tools.
The main takeaway for me is abstraction: learning to focus on the parts of a system that matter for understanding its behavior.
The hard part of learning to write TLA+ specs is learning to think abstractly about the system.
— Brannon Batson, quoted in the video
State machines
- A state is an assignment of values to variables.
- A behavior is a sequence of states.
- A state machine specifies the possible initial states and which states can follow any given state.
The goal is to check that the system satisfies the required properties in every allowed behavior.
More material
- The TLA+ Video Course, by Leslie Lamport.
- How Amazon Web Services Uses Formal Methods, on how AWS adopted TLA+.
- TLA+ Foundation.
- TLA+ GitHub organization.