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.
