TLC -- The TLA+ Model Checker

Leslie Lamport and Yuan Yu
Microsoft Research
Mountain View, California

Last modified 20 January 2003

TLC is a model checker for specifications written in TLA+. TLA+ is a specification language based on TLA, the Temporal Logic of Actions. See the TLA web page for general information about TLA.

A description of TLC and directions for using it, along with an introduction to writing specifications in TLA+, are contained in Specifying Concurrent Systems .

The Current Version

The version of TLC available from the Microsoft Research download site is

     TLC Version 2.0 of 17 January 2003

See the main TLA+ tools page for how this version differs from the version described in Specifying Concurrent Systems .

Installing and Running the Current Version

TLC is available for Windows or Unix. See the main TLA+ tools page for instructions on how to obtain, install, and run TLC. To try it out, download the "supporting material" from the web page for Specifying Concurrent Systems . Look for any specification that has a configuration (.cfg) file and run TLC on it.