Wouldn't Frama-C and some of its plugins do this job? I've seen (I think?) Airbus (working with Atos?) people write custom Frama-C plug-ins to implement some static analysis & proof on their code, with great success.