The process isolation enforceable by commodity hardware is too weak to protect secrets from malicious code running on the same machine: Spectre-era attacks have exploited timing side channels derived from contention on shared microarchitectural resources to extract secrets. We describe our work in progress on specifying and verifying \emph{strong timing isolation} for synthesizable hardware. We reason about the cycle-accurate semantics of circuits with respect to a trustworthy formulation of strong isolation based on “air-gapped machines” and develop a modular proof strategy that sidesteps the need to prove functional correctness of processors. We demonstrate our method on a multicore, pipelined, RISC-V design formalized in Coq. Finally, we discuss future directions toward composing isolation guarantees with speculative, constant-time guarantees to obtain a software-to-hardware, end-to-end guarantee of timing side channel freedom.