Specification and Verification with the TLA+ Trifecta: TLC, Apalache, and TLAPS

TL;DR

This paper discusses the use of TLA+ tools—TLC, Apalache, and TLAPS—for specification and verification, demonstrating their combined strengths through an example and proposing an adaptable workflow.

Contribution

It introduces a comprehensive workflow integrating multiple TLA+ tools for varied analysis depths, enhancing verification flexibility.

Findings

The tools have complementary strengths and weaknesses.

An example with Safra's distributed termination detection illustrates their use.

A flexible workflow supports different analysis levels.

Abstract

Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their complementary strengths and weaknesses, we suggest a workflow that supports different types of analysis and that can be adapted to the desired degree of confidence.