Alloy

The same as TLA+, right? So there are different families.

So for model checking tools like TLA+, Quint, Alloy is also one, it's a bit different but also in there, you can just specify what you want and then you have automatic proofs.

And you don't even have to go all the way to proofs, you can also get value just from like random simulation.

So if you're like, if you don't have time to go and reduce your state space such that the tool can find a proof for you or like tune the spec and see if you can actually prove it, you can also get value out of just like running simulations.

I'm super excited about the evolutions on like, especially with Lean, a lot of, like, AI is getting good at writing Lean proofs.

There's a lot of debate on, on things there.

But I think, like, the main point that concerns me with this is who is writing the specifications, right? 'Cause I, I think on a lot of these scenarios, people are relying on getting AI to also write the specifications, and then you get a proof, but it's a proof of what? Did you really check? So I think tools like TLA+ and Quint and Alloy, they can help you iterate a bit more.

So especially with Quint, we've done a lot of things just to help you understand what you have specified.