what sel4 shows is that it's entirely preventable with a rewrite from scratch by a team of formal-methods ph.d.s over many years, if they invent a design that allows the kernel to only be a few thousand lines of code so that the titanic effort of formal verification becomes feasible, barely. it's not something you can do with a codebase of millions of lines of code or a codebase that wasn't written from scratch with formal verification in mind. yet, anyway