Introduction to formal validation with TLA+ and Pluscal

Formally validating an algorithm ensures that the design does not contain any logical errors. For small algorithms, it is fairly simple to keep track of all possible states of the system. However, when concurrency and non-determinism added by the network are taken into account, it is not possible to keep track of all possible states of the system.

Formal verification is the process of proving the correctness of a system against a formal specification and properties, using formal mathematical methods. There are different types of formal verification, some of which can be used to verify algorithms, others to verify implementations.

There is a notable difference between formal verification and formal validation, which are often associated with each other. Validation ensures that the specified product meets the requirements, while verification ensures that the product complies with the specifications.

For this introduction, I will focus on formal validation, more specifically on TLA+, which uses model checking, exploring all possible states of a system to verify properties.

TLA+

TLA+ (Temporal Logic of Action) is a language used to model programs or systems, particularly concurrent and distributed programs or systems. This tool, created by Leslie Lamport, is based on the idea that the best way to describe a system accurately is to use simple mathematics. It is a formal verification tool that can detect fundamental design errors.

TLA+ is based on set theory and defines a system or program as a set of possible states of the system and a set of transitions between these states. TLA+ is written in a formal language of logic and mathematics. The precision required of specifications written in this language makes it possible to detect design errors before implementation.

TLA+ itself is rather complex, especially when you start trying to model programs with numerous transitions. TLA+ also has a syntax that is unfamiliar to developers, which makes it quite difficult to learn.

TLA+ is extremely expressive and allows you to describe the functioning of an algorithm or system with great precision. But this expressiveness is its main drawback because, in order to start writing proofs, you need a great deal of knowledge and practice with the language. Modeling an algorithm in pure TLA+ is much more time-consuming, both in terms of learning the language and the tool, and in terms of writing the specification.

PlusCal

To simplify this task for developers, Leslie Lamport created PlusCal¹, a specification language that compiles to TLA+. PlusCal is more similar to imperative programming².

PlusCal is much less expressive than TLA+, which makes it easier to use. PlusCal was designed to be written like pseudo code, with two syntaxes, one similar to C and one similar to Pascal. This allows developers who are comfortable with these syntaxes to learn how to write specifications more quickly.

There are several important concepts in PlusCal. It is an “algorithmic” language, meaning that an algorithm is described using states and transitions between these states. Each PlusCal specification contains only one algorithm and is single-process, meaning that it has only one execution thread. In order for the algorithm to have multiple concurrent execution threads, you need to add what are called processes.

A process is an algorithm that will be executed by a defined number of threads. Each process can have between 1 and N threads, and there can be several different processes in an algorithm.

For example, in a video compression service, we can imagine a process that downloads a video and places it in a buffer, a process that retrieves a video from the buffer, compresses it, and saves it. We can represent this service by an algorithm with two processes, each with a defined number of threads. The advantage of proving an algorithm like this would be to verify that the buffer never overflows and that there are no concurrency issues when reading and writing to the buffer.

Fairness in PlusCal

Before modeling an algorithm, there is something crucial to determine: how a program chooses which next state to choose. The algorithm defines the steps that can be chosen, but does not certify that the algorithm will choose to change states. We must therefore define the fairness with which transitions between states occur.

There are two types of fairness: weak fairness and strong fairness.

1. Weak fairness states that if transition A is possible at all times, then this transition must occur.
2. Strong fairness states that if transition A is possible, even if it is not possible many times, then this transition must occur.

PlusCal allows fairness to be defined at the state, process, or algorithm level. PlusCal and TLA+ can therefore be used to model systems or programs, and the TLC Model Checker can be used to verify these specifications. It creates a finite state model from the TLA+ specifications to verify the system.

The system is composed of the algorithm variables and all processes and their variables. In a system state, we find the state of each process, its variables, and the state of the algorithm variables.

TLC constructs the system state graph starting from the initial state. It then traverses all possible transitions from this initial state and continues recursively until all possible paths have been explored. The possible transitions from a state are constructed by TLC, evaluating all possible scenarios, for example, a transition through different processes that advance in its state graph.

TLC therefore allows us to start from a single state graph of a process, which is simple for a human to model, to the set of transitions of the system, to the graph of accessible states of the entire system, taking into account each process and each variable, which is simple for a computer to deduce. So the more processes we put into competition, the more the number of states and the number of transitions increases.

And it is when creating this graph of accessible system states that TLC will verify the modeling against the specification.

What does TLC verify?

TLC verifies three things:

It verifies that there is no deadlock; a deadlock situation is when a state has no transition to exit that state. Note that a deadlock is different from a planned end to the program.

It checks for invariants; an invariant is a mathematical formula that must be true for every possible state of the system (for example, for our single-writer database, an invariant is that the number of open write transactions on a database is less than or equal to 1).

It checks properties; this is a temporal property that is true for each execution of the system (using the same example, a property is that every user who wants to open a write transaction must eventually succeed).

Learning TLA+ and formal modeling

Resources for learning TLA+ and formal modeling can be found on the internet. Leslie Lamport offers an interactive website with several very interesting resources.

1. The TLA+ Video Course is a 10-chapter course, each containing a video and exercises. I highly recommend this resource, even though PlusCal would suffice for your use case. This course allows you to think differently about interactions in a program, abstracting away the exact implementation and focusing on its design.

2. The PlusCal Tutorial is an 11-chapter course, with each chapter featuring a text-based explanation and questions and answers to ensure comprehension. This course provides an overview of PlusCal syntax and all its possibilities.

To gain a deeper understanding of Leslie Lamport’s programming design, I also recommend this presentation by Leslie Lamport at Stanford in 2024.

I also find Hillel Wayne’s resources very interesting, particularly this blog post on the subject of message queue representation in TLA+. He is also responsible for the website (https://learntla.com) [https://learntla.com], which presents TLA+ from a different angle than Leslie Lamport’s, allowing for a more in-depth understanding.

I practiced formal validation, TLA+, and PlusCal during my time at Dassault Systèmes. I wrote specifications to validate algorithms and validated these algorithms, using the above resources to train myself.