Surely there is some middle ground in design space between rust and ada on one side (fully in the compiler) and c (with sel4-style checking - proof checking on a post compilation artifact) on the other.
Note that the c in sel4 and ada have stronger safety and correctness guarantees than rust
Rust can be written as simply as you want it to be written. Or, you can go crazy with generics or metaprogramming.
In theory you can do that, in practice you can't. Becoming a good $language programmer necessarily involves reading other people's code, for example when diagnosing issues in misbehaving libraries. You have to be familiar with every common language feature that other developers use, otherwise you won't be able to do your job properly.
The specification and proofs are open-source [0], but I suspect that they are tailored for seL4-related uses and probably aren't well-suited for "general-purpose" C code. I think using their proofs would also necessitate writing a specification for your own code which is probably going to be an ordeal in and of itself.
They do have a style guide [1] as well, but that's just a small part of the full verification process (described in [2]).
[0]: https://github.com/seL4/l4v
[1]: https://docs.sel4.systems/processes/style-guide.html#verific...
[2]: https://trustworthy.systems/publications/nicta_full_text/737...