[cyphar]

> The main reason seL4 was written in Haskell and again in C was to cross-verify behavior.

seL4 was modeled in Haskell, then written in C. Then they used tools to verify that the Haskell models matched the C code.