A TLA+ Proof System

Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz

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 \tlatwo proof can also be used to certify the theorem in Isabelle/TLA+.

LPAR 2008 Workshop Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA 2008).

Available as: PDF

Reference

@InProceedings{chaudhuri:proof,
    Author       = "Kaustuv Chaudhuri and Damien Doligez and Leslie Lamport and Stephan Merz",
    Year         = 2008,
    Title        = "A {TLA\textsuperscript{+}} Proof System"
    Editor       = "Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and
                    Konev, B. and Schulz, S.",
    BookTitle    = "{Proc. of the LPAR Workshop Knowledge Exchange:
                    Automated Provers and Proof Assistants (KEAPPA'08)}",
    Place        = "Doha, Qattar",
    Series       = "CEUR Workshop Proceedings",
    Number       = "418",
    Pages        = "17--37",
    URL      = "http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-418/",
}