Linear Temporal Logic (LTL) is one of the most common formalisms for expressing properties of systems in formal verification and other fields. However, its propositional nature limits its applicability to finite-state systems, whereas many interesting scenarios often require reasoning in an infinite-state settings. Indeed, many formalisms and techniques have been proposed in the last decades to specify and verify infinite-state systems. This talk presents our take at the problem. We recently introduced LTL Modulo Theories (LTLMT), a first-order extension of LTL that provides both a general and expressive theoretical framework to reason about infinite-state specification and verification, and encouraging early experimental evidence of its applicability, thanks to the ability to exploit efficient off-the-shelf Satisfiability Modulo Theories solvers. After introducing the necessary background and defining LTLMT, we will go through early results in the area, and explore current directions, recent results and many future developments.