Even the non-formally-verified L4 operating systems are no fun to bughunt in. It's just a very clean, simple design without a lot of attack surface. You end up looking at what people build on top of it instead.
Yeah, that's by far the most likely. Note that one of Gernot's non-goals is "Stopping you from shooting yourself in the foot": this is to be taken seriously. The userland libraries provided by SeL4 have no proof evidence at all, and IME look and feel like any other C codebase. It's very likely that they the same class of security problems. Further, it's /very/ difficult to build anything on SeL4 without using said libraries (ease of use is another non-goal, remember?), so I'd expect many real systems to be built on them and thus share some class if issues among them.
