We present a library-level formalisation of Hennessy-Milner Logic (HML) - a foundational logic for labelled transition systems (LTSs) - for the Lean Computer Science Library (CSLib). Our development includes the syntax, satisfaction relation, and denotational semantics of HML, as well as a complete metatheory including the Hennessy-Milner theorem - bisimilarity coincides with theory equivalence for image-finite LTSs. Our development emphasises generality and reusability: it is parametric over arbitrary LTSs, definitions integrate with CSLib's infrastructure (such as the formalisation of bisimilarity), and proofs leverage Lean's automation (notably the grind tactic). All code is publicly available in CSLib and can be readily applied to systems that use its LTS API.

翻译：本文介绍了在Lean计算机科学库（CSLib）中对亨内西-米尔纳逻辑（HML）——一种用于标记转移系统（LTS）的基础逻辑——进行的库级形式化。我们的开发涵盖了HML的语法、满足关系与指称语义，以及包含亨内西-米尔纳定理（对于图像有限LTS，互模拟等价与理论等价性一致）在内的完整元理论。本工作强调通用性与可复用性：其参数化设计适用于任意LTS，定义与CSLib的基础设施（如互模拟的形式化）深度融合，证明过程充分利用了Lean的自动化工具（特别是grind策略）。所有代码已在CSLib中公开，可直接应用于使用其LTS API的系统。