Growing a modular framework for modal systems: HOLMS

We present HOLMS (HOL Light Library for Modal Systems), an evolving modular framework for mechanising modal reasoning within the HOL Light proof assistant. Building on earlier work on G¨odel-L¨ob logic (GL), HOLMS introduces a compositional architecture to formalise modal adequacy proofs and implement automated decision procedures for various normal modal systems, currently including K, T, K4, and GL. To clarify the compositional nature of our framework and illustrate how it bridges general-purpose proof assistants, enriched sequent calculi, and formalised mathematics, we highlight some design choices and structural features of HOLMS, such as its use of the metalanguage, embedding strategies, and modularity metrics.