Last updated 13 January 2018. Beginner-friendly (hopefully!) resources for learning TLA+/personal reading list. This leans heavily on Leslie Lamport's TLA homepage.
- Hyperbook: Downloads as a .zip; last updated August 2015
"This is the start of a hypertext "book" containing two tutorials: Principles of Concurrent Computing and Specification of Concurrent Systems. The tutorials are two tracks that share much text--especially at the beginning. Both tutorials are based on TLA+. The Principles track, which I hope will eventually be suitable for an undergraduate course on concurrent computing, will mainly use the PlusCal algorithm language rather than TLA+ for describing algorithms. There is also a TLA+ Proof track that explains how to use the TLAPS proof system."
- TLA video course: Video course that assumes basic programming knowledge and some math. Downloads and complete transcripts are available; last updated December 2017.
- Specifying Systems: By Leslie Lamport; link to order through publisher or download for personal use (license details at the download page).
- Learn TLA website
- TLA+ Toolbox is the IDE that Learn TLA recommends
- Dr. TLA+: Lectures on algorithms and TLA+ implementation
- TLA+ in Practice and Theory: Four-part video lecture series on math and design principles/concepts used in TLA+
- Leslie Lamport at Heidelberg
"An algorithm is not a program, so why describe it with a programming language? PlusCal is a tiny toy-like language that is infinitely more expressive than any programming language because an expression can be any mathematical formula."
- Leslie Lamport at Microsoft: "Thinking Above the Code"
- Don Knuth: "The Analysis of Algorithms"
- Learning PlusCal