The problem with verifying real-world software is to give a clear and unambiguous definition of what "correct" means in context.

You cannot catch bugs in the specs that way.