← All papers
Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
cs.LO
Jun 25, 2026 · v1
cs.PL
TL;DR
Formalizes a many-sorted hybrid polyadic modal logic in Lean 4, with soundness proof and applications to code verification and security protocols.
Abstract
We present a Lean formalization of a general hybrid modal logic with many-sorted signatures and polyadic modal operators. The system borrows ideas from both algebraic specification and dynamic logics, and is designed to serve as a uniform axiomatic foundation for specifying and verifying programming languages and security protocols. We expose a DSL for users to define languages and protocols as many-sorted signatures, specify the relevant domain-specific axioms, and reason about program executions or protocol runs. We provide a machine-checked proof of its soundness theorem and showcase the framework's versatility through several applications: an imperative programming language for code verification, the BAN logic for security protocols, and the modal system S5. We have designed our formalization to be intrinsically sorted, that is, well-sorted formulas in the base language are well-typed terms in Lean. Thanks to intrinsic sorting, all domain specific applications can be easily embedded in our framework via the DSL, at no additional syntactic overhead required for the user to prove. All code presented in this paper is openly accessible in the following repository: https://github.com/alexoltean61/msphml-lean
Problem
Modal and hybrid logics lack a unified, machine-checked framework that can be instantiated across diverse verification tasks (programming languages, security protocols).
Approach
The authors formalize the many-sorted hybrid logic H_Sigma(@,forall) in Lean 4 using intrinsic sorting: well-sorted formulas are well-typed Lean terms by construction. They expose a DSL for defining signatures in BNF-like notation and prove the soundness theorem for arbitrary axiomatic extensions.
Results
Three applications demonstrated: Hoare-like verification of an imperative language, BAN logic analysis of security protocols (including Needham-Schroeder), and an S5 modal system. Code is open-source.