The TLA⁺ Proof System

This repository hosts what is collectively called the TLA⁺ Proof System, or TLAPS. It consists of the TLA⁺ Proof Manager tlapm that interprets TLA⁺ proofs & manages their state, as well as interfaces to automatic backend provers such as SMT solvers like Z3, the tableau prover Zenon, the Isabelle/TLA⁺ object logic, and the LS4 decision procedure for propositional temporal logic.

TLAPS development is managed by the TLA⁺ Foundation. For documentation, see http://proofs.tlapl.us. For information on TLA⁺ generally, see http://tlapl.us.

Installation & Use

Past versioned releases can be downloaded from the GitHub Releases page. For the latest development version, download the builds attached to the 1.6.0 rolling pre-release or follow the instructions in DEVELOPING.md to build TLAPS from source.

Once TLAPS is installed, run tlapm --help to see documentation of the various command-line parameters. Check the proofs in a simple example spec in this repo by running:

tlapm examples/Euclid.tla

Documentation is hosted at http://proofs.tlapl.us, or can be viewed locally from this repository starting at doc/web/index.html.

Developing & Contributing

For instructions on building & testing TLAPS as well as setting up a development environment, see DEVELOPING.md.

We welcome your contributions to this open source project! TLAPS is used in safety-critical systems, so we have a contribution process in place to ensure quality is maintained; read CONTRIBUTING.md before beginning work.

Authors

The following people were instrumental in creating TLAPS:

• Kaustuv Chaudhuri (@chaudhuri)
• Denis Cousineau
• Damien Doligez (@damiendoligez)
• Leslie Lamport (@xxyzzn)
• Tomer Libal (@shaolintl)
• Stephan Merz (@muenchnerkindl)
• Jean-Baptiste Tristan (@jtristan)
• Hernán Vanzetto (@hvanz)

License & Copyright

Copyright © 2008 INRIA & Microsoft Corporation
Copyright © 2023 Linux Foundation

Licenses:

• Main codebase licensed under 2-Clause BSD
• Contents of translate directory licensed under LGPL2.1+LE