A series of video lectures on TLA+ that assumes only a basic understanding of programming concepts. It does not discuss PlusCal.
The LearnTLA Web Site This web site, written and maintained by Hillel Wayne, is a beginning course in PlusCal. It covers just about all of PlusCal's programming-like constructs, but not all of the TLA+ mathematical operators that can be used in PlusCal expressions. There are currently a number of minor problems with this course, plus one major one. A PlusCal algorithm can be written in either of two syntaxes; the book uses the P syntax, while most engineers will prefer the C syntax. I hope these problems will eventually be corrected.
Practical TLA+ This links to a web page about a book by Hillel Wayne that provides a good complete course on PlusCal. The page contains a link to the book and my detailed comments on it.
The PlusCal Manual [show]
PlusCal has two syntaxes: a C-syntax similar to that of C-based languages like C# and Java, and a P-syntax similar to that of older languages like Pascal. Most users will prefer the C-syntax. There are versions of the manual for both:
Papers About PlusCal [show]
A book that you can download. It contains a complete description of TLA+ and the TLC model checker as of 2002 when it was published, which was before the Toolbox was developed. There have been changes to the TLA+ language since then--the major ones being the addition of recursive operator definitions and of constructs for writing proofs. All the changes are described here. A 7-page "cheat sheet" extracted from the book summarizes the TLA+ language and definitions from its standard modules.
This is a hypertext book that I intended to be the way to learn TLA+ and PlusCal, until I realized that people don't read anymore and I made the video course. It's unfinished, but it still provides a good introduction to TLA+, PlusCal, and the TLAPS proof system.