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.
There is also a summary of TLA+ which may be helpful for reference as you are getting started.
- 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.
- 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.