[Someone]

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

I agree, but it’s not fair to imply that the verification was incorrect if the problem lies elsewhere.

This is a nice example of how careful you have to be to build a truly verified system.

[amoss]

But is fair to state that the verification was *incomplete*, which is what the article does.

[lmm]

The problem was in Lean though, so it seems fair.