Some unmentioned theorem provers/frameworks:
Isabelle, a powerful prover with support for code generation in (mostly functional) languages. The sel4 project is a notable user of Isabelle. There is also a new framework called Igloo, which aims to provide language agnostic end-to-end proofs from protocol to implementation.
Then there is Event-B, of which I know less about, but which powers the autonomous Paris metro line, an impressive feat.
There’s also Verifpal.
A few weeks ago a fellow Lobster (@soatok) mentioned https://blog.filippo.io/bleichenbacher-06-signature-forgery-in-python-rsa/ from Filippo Valsorda while discussing the latest Cryptography Dispatches: https://lobste.rs/s/mkzcfk/cryptography_dispatches_reconstruct (from the same author).
In both case, it was simply researchers reading the code and finding what could go wrong.
A: The customer reports them. It’s not a bug if the customer doesn’t report it, and it’s a feature if there’s a workaround.
This attitude might work fine for some software where you can easily patch bugs as you go along. What about when the software is safety critical? Or when a bug means there’s a security vulnerability? Maybe the bug results in a multi-hundred million dollar recall?