I can't imagine how writing C directly could possibly be better than using a language like Dafny and then generating C code.

Edit: Dafny: A verification language capable of enforcing invariants