It's written in C in the same way it's written in assembly: C is just used as part of the process to go from a high level spec to executable code. You can als

It's written in C in the same way it's written in assembly: C is just used as part of the process to go from a high level spec to executable code. You can also compile eg Haskell via C. The subset of C used in seL4 is highly constrained.