Learning Material
Getting Started
The best way to start learning TLA+ is with the TLA+ Video Course, which is actually very engaging. Then read the first 80 pages of the Specifying Systems book, which is somewhat less engaging, but very helpful. The official repository of TLA+ learning material can be found here.
Note: there’s also a language that compiles into TLA+ called PlusCal. It is slightly less powerful (and in fact you may need to use TLA+ expressions inline); however, it looks more like a programming language.Practical TLA+ is a good book if you want to learn it. I’m sure it’s sufficiently powerful to work the examples on this site. AWS uses both TLA+ and PlusCal for different algorithms. However, as PlusCal compiles to TLA+, understanding TLA+ is generally considered a good idea, regardless of which one you use.
The TLA+ Language Manual for Engineers provides a semi-comprehensive guide to the TLA+ language.
The Learn TLA Website has both TLA+ and PlusCal information. It is less comprehensive, but somewhat more accessible, than the TLA+ Language Manual for Engineers.
There is also a summary of TLA+ which may be helpful for reference as you are getting started.
Advanced Concepts
Want structured learning?
- Specifying Systems: Pages 81-227: Advanced but well-explained examples
- Weeks of Debugging Can Save You Hours of TLA+ (Video)
- Blocking Queue
- Using TLA+ in the Real World to Understand a Glibc Bug
- TLA+ in Practice and Theory: Provides both mathematical and historical context for TLA+. It is also an accessible but deep explainer to some of TLA+’s key concepts.
Know what you’re looking for?
- TLA+ Examples Repository: Highly advise you read each algorithm along with a paper or explainer, to correlate concepts to code.
- Advanced Concepts from TLA+ Website: Provide references for very specific parts of TLA+.
- Specifying Systems: Pages 228-End. Basically a reference manual.