Viral TLA+ tweet has Reasonable preview agents that turned 16,000 specs into 3,000 machine-checked proofs

Real world TLA+ examples sit at foundation.tlapl.us/industry. The Intel paper applied TLA+ as a step before writing the hardware description, though from what I hear VLSI mostly uses other tools these days.

Latest I saw on the hardware side was Simon Jantsch of Siemens speaking on temporal specification languages at the ETAPS 2025 industry day, mostly proprietary symbolic model checkers for LTL. TLA+ is basically a successor to LTL, and LTL is still in use.

It took me 10 minutes to dig up a definition. TLA+ is a formal specification language for designing, modeling, documenting and verifying reactive systems. The post buries that fact.

I gave up partway through. Take a writing class, this was painful to read.

People here slam AI writing and then slam a person writing his way through internet history the exact same way. You can't win with an audience like this.

17 mentions of TLA+ before anyone defines the acronym. Bit ironic given what TLA stands for.

I use TLA+ indirectly through Quint. My instruction is: before implementing any feature, model it in Quint, confirm no counterexample for the system as a whole, then keep the docs and implementation aligned with the model. Much slower, but it caught a pile of transaction and atomicity bugs on its own. The messy case is Cloudflare D1 and KV timeouts, which I model as a binary outcome where the transaction may simply not complete, then guard the state so it retries.

The hard part for me is still the jump from reading examples to writing a useful invariant.

I did a lot of distsys work with TLA+ and still think that is its best use. What is really hard is making sure your code matches what you proved.

I can't follow any of this. It says everything and nothing at the same time, and it makes TLA+ sound like the most tedious and academic thing ever.

Plain version: you define initial states and every possible state transition, it brute forces all states, and you attach assertions to check. That is the loop.

My regular engineer take: TLA+ is fancy testing that auto-generates all the relevant cases, but you have to write the code in a special language and prove a translation of your real code. The translation is usually manual, so you get a proof of something that is not quite your production code.

I encourage anyone with self-contained, state-machine style problems to try this. I pointed Opus with TLA+ at our clustering and failover logic and found a catastrophic bug in a state sequence nobody wrote unit tests for. The TLA+ invariants, written by Opus too, were the only thing that caught it.

Hint: if you have a UI, especially a nontrivial SPA, expect to be humbled at what TLA+ can surface there.

I had Astra add TLA+ and Lean verification tests to a project with complex state and many small agent-generated algorithms. It surfaced 33 classes of bugs, several with multiple instances, plus bugs in widely used libraries and a Rosetta 2 Intel emulation bug that was affecting me.

If you don't even check what you are formalizing you must really trust the agents. I guess if they find real verifiable bugs then it is good.

Agreed on the framing. Vibe-coded TLA+ is just a tool that helps the agent do better work. It does not magically prove the code is 'correct' in any useful sense.