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
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.
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.
TLA+ is a specific kind of formal verification framework for software. The overall idea is that you can "prove" that some software works, rather than the typical "seems like it works" we aim for.
But under the covers, all formal verification schemes are (imho) best viewed as "very fancy testing". There are a few kinds of this fancy testing. TLA+ is the kind that can auto-generate all the relevant test cases for your code (there's more to it than that, but this definition works for now). So now instead of "I wrote a bunch of test cases, all that I could think of, and they pass" you have "I used TLA+ so I know I'm exercising all the possible test cases and they pass".
Here's the problem though: to achieve that trick, you have to write your code in a special language (TLA+). It isn't a tool that can be just pointed at regular production code.
So what you get to "prove" is a translation of your actual code into TLA+ code. It may be possible to auto-translate one to the other (I asked the original author if they did that, but no reply yet). Usually it's a manual process.
Therefore you have "proof" but not quite as you know it, because you proved something different than what runs. But still more useful than a wet finger raised into the wind.
For this reason it's typically only used on narrow risky pieces of code (quorum voting is the canonical use case).
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?
We are all good as long as we are all in agreement that vibe-coded TLA+ is just a tool for the agent to do better work, not something that magically proves the code is "correct" in a useful sense
Hahaha this is so funny... people here get slammed all the time of using AI for writing and here be, just someone writing his way through Internet history and gets slammed for it just the same... you can't hardly win with an audience like this... haha
If the author threw this into Claude to add some load-bearing similes to their unedited monologue, it would only make it more insufferable to anyone complaining about it now.
I've always thought CSP as a robust design pattern where you have no shared state between components and they must communicate with each other using message passing. It also requires synchronous communication (rendezvous-style). If you follow those rules you can have a pretty robust system. Aside from these abstract rules, CSP has more formal research (algebra) but I'm not sure if there are any decent tools available.
TLA gives you a full toolbox and in theory can model whatever you can express. That's very different from a design pattern.
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.
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
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
* It will brute force all states.
* You can add a variety of assertions.
TLA+ is a specific kind of formal verification framework for software. The overall idea is that you can "prove" that some software works, rather than the typical "seems like it works" we aim for.
But under the covers, all formal verification schemes are (imho) best viewed as "very fancy testing". There are a few kinds of this fancy testing. TLA+ is the kind that can auto-generate all the relevant test cases for your code (there's more to it than that, but this definition works for now). So now instead of "I wrote a bunch of test cases, all that I could think of, and they pass" you have "I used TLA+ so I know I'm exercising all the possible test cases and they pass".
Here's the problem though: to achieve that trick, you have to write your code in a special language (TLA+). It isn't a tool that can be just pointed at regular production code.
So what you get to "prove" is a translation of your actual code into TLA+ code. It may be possible to auto-translate one to the other (I asked the original author if they did that, but no reply yet). Usually it's a manual process. Therefore you have "proof" but not quite as you know it, because you proved something different than what runs. But still more useful than a wet finger raised into the wind.
For this reason it's typically only used on narrow risky pieces of code (quorum voting is the canonical use case).
No wonder GitHub keeps going down.
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?
I guess if they found real verifiable bugs then it's good
TLA gives you a full toolbox and in theory can model whatever you can express. That's very different from a design pattern.
https://news.ycombinator.com/item?id=48287718
With link to pdf, github