Skip to Main content Skip to Navigation
Conference papers

Verifying Safety Properties With the TLA+ Proof System

Kaustuv Chaudhuri 1, * Damien Doligez 2 Leslie Lamport 3 Stephan Merz 4 
* Corresponding author
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
4 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
Abstract : TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. This paper documents the first public release of TLAPS, distributed with a BSD-like license. It handles almost all the non-temporal part of TLA+ as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties.
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Kaustuv Chaudhuri Connect in order to contact the contributor
Submitted on : Wednesday, November 10, 2010 - 3:45:59 PM
Last modification on : Friday, January 21, 2022 - 3:15:34 AM
Long-term archiving on: : Friday, February 11, 2011 - 3:13:43 AM


Files produced by the author(s)




Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. Verifying Safety Properties With the TLA+ Proof System. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. pp.142--148, ⟨10.1007/978-3-642-14203-1_12⟩. ⟨inria-00534821⟩



Record views


Files downloads