Comment by deterministic

"The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct (and now has a PR addressing)."

In other words, the code was proven correct according to spec by LEAN. Which is exactly what LEAN claims to do.