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.