Skip to content

tlaplus/tlapm

Folders and files

NameName
Last commit message
Last commit date
Dec 6, 2024
Aug 24, 2024
Aug 22, 2024
May 4, 2024
Jan 2, 2025
Feb 1, 2022
Aug 21, 2024
Feb 26, 2024
Jan 11, 2025
Jan 7, 2024
Jan 2, 2025
Jan 2, 2025
Feb 7, 2024
Sep 17, 2024
Sep 17, 2023
Aug 26, 2024
Mar 17, 2020
Jan 6, 2025
Mar 17, 2020
Dec 2, 2024
Dec 5, 2024
Dec 2, 2024
Dec 4, 2024
Dec 5, 2024
Jun 8, 2023
Nov 4, 2024
Nov 21, 2019
Mar 17, 2020
Nov 4, 2024
Jun 25, 2023
Dec 2, 2024

The TLA⁺ Proof Manager (tlapm)

Build & Test

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.

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 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.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 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.

Authors

The following people were instrumental in creating TLAPM:

License & Copyright

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

Licenses: