Learning TLA+

Leslie Lamport

Last modified on Thu 23 December 2021 at 17:45:03 PST by lamport -->

You'll miss a lot on this web site unless you enable Javascript in your browser.

The TLA+ Video Course

A series of video lectures on TLA+ that assumes only a basic understanding of programming concepts.  Most beginners will find this the best way to learn TLA+.  However, it does not discuss PlusCal.  Useful TLA+ operators not described in the videos are explained here.

The PlusCal Tutorial

This is a 14-session tutorial that teaches how to write and check algorithms in PlusCal.  It assumes only a basic understanding of programming concepts. 

Here is some additional material about PlusCal.

Hillel Wayne's Web Site and Book       [show]

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:
C-Version        P-Version

Papers About PlusCal       [show]

The TLA+ Book 

A book titled Specifying Systems 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.

The TLA+ Hyperbook  

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.

The TLA+ Google Group

You can use this group to communicate with members of the TLA+ community, including the maintainers of the tools.  Post a message if you have a question, want to report a bug, or just want to tell us what you're doing with TLA+.  The easiest way to post a message is to send email to x@googlegroups.com where x should be replaced by tlaplus