I also had ideas of an operating system design and the capabilities I had considered uses the same features of interposition and delegation as seL4 does. There

I also had ideas of an operating system design and the capabilities I had considered uses the same features of interposition and delegation as seL4 does. There are other advantages than just what they list there; for example, you can apply a filter to audio, or you can use proxy capabilities for implementing network transparency. The real-time stuff is something I had considered as allowing as an optional implementation; my idea was for a specification rather than only a single implementation. Another feature I wanted though, is that all programs operate deterministic except for I/O. Without I/O, you can't determine the date/time or how long a program takes, can't check for processor features (if you use something that the hardware does not support though, the operating system may emulate it), etc. I had thought to use a mixture of hardware support and software support to implement it, though. (There is a note in the document about attacks with capability implemented in hardware, but I do not have the referenced document and I don't know if that attack applies to what I am thinking of doing.)