> I hear good things about seL4 but that wasn't written so much as translated from Haskell during a formal process that makes Rust look like finger painting.

It's actually more fun than that. They have two implementations of seL4, and they use formal proofs to show that the Haskell model is identical to the C implementation. How much fun is that! /s