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

• URL: http://arxiv.org/abs/2604.14038v1
• Date: Wed, 15 Apr 2026 16:18:44 GMT
• Title: KindHML: formal verification of smart contracts based on Hennessy-Milner logic
• Abstract summary: Real-world attacks often exploit flaws in the business logic of smart contracts.<n>We present an automated approach to the formal verification of smart contracts.<n>Our results show that the proposed approach can effectively verify non-trivial temporal properties of smart contracts.
• Score: 1.8594711725515678
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• GoAT-X: A Graph of Auditing Thoughts for Securing Token Transactions in Cross-Chain Contracts [52.51342355102833]
  Cross-chain bridges, the critical infrastructure of the multi-chain ecosystem, have become a primary target for attackers.<n>Existing defenses, such as bytecode-level static analysis, are ill-equipped to handle the semantic complexity of cross-chain interactions.<n>We propose GoAT-X, a framework that shifts automated cross-chain smart contracts auditing from pattern matching toward systematic first-principles verification.
  arXiv  Detail & Related papers  (2026-04-27T11:34:21Z)
• SmartGraphical: A Human-in-the-Loop Framework for Detecting Smart Contract Logical Vulnerabilities via Pattern-Driven Static Analysis and Visual Abstraction [0.30586855806896046]
  This paper introduces SmartGraphical, a novel security framework specifically engineered to identify logical attack surfaces.<n>By synthesizing the context-dependent nature of logical bugs, SmartGraphical enables developers to interpret warnings within a visualized structural context.<n>Our findings indicate that this hybrid methodology significantly enhances the interpretability and detection rate of non-trivial logical security threats in smart contracts.
  arXiv  Detail & Related papers  (2026-03-09T16:35:17Z)
• One Signature, Multiple Payments: Demystifying and Detecting Signature Replay Vulnerabilities in Smart Contracts [56.94148977064169]
  lacking checks on signature usage conditions can lead to repeated verifications, increasing the risk of permission abuse and threatening contract assets.<n>We define this issue as the Signature Replay Vulnerability (SRV)<n>From 1,419 audit reports across 37 blockchain security companies, we identified 108 with detailed SRV descriptions and classified five types of SRVs.
  arXiv  Detail & Related papers  (2025-11-12T09:17:13Z)
• ContractTrace: Retracing Smart Contract Versions for Security Analyses [4.126275271359132]
  We introduce ContractTrace, an automated infrastructure that accurately identifies and links versions of smart contracts into coherent lineages.<n>This capability is essential for understanding vulnerability propagation patterns and evaluating the effectiveness of security patches in blockchain environments.
  arXiv  Detail & Related papers  (2024-12-30T11:10:22Z)
• Soley: Identification and Automated Detection of Logic Vulnerabilities in Ethereum Smart Contracts Using Large Language Models [1.081463830315253]
  We empirically investigate logic vulnerabilities in real-world smart contracts extracted from code changes on GitHub. We introduce Soley, an automated method for detecting logic vulnerabilities in smart contracts. We examine mitigation strategies employed by smart contract developers to address these vulnerabilities in real-world scenarios.
  arXiv  Detail & Related papers  (2024-06-24T00:15:18Z)
• Solvent: liquidity verification of smart contracts [2.680854115314008]
  A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets. We propose solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity.
  arXiv  Detail & Related papers  (2024-04-27T10:54:50Z)
• LookAhead: Preventing DeFi Attacks via Unveiling Adversarial Contracts [15.071155232677643]
  Decentralized Finance (DeFi) has resulted in financial losses exceeding 3 billion US dollars.<n>Current detection tools face significant challenges in identifying attack activities effectively.<n>We propose LookAhead, a new framework for detecting DeFi attacks via unveiling adversarial contracts.
  arXiv  Detail & Related papers  (2024-01-14T11:39:33Z)
• Token-Level Adversarial Prompt Detection Based on Perplexity Measures and Contextual Information [67.78183175605761]
  Large Language Models are susceptible to adversarial prompt attacks. This vulnerability underscores a significant concern regarding the robustness and reliability of LLMs. We introduce a novel approach to detecting adversarial prompts at a token level.
  arXiv  Detail & Related papers  (2023-11-20T03:17:21Z)
• Enhancing Smart Contract Security Analysis with Execution Property Graphs [48.31617821205042]
  We introduce Clue, a dynamic analysis framework specifically designed for a runtime virtual machine.<n>Clue captures critical information during contract executions, employing a novel graph-based representation, the Execution Property Graph.<n> evaluation results reveal Clue's superior performance with high true positive rates and low false positive rates, outperforming state-of-the-art tools.
  arXiv  Detail & Related papers  (2023-05-23T13:16:42Z)
• Safety Verification of Declarative Smart Contracts [4.303272418564008]
  This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon. Our evaluation on 20 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools.
  arXiv  Detail & Related papers  (2022-11-26T15:02:37Z)
• ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning [80.85273827468063]
  Existing machine learning-based vulnerability detection methods are limited and only inspect whether the smart contract is vulnerable. We propose ESCORT, the first Deep Neural Network (DNN)-based vulnerability detection framework for smart contracts. We show that ESCORT achieves an average F1-score of 95% on six vulnerability types and the detection time is 0.02 seconds per contract.
  arXiv  Detail & Related papers  (2021-03-23T15:04:44Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.