Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker
cs.LO
Feb 17, 2026 · v1
TL;DR
Formalizes Hennessy-Milner Logic syntax, semantics, and the Hennessy-Milner theorem in Lean's CSLib, using the grind tactic and CSLib's LTS API.
Abstract
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.
Problem
Hennessy-Milner Logic (HML) is a foundational logic for reasoning about labelled transition systems, but no library-level formalization existed that integrated with a broader computer science proof infrastructure.
Approach
The authors formalize HML syntax, satisfaction relation, and denotational semantics in Lean as part of CSLib (the Lean Computer Science Library). They prove the full metatheory including the Hennessy-Milner theorem: bisimilarity coincides with logical equivalence for image-finite labelled transition systems. The development is parametric over arbitrary LTSs and leverages Lean's grind tactic for automation.
Results
The complete formalization is publicly available in CSLib. It integrates with existing CSLib infrastructure (e.g., the bisimilarity formalization) and can be applied to systems using CSLib's LTS API.
