Beware of bugs in the above code; I have only proved it correct, not tried it.
– Donald Knuth
It's not just hypothetical either. There was a bug in a sorting algorithm a few years back that had been 'proved' correct. I think it was to do with numbers wrapping, and that hadn't been considered in the mathematical proof.
WPA2 also had an exploit (KRACK) while the handshake algorithm itself was "proven to be secure". Formal verification is a powerful tool but it does not guarantee bug-free code: it merely guarantees that the particular bugs you checked for are not possible.
It's not just hypothetical either. There was a bug in a sorting algorithm a few years back that had been 'proved' correct. I think it was to do with numbers wrapping, and that hadn't been considered in the mathematical proof.