Comment by samus

> The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program.

It is a nothingburger problem because one is going to have that problem as well even when not employing formal methods. Except without FM the spec will be in natural language and therefore it will be impossible to mechanically verify the end product with it. And since natural language specs are highly liable to be ambiguous or contain unintended holes, LLMs won't save us either.