How to ruin Linus's vacation

The trouble with formal proofs is that the logical errors and bad assumptions made when writing the code tend to be propagated into the formal proofs, where they typically remain equally unnoticed. Or worse, the proof is fine, but the code deviates in subtle ways due to abstraction mismatches and model simplification.

At least as I understand the state of the art in formal code proofs, the only place they work is places where they aren't particularly useful; places where things like timing, instruction reordering, hardware errors and concurrency are not considerations.