Using a provably correct security model is beneficial as it limits adversarial power. As long as the protocol is followed and the proofs are correct, the adversary cannot violate the security properties claimed. However, there are still factors stopping pure security from existing. For example, implementations can be wrong, or hardware can introduce attacks not previously considered.