"The proof was only as good as the spec." Is the sentence which will go on the tombstone of Formal Verification.

The spec has always been the problem. Whether the flaws in the spec arise from the customer or from the developer filling in the gaps in the spec incorrectly.

If I built an entire system and the spec does not mention access control logic, then formal verification will neither prove nor disprove that the software is secure. It's just not in the spec...

You have to know exactly what security properties you want. By the time you've written them down succinctly and correctly as a spec, you might as well have written them down succinctly and correctly as code.

The spec has to be just as detailed and will be just as error-prone as the code itself.