It is sometimes necessary to add auxiliary variables to a description
of an algorithm or system to show that it implements a higher-level
The paper Auxiliary Variables in TLA+ by Leslie Lamport and
Stephan Merz is a manual on how to do that for descriptions and
specifications written in TLA+.
This page contains a link to that paper and a link to a zip
file containing the TLA+ specifications of all the examples in
The zip file contains the TLA+ source files of the
examples, their pretty-printed versions, and the toolbox directories
containing small TLC models for checking the specifications.
To run those models from the Toolbox, create specifications
for each of the following root modules:
Click here for the paper. Right-click here to download the zip file.