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.
>>kybern+(OP)
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.