This volume contains the papers presented at the TLA⁺ Community Meeting 2018 held on July 18, 2018 in Oxford, as part of FLoC, the Federated Logic Conference.

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.

The TLA⁺ Community Meeting is 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 program of the 2018 edition consists of a keynote presentation by David Langworthy on his experience in applying TLA⁺ in a commercial software engineering environment, a tutorial by Markus Kuppe on techniques for fighting state space explosion when using TLC, and six contributed talks that present interesting case studies or the development of tools that complement the existing TLA⁺ tools. Further information on the meeting is available from its Web page at http://tla2018.loria.fr/.

We are grateful to the organizers of FLoC 2018 for providing the infrastructure for organizing the meeting and their help with preparing it.