The first reason formal verification has never taken off is that it's difficult. The second reason, that most people don't get to because of the first reason, is that formal verification is really brittle. It is only verified under the very specific setup of the problem. Close doesn't count in math.

The first reason prevents humans from engaging with them, the second reason is what will make it difficult even for LLMs. I mean, I'm glad we are trying, but I'm dubious they will be the panacea some people proclaim.

Close can count in math - fuzzy logic and probability are a thing.

But I think you have it backwards. Close doesn't count in IT security. "Almost secure" means unsecure. Security is the compelling argument for formal verification.