I must admit that I don't really understand the RedLeaf design if it doesn't use hardware protections you cannot run C or use unsafe Rust "safely"?? Everything in 100% safe Rust isn't going to happen ever so it isn't really a seL4 competitor more a research prototype.

That said I can imagine a two layer system: if you use 100% safe Rust you have a 'fast path' direct access, otherwise you fallback to slower hardware protection.