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.

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

I love TLA+ to describe systems precisely yet succinctly and reason about them. But as someone who's been using formal methods to help software development for many years, this whole industry around tools to connect such a wonderful mathematical language and others like it, like Lean, with AI, to the point of hiding the reasoning from people, confuses me.

Proving programs correct end-to-end (i.e. code to high-level properties) - as this company and others purport to do - is so difficult that humans have only been able to do it for very small programs (~10KLOC) and even then, in very specialised cases, where the programs have been written in an extra-simple way (often at the cost of performance, because performance often requires more complicated algorithms). If AI becomes at least an order of magnitude more capable than humans at software development, which is what will be required for this task, would it need our help to write various tools and harnesses that help with the task? After all, writing these tools is so much easier than using them for that goal that I don't understand the hypothesis behind AI capability here.

This company says: they're "developing the agentic frameworks to make these correctness guarantees accessible to all software engineers". But developing all that is the easy part! If AI can do the hard part, why does it need our help to make this accessible, it can surely find a way to do that easy part itself! It's like saying, "Soon we'll have a machine that can harness so much energy to boil an ocean; we've built a service that lets you order a taxi to take the machine to the beach!" Why would an AI that is so much better than us at writing software need our help writing any kind of software for it?

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.

Real world applications of TLA+: https://foundation.tlapl.us/industry/index.html.

The Intel paper shows how TLA+ was applied as a step prior to writing the hardware description. I'm not sure if it caught on, it seems like other tools are used nowdays, does anyone here in the VLSI industry know?

17 mentions of “TLA+” before defining the acronym.

Took 10 minutes to find this: TLA+ is a formal specification language developed to design, model, document, and verify reactive systems.

TLA is pretty excellent for the job it does. In the past, the general issue with tools like this has been keeping the implementation code in sync with the model. Implementing verification tests from model across to the implementation can be tedious and very time consuming.

Now that we have assistants that excel at tedious and time consuming tasks, it’ll be interesting to see if the dominant approach is still using dedicated modeling languages like TLA+ with generated verification harnesses. Or if it’s easier to use something closer to the implementation, similar to what the Stateright project [1] is trying to do.

[1] https://github.com/stateright/stateright

Currently-working-Nitter-instance URL for Cherny's tweet: https://shitter.thepixora.com/bcherny/status/210254334910233...

Take a writing class. This was painful to read.

the jump from reading examples to writing a useful invariant is still the hard part

See:

https://news.ycombinator.com/item?id=48287718

With link to pdf, github

If you don't even check what you're formalizing you must REALLY trust the agents.

I guess if they found real verifiable bugs then it's good

Time to discover communicating sequential processes instead :P

the secret's out, but I think I'm still in a minority which has alloy models in addition to TLA+ ones

If the article's author's writing is this bad, imagine how they write software... shudder.

I did a lot of distsys work With tla+. I still think it’s the best use. It’s really hard to make sure your code matches what you prove.

The header is buggy.

most annoying post I've read