[dhekir]

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.