Proofs and Proof Certification in the TLA + Proof System.

TLA + is a specification 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 + specifications. 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 different 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 first give an overview of the overall design of tlaps and its proof language and then focus on proof certification in tlaps. Since the use of different 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 certification, 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 confidence in the soundness of tlaps. 1 The TLA + proof language TLA + [4] is a specification 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 [2, 3] has been designed as an interactive proof assistant for deductively verifying TLA + specifications. Designed to be independent of any particular theorem prover, it is based on a hierarchical proof language. As a simple example of the TLA + proof language, let us consider the proof of Cantor’s theorem. Given the definitions 1