> I also haven't seen one large-scale network-facing C project written using reasonable development practices (i.e. not absurdly expensive formal verification) that hasn't had some sort of terrible remote code execution vulnerability.

This has gotten a lot better with static code analysis (clang-analyzer, Coverity, ...) and whitebox-fuzzing (libfuzzer, afl, ...). Both simply point you to the bugs and don't require a formal spec.

Together with Valgrind, these tools have revolutionized C programming for me.