There's no end to bugs like these in Linux. Millions of Lines of Code can easily hide many, many of these. Code that runs in supervisor mode.

None of this can ever affect seL4[0] nor a system built on it, due to its architecture.

0. https://sel4.systems/