Correct. Also claiming that it's mildly secure is also inviting hackers. Damned if you do, damned if you don't.
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.