I suppose different people may answer your questions in different ways, depending on how they define words like "proof" and "correct". I would answer like this:

I suppose different people may answer your questions in different ways, depending on how they define words like "proof" and "correct". I would answer like this: the proof was correct, but it was solving the wrong problem (unbounded ints rather than bounded). Inside a formal system it's relatively easy to understand what's going on; the real difficulties are at the boundaries: how do we build a formal model of a real system, and how do we translate formal results back to the original system? It's a lot like programming: manipulating data is easy, the problems are getting the right data and interpreting what the output means. In this case, the model didn't capture overflow; so the proof is valid for that model, but it's not a useful model for Java's ints.