Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS

Igor Konnov, Markus Kuppe, Stephan Merz

Abstract Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their complementary strengths and weaknesses, we suggest a workflow that supports different types of analysis and that can be adapted to the desired degree of confidence.

Available as: PDF
The accompanying TLA+ specifications are available on GitHub.

Reference

@InProceedings{konnov:trifecta,
  author =       {Igor Konnov and Markus Kuppe and Stephan Merz},
  title =        {Specification and Verification with the {TLA\textsuperscript{+}} {Trifecta}: {TLC, Apalache, and TLAPS}},
  booktitle = {11th Intl. Symp. Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2022)},
  year =      2022,
  editor =    {Tiziana Margaria and Bernhard Steffen},
  volume =    13701,
  series =    {Lecture Notes in Computer Science},
  pages =     {88--105},
  address =   {Rhodes, Greece},
  publisher = {Springer},
}