Automatic verification of TLA+ proof obligations with SMT solvers

Abstract. TLA+ is a formal specification language that is based on ZF set theory and the Temporal Logic of Actions TLA. The TLA+ proof system tlaps assists users in deductively verifying safety properties of TLA+ specifications. tlaps is built around a proof manager, which in-terprets the TLA+ proof language, generates corresponding proof obli-gations, and passes them to backend verifiers. In this paper we present a new backend for use with SMT solvers that supports elementary set theory, functions, arithmetic, tuples, and records. Type information re-quired by the solvers is provided by a typing discipline for TLA+ proof obligations, which helps us disambiguate the translation of expressions of (untyped) TLA+, while ensuring its soundness. Preliminary results show that the backend can help to significantly increase the degree of automation of certain interactive proofs.