Comment by AnimalMuppet

1 day ago

LLM-style AI isn't great for formal verification, not so far as I understand. And the recent advances in AI didn't do much for the kind of AI that is useful for formal verification.

You don’t use AI to perform formal verification. You give the agent access to verification tools whose output can then be fed back to the model.

It’s the same design as giving LLMs the current time, since they can’t tell time themselves, either.