We present a decision procedure for IS4, an intuitionistic modal logic first formulated by Fisher Servi. The logic has two independent modalities and is interpreted over birelational Kripke models. Unlike other intuitionistic modal logics, the problem of decidability of IS4 has been open for almost thirty years, since it has been posed in Simpson’s PhD thesis in 1994. Our result is obtained by defining a proof-search algorithm based on a labelled sequent calculus that explicitly incorporates the two accessibility relations of Kripke models for the logic. The search algorithm outputs either a proof or a finite countermodel, thus additionally establishing the finite model property for IS4.