One of the problems with proving programs is that proofs tend to get as complex as the code they're proving, at which point one has to be wary of bugs in proofs. One (possibly only) way around this would be to prove an automated proof checker and use it to prove better automated proof checkers, and so on, up until you get a tool you trust that can reliably make proofs for you.