We introduce a dependently typed machine-checked framework for verifying timing properties of raw (stripped) machine code binaries within the Rocq interactive theorem-proving environment. By formalizing instruction timings and integrating them with an abstract interpreter, we provide high-assurance, high-precision timing guarantees that are applicable to a wide range of systems. This allows users to ensure that real-time systems and cryptographic algorithms meet their critical performance and security requirements.