For me, SeL4's verification is important because it can actually provide formal real-time guarantees. Before SeL4, if you wanted to write a hard real-time syst

For me, SeL4's verification is important because it can actually provide formal real-time guarantees. Before SeL4, if you wanted to write a hard real-time system, you pretty much had to either forego an OS, or forego formal verification (or, usually, both). Having the option to write a RTOS without also writing a bunch of boilerplate (and probably incorrect) scheduler / resource allocation code, or dedicating a core to a task because you couldn't reason about resource consumption otherwise, is pretty exciting! Sure, it may not help much with securing normal userland applications, but in many embedded systems meeting deadlines is more important than any security functionality could be; the confinement properties are in some sense just consequences of having to reliably hit deadlines and isolate resources.