// HACKER NEWS — CYBERSECURITY
What TLA+ can and can't check
Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+1 to find race conditions in code.
And now everybody on the internet is talking about formal verification.
As a long-time educator (1 2) and advocate of TLA+, this is really exciting! TLA+ is great at designing complex concurrent systems and making sure they're bug-free.2 As a long-time advocate of level-headedness, this new euphoria worries me. I read a lot of people saying that formal methods will solve the problem of agentic software development once and for all, and that's nonsense.
Enough words have been spilled about the weaknesses of TLA+ in terms of what it can guarantee, like how correct designs don't automatically translate into correct code. So I'd like to focus on a different limitation for this newsletter: to verify a property, we need to have a property to verify! So what are the properties that TLA+ can't even express?
(This assumes some basic knowledge of TLA+. If you're a total beginner, check out those [1] [2] things above or read here.)
TLA+ divides the system into a set of behaviors. Each behavior is a sequence of states, like "light one is green, then yellow, then red". In each state we can express a regular boolean expressions like "Light four is green" or "All lights are red." We can also modify expressions with three "temporal" logical operators:
When we say that P is a property of the system, we mean it is true in the initial state of every behavior. So if we check the property []P, that means that []P is true in every initial state, and then by the definition of "always" means that P is true in every future state from that initial state, meaning it is true in every state of every behavior. We call this an invariant, and is one of the most foundational properties we check in TLA+.
We can also compose [] with primes to get action properties, or change variants. [](x' >= x) is true if the new value of x is always greater than equal to the old value of x. Another fun one is [](P => P'): once P is true, it can never become false again. The actual TLA+ is a little more complicated because of a thing called "stutter-invariance", but that's extra details. Action properties and invariants are both safety properties, which roughly means "something bad never happens". I wrote an article on safety and liveness here.
Liveness, btw, is "something good always happens". All liveness properties are based off of <>. By itself, <>P just means "P is true in at least one state of every behavior", which is usually too weak to be a good system property. But with composition, we can make more interesting liveness properties:
There's a couple of other operators, like ENABLED and <>_v, which open up other tricks, but the majority of the stuff we check are invariants, action properties, and liveness. And refinement, which is a combination of safety and liveness and a topic unto itself.