Introduction to TLA+ Model Checking in the Command Line

Marianne Bellotti
Jan 18, 2019 · 7 min read

Otherwise known as “wait, you mean I can use the TLA toolbox from the command line?”

I started playing around with TLA+ and its more programmer friendly variant PlusCal about a year ago. At that time the amount of documentation that was understandable to people like me who do not enjoy reading white papers full of mathematical notation was slim to none. (Today you can buy Hillel Wayne’s excellent book Practical TLA+) So I started reading other people’s code (errr…specs) and began piecing together some idea of how things were done.

TLA+ is a tool to model and verify concurrent systems, finding bugs in them before you have written any code by testing every possible combination of inputs. You might say “well how is that different from fuzzing inputs in more conventional functional tests?” and the answer is because TLA+ also simulates the kind of timing issues commonplace with distributive or concurrent systems. As microservices continue to dominate conversations about modern architecture, the question of what happens when a service sends a request that never arrives or arrives before something else has finished or gets repeated become more and more relevant. TLA+ allows you to test for these scenarios.

Beyond that it’s a radically different way of thinking about computer programs. It’s not a programming language so one has to abandon certain mental crutches and really think about how we represent what we mean. You can write an excellent model and then write code that doesn’t actually do things the way the model is describing. So you have to think about how your favorite frameworks and libraries actually do what they do.

I’m a huge fan of anything that might bring unvocalized assumptions up to the surface where people can explore them. It’s hugely difficult to build a complex system of services if two teams are not in sync about their assumptions.

The best way to think of TLA+ is like drawing a blueprint for software you’re going to build. I’ve seen people use it to test algorithms, but I’ve also seen people use it to model user flows throughout an application.

However the Toolbox is Awful

When you’re ready to test your models in TLA+ virtually every resource will direct you to the TLA+ Toolbox. The toolbox is a java application that looks a bit like it’s supposed to be an IDE and allows you to translate PlusCal into TLA+, configure models, test them and explore errors. Its UX is awful, simply awful. How you open a TLA file in the toolbox is not intuitive, things will often fail without any errors (or rather the toolbox will do what you’ve told it to do, which is nothing because you needed to click some buttons you didn’t click first). It’s literally exhibit A for why software developers should respect the skills of designers on their teams.

On top of that I find it a little clunky. I generally don’t work with full scale IDEs if I can avoid it. I prefer the stripped down elegance of TextMate, Sublime or Atom. Sometimes this means I miss out on valuable features, but I’m a person who currently has over thirty tabs open in Chrome, three projects open in TextMate and at least one WiP up in Scrivener…. I like to use my computer’s memory, okay? This is a light day.

At some point while I was noising around other people’s TLA+ specs to try to understand the language I realized that there seemed to be command line versions of the key tools from the toolbox. Rather than open up the toolkit I could compile PlusCal and test my models from my terminal and even more exciting … from other scripts.

Wait… there’s a command line version?

Yup! If you’ve downloaded the TLA+ toolbox, you already have the command line tools installed on your computer. To configure them there’s a helpful set of shell scripts you can download here.

One of the first things I did with this knowledge was build a little proof of concept python application that parsed other python programs and tried to write models in PlusCal based on what they were going to do. I wanted to learn more about bytecode and AST and this seemed like a fun way to do it. It was partially successful in that I could write a few simple programs that became working models, but eventually I hit a wall trying to learn two new things at the same time.

But the potential of command line interfaces is still the same. If model checking can be executed via command line, then it can be executed by other programs. You can update your models and test them automatically the same way you might do with other forms of testing in continuous integration.

pcal: Translating PlusCal to TLA+

Once you have installed and configured the command line toolbox, you can start translating PlusCal comments in your specs to TLA+ using the pcal command.

Note that pcal will assume the extension .tla so you can leave it off if you want. For the sake of clarity I will include it.

The basic command is:

Unlike command line tools you might be used to pcal is very particular about order of arguments. The name of the file you want to translate should always be last, any flags should come before it.

-version does something that might be unexpected. Rather than telling you the version of pcal you have installed, it lets you pick which version of PlusCal the translator will assume it’s translating (this currently goes up to 1.8)

If you want to see the AST for your PlusCal you can use the -writeAST flag to forego the rest of the translation just to output the AST.

This is super useful tool but not without its bugs. For example, I understand that-spec and -spec2 are supposed to let you choose between version 1 and 2 of TLA+, but I’ve never been able to get them to work.

Defining Models with Configuration files

If you’re used to the Toolbox interface, you’re probably wondering how you can configure your invariants and other test cases. The answer is the .cfg file automatically generated for you by the pcal command.

Normally it will look like this:

But there are a variety of parameters you can set before checking your models. The most useful of these areINVARIANT and PROPERTY which specify which invariants and which temporal properties to test respectively.

Here’s a full list of all the possible configuration settings

I have not been able to figure out what the difference between the singular form of the parameter (eg CONSTANT) and the plural form of the parameter (eg CONSTANTS) is. Both can take multiple values if separated by a space. It might be that there’s some backwards compatibility issue involved here but…. ¯\_(ツ)_/¯

Make sure you add your custom configuration below the line. If you put them above that comment line, pcal will overwrite them every time you translate.

tlc: Checking the Models

Now it’s time to run the model checker! Like pcal the .tla extension is optional. The basic command looks like this:

And this will produce the following output:

This tells you what modules were imported and how many states the model has. If you’re curious the actual spec we’re running here is the wire transfer example in Hillel Wayne’s book. That particular spec has a temporal property that we know will be violated by the algorithm. This is what that looks like:

If you are already familiar with the Toolbox, this looks pretty much like the output you’d see before, expect without the highlighting.

By default tlc stops at the first invariant error. If you’d like it to continue, you use the flag -continue. In general tlc's options are split into two types: MODE-SWITCHES and GENERAL-SWITCHES. Mode switches change how the models are run, from switching from breadth-first to depth-first, to picking a seed number for randomization. General switches allow you to specify different configuration files, how much detail is printed to stdout.

I hope this is enough to get you started. I will update this post from time to time as I figure out more about how the tools work. Happy Model Checking!

Because software is eating the world

Marianne Bellotti

Written by

Software Safety
Marianne Bellotti

Written by

Author of Kill It with Fire Manage Aging Computer Systems (and Future Proof Modern Ones)

Software Safety

How do we build software that is safe? Exploration of formula specifications, safety science and algorithm ethics. Header art courtesy of

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store