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. The 2018 meeting consisted of tutorials that presented recent developments concerning the TLA+ language and tools, and of contributed talks.

Keynote: David Langworthy, Microsoft Research
TLA+ in Engineering Systems: Quinceañera

Dave related experience and anecdotes from 15 years applying TLA+ in a commercial software engineering environment with a look toward the future.

Contributed talks were sollicited that present work of interest to users of TLA+ or PlusCal, such as: The presentations were informal and left sufficient time for discussions. The meeting did not have formal proceedings, but videos and slides of the presentations are available on the Web.

The meeting took place in Oxford, Great Britain, on July 18, 2018, colocated with FM 2018.

Organizers: Leslie Lamport and Stephan Merz