> For each kind of bug, you need a different proof. Not necessarily; if your definition of security and correctness is sufficiently general and if you can prov

> For each kind of bug, you need a different proof. Not necessarily; if your definition of security and correctness is sufficiently general and if you can prove that your program conforms to those definitions, you have effectively proven your program to be secure and correct for all bugs. Unless of course your definition of security and correctness was too narrow, which as you note is where the crux of the problem is. But this is not a hopeless task, there is a lot of active research in building axiomatic definitions of what security and correctness mean, so in theory it could be possible to prove a program 100% correct if the axioms are self-evident.