More importantly, a good specification is one that is triple-checked: by inspection by a human, having the program to conform to it, and by having to satisfy a bunch of nontrivial theorems about the spec that a human would expect from programs conforming to the spec. Sel4's integrity, confidentiality, and worst-case-execution-bounds proofs are an example of this... it's quite unlikely for a program to simultaneously provably satisfy a specification, the specification to provably satisfy nontrivial (first order) properties, and for those properties to nonetheless be defined incorrectly. Obviously there can still be holes in your model (for example, not considering certain side channels), but that's a pretty different situation from accidentally proving a different thing than you thought you were.