Supplementary material on the design of TLAPS

The TLA+ Proof System is developed at the Joint Centre of Microsoft Research and Inria in Saclay. The main home page is here; it contains the links for downloading TLAPS as well as documentation relevant for users. This page collects supplementary information of use for developers, on the design of TLAPS and some of its back-end provers.

The SMT Backend

The SMT backend is the main workhorse of TLAPS and is by default called first on every proof obligation. Its design is described in the papers listed below, and more details appear in Hernán Vanzetto's PhD thesis. A variant of the backend can be used to produce input in TPTP-FOF format for use with automated first-order provers such as E or Spass. The translation from TLA+ set theory to (possibly multi-sorted) first-order logic relies on rewriting rules documented here.

Some case studies demonstrating the reduction in proof size obtained thanks to the SMT backend are also available:

[ Memoir | Paxos ]

References
  1. Stephan Merz, Hernán Vanzetto. Automatic Verification Of TLA+ Proof Obligations With SMT Solvers. 18th Intl. Conf. Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18). © Springer, LNCS 7180, pp. 289-303 (2012). [PDF | Springer Link]
  2. Stephan Merz, Hernán Vanzetto. Encoding TLA+ into Many-Sorted First-Order Logic. 5th Intl. Conf. Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016). © Springer, LNCS 9675, pp. 54-69 (2016). [PDF | Springer Link]
  3. Stephan Merz, Hernán Vanzetto. Refinement Types for TLA+. 6th Intl. Symp. NASA Formal Methods (NFM 2014). © Springer, LNCS 8430, pp. 143-157 (2014). [PDF | Springer Link]
  4. Hernán Vanzetto. Proof Automation and Type Synthesis for Set Theory in the Context of TLA+. PhD thesis, Université de Lorraine, 2014.

The Isabelle Backend

Isabelle/TLA+ is a faithful encoding of the set theory of TLA+ as an object logic in the proof assistant Isabelle. Pretty-printed versions of the Isabelle theories making up the encoding are available here. The sources of the Isabelle theories are part of the TLAPS distribution and are therefore not replicated here.
Stephan Merz