[Intermernet]

The sneaky thing they did is write seL4 in Literate Haskell, and then translate it to C. That involves some serious understanding of both languages!

http://ssrg.nicta.com.au/projects/seL4/tech.pml