It means that the correctness properties that were formally proved are not necessarily what you would intuitively understand as "correct". E.g. you can formally prove that a buggy factorial(n) always outputs (n - 1)! by incorrectly defining what you want to prove. The function behaves according to what you proved, it's just not the expected behaviour.

It's a joke. You'd expect that a proof of correctness to be the Holy Grail. Nothing could be wrong, since it's proved correct. And yet, after running it, you could still find a bug in it, because you may have made a mistake in your proof.

To the other comments here I have to add - proofs (in math, science, computer science, any subject area..) never reflect absolute reality, but rather just your view of reality or the parts of reality that you have chosen to model.

So the reality of your "proven" program will never 100% match the reality of it running on hardware or some other software context than you anticipated. Let's call this the Hacker's Postulate...

As for math specifically I think this is a very deep and interesting philosophical tangent to go down.

In addition to the sibling answers, one could have verified an algorithm mathematically, but made a typo in the code.