A provably correct embedded verifier for the certification of safety critical software