I was reading Hillel Wayne’s new post TLA+ Won’t Solve Everything and became fixated on one of the things he says cannot be expressed in TLA⁺:

Possibility and reachability properties: that it’s always possible to make P true, even if you don’t actually decide to. Things like “I can always shut down the computer” or “A user can always change their password”. These can’t be expressed with <>P because that’s “for all behaviors, P happens at least once”, we actually want “for all behavior prefixes, there is at least one behavior where P happens at least once”.

[Read More]

Here are my thoughts on the free online textbook Is Parallel Programming Hard, And, If So, What Can You Do About It? by Paul E. McKenney, author of the Linux kernel’s RCU synchronization mechanism. I read a lot of this textbook, got my fill, and probably won’t read more of it in the near future so wanted to write this review while it is all still fresh.

Set & Setting

Here I’ll talk about the mindset/life phase and physical setting I was in when I started reading this textbook. This might be like the tedious personal flavor preamble they have on recipe websites so skip ahead if that does not interest you.

This post stems from a recent conversation with Heidi Howard where we talked about the changing role of TLA⁺ & finite-state model checking in both research and industry. For a long time, users of TLA⁺ (or other formal specification languages like Quint) had a classic 80/20 payoff/effort choice available to them: they could either put in a large amount of effort to formally prove their system properties correct with 100% confidence, or for 20% of that effort they could model-check their system and get perhaps 80% of that confidence. This economic calculation might no longer hold. The summer of 2026 has seen fairly astonishing improvements in the field of automated theorem proving. System correctness theorems are generally shallow but broad, eschewing deep math knowledge but requiring many tedious steps. Thus people formally specifying their system have a new option, where they can pay some amount of money to various companies in exchange for a decent chance of getting an incomprehensible auto-generated correctness proof for their system properties. Assuming you trust your proof system the incomprehensibility is not such a drawback, but anyway. That isn’t what this post is about: I am interested in examining what role finite-state model checking can still play in this new world.

I’ve been a fan of security tokens for a decade now and have accrued quite a collection. This redundancy isn’t a bad thing, as security tokens are easily misplaced and the only way to recover from a lost token is using a second token that is also registered with the service you’re trying to access. I use security tokens whenever I can! SSH authentication, universal two-factor (U2F) authentication, passwordless local login, sudo command elevation, and git commit signing are all things I use security tokens for every day. When I take my laptop traveling, there also travels a yubikey. However, it took me an oddly long time to realize that I’m a relic of a bygone era. Laptops and smartphones all have built-in security tokens these days! I’ve been carrying around yubikeys when an even better one is built right into my macbook. This post is about how I use security tokens, and how I configured my laptop’s secure element to replace my yubikey collection.

Despite the title this is less a directive and more a description of what has already happened, and how I came to realize it. Still, there are many who remember StackOverflow as a revelation in the mid-2010s and think some vestige of those times remain. They think if they make an effort to distill their confusion into a question and post it there they will be rewarded. Perhaps some scarce few will, but a better way exists.

Here I’ll talk about a type of TLA⁺ contract I’ve worked on a few times, and why it didn’t work out as well as hoped. I’m not trying to torpedo other peoples’ contracts here - I just hope to share this experience so others can structure their TLA⁺ contracts differently, hopefully leading to greater success for both parties and industry usage of TLA⁺ as a whole.

The proposal

The contract proposal goes like this: a client wants to build a distributed system, and has read that TLA⁺ is effective at modeling such things. Conventional wisdom holds that it’s always cheaper to catch bugs earlier in the development pipeline, and what’s earlier than the design stage? However, they don’t have any in-house TLA⁺ knowledge and are unsure about whether they want to invest in training or hiring. Instead, they email me a proposal: could I do a short 1-3 month contract where I specify their system in TLA⁺ for them? The benefits of this setup are generally reasoned as follows:

The 2025 TLA⁺ Community Event was held last week on May 4th at McMaster University in Hamilton, Ontario, Canada. It was a satellite event to ETAPS 2025, which I also attended, and plan to write about in the near future. I gave a talk somewhat-hucksterishly titled It’s never been easier to write TLA⁺ tooling! which I will spin into a general account of the state of TLA⁺ development here. The conference talks were all recorded, so if you’d like this blog post in video form you can watch it below:

Although it isn’t usually taught that way, a lot of TLA⁺ newcomers develop the understanding that TLA⁺ is just a fancy domain-specific language (DSL) for breadth-first search. If you want to model all possible executions of a concurrent system - so the thinking goes - all you have to do is define:

1. The set of variables modeling your system
2. The values of those variables in the initial state(s)
3. Possible actions changing those variables to generate successor states
4. Safety invariants you want to be true in every state

The model checker will then use breadth-first search (BFS) to churn through all possible states (& thus execution orders) of your system, validating your invariants. If one of your invariants fails, BFS gives you the shortest execution path reaching that state. It even checks for deadlock by finding states with no possible successor states.

TLA⁺ was developed by Leslie Lamport, originator of \(\LaTeX\), so it’s unsurprising that TLA⁺ syntax looks pretty \(\LaTeX\)-y. It’s a very mathy language, with much use of symbols like (among others) \A,\E, /\, \/, and \in denoting \(\forall\), \(\exists\), \(\land\), \(\lor\), and \(\in\) respectively. The language tools include a tla2tex command to format TLA⁺ specs into \(\LaTeX\) for integration in research papers. However, research papers are not where I spend the most time looking at TLA⁺. Here’s the tale of how I brought those beautiful symbols into the code editor, and how I learned to work with others in FOSS along the way!

TLA⁺ sees a lot of use modeling distributed systems. The ability to explore all possible interleavings of events makes concurrency simple to reason about. For this TLA⁺ uses something called finite model-checking, which is really just a breadth-first search through the entire state space. The key here - and this really must be emphasized - is that the model is finite. There can’t be an infinite number of states, or of course the model checker will run forever.