"Before we prove our code is correct, we need to know what is 'correct'. This means having some form of specification, or spec, for what the code should do, one where we can unambiguously say whether a specific output follows the spec"

What's the difference between the specification and code at that point? If it's that detail oriented, then isn't the chance of bugs in the specification at least as likely as being in code?