Formal proofs for real time systems