by Someone 3 days ago
> 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.
But is fair to state that the verification was *incomplete*, which is what the article does.
The problem was in Lean though, so it seems fair.