The difference between theory and practice, is that in theory there is no difference, but in practice - there is.

So far, every "provably secure design" I've seen ended up being insecure in practice due to the things people abstract away.

I'm not saying it's impossible, but I have not seen it done perfectly thus far.

We've seen more success by having many many iterations and widespread usage of common designs and patterns. These are not perfectly secure by any means, but they are secure enough against common threats to make it functionally equivalent until we figure it out.