Boris Cherny's TLA+ tweet hit 1M views. Here's what the internet is missing.
The internet discovers TLA+. Now what?
A viral tweet from Boris Cherny introduced TLA+, a 30-year-old formal modeling language, to a massive audience. TLA+ describes possible system behaviors and temporal properties, but it only checks finite models and doesn't verify the implementation. Reasonable built an agentic pipeline that turned 16,000+ TLA+ specs into 3,000+ machine-checked Verus proofs, moving from specification to verified Rust code.
TLA+ gives us a compact language for saying what a system is allowed to do and what must always or eventually be true of it.
- morningsam
Currently-working-Nitter-instance URL for Cherny's tweet: https://shitter.thepixora.com/bcherny/status/210254334910233...
- lopatin
I would encourage everyone to try this on some self-contained, state-machine like problems, if they have them. At my company, some experts were optimizing our clustering and failover logic by adding a bit more state (and hence complexity). Despite me not being an expert in that area, I was able to find and prevent a catastrophic bug by pointing Opus armed with TLA+ at the problem. It was a bug that was not possible in the prior implementation of the system and no one thought to write unit tests for the sequence of steps that triggers it, so initially went unnoticed. The only thing that caught it was the TLA+ invariants, which, yes, were written by Opus as well.
As a side note, there's a lot of talk about programming being not fulfilling anymore. But the above exercise was probably the most fun I've had with engineering in a long time, and would have been nearly impossible for me personally without AI. Perhaps it was the novelty of the TLA+ stuff, but I think it offers a glimpse into what our jobs could actually be in the future, beyond simply telling Claude to do what you used to do manually and then clicking enter. There are much more ambitious and fulfilling use cases for it.
- stevefan1999
I indirectly use TLA+ through https://github.com/quint-co/quint. I added instructions that "before you implement any feature, please use Quint to model it and make sure no counterexample for the system as a whole, reiterate the design with Quint as well and make sure your documents and implementation follows the formal model and docs".
The result, while takes much longer, is quite magical. A lot of transaction and atomic bugs were found and fixed just by having such simple instruction alone.
However, sometimes it is not all magical especially around external resources. Cloudflare, unfortunately, sometimes have hiccups on D1 and KV with timeout, which is more or less a force majeure.
Fortunately, that means I will have to model the action as a binary event, that the transaction may not complete as we would have thought guaranteed, and by add extra guard around it, so that the state would have to be retried.
I was able to workaround it like that so far. Keep in mind the more conditions and constraints, the beefier your CPU might need since it is on the scale of NP
- listless
I can’t understand any of this. It’s saying everything and nothing at the same time. Whatever TLA+ is this article makes it sound like the most tedious and academic thing ever.
- bsenftner
Took 10 minutes to find this: TLA+ is a formal specification language developed to design, model, document, and verify reactive systems.