Firstly, it is C++, not C.

Secondly, non-C/C++ use in OSs is uncommon, and thus considered research.

Thirdly, the microkernel with the strongest formal proof of correctness, seL4, is written in C.