TLA Plus Foundation

TLAPS Proof System

The TLA+ Proof Manager (TLAPS) is a proof system for TLA+ specifications, enabling formal mathematical proofs of system properties. It integrates with back-end provers and supports interactive proof development.

GitHub

Documentation

📖
Documentation
https://tla.msr-inria.inria.fr/tlaps/

SDKs

📦
GitHubRepository
https://github.com/tlaplus/tlapm

API entry from apis.yml

apis.yml Raw ↑ 
aid: tla-plus-foundation:tlaps-proof-system
name: TLAPS Proof System
description: The TLA+ Proof Manager (TLAPS) is a proof system for TLA+ specifications, enabling formal
  mathematical proofs of system properties. It integrates with back-end provers and supports interactive
  proof development.
humanURL: https://tla.msr-inria.inria.fr/tlaps/
tags:
- Proof System
- Formal Verification
- Mathematics
properties:
- type: Documentation
  url: https://tla.msr-inria.inria.fr/tlaps/
- type: GitHubRepository
  url: https://github.com/tlaplus/tlapm