Important dates

submission: April 15
notification:   May 15
workshop: July 18


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.

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

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

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 by April 15, 2018. Please indicate if you want to give a short or long presentation (20 or 40 minutes, plus discussion). Notification will be given by May 15, 2018. The abstracts and presentations given at the event will be made available on the Web.

The meeting will take place in Oxford, Great Britain, on July 18, 2018, colocated with FM 2018. Participants are required to register through the FLoC 2018 Web site. Note that FLoC organizes a workshop dinner on July 18. Participants at the TLA+ Community Event are welcome to attend.

Organizers: Leslie Lamport and Stephan Merz