It might be that I’m unfamiliar with the matter, but as I understand it, in order to prove a statement, the statement must correctly model the reality of the code.
In that case, how can you be truly sure that, when formally verifying a program, you have correctly modelled the software you’re trying to verify?
Couldn’t it very well be that you proved something that wasn't actually your program?
Couldn’t it very well be that you proved something that wasn't actually your program?