Maybe sel4? I'm not in embedded so maybe I'm being pretty silly here, but I think being formally proven and realtime are pretty good things to have in the case

Maybe sel4? I'm not in embedded so maybe I'm being pretty silly here, but I think being formally proven and realtime are pretty good things to have in the case of an expensive, long lived space project. That said, this is on the scale that I'm surprised off-the-shelf things are even being considered. I'd have thought they'd just roll something bespoke and that's the end of that.