seL4 seems pretty boring. It’s a software kernal that has been designed with total security at its core - an increasingly critical thing at a time where the ever increasingly complexity of software due to a libraries-all-the-way-down approach to software engineering has led to huge cybersecurity breaches (such as the Spectre attack).
It’s also an interesting component in a theoretical tool chain for modern spacecraft engineers. Alongside advances in microprocessors that are being designed to use the open-source RISC-V ISA, I can see a new breed of space hardware that will be built with true total-security in mind.
In fact, Australia has already developed a spacecraft that uses seL4 - a QB50 cubesat a few years ago.
I think it’s wise to keep an eye on seL4 and RISC-V for space applications. They are two emerging building blocks that make a lot of obvious sense to base future spacecraft designs on.