> Repeating myself, when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target.

Yes, and that would be relevant if this was a verified software system. But it wasn't: the system consisted of a verified X and unverified Y, and there were issues in the unverified Y.

The article explicitly acknowledges this: "The two bugs that were found both sat outside the boundary of what the proofs cover."