In this talk we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi [1]. This solves a problem that has been open for almost thirty years since it had been posed in Simpson’s PhD thesis in 1994 [2]. We obtain this result by performing proof search in a labelled deductive system [3] that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. This system inherits the advantages of labelled systems for both intuitionistic propositional logic and classical modal logics: in particular, all inference rules are invertible (i.e. we never delete information bottom-up in proof search) and there is a direct correspondence between sequents and models which lets us build a countermodel by interpreting (and extending) the labelled sequent at which proof search terminates. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area [4]. [1] Gisèle Fischer Servi. Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico dell’ Università Politecnica di Torino, 1984. [2] Alex Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1994. [3] Sonia Marin, Marianela Morales, and Lutz Straßburger. A fully labelled proof system for intuitionistic modal logics. Journal of Logic and Computation, 2021. [4] Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, and Lutz Straßburger. Intuitionistic S4 is decidable. In 2023 Symposium on Logic in Computer Science (LICS2023), 2023.