Choose the language by what breaks in your system: TLA+ and Quint describe behavior step by step, Alloy describes objects and the links between them. Quint reads like ordinary code, TLA+ and Alloy like formulas. Use Quint for product rules over time, TLA+ for strict proofs, Alloy for the structure of data and access rights.
How TLA+, Alloy and Quint differ: one task, three languages
All three languages share one idea: the rules of a system are written apart from the code, and a program itself looks for a violation in them. If there is one, it shows how to reach it. This is model checking, and each language has its own notation and its own checking program. TLA+ was created by Leslie Lamport for describing concurrent and distributed systems. Alloy was created in the Software Design Group at MIT. Quint was designed as a modern alternative to TLA+ for engineers.
Summary: TLA+, Alloy and Quint side by side
The main difference is what exactly they describe. TLA+ and Quint describe the behavior of a system step by step: cart, payment, order, and what can go wrong between steps. This is how race conditions and lost data are found. Alloy describes structures and links: who reports to whom, who has which rights. It looks for a small example where a rule is broken, for instance an employee with two bosses. The other differences follow from this.
| TLA+ | Alloy | Quint | |
|---|---|---|---|
| What it describes | the behavior of a system step by step, especially concurrent and distributed | objects and the links between them and how they change | behavior step by step, as in TLA+ |
| Notation | mathematical | relational logic | looks like ordinary code |
| What checks it | TLC or Apalache | the Alloy Analyzer, which finds structures for the constraints | TLC or Apalache, with a quick random simulation |
| What it shows | a chain of steps to the violation | an example of a structure where the rule is broken | a chain of steps to the violation |
| Maturity | since 1999, more books and examples | since 1997, its own community | since 2021, younger |
| Who it suits | those who need strict guarantees | those who design data and access rights | product teams without a math background |
How to read the table row by row. “What it describes” is the most important: the choice depends on it. “Notation” sets the entry step: Quint has the lowest, with TLA+ and Alloy you have to get used to formulas. “What checks it” reminds us that the languages rely on different checking programs: Apalache and TLC both fit TLA+ and Quint, while Alloy has its own analyzer. “What it shows” explains what you get at the output: a chain of steps or an example of a structure. “Maturity” hints where there are more examples and more people to ask.
The border between the languages is not absolute. In version six Alloy added mutable state and temporal logic, that is, it learned to describe steps in time too. And Quint and TLA+ can be used for data structures. So the choice is set by what breaks more often in your system: the order of events or the structure of links.
How TLA+ differs from Alloy
TLA+ was created by Leslie Lamport, and it rests on the idea that the best way to describe things precisely is simple mathematics. It looks for the chain of steps on which a rule breaks, for example a double payment and two orders. Alloy looks for an example of a structure instead of a chain, and checks properties of a model by building counterexamples. Take TLA+ for the order of events and Alloy for links and access rights.
How TLA+ differs from Quint
They describe the same thing, and only the notation differs. Quint is designed as a syntax that suits engineers, and the same programs check both notations. TLC goes through states one by one, while Apalache is symbolic and considers all chains up to a given length.
How Alloy differs from Quint
Alloy has its own checking program: the Alloy Analyzer takes the constraints of a model and finds structures that satisfy them. Quint has no such program of its own, and two other programs check it, TLC and Apalache. So the choice often comes down to what breaks: links between objects or the order of steps.
What to choose: TLA+, Alloy or Quint
Product rules over time and a team without maths: take Quint. You need strict proofs for a complex distributed system: take TLA+ and set aside time to learn it. You need to check the structure of data or access rights: take Alloy. Ideas from one notation can be carried to another, because the rules stay the same. How Quint relates to test engines such as Jest and QUnit is covered in the article Quint vs QUnit and TLA+, and examples of the errors it finds are in the article on race conditions and lost data.
FAQ
TLA+ describes the behavior of a system step by step and looks for the chain of steps where a rule breaks. Alloy describes objects and the links between them and looks for an example of a structure where a rule is violated.
They describe the same thing, and only the notation differs: Quint looks like ordinary code, while TLA+ uses mathematical notation. The same programs check both notations, TLC and Apalache.
For product rules over time and a team without maths, take Quint; for strict proofs about a complex distributed system, TLA+; for the structure of data and access rights, Alloy.
TLA+ and Quint are checked by TLC and Apalache. Alloy has its own analyzer, Alloy Analyzer, which takes the constraints of a model and finds structures that satisfy them.