[fpgaminer]

A caveat to this, which doesn't diminish your point but is interesting to consider, is that we prove the papers based on quite a lot of assumptions. For example, we may have 100% correct proofs that a given symmetrical encryption primitive is secure, but it's only secure under the common assumptions that A) the attackers are polynomial time, and B) that we don't care about any information the attacker may already have.

A is fairly obvious; we don't consider attackers who can perform infinite computation per second, because that's not practical. B is more subtly interesting. Most encryption systems reveal the length of the plaintext that's been encrypted, or at least some information about the length. But we don't consider that relevant in most of our proofs, because it's assumed to be information the attacker has a priori.

Of course in practice leaking length of the plaintext has sometimes made attacks on the overall system possible (encrypted VOIP calls can be partially decrypted because their packet lengths leak information about the speech being encoded).

We just ignore those problems in most of our proofs because building encryption primitives that don't leak that information is much, much harder and it's not _usually_ a problem.

Again, none of this detracts from the thrust of the arguments in this thread: formally verified code is objectively better than non-formally verified code; approaching the limits of our abilities today. The problems these assumptions may or may not introduce are universal to all implementations.