Verifying Safety Properties with the TLA+ Proof System

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz

Abstract

TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs. The TLA+ proof language is declarative, and understanding proofs requires little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. Proofs are written in the same language as specifications; engineers do not have to translate their high-level designs into the language of a particular verification tool. A proof manager interprets a TLA+ proof as a collection of proof obligations to be verified, which it sends to backend verifiers that include theorem provers, proof assistants, SMT solvers, and decision procedures.

© Springer-Verlag 2010

Available as: PDF

Reference

@InProceedings{chaudhuri:tlaps,
  author =       {Kaustuv Chaudhuri and Damien Doligez and Leslie Lamport and Stephan Merz},
  title =        {Verifying Safety Properties with the TLA\textsuperscript{+} Proof System},
  booktitle = {5th Intl. Joint Conf. Automated Reasoning (IJCAR 2010)},
  pages =     {142-148},
  year =      2010,
  editor =    {J{\"u}rgen Giesl and Reiner H{\"a}hnle},
  volume =    6173,
  series =    {Lecture Notes in Computer Science},
  address =   {Edinburgh, UK},
  publisher = {Springer},
}