To get to that point (mixed criticality, some processes and drivers can be critical and others not be), you need to be able to reason about time.

That's exclusively seL4 right now, and the very state of the art.

(incidentally, we really should be putting our weight behind seL4, it really is good)