As the design document states: It’s meant to be simple but sufficient for the target domains. More generality means more complexity. The proposed model should serve almost all present use cases. Even Cog System’s “ultra-secure phone" fits this model: All the dynamicism, such as run-time installable apps, happen inside a virtual machine with an Android guest. From the seL4 PoV, the phone is a simple, static architecture with a fixed number of protected components: the “use VM” containing a full Android system with virtual drivers, the VMM, a console, a I/O multiplexing component, a “driver VM” (which should eventually become individual driver components), a network encryption component and a storage encryption VM. If the Platform supports this use case, it will definitely support most others.

For the (presently very small) class of deployments that need more generality, a different framework is needed. Such more general frameworks may be standardised in the future (and may or may not be extensions of the Core Platform), but for now this is not the aim. If you want a system where a fully general OS is needed, Genode is likely your best choice (at the expense of losing most of the assurance).