Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+1 to find race conditions in code.
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.
(This assumes some basic knowledge of TLA+. If you're a total beginner, check out those [1] [2] things above or read here.)
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+.
