Proofs in TLA+: Theory and Practice

Jael Kriener

The temporal logic of actions (TLA) is a specification language for concurrent and distributed computation, together with a suit of tools to reason about them. In particular the TLA proof system (TLAPS) allows users to proof safety and liveness theorems interactively.

The emphasis in the TLA+ project is very much on pragmatic usability and industrialisation; hence, TLA is very expressive (ZFC + multi-modal logic). The challenges in developing a sound and practical proof system for it are manifold.

The most ambitious application project for TLAPS to date is the verification of determinacy in a real time kernel, which we are currently undertaking with our partners at the French Commissariat à l’énergie atomique et aux énergies alternatives (CEA).

In this talk, I will give an introduction to specifying systems and verifying properties with TLA and TLAPS. Depending on time and audience interest I will then go into details on the theoretical aspects and the challenges we face in implementing TLAPS and/or on our project with CEA.