You make no sense. The proof is obviously not coded in C because C is not a language you can write proofs in. But all of the instructions executed when running L4 were emitted by a C compiler.

(This is not to suggest that I would ever advise coding anything whatsoever in C.)

Unless... maybe you are saying all the C code in L4 was not actually coded by anybody, but was rather emitted by programs written in these other languages, and L4 is properly a program coded in those languages, with just a transitory C representation on the way to machine code?

i wouldn't mind C if every program written in it was written to the standard of seL4, but alas, that isn't the case, and usually it's not even close. i'm also quite sure that getting even close to it would make you want to use another language instead.