The TLA+ Video Course
Last modified 16 August 2017
This is a work in progress that consists of the beginning of a
series of video lectures to teach programmers and software engineers
how to write their own TLA+ specifications. It assumes a basic
understanding of programming concepts. Some knowledge of
elementary mathematics, such as might be taught in a beginning
university math course for computer scientists, would also be
A Word of Warning
These videos are not light entertainment.
They require careful viewing and actual thinking.
You may often stop videos to digest what you've just seen, and
perhaps to skip back and view it again.
To accompany the videos, coffee will be better than popcorn.
The lectures can be watched on the Web. However, people with
slow network connections might prefer to download lower resolution
versions of the videos and watch them off-line.
Instructions on how to do that are given
The script of each video is also provided.
It contains everything shown and said on the video, except for shots
of the author.
It can be useful for the hearing impaired, viewers who want to review
a lecture, and people who hate videos.
However, the html file that displays the video may be needed to download
- Introduction to TLA+
Explains what TLA+ is and why you might want to use it.
It introduces the concept of a state machine.
- State Machines in TLA+
Shows how a simple state machine is described in TLA+,
giving the first glimpse of a TLA+ specification.
- Resources and Tools
Describes resources for learning about TLA+.
Explains how to download the Toolbox and shows how
to use it to open a spec, view the pretty-printed version,
and run TLC on it.
- Die Hard
We save the lives of two Hollywood action heroes.
On the way, you will start learning to write
TLA+ specs and checking them with the parser and with TLC.
- Transaction Commit
Commitment, in marriage and
database transactions, is specified. You also
how to use mathematical functions in specifications.
- Two-Phase Commit
How commitment is achieved, in marriage and database
transactions. You also learn about records in TLA+
and some more about using TLC.
- Paxos Commit
Specifies a real fault-tolerant algorithm
for committing database transactions. It explains a few
mathematical operations for constructing and combining sets.
Before watching any lecture off-line, download
and extract its contents into a folder. Let's suppose you name the
That folder should then contain
tlavideo.js and the folder
To watch a lecture off-line, download the lecture's video file and
zip file, which will have the same first names, into the
Let's suppose those files are named
Extract the contents of
One of the extracted files will
(For most lectures, the zip file will contain only that file.)
To view the video, open a Web browser on this html file.