KindHML: formal verification of smart contracts based on Hennessy-Milner logic

Computer Science > Cryptography and Security [Submitted on 15 Apr 2026] KindHML: formal verification of smart contracts based on Hennessy-Milner logic Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini, Vadim Malvone Smart contracts deployed on blockchains such as Ethereum routinely manage large amounts of assets, making their security critical. Empirical studies show that real-world attacks often exploit flaws in the business logic of contracts that unfold across multiple transactions, such as liquidity or front-running attacks. Detecting these attacks requires reasoning about expressive temporal properties beyond the capabilities of existing analysis tools. In this paper, we present an automated approach to the formal verification of smart contracts, enabling the specification and verification of complex temporal properties. Our approach provides a fully automated encoding into Lustre -- the specification language supported by the Kind 2 model checker -- of an expressive subset of Solidity contracts and temporal specifications based on first-order Hennessy-Milner Logic. This encoding allows us to leverage Kind 2 to determine whether the contract respects the specification or not. We implement our approach in a toolchain that integrates the translation and verification steps, and we evaluate its effectiveness and performance on a benchmark of smart contracts and temporal properties capturing complex attack scenarios. Our results show that the proposed approach can effectively verify non-trivial temporal properties of smart contracts and detect violations that are beyond the reach of existing analysis tools. Subjects: Cryptography and Security (cs.CR); Logic in Computer Science (cs.LO) Cite as: arXiv:2604.14038 [cs.CR]   (or arXiv:2604.14038v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2604.14038 Focus to learn more Submission history From: Enrico Lipparini [view email] [v1] Wed, 15 Apr 2026 16:18:44 UTC (81 KB) Access Paper: view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-04 Change to browse by: cs cs.LO References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)