Model checking of real-time systems is a well-studied topic, with Metric Interval Temporal Logic ( \(\textsf{MITL}\) ) playing a key role in expressing timed properties. We present \(\textsc {Tempora}\) , a new tool for \(\textsf{MITL}\) model checking under pointwise semantics, that integrates both past and future modalities. \(\textsc {Tempora}\) is based on a recent translation from \(\textsf{MITL}\) to the model of Generalized Timed Automata (GTA) [3] and the zone-based algorithms for reachability and liveness in \(\text {GTA}\)  [2, 3]. A straightforward implementation of the construction proposed in [3] falls short of state-of-the-art performance. Through a series of conceptual and engineering optimizations, we significantly improve its scalability and obtain a tool that outperforms existing approaches. In this work, we present the key techniques underlying these improvements and introduce our tool.