I think a scheme as simple as running two Linux VMs, where you have isolated the services that have real-time guarantees into their own VM, lets you benefit from seL4.

This is tangential to your comment, but it's worth mentioning that you can often begin securing a (Linux) system with seL4 by putting the entire system into a VM. Then, you iteratively port components to run "natively" over seL4 -- a process called "cyber retrofit" [0, 1].

BTW, it was probably just a typo but I believe "se" in seL4 is not a shortening of "secure", but an initialism for "secure embedded". Which is why it's not "secL4".

[0] https://sel4.systems/About/how-to-use.html

[1] https://trustworthy.systems/publications/abstracts/Klein_AKM...

A system with two seL4 tasks, (1) a flight control system, and (2) a VMM running Linux, uses seL4's formally proven safety properties to meet the timing and separation requirements of the critical flight control system... and run a bunch of less critical stuff on Linux that no one wants to rewrite.