“We posted a meme that like Claude and ChatGPT and other tools, they will tell you you're absolutely right. But formal methods tools, they'll tell you you're absolutely wrong.”

…on top of TLA Plus. TLA Plus syntax, you can see it's kind of like very mathematical, hard for people to onboard. So we started with a different syntax and also would develop like more tooling on top of TLA Plus for like making things easier for industry applications. So it's just another version.

TLA Plus seems very rooted in like analytic philosophy and logic, right?

Right. I think that information is probably better for engineers. Engineers want to know what's wrong with a thing. What's right with it is that's fine. Like let that go.

And it's also helpful if you are trying to make optimizations in your code. So not only applying fixes and checking if that fix apply, but applying optimizations and checking that optimizations are not going to break any existing behavior that you have. This is a nice use case from AWS. So AWS…

So AWS is an interesting one because they just hired the creator of the lean language, which is another formal specification language. Do you have an opinion on the difference between TLA Plus and Lean or other formal specification languages like that?