> The mathematical proof might be 100% solid and hacker proof. The implementation will probably never be.

I agree, I see a few ways that it could go wrong:

- Code is proven correct against the specification, but specification is wrong/buggy

- source code is correct/secure, but compiler is overzealous and botch the securities guarantees.