There have been a number of successes in the past few years in use of formal methods for verification of real-time systems, and also in source-to source transformation of these systems for improved analysis, performance, and schedulability. What has been lacking are formal proofs that these transformations preserve, or establish program properties. We have previously developed a set of compiler transformation rules for safe and profitable speculative execution in real-time systems. In this paper, we present formal proofs that our transformations preserve both the semantic and the timeliness properties of programs. Our approach uses temporal logic, enhanced with a denotational-semantics-like representation of program stores. While the paper focuses on the speculative execution-transformations, the approach is applicable to other real-time compiler-based transformations and code optimization.