GoKawiilMost engineers’ first objection to using TLA+ is, the syntax is hostile. It looks like LaTeX, not like code. But now, frontier LLMs can generate TLA+ easily. It’s still your responsibility to understand your system and define what “correctness” means, and you need a high-level understanding of temporal logic. I’ll explain temporal logic in this article. At the end I’ll show an example prompt to start a TLA+ spec with Claude.
Subscribe for new articles
A toy problem #
Here’s a classic puzzle. You have a can of beans. Each bean is white or black. The can starts nonempty. While there are at least 2 beans:
Choose 2 beans.
If they’re the same color: discard both, add 1 white bean.
If they’re different colors: discard both, add 1 black bean.
Two questions:
Can the number of beans ever reach zero? If the algorithm terminates with b = 1, what must have been true at the start?
You could think really hard. Or you could write it down in TLA+ and let a model checker answer both questions automatically. The whole point is to avoid thinking—or at least, to have a machine verify that your thinking was correct. Or convince your friends that your thinking is correct, or convince the peer-review panel for your research paper.
... continue reading