Comment by ktRolster

It demonstrates a difficulty of formal verification. You can prove the program matches the specification, but how do you know the specification is correct?

Quis custodiet ipsos custodes?