Learning TLA+ (original) (raw)

| Leslie Lamport Last modified on 25 October 2024 | | | --------------------------------------------------- | |

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.

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.

A Book About TLA

A final draft of a book titled A Science of Concurrent Programs about TLA, the logic underlying the TLA+ language. It is for computer scientists and for users of TLA+ who want to understand its mathematical foundation and the rationale that underlies the language.

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.