Learning TLA+ and Model Checking

This page lists some external resources one could use to learn more about TLA+ and related topics.

First things first:

1. Setup your IDE. Visual Studio code with tlaplus plugin tlaplus plugin is recommended.
2. If you have questions or if you feel stuck at any point, reach out to the community.

Then as good kickstart to TLA+, start with Leslie Lamport — The Paxos algorithm or how to win a Turing Award. Part 1 and Part 2. It is a good introduction on TLA+ and uses Paxos and Consensus as an example.

After that, you can start digging into Lamport’s video course available on the website. If you prefer a written medium, Specyfing systems: by Leslie Lamport is still the reference book for TLA+ and its tools. It’s well written and easy to follow.

After learning some TLA+, it might be helpful to start learning some Pluscal. Checkout the pluscal page for more info and some resources.

Don’t just learn the theory, start by solving some small exercises.

• The Specification Language TLA+: Another good manuscript by Stephan Merz explaining TLA+ specification language: Sect. 2 introduces TLA+ by way of a first specification of the resource allocator and illustrates the use of the tlc model checker. The logic TLA is formally defined in Sect. 3, followed by an overview of TLA+ proof rules for system verification in Sect. 4. Section 5 describes the version of set theory that underlies TLA+, including some of the constructions most frequently used for specifying data. The resource allocator example is taken up again in Sect. 6, where an improved high-level specification is given and a step towards a distributed refinement is made. The fnal Sect. 7 contains some concluding remarks.

A collection of resources about TLA+ can be found on the awesome-tla+ repository. Feel free to contribute with your useful links.