There is always a specification, the question is "was this issue found against a version of seL4 that had been fully specified or not?". I worked at the lab, I

There is always a specification, the question is "was this issue found against a version of seL4 that had been fully specified or not?". I worked at the lab, I wasn't aware of any bug/issue on the fully specified kernel, that is why I am unsure if this counts or not. I would need to have a look at the source code and proofs to confirm.