[kenjackson]

what's the largest program you've proved correctness of?

But that's the point. With security code, while you may not prove the correctness of it, there's a black hat that's trying to find a counterexample to your "proof".

Whereas for 99% of proofs that are published in the literature no one is trying to prove that there are flaws in the proof. As someone who reviewed CS papers I would always try to really read at least one proof in the paper. Not skim, but really scrutinize it. Probably 75% of the time I could find a problem with the proof. Usually one that was easily corrected, but it was still wrong. But it took substantial effort to do this (which is why I only did one per paper and just read the other proofs).

Some recommended reading: http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/l...