Skip to Main content Skip to Navigation
Conference papers

A TLA+ Proof System

Abstract : We describe an extension to the TLA+ specification language with constructs for writing proofs and a proof environment, called the Proof Manager (PM), to checks those proofs. The language and the PM support the incremental development and checking of hierarchically structured proofs. The PM translates a proof into a set of independent proof obligations and calls upon a collection of back-end provers to verify them. Different provers can be used to verify different obligations. The currently supported back-ends are the tableau prover Zenon and Isabelle/TLA+, an axiomatisation of TLA+ in Isabelle/Pure. The proof obligations for a complete TLA+ proof can also be used to certify the theorem in Isabelle/TLA+.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Wednesday, November 12, 2008 - 3:48:00 PM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM
Long-term archiving on: : Monday, June 7, 2010 - 10:54:18 PM


Files produced by the author(s)


  • HAL Id : inria-00338299, version 1
  • ARXIV : 0811.1914



Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. A TLA+ Proof System. Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar. ⟨inria-00338299⟩



Record views


Files downloads