[_hl_]

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.

[a1369209993]

More pointily: "correct" is not a formal property of a program, so you can't actually prove it in the first place. Rather you have proved some actual formal properties of the program (eg, always terminates, does not branch dependent on cryptographic secret data, etc[0]), which may, or may not, have any relevance to it's actual intended behviour.

0: Strictly speaking, even those are only English-language descriptions of formal properties, and you still need to worry about whether the formalization actually means what you think it means.