I mean this is demonstrably untrue: SEL4 is written by mere mortals, in C. It's safer than rust, there are formally verified security guarantees that include and go beyond the memory safety of rust.
It is the case though that c is an incredibly shitty language to do this sort of static analysis on because for example it's easy to do shenanigans like lexical macros that make the static analyzers job much much harder.
But fine. With that kind of dishonesty I could claim that the Linux kernel is written in nothing: I have compiled it and deleted the source code. Look ma, it’s no-code kernel.
[1] Kind of a bummer though that you cannot change any of the C code any more now that the verification code is gone.
Funky macros can still make static analysis more complex by introducing layer(s) of indirection of course.
But that's not a safe language; that's a safe work. ANY programming work - regardless of language - can be made safe via such expensive means, which puts this square into the space of "argument ad absurdum". You could argue that brainfuck or assembler can be made safe via these means, but everyone would rightly ridicule you for it.
If you used something else, you'd need to trust a lot more code.
There's CakeML, which is a formally verified subset of Standard ML [0]