TLA+ is a speci cation language originally designed for specifying concurrent and distributed systems and their properties. It is based on Zermelo-Fraenkel set theory for modeling data structures and on the linear-time temporal logic TLA for specifying system executions and their properties. The TLA+ proof system (tlaps) has been designed as an interactive proof assistant for deductively verifying TLA+ speci cations. Designed to be independent of any particular theorem prover, it is based on a hierarchical proof language. A proof manager interprets this language and generates proof obligations corresponding to leaf proofs, which can be discharged by di erent back-end provers. The current release, restricted to non-temporal reasoning, includes Isabelle/TLA+, an encoding of the set theory underlying TLA+ as an object logic in the proof assistant Isabelle, the tableau prover Zenon, and a back-end for SMT solvers. This article will rst give an overview of the overall design of tlaps and its proof language and then focus on proof certi cation in tlaps. Since the use of di erent back-end provers raises legitimate concerns about the soundness of the integration, we expect backend provers to produce proofs that can be checked by Isabelle/TLA+, our most trusted back-end, and this is currently implemented for the Zenon back-end. I will review our experiences with proof certi cation, and to what extent it has contributed to avoiding soundness bugs, and will indicate future work that we intend to carry out in order to improve our con dence in the soundness of tlaps.
theorem Cantor = 8S : :9f 2 [S ! subset S ] : Surj (f ; subset S ) proof h1i1: assume new S ;
9f 2 [S ! subset S ] : Surj (f ; subset S ) prove false h2i: pick f 2 [S ! subset S ] : Surj (f ; subset S )
obvious h2i2: :Surj (f ; subset S ) h3i1: define D = fx 2 S : x 2= f [x ]g h3i2: D 2 subset S
obvious h3i3: D 2= Range(f )
by def Range h3i4: qed
by h3i2; h3i3 def Surj h2i3: qed
by h2i2 h1i2: qed by h1i1 where subset S denotes the powerset (the set of all subsets) of S . A hierarchical proof of that theorem appears in Figure 1. Proof steps carry labels of the form hd in, where d is the depth of the step (which is also indicated by indentation in the presentation of the proof), and n is a freely chosen name|in the example, steps at any given level are just numbered. There are many di erent ways to write any given proof; in fact, Cantor's theorem could simply be proved by one of the automatic proof backends available in tlaps. The user chooses how to decompose a proof, starting a new level of proof that ends with a qed step establishing the assertion of the enclosing level. Assertions appearing at the leaves of the proof tree are considered trivial enough to be passed to the automatic provers of tlaps.
Step h1i1 reformulates Cantor's theorem as a sequent (TLA+ sequents are written as assume . . . prove . . . ) that assumes given some set S for which there exists a surjective function from S to subset S , in order to prove a contradiction. Step h i 1 2 deduces the assertion of the theorem from that sequent. (In general, proofs of qed steps are written before the proofs of the steps that precede it.) The level-2 proof starts by picking some such surjective function f and then shows that it cannot in fact be surjective|hence h i 2 3 deduces a contradiction. The main argument of the proof appears in the level-3 step, which de nes the diagonal set D S , which can by de nition not be in the range of f .
The proof of Cantor's theorem shows some of the main features of the TLA+ proof language. Hierarchical structure is the key to managing complexity. All proof obligations that appear in a proof are independent of one another and can be elaborated and veri ed in any order. In general, facts and de nitions to be used to establish leaf proof steps must be cited explicitly in order to keep the search space for the automatic proof backends manageable.
In our experience, the proof language scales well to large proofs. tlaps is integrated into the TLA+ Toolbox, an Eclipse-based IDE that provides features to help reading and writing hierarchical proofs. In particular, proof levels can be hidden or expanded selectively, and the results of proof checking are indicated by color coding. The prover also maintains a database of ngerprints of proof obligations in order to remember what it has already proved previously| even if the proof has been reorganized, or if a step has been deleted and reinserted. 2
Proof checking in TLAPS users will check the proof only at the very end, after proof development has nished. The proofs that Zenon produces are detailed and can be checked without any signi cant proof search. We suspect that checking SMT proofs could become more problematic because SMT solvers can handle much larger formulas that may lead to correspondingly larger proof traces. Techniques for compressing SMT proofs by transforming them in order to avoid redundant steps are then likely to be of interest.
We have yet to nd our rst Zenon bug. However, certain transformations carried out by the proof manager are critical for soundness, and these should also be checked. The operations of the proof manager fall into two categories. First, it maintains the context of the current proof step, including the symbols that are currently declared and the facts and hypotheses that can be used. The proof language has a block structure with clear scoping rules, and therefore errors in this part can in general be avoided by enforcing a clear program structure.
Secondly, the proof manager is responsible for eliminating references to state variables in (non-temporal) TLA+ formulas. State variables appear in formulas describing state and transition predicates, such as x > c or x > c ^ x 0 = x 1 where x is a state variable and c is a constant.2 Such formulas are evaluated over pairs of states, with the convention that unprimed variable occurrences denote the value of the variable in the rst state, and primed occurrences in the second state. If P is a state predicate (i.e., a formula without free primed state variables), the notation P 0 refers to a copy of P where all state variables have been replaced by their primed versions, so (x > c)0 is x 0 > c. Similarly, for any transition predicate A, the notation enabled A denotes A with existential quanti cation over all primed state variables, so3 enabled (x > c ^ x 0 = x 1) 9x 0 : x > c ^ x 0 = x 1
Since backend provers implement standard rst-order logic and do not know about state variables, they handle x and x 0 as two unrelated rst-order variables, and the proof manager must expand notation such as the above. Although this is not di cult as long as de nitions are completely expanded, it is easy to get the translation wrong in the presence of unexpanded de nitions, in the case of more complicated expressions such as (enabled A)0, or when expressions appear in argument positions of operators. The soundness of these transformations should therefore be checked by the trusted backend Isabelle/TLA+ of tlaps, and indeed we have already seen errors in our implementations of these operations. However, this requires a proper de nition in Isabelle not only of the set theory underlying TLA+, but also of the notions of state, state variables, and state and transition expressions. 3
Conclusion tlaps is based on a hierarchical proof language that results in a clear proof structure and enables independent checking of the di erent proof obligations that arise in a proof. From a logical point of view, TLA+ proof trees correspond to natural-deduction proofs. The language is interpreted by the proof manager that tracks the context, computes the proof obligations, and translates them to the input formats of backend provers. tlaps provides an option for retrieving proof traces produced by the backends and having them certi ed by Isabelle/TLA+, 2The category of each symbol appearing in a TLA+ module is declared in the header part of the module. 3Semantically, the state predicate enabled A holds in a state s if there is some state t such that A holds over the pair (s; t). a faithful encoding of the TLA+ set theory as an object logic in the proof assistant Isabelle. This is currently implemented for the tableau prover Zenon, and we plan to extend proof certi cation to the SMT backend. However, in our experience, it is much more likely that a proof is meaningless because of some error in the underlying speci cation than because of an error in one of the backends. Moreover, the proof manager implements some transformations that are critical for the overall soundness of the system, and these are currently not checked. In the near future, we plan to extend tlaps for supporting temporal reasoning, and in particular the veri cation of liveness properties, and this will pose new challenges for proof certi cation. Acknowledgement The development of tlaps is a joint e ort carried out at the Joint Microsoft Research-INRIA Centre in Saclay. Kaustuv Chaudhuri, Denis Cousineau, Damien Doligez, Leslie Lamport, and Hernan Vanzetto contributed to di erent aspects of the work reported here.