TLA+ Community Meeting 2023
Saturday, April 22, 2023
Paris, France

Invariants in Distributed Algorithms

Annie Liu, Scott D. Stoller, Saksham Chand, Xuetian Weng

Computer Science Department, Stony Brook University

We will discuss making invariants explicit in specification of distributed algorithms. Clearly this helps prove properties of distributed algorithms. More importantly, we show that this helps make it easier to express and to understand distributed algorithms at a high level, especially through direct uses of message histories. We will use example specifications in TLA+, for verification of Paxos using TLAPS, as well as complete executable specifications in DistAlgo, a high-level language for distributed algorithms.