1. 5

  2. 3

    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.

    1. 2

      There’s also Verifpal.

    2. 2

      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.

      1. 0

        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.

        1. 2

          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?