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).
- metabagel
Love the inline footnotes!