[isubasinghe]

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.

[ryao]

How does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?