TLA+ can't check what it can't express
What TLA+ can and can't check
Boris Cherny's claim that Claude Opus used TLA+ to find race conditions has sparked excitement about formal verification. But TLA+ has limits: it can't express reachability properties (like proving a game is winnable), hyperproperties (like energy-saving mode always uses less power), or properties over multiple steps or real time. While hacks like auxiliary variables and self-composition exist, they're messy and don't compose well. TLA+ is great for invariants and liveness, but not a silver bullet for agentic coding.
To verify a property, we need to have a property to verify! So what are the properties that TLA+ can't even express?
- sourdecor
I discovered Quint[0] due to this comment[1] on HN. Quint is "an executable specification language [which works in JavaScript] with delightful tooling based on the temporal logic of actions (TLA)". I think it is awesome and anybody interested in TLA+ should check it out.
- singron
I love this. This is great to read if you are trying to use TLA+ for something.
In a different vein, another thing TLA+ isn't great at is modeling atomics and in particular weak-memory semantics or anything that's not sequentially consistent. If you translate your algorithm to pcal, it will run as if it was sequentially consistent. If you need to model non-sequential-consistency, then that needs to be spelled out with explicit logic to TLA+, which is probably too complicated and error-prone to do by hand. The C/C++/Rust memory models permit a lot of wacky stuff. I imagine you need to add read caches and writeback buffers for each variable with cache-flushing instructions at appropriate points, but maybe there is a more elegant way to do it.
If you use rust, miri and loom both have analyzers that can check some non-sequentially-consistent behavior (and loom doesn't actually implement sequential-consistency at all).
- adamddev1
Great write-up. People keep saying "we can just write tests" or more recently "we can use formal verification," thinking these are sufficient safeguards we can use and then relegate all the implementation to LLMs. But the fact is that probabilistic guessing machines can't save them. People can't escape the need to actually understand the things they are building.
- rrook
i think part of this is a shortcoming of our programming languages. generally, languages allow for the expression of partial graphs, which makes the verification problem technically challenging. my take is that a language that only exposes closed-graph semantics could help bridge the gap between the model and the implementation, even if not absolute.
- metabagel
Love the inline footnotes!