TLA+ Proofs

TL;DR

This paper explains how to write and verify proofs in TLA+ using TLAPS, demonstrating the process with Peterson's mutual exclusion algorithm and highlighting tools for managing complex proofs.

Contribution

It introduces the TLA+ proof system TLAPS and illustrates its features and usability with a practical example, enhancing proof management for complex systems.

Findings

TLAPS effectively verifies TLA+ proofs.

The Toolbox aids in managing large proofs.

Practical example demonstrates proof process.

Abstract

TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual exclusion algorithm as a simple example to describe the features of TLAPS and show how it and the Toolbox (an IDE for TLA+) help users to manage large, complex proofs.