Important dates

to be announced


TLA+ is a formal language for specifying systems that is used in academia and industry. Tool support for TLA+ is provided through the TLA+ Toolbox, an Integrated Development Environment for writing TLA+ specifications and analyzing them using the TLA+ tools. The tools include the TLC model checker, the PlusCal algorithm language and translator, and the TLA+ Proof System.

Members of the TLA+ community exchange online via the TLA+ Google group. The TLA+ Community Meeting is intended as a forum where practitioners and researchers interested in the use and further development of the TLA+ specification language and its associated tools meet and discuss. It will consist of tutorials that present recent developments concerning the TLA+ language and tools, and of contributed talks.

Contributed talks are sollicited that present work of interest to users of TLA+ or PlusCal, such as:

The presentations should be informal and leave sufficient time for discussions. There will not be formal proceedings, and presentations of relevant work published elsewhere are welcome.

Proposals for presentations, with a short (1-2 page) abstract summarizing the content, are invited to be sent to

The workshop will take place in Oxford, Great Britain, on July 18, 2018, colocated with FM 2018.

Organizers: Leslie Lamport and Stephan Merz