sel4 is the example of building a safe C program if you go above and beyond in effort.

It's provably safer than rust, e.g.

There are obviously multiple levels of correctness. Formal verification is just the very top of that spectrum, but it does comes at extraordinary effort.