This repository hosts the TLA⁺ Proof Manager TLAPM, formerly known as TLAPS. TLAPM translates TLA⁺ proof constructs into forms understood by an array of backend solvers & theorem provers, enabling machine-checked proofs of correctness for TLA⁺ specifications. TLAPM's development is managed by the TLA⁺ Foundation. For documentation, see http://proofs.tlapl.us. For information on TLA⁺ generally, see http://tlapl.us.
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 TLAPM from source.
Once TLAPM 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.tlaDocumentation is hosted at http://proofs.tlapl.us, or can be viewed locally from this repository starting at doc/web/index.html.
For instructions on building & testing TLAPM as well as setting up a development environment, see DEVELOPING.md.
We welcome your contributions to this open source project! TLAPM 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.
The following people were instrumental in creating TLAPM:
- 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)
Copyright © 2008 INRIA & Microsoft Corporation
Copyright © 2023 Linux Foundation
Licenses:
- Main codebase licensed under 2-Clause BSD
- Contents of
translatedirectory licensed under LGPL2.1+LE