Other Relevant Work
Last modified 16 April 2018
This page contains links to pages outside the TLA+ and TLAPS web sites
that are related to TLA. Most of the sites listed are old, and
there are undoubtedly more recent sites that should be here. If
you'd like links to your work added to this page, contact us.
- Large Scale Model Checking 101
- This is a video by Markus Kuppe giving practical advice on
using the TLC model checker for checking large models.
Dated April 11, 2018.
- A TLA+ Workshop
- These are the slides of talks and the submitted papers from
a TLA+ workshop that was held in Paris on 27 August 2012 in conjunction
with the FM 2012 conference.
- A page containing several papers on TLA by Stephan Merz, as well as
a link to
Merz's encoding of TLA in the higher-order logic of the generic interactive
theorem prover Isabelle. (That page includes a machine-checked proof
The Dagstuhl RPC-Memory Example.)
- Work With and On Lamport's TLA .
- Publications by
the Networks and Distributed Systems group at the University of
Bielefeld, headed by
Peter Ladkin. They are all dated 1996 and 1997, but at least
some of them are still worth reading.
Tools for TLA based specifications
- This page describes work done in the early 1990s at the
of Dortmund, Department of Computer Science by the
Computer Networks and Distributed Systems group
headed by Dr. Heiko Krumm.