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

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.