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.
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.
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?
The last I learned of this was at the talk Temporal specification languages in industrial hardware verification by Simon Jantsch of Siemens at the ETAPS 2025 industry day track. Unfortunately I can't find the video posted anywhere, but predominantly the talk spoke of using proprietary symbolic model checkers for Linear Temporal Logic (LTL). It is reasonable to call TLA+ a successor to LTL, although LTL is definitely still used.
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 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).
This makes sense to me but if I continue with the "fancy testing" analogy it seems like there is no accounting for interactions beyond the system itself: it has perfect unit and integration testing but only for a myopic amount of global state.
I am curious about the limits of what one can expect this language to solve and therefore the types of programs/domains to which it is more/less suited. Why is determining quorum the canonical use case?
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 had a similar experience having Astra add TLA+ and Lean verification tests to a project with somewhat complex state and many small algorithms (almost all generated by coding agents). The system had been working quite well, but adding formal verification surfaced 33 classes of bugs, some of which had several instances.
I completely agree with you about how fun these things can be. I've long believed in automated testing methods that were beyond what I could justify. I learned about formal methods in college in the 1980s and have never been able to justify (even to myself) applying them. Now a volunteer project I've been working on has 100% standard test coverage, many property-based tests, and 1000s of formal verification tests. That combination has surfaced multiple bugs in widely used underlying libraries and a bug in Rosetta 2's Intel emulation that was affecting me. And that's all just on the testing front. I'm having a lot of fun with all this.
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
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 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?
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).
This is not true. It has been done. I’ve seen it done for an entire OS too. Humans are very capable of doing this. The issue is this is seldom done practically speaking because the effort is not worth the benefit when the program becomes too complex.
For simple programs and small domains it’s worth it. For example type checking. Type checking proves one aspect of your program (the types) is fully correct.
If you're talking about seL4, it is tiny and intentionally simplified. I'm not aware of programs larger than ~10KLOC that have ever been verified end-to-end.
I have long being fascinated by the the field and curious about it on an amature level, i took some basic proof verification and distributed computing classes back in the grad school days, but I'm clearly not an expert in the field by any means. From the article, it seemed like there are plenty of "traps" that i did not even consider - starting from lean hatches like assume(false), expressive power of TLA+ (CTL, ATL), and ofc challenges of tying an real implementation to a proof. To me all three of the above seem challenging enough to deserve their own tools, and i would appreciate smart people putting effort into addressing these rough edges.
Question to you: i can understand how proof verification like z3 or lean requires a special language and an inference engine; given that model checkers like tla+ are mostly about exploring possible program states and checking properties of such states and chains of states, i do not quite understand why it can't be done with a conventional imperative language to express state transitions and invariants - especially an interpreted one like python (esp with continuation support) or a language targeting a vm like wasm where one should be able to snapshot program state?
The state space you get when using real programming languages like Python is much, much larger than the one you get when abstracting your system design into TLA+. Thus when testing real systems you can only explore very small portions of the state space. This is a real thing people do, although it isn't yet widespread - the term to look for is deterministic simulation testing. Making a DST harness that can handle exploring an application state space without requiring large modification to the application itself is very challenging. Currently Antithesis are the only ones I know who have done it (disclaimer: no connection to this company, I just think they are very cool).
TLA+ is not a model checker. It's a general language for writing mathematics, akin to Lean, only Lean focuses on high mathematics while TLA+ focuses on dynamic systems. There are a proof checker and at least one model checker that work on subsets of TLA+.
As to why TLA+ is better at describing systems than programming languages, the reason is that it's much more general. It can say things like "a routine that sorts in a quadratic number of steps or less" rather than a specific sorting algorithm, and it allows stating (and proving) that a specific sorting algorithm matches that description or not. Most TLA+ formulas are too abstract to be compiled or run (i.e. they describe too many potential algorithms).
For me the barrier to proving the "hard bits" was never that I couldn't reason about it—I quite enjoyed formal methods in school, and when introduced to them by coworker's who'd done similar—but it was that I didn't have the time to dedicate to learning enough about how to model my problem in a particular new language or system when none of my coworkers were spending such time and my boss wasn't already convinced.
The AI tools are great at lowering the learning curve by changing "how would I possibly express this" to "ah, let's see if this expression of it is actually right?" and "hm, is there a simpler way to express the same thing?"
Like StackOverflow for javascript questions, but for an area that was far to obscure to have a good library of example answers.
I'm not looking to prove the entirety of every system. Usually just some core bits. And often not connected automatically to the code (which may not be gonna change much).
Time to discover communicating sequential processes instead :P
That stuff gets rediscovered all the time, the latest example probably being golang
wait this is new to me so is this like a different kind of tla?
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.
I am learning TLA+ but I do not know CSP, is CSP better?
They’re completely unrelated. The GP was making a joke.
Nah, jump straight to pi-calculus.
See:
https://news.ycombinator.com/item?id=48287718
With link to pdf, github
Take a writing class. This was painful to read.
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
You can be bad at writing with or without AI.
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.
Yep. Unreadable
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?
The last I learned of this was at the talk Temporal specification languages in industrial hardware verification by Simon Jantsch of Siemens at the ETAPS 2025 industry day track. Unfortunately I can't find the video posted anywhere, but predominantly the talk spoke of using proprietary symbolic model checkers for Linear Temporal Logic (LTL). It is reasonable to call TLA+ a successor to LTL, although LTL is definitely still used.
Took 10 minutes to find this: TLA+ is a formal specification language developed to design, model, document, and verify reactive systems.
TLA+ is what unit testing looks like when a mathematician designs it.
It takes about 5 seconds to open Wikipedia and type "TLA+".
The LLMs used to write these things, do not start by using empathy and a theory of whats in other peoples minds.
It reminded me of zombo.com but more like a slop version.
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
17 mentions of “TLA+” before defining the acronym.
Which is ironic and funny given the other common use of those letters.
The header is buggy.
most annoying post I've read
the jump from reading examples to writing a useful invariant is still the hard part
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.
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.
* You define initial states and all possible state transitions.
* It will brute force all states.
* You can add a variety of assertions.
Here's my regular engineer explanation:
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).
This makes sense to me but if I continue with the "fancy testing" analogy it seems like there is no accounting for interactions beyond the system itself: it has perfect unit and integration testing but only for a myopic amount of global state.
I am curious about the limits of what one can expect this language to solve and therefore the types of programs/domains to which it is more/less suited. Why is determining quorum the canonical use case?
This is misleading. Testing and formal verification are vastly different.
Four-letter acronyms or longer.
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 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.
hint: if you have an UI, you might be surprised what TLA+ can do for you. if you have a nontrivial SPA, expect to be humbled.
Do you happen to have any intuition pump here? Any term of art or class of tests to throw LLMs at to get a sense for these?
I had a similar experience having Astra add TLA+ and Lean verification tests to a project with somewhat complex state and many small algorithms (almost all generated by coding agents). The system had been working quite well, but adding formal verification surfaced 33 classes of bugs, some of which had several instances.
I completely agree with you about how fun these things can be. I've long believed in automated testing methods that were beyond what I could justify. I learned about formal methods in college in the 1980s and have never been able to justify (even to myself) applying them. Now a volunteer project I've been working on has 100% standard test coverage, many property-based tests, and 1000s of formal verification tests. That combination has surfaced multiple bugs in widely used underlying libraries and a bug in Rosetta 2's Intel emulation that was affecting me. And that's all just on the testing front. I'm having a lot of fun with all this.
Currently-working-Nitter-instance URL for Cherny's tweet: https://shitter.thepixora.com/bcherny/status/210254334910233...
Wow, 16 PRs?
No wonder GitHub keeps going down.
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
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
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
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?
This is not true. It has been done. I’ve seen it done for an entire OS too. Humans are very capable of doing this. The issue is this is seldom done practically speaking because the effort is not worth the benefit when the program becomes too complex.
For simple programs and small domains it’s worth it. For example type checking. Type checking proves one aspect of your program (the types) is fully correct.
That might be what pron's talking about. seL4 is only 10-20K lines of code as far as I remember. Maybe you have another OS in mind, though.
If you're talking about seL4, it is tiny and intentionally simplified. I'm not aware of programs larger than ~10KLOC that have ever been verified end-to-end.
I have long being fascinated by the the field and curious about it on an amature level, i took some basic proof verification and distributed computing classes back in the grad school days, but I'm clearly not an expert in the field by any means. From the article, it seemed like there are plenty of "traps" that i did not even consider - starting from lean hatches like assume(false), expressive power of TLA+ (CTL, ATL), and ofc challenges of tying an real implementation to a proof. To me all three of the above seem challenging enough to deserve their own tools, and i would appreciate smart people putting effort into addressing these rough edges.
Question to you: i can understand how proof verification like z3 or lean requires a special language and an inference engine; given that model checkers like tla+ are mostly about exploring possible program states and checking properties of such states and chains of states, i do not quite understand why it can't be done with a conventional imperative language to express state transitions and invariants - especially an interpreted one like python (esp with continuation support) or a language targeting a vm like wasm where one should be able to snapshot program state?
F-Star and Dijkstra Monads (which are apparently not really monads?) might get you to what you're looking for
The state space you get when using real programming languages like Python is much, much larger than the one you get when abstracting your system design into TLA+. Thus when testing real systems you can only explore very small portions of the state space. This is a real thing people do, although it isn't yet widespread - the term to look for is deterministic simulation testing. Making a DST harness that can handle exploring an application state space without requiring large modification to the application itself is very challenging. Currently Antithesis are the only ones I know who have done it (disclaimer: no connection to this company, I just think they are very cool).
TLA+ is not a model checker. It's a general language for writing mathematics, akin to Lean, only Lean focuses on high mathematics while TLA+ focuses on dynamic systems. There are a proof checker and at least one model checker that work on subsets of TLA+.
As to why TLA+ is better at describing systems than programming languages, the reason is that it's much more general. It can say things like "a routine that sorts in a quadratic number of steps or less" rather than a specific sorting algorithm, and it allows stating (and proving) that a specific sorting algorithm matches that description or not. Most TLA+ formulas are too abstract to be compiled or run (i.e. they describe too many potential algorithms).
Doesn't it only need to become an order of magnitude more capable than humans at theorem proving, not general software development?
For me the barrier to proving the "hard bits" was never that I couldn't reason about it—I quite enjoyed formal methods in school, and when introduced to them by coworker's who'd done similar—but it was that I didn't have the time to dedicate to learning enough about how to model my problem in a particular new language or system when none of my coworkers were spending such time and my boss wasn't already convinced.
The AI tools are great at lowering the learning curve by changing "how would I possibly express this" to "ah, let's see if this expression of it is actually right?" and "hm, is there a simpler way to express the same thing?"
Like StackOverflow for javascript questions, but for an area that was far to obscure to have a good library of example answers.
I'm not looking to prove the entirety of every system. Usually just some core bits. And often not connected automatically to the code (which may not be gonna change much).