[fuklief]

> 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.

[gargravarr]

- someone just outright botches the implementation. Heartbleed wound up in OpenSSL for years before anyone noticed.