Proofs and Proof Certication in the TLA+ Proof System

Second International Workshop on Proof Exchange for Theorem Proving

Stephan Merz

Others  :  http://ceur-ws.org/Vol-878/invited2.pdf
PID  :  43481

来源: CEUR

【 摘 要 】

TLA+ is a specication language originally designed for specifying concurrent and dis- tributed 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+ specications. 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 dierent back-end provers. The current release, restricted to non-temporal reasoning, includes Isabelle/TLA+, an encoding of the set the- ory 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 certication in tlaps. Since the use of dierent back-end provers raises legitimate concerns about the soundness of the integration, we expect back- end 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 certication, 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