The TLA+ Video Course
Last modified 14 May 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
The lectures can be watched on the web. However, people with
slow network connections might prefer to download lower resolution
versions of the video and watch them off-line.
Instructions on how to do that are given
- 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.
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.