Post #1546561

@regehr It didn't find bugs in *the portion of the code that was formally verified*. Which left the parser (out of scope for the proofs, but obviously part of the attack surface... oops!), and... the lean runtime itself.