With what, Frama-C? Good luck getting it adopted outside domains that enforce its use for code certification.

Frama-C is a specific compiler. It has not much to do with proving your own code. (And C ain't a good language for writing code you want to prove correct in.)

You are right that after having proven your code correct, you might want to use an implementation (compiler or interpreter), that is also proven correct. But those are still two different things.

Frama-C is a framework for code analysis. It can help proving code with the aid of ACSL (JML-like notation for C contracts).

But I agree that C is not the best language for writing critical code.