> IIRC seL4 had a couple bugs where the code _and_ the formal model both got it wrong in the same way, and it therefore passed the proof. I haven't heard this

> IIRC seL4 had a couple bugs where the code _and_ the formal model both got it wrong in the same way, and it therefore passed the proof. I haven't heard this one yet. How did they find it, then?