Verifying Safety Properties With the TLA+ Proof System

TL;DR

This paper introduces TLAPS, a proof system for TLA+ that facilitates the mechanical verification of safety properties, supporting hierarchical proofs and various backend verifiers, and is suitable for formal safety verification.

Contribution

It presents the first public release of TLAPS, enabling formal verification of safety properties in TLA+ with support for hierarchical proofs and multiple backend verifiers.

Findings

Handles most non-temporal TLA+ proofs

Supports safety property verification like invariance and step simulation

Distributed with an open-source license

Abstract

TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. This paper documents the first public release of TLAPS, distributed with a BSD-like license. It handles almost all the non-temporal part of TLA+ as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties.