arXiv CSopen access

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

KindHML: formal verification of smart contracts based on Hennessy-Milner logic Massimo Bartoletti 1 , Angelo Ferrando 2 , Enrico Lipparini ( Malvone 4

arXiv:2604.14038v1 [cs.CR] 15 Apr 2026

2

)1

, and Vadim

1 Università degli Studi di Cagliari, Cagliari, Italy Università degli Studi di Modena e Reggio Emilia, Modena, Italy 3 Télécom Paris, Institut Polytechnique de Paris, France

Keywords: smart contracts · formal methods · verification 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.

1

Introduction

In recent years we have seen a steady rise of smart contracts that implement financial ecosystems on top of public blockchains, and control today tens of billions of dollars worth of crypto-assets. The peculiarities of the setting (i.e., the absence of intermediaries, the immutability of code after deployment, some problematic design choices in smart contract languages) make smart contracts an appealing target for attackers, as bugs might be exploited to steal cryptoassets or just cause disruption. This is witnessed by a long history of attacks, which overall caused losses exceeding 6 billions of dollars [18]. Several vulnerability detection tools for smart contracts have been developed in recent years. For Ethereum — largely the main smart contract platform —

dozens are available [46,34,53], spanning techniques from static analysis and symbolic execution to fuzzing, and, recently, machine-learning [41] and LLMs [50,21]. However, their effectiveness in preventing real-world attacks remains debated. Despite the availability of multiple vulnerability detection tools, attacks against smart contracts continue to proliferate, exploiting subtle flaws in the contracts’ business logic rather than well-known vulnerability patterns. Empirical studies confirm this trend. For instance, the analysis in [18] shows that existing vulnerability detection tools could have prevented only about 8% of $2.3 billion in total losses due to attacks, and only when these attacks exploited well-known vulnerabilities such as reentrancy. The problem is that many high-impact incidents stem instead from logic errors in contract implementations — i.e., flaws in protocol logic or economic rules. Such errors typically fall outside the scope of vulnerability detection tools, which are mainly designed to identify specific classes of bugs (e.g., overflows and reentrancy). In contrast, formal verification offers a principled defense against these attacks, as it enables developers to verify that smart contracts satisfy a specification capturing their intended behaviour. For Solidity, the most widely adopted smart contract language, a few formal verification tools have been developed that can verify (or refute) user-defined properties concerning the business logic of a contract. Notable tools include SolCMC [4], shipped with the Solidity compiler, and the Certora Prover [30], a leading tool in the smart contract auditing industry. However, a key limitation of these tools lies in the expressiveness of the properties they support [9,7]. For example, several real-world attacks exploit liquidity weaknesses in smart contracts, whereby an attacker drives the contract into a state in which a legitimate user can no longer perform an otherwise permitted action, such as withdrawing tokens. Such vulnerabilities have been exploited in practice to steal or permanently freeze crypto-assets [3]. Another widespread type of attack is front-running, where the adversary exploits the transaction sequencing mechanism in order to obtain a profit at the expense of legit users [22,47]. Both liquidity and front-running attacks involve behaviours that span multiple transactions and depend on the evolution of the contract state over time. Capturing these vulnerabilities therefore requires reasoning about temporal properties — for instance, that certain actions remain eventually enabled for honest users, or that an adversary who front-runs a user’s transaction cannot break some desired invariant. Such properties go beyond those typically supported by existing smart contract verification tools such as SolCMC and the Certora Prover. Contributions We propose KindHML, a tool that verifies complex temporal properties of smart contracts. KindHML takes as input a contract, written in a purified version of Solidity, and a set of user-defined properties. Such properties are expressed in a novel specification language (CHML), which extends first-order Hennessy-Milner logic with domain-specific constructs for the smart contracts setting. In particular, CHML can express liquidity and front-running properties that are out of the scope of what can be expressed in existing verification tools for smart contracts, including industrial tools such as SolCMC and the Certora Prover, as well as academic tools. We experiment KindHML on

a benchmark of smart contracts, showing that it can effectively verify complex properties. KindHML provides developers with useful feedback, by detecting logical errors that would otherwise remain unnoticed. In particular, when KindHML detects a property violation, it produces a concrete execution trace that leads the contract to a state from which the desired asset exchange is unrealisable. To the best of our knowledge, KindHML is the first tool capable of verifying front-running properties of smart contracts. Summing up, the main contributions of the paper include: – CHML, a novel temporal logic that can express complex temporal properties of smart contracts (encompassing, e.g., liquidity and front-running); – a fully automated toolchain that encodes CHML properties and an expressive fragment of Solidity into Lustre [27], and verifies the resulting specification using Kind 2 [19]; – an empirical evaluation of the effectiveness of the proposed approach. Our toolchain and experimental data are publicly available on github. Structure. The paper is organized as follows. In Section 2 we describe the system model. In Section 3 we introduce some use cases, that we use to present CHML (Section 4) and the encoding of CHML to first-order logic Section 5. Implementation details and experimental evaluation are in Section 6. Related work is discussed in Section 7. Finally, in Section 8 we draw some conclusions and discuss future work.

2

System model

We consider a system model inspired by stateful account-based platforms such as Ethereum. In particular, we formalize a fragment of Solidity, the main contract language in the Ethereum platform. For simplicity, we describe here an untyped version of the language, where type declarations are omitted, and booleans are encoded as integers. The concrete language we have implemented in our tool is typed, and it features a type system to rule out type mismatches. 2.1

Background

From the perspective of smart contract programming, a blockchain can be viewed as an asset-exchange state machine. The global state records the assets owned by each account. User-created transactions trigger state transitions that may transfer assets among accounts. In Solidity, accounts are of two kinds: externally owned accounts (EOAs) and contract accounts. EOAs are controlled by users through cryptographic keys and can initiate transactions, while contract accounts are controlled by the code of a deployed contract and can execute transactions only in response to calls from other accounts. Such calls resemble method invocations in object-oriented languages, with contracts playing the role of objects whose methods can be

invoked by other contracts and EOAs. The global state of the blockchain can thus be seen as a mapping that assigns to each EOA its balance of native assets (e.g., ETH in Ethereum), and to each contract account both a balance and a storage. The storage contains the persistent variables and data structures (e.g., key-value maps) that overall define the contract state. Transactions can update the balance and the storage of the invoked accounts, as well as the balance of the transaction sender. Despite this resemblance, smart contracts differ from objects in several key aspects. In particular, smart contracts execute in a public, permissionless environment in which transaction ordering is determined through a consensus protocol among mutually untrusted (possibly, adversarial) nodes. Moreover, once deployed on the blockchain, the code of a smart contract cannot be modified. As a consequence, bugs discovered after deployment cannot be fixed, making it critical to verify the security of contracts before they are deployed. 2.2

Syntax of the Solidity fragment

A contract can be seen as a public API through which users exchange tokens. For simplicity, we assume a single token type — typically, the native cryptocurrency provided by the underlying blockchain (e.g., ETH for Ethereum). Users → c ::= contract C { − p }

Contract

p ::= f(x1 , . . . , xk ){s}

Procedure

s ::= | skip | require e | x=e | x[e1 ] = e2 | e1 .transfer(e2 ) | s1 ; s2 | if e then s1 else s2 | C . f(e1 , . . . , ek )$e

Statement skip require condition assignment map update token output sequence conditional contract call

e :: = | null | n | X | x | e.x | e.x[e′ ] | e ◦ e′ | sender | value | this

Expression undefined integer constant address constant variable lookup field lookup map lookup operation transaction sender transaction value self address

Fig. 1: Syntax of contracts.

interact with a contract via addresses, which serve as pseudonymous identifiers corresponding to their public keys. We use colors to discriminate between different types of addresses: user addresses A, B, . . . are in red, contract addresses C, D in blue, and arbitrary (user or contract) addresses X, Y, . . . in black. We specify a contract C as a finite set of procedure declarations of the form: f(x1 , . . . , xk ){s} where f is the procedure name, x1 , . . . , xk is the sequence of formal parameters, and s is the procedure body (see Figure 1). We assume that all the procedures in a contract have distinct names, and a special procedure, called constructor, which must be called (only once) before any other call. Statements and expressions extend those of a standard loop-free imperative language with a few domain-specific constructs: – X.transfer(n) transfers n token units from the contract to address X; – X.balance is a special key, associated to the storage of address X, representing the amount of tokens owned by that address. Unlike other keys, the balance cannot be updated through assignments; rather, its updates are handled automatically by the contract semantics; – require e aborts the execution of a procedure, rolling-back its effects, if the boolean condition e is false; otherwise, it continues the execution. We formalize the syntax of our Solidity fragment in Figure 1. Note that KindHML includes a type system that rules out ill-typed contracts. 2.3

Semantics of the Solidity fragment

Users interact with contracts by sending transactions, which trigger calls to the contract API. They have the form A : C.f(v1 , · · · , vk )$n where: – A is the address of the user who signed the transaction. This address can be accessed within a contract through the expression sender; – C is the called contract (identified by its address); – f is the called procedure, and v1 , · · · , vk are the actual parameters; – n is the number of tokens transferred from the sender to the contract along with the call. This value can be accessed within a contract through the expression value. We omit zero values for brevity. We model the interactions between users and contracts as a transition system between blockchain states σ, σ ′ , . . . A blockchain state σ maps each address X to a storage σ(X). For contract addresses, the storage is a key-value map that associates a value to each field (including the special field balance). For user addresses, the storage is a special case in which the only valid key is balance. Executing a transaction A : C.f(v1 , · · · , vk )$n in state σ amounts to the following steps: (i) check that the sender has sufficient balance to transfer n tokens to the contract; (ii) check that the procedure f with the expected signature belongs to the contract C, and retrieve its statement s; (iii) define a state σ ′′ that accounts for the transfer of n tokens from the sender A to the contract C; (iv) map the formal to the actual parameters of the called procedure, also taking the special variables sender, value, and this into accoiunt; (v) evaluate the

statement s in state σ ′′ , producing a new state σ ′ . If some require commands in the statement s fail, then the evaluation of s gives ⊥, representing an execution error. This makes the premise false, and so the transition does not happen. We use the standard notation {v/x} to represent a partial function mapping x to v. This can be composed with other partial functions as usual: e.g., ρ{v/x} is the function ρ′ such that ρ′ (x) = v and ρ′ (y) = ρ(y) for y ̸= x. We use the syntactic sugar σ(X.x) to denote the value of key x at address X, and σ{v/X.x} to denote an update of key x at address X in storage σ. More formally, we define: σ(X.x) = σ(X)(x)

σ{v/X.x} = σ{f/X } where f = σ(X){v/x}

State transitions between blockchain states are labelled with the transactions fired by users. The transition relation −→ is specified by the following rule: σ(A.balance) ≥ n

f(x1 , . . . , xk ){s} ∈ C

′′

σ = σ{σ(A.balance)−n/A.balance}{σ(C.balance)+n/C.balance} ⟨s, σ ′′ ⟩ρ ⇒ σ ′

ρ = {v1/x1 · · · vk/xk }{A/sender}{n/value}{C/this} A : C.f(v1 ,··· ,vk )$n

σ −−−−−−−−−−−−→ σ ′ We say that a transaction T is valid in a blockchain state σ when there exists T T some σ ′ such that σ − → σ ′ . We write σ − → ̸ when T is not valid in σ. We now comment the five premises of the rule: – The premise σ(A.balance) ≥ n checks that the sender has sufficient balance to transfer n tokens to the contract. – The second premise checks that the procedure f with the expected signature belongs to the contract C, and retrieves its statement s. – The second line defines a state σ ′′ that accounts for the transfer of n tokens from the sender A to the contract C. – In the third line, we define a map ρ from the formal to the actual parameters of the called procedure. The map also includes bindings for sender and value, and for the keyword this, which is associated to the address of the called contract. We will use this map when giving semantics to expressions and statements.

JnullKρ,σ = null JxKρ,σ = ρ(x)

JnKρ,σ = n

JeKρ,σ = X Je.xKρ,σ = σ(X.x)

JeKρ,σ = n Je′ Kρ,σ = n′ Je ◦ e′ Kρ,σ = n ◦ n′

JXKρ,σ = X JeKρ,σ = X Je′ Kρ,σ = k Je.x[e′ ]Kρ,σ = σ(X.x)(k)

y ∈ {sender, value, this} JyKρ,σ = ρ(y)

Fig. 2: Semantics of expressions.

⟨skip, σ⟩ρ ⇒ σ JeKρ,σ = true ⟨require e, σ⟩ρ ⇒ σ JeKρ,σ = v

JeKρ,σ = false ⟨require e, σ⟩ρ ⇒ ⊥

x ̸∈ {balance, sender, value, this} ⟨x = e, σ⟩ρ ⇒ σ{v/C.x}

ρ(this) = C

Je1 Kρ,σ = k

Je2 Kρ,σ = v ρ(this) = C f ′ = σ(C.x){v/k} ′ ⟨x[e1 ] = e2 , σ⟩ρ ⇒ σ{f /C.x}

Je1 Kρ,σ = X

Je2 Kρ,σ = n

σ

′

ρ(this) = C

σ(C.balance) ≥ n

= σ{σ(X.balance)+n/X.balance}{σ(C.balance)−n/C.balance} ⟨e1 .transfer(e2 ), σ⟩ρ ⇒ σ ′ ⟨s1 , σ⟩ρ ⇒ σ ′′ ⟨s2 , σ ′′ ⟩ρ ⇒ σ ′ ⟨s1 ; s2 , σ⟩ρ ⇒ σ ′ JeKρ,σ = b ⟨sb , σ⟩ρ ⇒ σ ′ ⟨if e then strue else sfalse , σ⟩ρ ⇒ σ ′ f(x1 , . . . , xk ){s} ∈ C ρ(this) = D

σ

′′

Jei Kρ,σ = vi (i ∈ 1..k)

JeKρ,σ = n ≤ σ(D.balance)

= σ{σ(C.balance)+n/C.balance}{σ(D.balance)−n/D.balance}

ρ′ = ρ{v1/x1 · · · vk/xk }{D/sender}{n/value}{C/this} ⟨C . f(e1 , . . . , ek )$e, σ⟩ρ ⇒ σ ′

⟨s, σ ′′ ⟩ρ′ ⇒ σ ′

Fig. 3: Semantics of statements. – Finally, the premise ⟨s, σ ′′ ⟩ρ ⇒ σ ′ evaluates the statement s in state σ ′′ (i.e., the state that results from σ after updating the caller and contract’s balances) producing a new state σ ′ . If some require commands in the statement s fail, then the evaluation of s gives ⊥, representing an execution error. This makes the premise false, and so the transition does not happen. The semantics of expressions is defined, in a big-step style, by the partial function J·Kρ,σ in Figure 2. The rules that inductively define this function are mostly standard. We just note that the evaluation of an ill-typed expression, such as 2 + A or C.x when x is not a field of C, is undefined. The semantics of statements is defined, also in a big-step style, by the relation ⟨·, σ⟩ρ in Figure 3. When this function is defined, it gives the new storage state σ ′ obtained after evaluating the statement. Note that the relation ⇒ is deterministic: therefore, also the state transition relation → − is deterministic. We say that a blockchain state is initial when all contracts have zero balance, their integer fields are set to 0, and their address fields are set to null .

3

Use cases

In this section we describe the use cases that we will use to validate our approach. 3.1

Bank contract

contract Bank { mapping ( address = > uint ) credits ; function deposit () payable { credits [ msg . sender ] += msg . value ; } function withdraw ( uint amount ) { credits [ msg . sender ] -= amount ; msg . sender . t r a n s f e r ( amount ) ; } }

Listing 1.1: A simple Bank contract. Consider the simple bank contract in Listing 1.1. Its storage consists of a single key-value map credits, which records the number of ETH units associated to each bank’s client. Its public interface consists of two functions, deposit and withdraw, which can be called by any account at any time. When an account invokes the function deposit, two effects occur: (i) an amount of ETH specified by the caller is implicitly transferred from the caller’s balance to the contract’s. In the code, the read-only variables msg.value and msg.sender denote, respectively, the amount and the caller; (ii) the caller’s credit recorded in the contract storage is increased by the same amount. The withdraw function has a dual effect: (i) decrease the number of credits of the caller; (ii) transfer amount ETH to the caller. Note that if some of the implicitly required conditions are not satisfied (e.g., the amount parameter of withdraw exceeds the caller’s credit), the transaction is reverted, meaning that all effects performed during its execution are rolled back. Despite its simplicity, the behaviour of this contract exhibits non-trivial properties, such as: – any user with a positive credit can always extract ETH; – the effect of two consecutive calls to deposit (resp., withdraw) by the same account is equivalent to a single call to the same function; – the effect of a call to deposit can be reversed by executing a suitable subsequent call; – each call affects the credits of exactly one account; – front-running a user’s deposit with someone else’s transaction has no effect on the user’s credits.

Reasoning about such properties requires a tool capable of handling both universal and existential quantification, as well as predicating about transactions fired across different execution paths. To the best of our knowledge, these features, in the level of generality required to precisely capture the properties above, are not supported by existing verification tools.

3.2

Bet contract

contract Bet { address oracle ; int rate ; constructor ( address o , int x ) payable { oracle = o ; rate = x ; } function join () payable { require ( balance ==2* value && player == null ) ; player = sender ; } function win () { require ( rate >100) ; player . t r a n s f e r ( balance ) ; } function set ( int x ) { require ( sender == oracle ) ; rate = x ; } }

Listing 1.2: A Bet contract.

Consider a simple bet contract with the following behaviour (see Listing 1.2). The constructor sets the oracle and the initial bet, i.e. the amount of tokens transferred upon deployment. The join procedure allows anyone to join the bet, by depositing into the contract an amount of tokens equal to the initial bet. The win procedure allows the previously joined player to withdraw the whole pot, provided that rate is greater than 100. Finally, the set procedure allows the oracle to set the rate. Consider an initial state σ0 where users A and B have 10 tokens each. We have the following computation, where as syntactic sugar we just write x to access a

field x within C, instead of writing C.x: A : Bet.constructor(M,1)$10

σ0 −−−−−−−−−−−−−−−−→ σ1

where

σ1 = σ0 {0/A.balance, 10/Bet.balance, M/Bet.oracle, 1/Bet.rate} B : Bet.join()$10

−−−−−−−−−−→ σ2 = σ1 {0/B.balance, 20/Bet.balance, B/Bet.player} M : Bet.set(150)

−−−−−−−−−→ σ3 = σ2 {150/Bet.rate} B : Bet.win()

−−−−−−−→ σ4 = σ3 {20/B.balance, 0/Bet.balance} At the end of the execution, B has withdrawn the entire pot from the contract.

contract Vault { address owner ; address recovery ; uint wait_time ; uint req_time ; address receiver ; int amount ; int state ; // 0 = IDLE , 1 = REQ constructor ( address r , int w ) payable { require ( msg . sender != r && w >=0) ; owner = msg . sender ; recovery = r ; wait_time = w ; state = 0 // IDLE } function withdraw ( address rcv , int amt ) { require ( state ==0) ; state = 1; // IDLE -> REQ require ( amt <= balance && msg . sender == owner ) ; receiver = rcv ; amount = amt ; req_time = block . number } function finalize () { require ( state ==1) ; state = 0; // REQ -> IDLE require ( block . number >= req_time + wait_time ) ; require ( msg . sender == owner ) ; receiver . t r a n s f e r ( amount ) } function cancel () { require ( msg . sender == recovery ) ; require ( state ==1) ; state = 0 // REQ -> IDLE } }

Listing 1.3: A Vault contract.

3.3

Vault contract

This contract allows the owner to deposit and withdraw tokens, with a mechanism to cancel pending withdrawal requests through a recovery key. Its behaviour is modelled as an automaton, i.e. certain actions are enabled only in certain states and at certain times. Once the vault contract (see Listing 1.3) have been deployed, it supports the following actions: (i) withdraw, which allows the owner to issue a withdraw request to the vault, specifying the receiver and the desired amount; (ii) finalize, which allows the owner to finalize the withdraw after the wait time has passed since the request; (iii) cancel, which allows the owner of the recovery key to cancel the withdraw request during the wait time. The action withdraw implements a state transition from IDLE to REQ, while finalize and cancel from REQ to IDLE.

4

CHML: a temporal logic for contracts

We now introduce our property specification language. Its foundation lies in Hennessy-Milner logic (HML) [28], a modal logic interpreted over labelled transition systems (LTSs), with a modal construct ⟨a⟩ ϕ to express the “possibility” of satisfying a state formula ϕ after performing the action a. More precisely, a state satisfies ⟨a⟩ ϕ if it admits an a-labelled transition to a state satisfying ϕ. Interpreting HML over the LTS of contracts in Section 2 would allow us to specify properties such as: “after firing transaction T, the balance of A is n”. However, specifying precise conditions on the reached state, such as “the balance of A is n”, is not particularly meaningful in our context. Rather, one is typically interested in relational properties between the pre- and post-state, such as “the balance of A is increased by n”. To capture this, we interpret formulae over sequences of blockchain states, and we introduce a construct old(e) that allows evaluating an expression e in the state before the last transition. Note however that the object referred to by the modal operator of HML is a constant. Consequently, applying HML to specify contract properties would require to explicitly provide the exact transaction T that leads to the new state. This would rule out the specification of more general and interesting properties such as: “Can A fire some transaction that increases her balance?”, or “Does there exist some address B ̸= A that can fire a transaction decreasing A’s balance?”. To overcome this limitation, we consider a first-order version of HML and extend the syntax of the modal operator to allow constraints over the individual fields of a transaction. The general form of our modal operator is the following: ⟨es : C.ef (e1 , . . . , ek )$ev ⟩ ϕ where es is an expression specifying the transaction sender, C is the target contract (a constant address), ef is the called procedure (either constant or variable), e1 , . . . , ek is a sequence of expressions representing the procedure parameters, and ev is an expression specifying the value transferred along with the transaction. Since we are adopting a first-order version of HML, variables occurring in

e ::= | n | X | f | x | e.x | e.x[e′ ] | sender | value | e1 ◦ e2 | old(e) | reverted

Expression integer constant address constant procedure constant variable field map entry transaction sender transaction value operation previous state transaction revert

τ ::= | bool | int | address | proc | args

Type bool integer address method any params

ϕ ::= | e | ¬ϕ | ϕ1 ∧ ϕ2 | ∀x : τ. ϕ | ⟨es : C.ef (e1 , . . . , ek )$ev ⟩ ϕ

Formula expression negation conjunction quantification transaction

Fig. 4: Syntax of contract specifications. the modal operator can be universally or existentially quantified. This makes it possible to express complex properties like those informally discussed earlier. 4.1

Syntax

We define properties of blockchain states as formulae ϕ, ϕ′ , . . ., with the syntax in Figure 4. The base case is given by (boolean) expressions on blockchain states, which extend those of the contract language with the constructs old(e) and reverted. Intuitively, old(e) evaluates the expression e in the previous computation state, while reverted is true whenever the transaction leading to the current state reverted (i.e., it is not valid). Logical negation and conjunction are standard; the other connectives can be obtained as syntactic sugar as usual. The formula ∀x:τ. ϕ universally quantifies over the variable x (of type τ). As usual, ∃x:τ. ϕ is syntactic sugar for ¬∀x:τ. ¬ϕ. The formula ⟨es : C.ef (e1 , . . . , ek )$ev ⟩ ϕ generalises the modal operator ⟨a⟩ of HML in order to allow a fine-grained treatment of transaction parameters. 4.2

Typing of CHML logic

While in Section 2 we followed a minimalist approach, presenting an untyped version of the contract language, here we opt for a typed presentation of the specification language, since the use of types therein is not as straightforward. However, for succinctness we only elaborate on the less standard aspects of our type system. KindHML includes a type checker that ensures the well-typedness of specifications and prevents typing errors. The types τ (see Figure 1) include the base types bool, int and address already (implicitly) used in the contract language, and the additional types proc and args. The type proc represents the set of all procedure names, while args represents the set of all possible sequences of procedure parameters. These types are typically used in synergy with quantification and the modal operator to specify transition invariants, i.e. properties that must hold for every possible

procedure call. For example, we can express the property “for all state transitions, the balance of A is preserved” as follows: ∀a : address. ∀f : proc. ∀x : args. ∀n : int. ⟨a : C.f (x)$n⟩ A.balance = old(A.balance) We rule out ill-typed specifications through a type system: its rules are mostly standard, with the only exception of the rules to ensure that old(e) expressions do not go out of scope. To this purpose, type judgments for expressions have the form Γ, n ⊢ e:τ, where Γ is a mapping from variables to types and n is a nonnegative integer representing the level of nesting of e within modal operators. The key typing rule for expressions is: Γ, n − 1 ⊢ e:τ n>0 Γ, n ⊢ old(e):τ The rest of the typing rules for expressions are standard. Typing judgments for formulae have the form Γ, n ⊢ ϕ. We say that ϕ is well-typed when ∅, 0 ⊢ ϕ, where ∅ is the empty typing environment. The key typing rules are those for quantified formulae and for the modal operator: Γ {τ/x}, n ⊢ ϕ Γ, n ⊢ ∀x:τ.ϕ Γ, n ⊢ es : address Γ, n ⊢ ev : int Γ, n + 1 ⊢ ϕ f(x1 :τ1 , . . . , xk :τk ) ∈ C ∀i ∈ 1..k: Γ, n ⊢ ei : τi Γ, n ⊢ ⟨es : C.f(e1 , . . . , ek )$ev ⟩ ϕ Γ, n ⊢ es : address Γ, n ⊢ ev : int Γ, n + 1 ⊢ ϕ Γ, n ⊢ x : proc Γ, n ⊢ y : args Γ, n ⊢ ⟨es : C.x(y)$ev ⟩ ϕ The rule for typing universal quantifications is straightforward: ∀x:τ.ϕ is typeable in Γ if ϕ is typeable in a typing environment that extends Γ with the binding from x to τ. We split the typing of the modal operator in two rules for convenience. In the first rule, f is a constant function name. In that case, the premises require all the function parameters to have the type declared in the contract (here we assume a typed version of the contract language). Note that ϕ must be typeable in a judgment with n + 1, since we are adding a nesting level. The third rule deals with the case where the function name is a variable x: in that case, the only possible parameter can be another variable y, which must have type args. For example, let C be a contract with a procedure f with zero parameters and a procedure g with one int parameter, and consider the formulae: ϕ1 = C.balance > old(C.balance) ϕ2 = ⟨A : C.f()$0⟩ ϕ1 ϕ3 = ∀x : proc. ∀y : args. ⟨A : C.x(y)$0⟩ ϕ1

The formula ϕ1 is not well-typed, since inferring a typing judgment ∅, 0 ⊢ old(C.balance) : int would require to satisfy the premise ∅, −1 ⊢ C.balance : int, which is forbidden by the rule premises. Instead, both ϕ2 and ϕ3 are well-typed, since the rule for typing the modal operator increases the n in the typing judgment, and ∅, 1 ⊢ ϕ1 . 4.3

Semantics

To interpret CHML, we first extend the contract semantics of Section 2 in order to have a left-total transition relation, admitting state transitions for all possible labels. The intuition is to flag blockchain states σ to indicate whether the last fired transaction was enabled or not. Formally, the states S of this extended system are pairs (σ, b) where σ is a blockchain state and b is a bit representing whether the last transaction was reverted (b = 1) or not (b = 0). We define the transition relation 7− → between flagged blockchain states as follows: T

σ −−→ σ ′

T

σ −− ̸→

T

(σ, b) 7−−→ (σ, 1)

(σ, b) 7−−→ (σ ′ , 0)

T

T

The relation 7− → is left-total: for all S and T, there exists S ′ such that S 7− → S ′. We interpret expressions and formulas over non-empty finite sequences Σ of flagged states. Given a (possibly empty) sequence Σ and a state S , we denote by S ::Σ the sequence with head S and tail Σ , with hd(Σ ) the head of Σ , and with tl(Σ ) its tail (which is possibly empty). The interpretation of expressions in contract specifications follows closely that in Figure 2. We only elaborate on the semantics of the new expressions, i.e. old(e) and reverted. The evaluation of old(e) in a sequence Σ is defined as Jold(e)KΣ = JeKtl(Σ ) , i.e. the evaluation of e in the previous step of the computation tl(Σ ). The evaluation of reverted just retrieves the revert bit from the heading flagged state, i.e. JrevertedKΣ = b whenever hd(Σ ) = (σ, b). The interpretation of formulae is defined in Figure 5. In the first rule, note that the type system ensures that only boolean expressions can be interpreted. The rules for logical connectives are standard. For universal quantification, we have two rules. The first rule deals with variables of any type except args: we substitute the variable x with any possible value of the same type, and require that the resulting formula is true. Note that these substitutions preserve welltypedness. The second rule deals with the case where x has type args: we substitute x in ϕ with any possible sequence of values v, provided that the resulting formula is well-typed. The rule for the modal operator requires the transaction T to be fully instantiated (this is guaranteed by the type system). It first computes the new state S reached upon firing T in the current state hd(Σ ), and then evaluates ϕ in S ::Σ . Since 7− → is left-total, this rule is always applicable. Our verification goal is to decide, given a formula ϕ and an initial state S , whether S ′ |= ϕ for all S ′ reachable from S .

Σ |= e

if JeKΣ = true

Σ |= ¬ϕ

if not Σ |= ϕ

Σ |= ϕ1 ∧ ϕ2

if Σ |= ϕ1 and Σ |= ϕ2

Σ |= ∀x:τ. ϕ

if τ ̸= args and Σ |= ϕ{v/x} for all v:τ

Σ |= ∀x:args. ϕ

if Σ |= ϕ{v/x} for all v such that ⊢ ϕ{v/x}

Σ |= ⟨T⟩ ϕ

if hd(Σ ) 7− → S and S ::Σ |= ϕ

T

Fig. 5: Interpretation of contract specifications. 4.4

Example: a bet contract

Consider a Bet contract with the following methods: (i) the constructor sets an oracle and the initial bet, which is the amount of tokens transferred upon deployment; (ii) join allows anyone to join the bet, by depositing into the contract an amount of tokens equal to the initial bet; (iii) win allows the previously joined player to withdraw the whole pot, provided that rate is greater than 100; (iv) set allows the oracle to set the rate. We show how to specify relevant properties of the bet contract in CHML. Consider the property: “if the rate is greater than 100 and the player has joined, then some user can fire some transaction to withdraw the entire pot”. We call this property winnability and formalise it in CHML as follows: ϕ1 = (Bet.rate > 100 ∧ Bet.player ̸= null) → ∃a : address. ∃f : proc. ∃x : args.
⟨a : Bet.f (x)$0⟩ a.balance = old(a.balance + Bet.balance) We expect ϕ1 to be true in all reachable states: the procedure to be called is win, and the only possible sender is Bet.player. Note instead that if we replace the ∃a with a ∀a, i.e. if we ask whether any user can withdraw the pot, then the property becomes false, despite the fact that anyone can call win. A general desirable property is liquidity, i.e. it is always possible to withdraw all tokens from the contract. For the Bet contract, it is always possible to achieve this goal in at most two steps. We formalise this property in CHML as follows: ϕ2 = Bet.player ̸= null → ∃a1 , a2 : address. ∃f1 , f2 : proc. ∃x1 , x2 : args.
⟨a1 : Bet.f1 (x1 )$0⟩ ⟨a2 : Bet.f2 (x2 )$0⟩ Bet.balance = 0 We now ask whether the contract is subject to attacks in which an adversary front-runs another user’s transaction in order to prevent the user from winning. In the Bet contract, we have such an attack when the player is willing to fire a win transaction, and the adversary front-runs it with a transaction that decreases the rate, making the player’s transaction revert. We formalise this frontrunning attack in CHML as follows: ϕ3 = ∀a : address. ∃b : address. ∃f : proc. ∃x : args. ⟨b : Bet.f (x)$0⟩ ⟨a : Bet.win()$0⟩ reverted

We expect ϕ3 to be true: indeed, any win transaction is reverted when Bet.oracle anticipates it with a transaction set(x) with argument x ≤ 100. If we modify ϕ3 by requiring that b ̸= Bet.oracle, we expect instead the property to be false, since only the oracle has the rights to call set.

5

Encoding in first-order logic

We now formalize our encoding from contracts and CHML into first-order logic, and refer to Section 5.3 for a worked example. We assume a set of state variables (SVars) and a set of transition variables (TVars), with types ranging over bool, int, address, proc, or address ⇒ τ with τ ∈ {bool, int, address}. Let Addr = {v | type(v) = address} be a finite set, let Contr = {C1 . . . , Cn } ⊆ Addr the set of contract addresses, and let Proc = {f1 , . . . , fp } the set of constants of type proc representing procedures. State variables include the following: balance : address → int representing address balances, revert : bool representing whether the last transaction reverted, constructedC : bool for every C ∈ Contr, representing whether C has already been constructed or not, and a variable for each field of each contract, with its given type. We denote the set of such variables as SVarsF . Transition variables include: tx .sender : address for the transaction sender, tx .value : int for the transaction value, cx : address for the called contract, fx : proc for the name of the called procedure, and a variable for each parameter of each procedure, with its respective type. Given a constant f ∈ Proc representing a procedure with parameters x1 , . . . , xk , we denote the set of variables corresponding to theseSparameters as TVarsP (f ) = {f _x1 , . . . , f _xk }. We also define TVarsP := f ∈Proc TVarsP (f ). Given these definitions, the encoding of expressions is straight-forward. Occurrences of this are replaced by the address constant that respresents the contract in which this appears. 5.1

Encoding the contract

We now show how to encode the state transition system of Section 2 into firstorder logic formulas. As common in SMT-based model checking [12], we define a formula Init that describes the set of initial states, and a formula Trans that describes the relation between current state variables, transition variables, and next state variables. V Init is the conjunction of the V following constraints: a∈Addr balance(a) ≥ 0 (balances are nonnegative), V c∈Contr constructedc = ⊥ (contracts have not been constructed yet), and v∈SVarsF v = default_value(type(v)) (all contract fields are set to a default value determined by their type). Since the imperative nature of the contract language allows variables to be updated multiple times within a single call, to capture intermediate states in the definition of Trans we introduce sets of temporary state variables SVarsj for j ∈ 1..m + 1 — where m is the maximum depth of statements — each SVarsi being a copy of SVars. For all v ∈ SVars, we denote with v i the corresponding

temporary variable in SVarsi . Finally, we introduce a copy nxSVars of SVars to represent “next” state variables, and, for all v ∈ SVars, we denote with v nx the corresponding variable in nxSVars. The formula Trans describes the relation between SVars, TVars, and nxSVars. We now define the encoding of a procedure f(x1 , . . . , xn ){s1 ; . . . ; sm } in a contract C. W.l.o.g., we assume that none of the si contains sequential compositions. Initially, the nesting level is i = 0, and we define SVars0 := SVars. We define an operator Φ that maps statements to first-order formulas, such that, for each si , Φ(si ) uniquely determines the values of all the variables in SVarsi+1 as a function of the values of the variables in SVarsi and in TVars. For brevity, in the description below we omit the constraints of the form v i+1 = v i , i.e., when the value of v does not change passing from nesting level i to i + 1, we do not explicitly write the equality. First, we encode the transfer of tx .value tokens from tx .sender to C made along with the call (which can be seen as an implicit default statement s0 ): Φ(s0 ) := ITE(send_enabled0 (tx .sender , C, tx .value), revert1 = ⊥ ∧ send0 (tx .sender , C, tx .value), revert1 = ⊤) where ITE is the standard if-then-else construct, and: send_enabledi (e0 , e1 , e2 ) := balance(e0 )i ≥ ei2 ∧ ei0 ̸= ei1 and ^

sendi (e0 , e1 , e2 ) :=

balance(a)i+1 =ITE a = ei0 ,

a∈Addr

balance(a)i − ei2 , ITE(a = ei1 , balance(a)i + ei2 ,
balance(a)i ) Then, for each statement si , we define the encoding Φ(si ) in Table 1. A procedure reverts if any of its statements si reverts, i.e. if reverti = ⊤ for some i ∈ 1..m + 1. If it does not revert, then the next state of each variable v is given by v m+1 . Overall, for a procedure p, the relation between current state variables and next state variables is given by:  _  ^ ^ ^ Trans p := ITE reverti , v nx = v 0 , v nx = v m+1 ∧ Φ(si ) i∈1..m+1

v∈SVars

v∈SVars

i∈0..m

Note that Trans p depends on all the SVarsj , for j ∈ 0..m + 1. However, by the definition of Φi given before, we have that for all i ∈ 1..m + 1 and v i ∈ SVarsi , there is an equation of the form v i = ψvi (SVarsi−1 , TVars), for a

Table 1: Encoding of contracts into first-order logic. Statement si FOL encoding Φ(si ) skip ⊤ require e reverti+1 = ITE(ei , ⊥, ⊤) x=e xi+1 = ei V i+1 x[e1 ] = e2 = ITE(a = ei1 , ei2 , x_ai ) a∈Addr x(a) 1 0 i 1 if e then si else si ITE(e , Φ(si ), Φ(s0i )) reverti+1 = ⊥ ∧ sendi (C, e1 , e2 ), e1 .transfer(e2 ) ITE(send_enabledi (C, e1 , e2 ), reverti+1 = ⊤)

suitable ψvi that only depends on variables in SVarsi−1 and in TVars. Hence, we can rewrite the equations in Trans p in the form v nx = χv (SVars, TVars), where each χv (SVars, TVars) is obtained by exhaustively substituting, for every variable v ∈ SVars and for every i ∈ 1..m + 1, all the occurrences of v i with ψvi (SVarsi−1 , TVars). After such substitutions, we obtain that Trans p only depends on SVars, TVars, and nxSVars. In order to encode a contract c ≡ C { (p1 , . . . , pk ) }, we simply define Trans c := switch fx {case p1 :Trans p1 | · · · | case pk :Trans pk } where the switch-case operator is just syntactic sugar for a sequence of nested ITEs. The encoding of a whole system is: Trans := switch cx { case c1 :Trans c1 | · · · | case ck :Trans ck } 5.2

Encoding the property

We now show how to encode CHML into first-order logic. Such encoding is rather straightforward except for the modal operator ⟨·⟩, for the operator old(·), and for the type args. First, note that the nesting of modal operators within a formula ϕ gives rise to a tree T , defined as follows. We associate to ϕ the root of the tree. Then, recursively, for every occurrence of the modal operator ⟨a⟩ψ, we associate to the subformula ψ a child of the current node, and to a the connecting edge. To each node V of the tree, we associate a copy of the set of state variables (denoted by SVarsV ), and to each edge E we associate a copy of the set of transition variables (TVarsE ). For v ∈ SVars, we denote with v V the corresponding fresh variable in SVarsV , and, similarly, for v ∈ TVars, we denote with v E the corresponding fresh variable in TVarsE . We define an operator ΦV,E that, given a node V and an edge E, maps expressions and formulae of the property specification language to first-order logic terms and formulae. For every formula ϕ not containing the modal operator, the old() operator, V E or variables of type args, we define ΦV,E (ϕ) := ϕ{SVars /SVars}{TVars /TVars}.

Now we consider the remaining cases. Let ϕ be a formula containing the subformula ⟨es : C.ef (e1 , . . . , ek )$ev ⟩ψ, and let V be the node associated to ϕ, E be the edge associated to ⟨es : C.ef (e1 , . . . , ek )$ev ⟩ψ, and V ′ be the child of V through E (i.e. the node associated to ψ). Then, we define: ΦV,E (⟨es : C.ef (e1 , . . . , ek )$ev ⟩ ψ) := ∃ SVars

V′

∃ TVars

E

. . V

E

V′

Trans{SVars /SVars}{TVars /TVars}{SVars /nxSVars} ∧ tx .sender E = ΦV,E (es ) ∧ cx E = C ∧ fx E = ΦV,E (ef ) ∧ EqParams ∧ tx .value E = ΦV,E (ev ) ′

∧ ΦV ,E (ψ) where, in the case in which ef is a procedure constant with k parameters (i.e. V ef ≡ f , for f ∈ Proc), EqParams := vi ∈TVarsP (f ) viE = ΦV,E (ei ). Otherwise, the only other case admitted by the CHML type checker is that ef is a variable with a single argument of type args, i.e. ef (e1 , . . . , ek ) ≡ x(arg), with x : proc and arg : args. In order to define EqParams in this second case, we explain how variables of the type args are dealt with in the encoding in first-order logic. The type args, from the perspective of the encoding in first-order logic, can be seen as compact way to allow reasoning about the set of the procedure parameters TVarsP inside the arguments of the modal operators. We associate to each variable arg : args a copy TVarsarg of TVarsP (and, for all v ∈ P TVarsP , we denote with v arg the corresponding variable in TVarsarg P ). Then, every quantification on arg corresponds to a quantification on all the variables in TVarsarg P . That is, for the ∀ case (the ∃ case is analogous):   ΦV,E (∀arg. ϕ) := v arg . ΦV,E (ϕ) ∀ v∈TVarsP

We then define EqParams := v∈TVarsP v E = v arg . Finally, if we are in a node V , with Vp being the parent of V , we define V

ΦV,E (old(ϕ)) := ΦVp ,E (ϕ) Note that the existence of the parent node Vp , for a node V that contains an old() expression is guaranteed by the type checker. 5.3

Encoding of the Bet contract

In this section we exemplify our encoding into first-order logic by applying it to our Bet contract and its winnability property.

Encoding the contract. Recall the contract Bet in Listing 1.2. We have: – Contr = {Bet} – Proc = {constructor, pay, join, set} – SVars = {balance, revert, constructedBet , oracle, rate, player}, where: • oracle, player : address • rate : int – TVars = {tx .sender , tx .value, cx , fx , constructor_o_addr, constructor_x, set_x}, where: • constructor_o_addr : address • constructor_x and set_x : int Init is defined as follows: Init :=

^

balance(a) ≥ 0

a∈Addr

∧ constructedBet = ⊥ ∧ rate = 0 ∧ oracle = null ∧ player = null Consider the procedure join. We have that (besides the implicit s0 representing the payable modifier): s1 ≡ revert2 = ITE(balance(C)1 = 2 · tx .sender ∧ playeri = null, ⊥, ⊤) s2 ≡ player3 = tx .sender

Encoding the property. Recall the winnability property ϕ1 from Section 4.4: ϕ1 = (Bet.rate > 100 ∧ Bet.player ̸= null) → ∃a : address. ∃f : proc. ∃x : args.
⟨a : Bet.f (x)$0⟩ a.balance = old(a.balance + Bet.balance) Let V be the node associated to ϕ1 , let V ′ be the node associated to: ϕ′1 := a.balance = old(a.balance + Bet.balance) and let E be the connecting edge associated to ⟨a : Bet.f (x)$0⟩.

For simplicity, we assume that the contract has already been constructed, and we ignore the method constructor. Φ(ϕ1 ) = (rateV > 100 ∧ playerV ̸= null) →  ∃a : address. ∃f : proc. ∃set_xx : int. ′

∃balanceV : address → int. ′

∃oracleV : address. ′

∃rateV : int. ∃tx .sender E : address. ∃tx .value E : int. ∃fx E : proc. ∃set_xE : int. V

E

V′

Trans{SVars /SVars}{TVars /TVars}{SVars /nxSVars} ∧ tx .sender E = a ∧ fx E = f ∧ set_xE = set_xx ∧ tx .value E = 0 ′

∧ balance(a)V = balance(a)V + balance(Bet)V

6



Evaluation

We describe in this Section the implementation of our tool, the design of our benchmark, and the results of the evaluation. Implementation. KindHML takes as input a contract in our Solidity fragment and a set of CHML properties, it type-checks and translates them to Lustre, and finally model-checks with Kind 2 (Figure 6). The translation to Lustre follows the encoding described in Section 5. Since Kind 2 does not support maps within properties, our translation flattens map variables into integers (one per address). By default, Kind 2 runs multiple engines in parallel, each employing a different model-checking technique (e.g., bounded model checking [11], k-induction [43], and IC3 [16]). As back-end SMT solver, we selected cvc5. Benchmark. We evaluate our approach on a benchmark of representative use cases, covering different levels of complexity both in the contracts code and in the properties. In the design of the properties, we focus in particular on those that are beyond the reach of current verification tools for Solidity. For each use case we provide a main Solidity implementation and some mutations that introduce logic errors that may affect the validity of some the given properties.

KindHML

Contract.sol Abstract Syntax Tree

Contract&Properties.lus

ANTLR Parser

Valid Visitor

Kind2

Invalid T.O.

Properties.hml

Fig. 6: Architecture of KindHML.

For each verification task — i.e., pair (property, mutation) — we provide the ground truth, i.e. a boolean telling whether the property holds or not for that mutation. We summarize below the use cases and their main properties; their CHML formalization is in Table 2; their Solidity code is in Section 3. Bank This is a wallet contract that allows users to deposit and withdraw tokens. The contract storage consists of a map that records the credits of each user. We study the following properties: additivity a user performing two consecutive deposits of, respectively, n1 and n2 tokens, obtains the same effect with a single deposit of n1 + n2 tokens. reversibility after a user deposits, the same user can perform a transaction that restores their balance to the one before the deposit. liquidity any user with credits n can always can fire a transaction that increases its balance of any n0 ≤ n; frontrun deposit front-running a user’s deposit with someone else’s transaction has no effect on the user’s credits. Note that all these properties have a strategic nature, in that they predicate about the existence of a sequence of transactions leading to some desired effect on the contract state. To the best of our knowledge, no verification tool for Solidity can express general strategic properties such as the ones above (see Section 7). Vault. This contract allows the owner to deposit and withdraw tokens, with a mechanism to cancel pending withdrawal requests through a recovery key. Its behaviour is modelled as an automaton, i.e. certain actions are enabled only in certain states and at certain times. We consider the following properties: two-step drainability in idle state, some user can perform two transactions (possibly, at different blocks) to transfer the entire balance to some user. two-step non-inflation in idle state, firing two transactions within a window of wait_time blocks does not increase the balance of any user. As before, these are strategic properties involving universal and existential quantifiers (on the users and fired transactions), and are not supported by other verification tools besides ours.

Table 2: Use cases and their properties. Use case

Property liquidity

additivity Bank reversibility frontrun deposit two-step drainability Vault

two-step non-inflation winnability

Bet

liquidity frontrunning

CHML specification ∀a:address. ∀n:int. (n ≥ 0 ∧ n ≤ credits[a]) → ∃f :proc. ∃xl:args.
⟨a : Bank.f (xl)$0⟩ credits[a] = old(credits[a]) − n ∧ balance[a] = old(balance[a]) + n ∀a:address. ∀c1 , c2 :int. ∃v12 , v3 :int. ∃r1 , r2 , r3 :bool. (c1 ≥ 0 ∧ c2 ≥ 0) →   ⟨a : Bank.deposit()$c1 ⟩ r1 = reverted ∧
 ⟨a : Bank.deposit()$c2 ⟩ v12 = credits[a] ∧ r2 = reverted
∧ ⟨a : Bank.deposit()$(c1 + c2 )⟩ v3 = credits[a] ∧ r3 = reverted
 ∧ r1 ∨ r2 ∨ (¬r3 ∧ v12 = v3 ) ∀a:address. ∀c1 :int. ∃f :proc. ∃xl:args. ∃c2 :int.
⟨a : Bank.deposit()$c1 ⟩ ⟨a : Bank.f (xl)$c2 ⟩ balance[a] = old(old(balance[a])) ∀a1 , a2 :address. a1 ̸= a2 → ∀n1 , n2 :int. ∀f :proc. ∀xl:args. ∃v1 , v2 :int. 
⟨a1 : Bank.deposit()$n1 ⟩ v1 = credits[a1 ]
∧ ⟨a2 : Bank.f (xl)$n2 ⟩ ⟨a1 : Bank.deposit()$n1 ⟩ v2 = credits[a1 ]
 ∧ v1 = v2 state = 0 → ∃a, b:address. ∃f1 , f2 :proc. ∃xl1 , xl2 :args. ∃c1 , c2 :int.
⟨a : Vault.f1 (xl1 )$c1 ⟩ ⟨a : Vault.f2 (xl2 )$c2 ⟩ balance[b] = old(old(balance[b] + balance)) state = 0 → ∀a, b, c:address. ∀f1 , f2 :proc. ∀xl1 , xl2 :args. ∀c1 , c2 :int.  ⟨a : Vault.f1 (xl1 )$c1 ⟩ block.number ≤ old(block.number) + wait_time →
 ⟨b : Vault.f2 (xl2 )$c2 ⟩ balance[c] = old(old(balance[c])) (Bet.rate > 100 ∧ Bet.player ̸= null) → ∃a : address. ∃f : proc. ∃x : args.
⟨a : Bet.f (x)$0⟩ a.balance = old(a.balance + Bet.balance) Bet.player ̸= null → ∃a1 , a2 : address. ∃f1 , f2 : proc. ∃x1 , x2 : args.
⟨a1 : Bet.f1 (x1 )$0⟩ ⟨a2 : Bet.f2 (x2 )$0⟩ Bet.balance = 0 ∀a : address. ∃b : address. ∃f : proc. ∃x : args. ⟨b : Bet.f (x)$0⟩ ⟨a : Bet.win()$0⟩ reverted

Bet This is a two-players bet on the price of a token, which is queried from an external oracle. We consider the strategic properties introduced in Section 4.4. Results. We run KindHML on each verification task on a 3GHz 64-bit Intel Xeon Gold 6136 CPU and GNU/Linux OS (x86_64-linux) with 64 GB of RAM, with Kind 2 (v2.3.0-ge8216dd) and cvc5 (v1.1.3-dev.152.701cd63ef) as backend SMT solver. The run-time limit for each verification task is 1000s of CPU time. A subset of the results is shown in Table 3. We mark each verification task as: “✗ (N steps)”, if the solver finds a trace that violates the property (with N being the length of the shortest trace leading to a violation), and “✓ (k = N )”, if it proves that the property holds in all possible states (with N being the length of the k-induction base case). Discussion. The results show that KindHML always returns an answer consistent with the ground truth, and that it is effective both at proving the validity of the property as well as finding violations. When it finds a counterexample, it does so extremely quickly (always in less than 1 second), and it returns as witness a sequence of transactions that can be replayed in the actual Ethereum, leading to a state from which the desired outcome is unreachable (an example can be found here). Proving that a property is valid can be more time-consuming, as it requires performing advanced deductive reasoning based on inductive techniques. When a property is proven to be valid, the user has the mathematical guarantee that it cannot be violated in KindHML semantics. Given that KindHML abstracts

Table 3: KindHML results on our benchmark. Use case

Bank

Vault

Bet

Property

Mutation Ground truth Result Time (s) v1 ✓ ✓ (k = 2) 668.7 v2 ✓ ✓ (k = 2) 333.8 liquidity v3 ✗ ✗ (1 steps) 0.3 v4 ✓ ✓ (k = 2) 512.1 v1 ✓ ✓ (k = 1) 2.6 v2 ✗ ✗ (0 steps) 0.1 additivity v3 ✓ ✓ (k = 1) 17.3 v4 ✓ ✓ (k = 1) 3.4 v1 ✓ ✓ (k = 2) 21.6 v2 ✓ ✓ (k = 2) 26.7 reversibility v3 ✗ ✗ (0 steps) 0.2 v4 ✓ ✓ (k = 2) 31.9 v1 ✓ ✓ (k = 1) 22.1 v2 ✓ ✓ (k = 1) 26.9 frontrun deposit v3 ✓ ✓ (k = 1) 307.8 v4 ✗ ✗ (0 steps) 0.3 v1 ✓ ✓ (k = 2) 33.9 two-step drainability v2 ✗ ✗ (0 steps) 0.2 v3 ✓ ✓ (k = 2) 34.4 v1 ✓ ✓ (k = 1) 0.4 two-step non-inflation v2 ✓ ✓ (k = 1) 0.4 v3 ✗ ✗ (0 steps) 0.1 v1 ✓ ✓ (k = 2) 84.2 winnability v2 ✗ ✗ (1 steps) 0.3 v3 ✗ ✗ (1 steps) 0.3 v1 ✓ ✓ (k = 5) 90.6 liquidity v2 ✗ ✗ (1 steps) 0.4 v3 ✓ ✓ (k = 5) 97.3 v1 ✓ ✓ (k = 2) 166.1 frontrunning v2 ✓ ✓ (k = 1) 0.3 v3 ✗ ✗ (1 steps) 0.3

some semantical aspects of Solidity (e.g. reentrancy), it is not guaranteed that, moving to the actual Ethereum blockchain, the property will preserved “as-is”; however, the output of KindHML guarantees that no conceptual error has been made in the business logic of the contract.

7

Related work

Analysis tools for smart contract can be roughly partitioned in two classes: vulnerability detection tools, which target pre-defined classes of bugs (e.g., reentrancy, overflows, etc.) and verification tools, that instead can statically determine whether user-defined properties are satisfied in any contract executions. While vulnerability detection tools are not designed to capture violations of user-defined temporal properties, some of them can detect restricted instances of liquidity and front-running vulnerabilities through ad-hoc analyses tailored to specific patterns. In that setting, liquidity vulnerabilities are often referred to as “Locked Ether”, which roughly means that there is some contract state where it is impossible for anyone to withdraw Ether from the contract. The tools capable of detecting this vulnerability include Slither [23], SmartCheck [45], Maian [39], Securify2 [49], ConFuzzius [48] and sFuzz [38]. Each tool, however, has its own

interpretation of the property, making a comparison difficult [42]. A similar situation occurs for front-running, often referred to as transaction order dependence in vulnerability classifications [1]. A few tools can flag patterns in which the outcome of a transaction depends on shared state that can be modified by a competing transaction. For instance, Oyente [36], Securify [49], EthRacer [32] and SailFish [15] introduce specific patterns to detect when Ether transfers (including the amount and receiver) are affected by transaction ordering. There are two key differences between these tools and ours: – While vulnerability detection tools can provide smart contract developers with a useful feedback, spotting parts of the code that may contain potential vulnerabilities, they cannot determine that a contract enjoys some desirable property across all possible executions. By contrast, KindHML is a formal verification tool, and as such it can establish that a given property holds universally, or up to a given bound on the number of transactions. – Vulnerability detection tools typically lack flexible mechanisms for specifying the properties to be analysed. In most cases, they target predefined, hard-coded properties, offering little or no programmability. By contrast, KindHML allows developers to verify arbitrary CHML specifications. As shown in Section 6, this flexibility is crucial to establish relevant properties of smart contracts, such as general liquidity properties predicating on who can withdraw, how much, and under which conditions. Moving to verification tools, many support only safety properties, including e.g. of SolCMC [4], Zeus [31], solc-verify [26], SmartACE [51] and VerX [40]. We discuss below tools that handle a broader class of properties. The Certora Prover [30] is one of the leading formal verification tools for Solidity. The tool takes as input a Solidity contract and a specification in its domain-specific language (CVL), which defines constraints on the execution of a contract and assertions that must be true in all states satisfying the given constraints. Certora compiles the Solidity contract and the CVL spec into a logical formula, and relies on off-the-shelf SMT solvers to determine if the spec is satisfied in all contract states. Compared to KindHML, the Certora Prover is an industrial-strength tool that supports the full Solidity language, while ours is a prototype that targets a representative fragment. This design choice impacts the way certain properties are formalized. For example, in CHML one can directly specify that a transaction transfers a given amount of ETH to an account by constraining the account balance before and after the transaction. In other words, KindHML assumes that ETH transfers neither fail nor propagate the received tokens. Expressing the same property in CVL is quite problematic, since in full Solidity ETH transfers are rendered as external calls, which may trigger further calls that propagate additional transfers or revert the execution [9]. Another key difference between CVL and CHML concerns the treatment of quantification. In CVL, all free variables in a rule are implicitly universally quantified, while CHML supports arbitrary nesting of universal and existential quantifiers. This flexibility is essential for expressing strategic properties of contracts. For instance, for liquidity we want to specify that for all users there exists some transaction that

the user can execute to achieve a desired effect on their balance. Mixing universal and existential quantifiers is also needed to express properties such as reversibility (cf. Table 2). Regarding verification, KindHML and the Certora Prover adopt different approaches to reporting property violations. KindHML provided a concrete witness in the form of a sequence of transactions that, starting from an initial blockchain state, leas to a state in which the specified invariant is false. This implies that violations detected by KindHML can be translated into executable proofs-of-concept (up-to the abstractions introduced by the considered Solidity fragment). By contrast, when the Certora Prover reports a violation, it witnesses it through a blockchain state that is not guaranteed to be reachable. While this approach speeds-up verification, it has the drawback that negative verification reports cannot be directly translated into concrete exploits; moreover, in some cases, a property reported as violated may in fact hold in all reachable executions. SmartPulse [44] verifies Solidity contracts against specifications written in a language based on Linear Temporal Logic (LTL). While this enables expressing liveness properties, it does not capture liquidity and frontrunning, which lie beyond LTL. Thus, SmartPulse and KindHML have uncomparable expressiveness. Moreover, practical use of liveness properties requires a fairness assumption, i.e. another LTL formula specifying the traces in which users perform the actions needed to reach a desired state. In SmartPulse, this formula must be anticipated and encoded by the designer. Instead, KindHML can automatically infer the transaction parameters that produce the desired state change. VeriSolid [37] takes as input a Solidity contract and its properties expressed in Computation Tree Logic (CTL), transforms the contract into an Abstract State Machine (ASM), and verifies the properties against the ASM using tools in the BIP toolchain, such as the nuXmv symbolic model checker [13]. The liveness properties specified in [37] are not accompanied by fairness assumptions (unlike SmartPulse), but in principle this seems doable without reworking the verification techniques (we note that a more recent extension of VeriSolid includes fairness assumptions [17]). Liveness properties expressed in CTL, however, cannot encompass the strategic properties addressed by KindHML. In particular, CHML allows one to mix universal and existential quantification, which seems beyond the scope of the version of CTL supported by VeriSolid. Solvent [8] is a verification tool targeted to liquidity properties. It translates a fragment of Solidity similar to the one considered here into SMT constraints [6]. The set of properties expressible by Solvent is a subset of CHML. In particular, Solvent supports properties with a specific pattern: a universal quantification, followed by an existential quantification over a transactions; however, while this pattern is sufficient to characterise typical liquidity properties (e.g., “every user can fire a transaction that produces a certain effect”), it does not cover more complex properties that require arbitrary combinations of universal and existential quantifiers, such as most of those in Table 2. Another difference between Solvent and KindHML concerns the techniques used. Indeed, Solvent relies on bounded model checking (BMC) to return a counterexample (if the property is

violated), or show that, up to a certain number of transactions, the property holds. Except that in simple cases, in which naive predicate abstraction suffices, Solvent is not able to prove that a property holds for all reachable states. On the contrary, KindHML leverages all the advanced model checking techniques implemented in Kind 2, enabling the tool to prove validity also for complex instances, besides benefiting from well-rounded heuristics. Besides formal verification tools, recent work has explored the use of LLMs to assess the validity of arbitrary contract-specific properties written in natural language [10]. This approach allows users to investigate — potentially — any class of properties, including those not expressible in CHML (e.g., properties mentioning arbitrarily long sequences of transactions or assumptions on contractto-contract calls). However, the approach has two significant weaknesses: natural language properties are intrinsically ambiguous, and there is no guarantee that the answers provided by the LLMs are correct. In contrast, KindHML follows a principled formal method approach, which guarantees the correctness of its answers. CHML vs. other logics. Several modal logics allow predicates to range not only over states but also over actions. Among these, one of the most influential is Hennessy-Milner logic (HML) [28], a dynamic logic interpreted over LTSs. HML introduces the modal constructs ⟨Act⟩ ϕ and [Act] ϕ — where Act is a set of actions and ϕ a propositional formula — to express the conditions “there exists an action a ∈ Act (resp., “for all actions”), after which ϕ holds”. Since in HML only properties of finite depth can be described, an extension of HML with recursion [29] (equivalent to the modal µ-calculus [2]) has been proposed, enabling the expression of a wide range of temporal properties, including safety and liveness. Another temporal logic that allows to predicate over actions is Action CTL* (sometimes denoted ACTL*) [20], whose expressive power lies between that of HML and HML with recursion. Strategic logics such as ATL [5] extend temporal logics to reason about strategies of agents in multi-agent systems. There are several differences between CHML and the previous logics. Compared to HML, the verification problem over CHML asks whether the property holds in every reachable state (hence, for example, safety properties are expressible). Compared to HML with recursion and to Action CTL*, CHML is more restrictive, as it does not allow branching over arbitrarily long paths nor the use of the finally operator (hence liveness is not expressible). Using the terminology of Action CTL*, the verification of properties in CHML can be thought as corresponding to the verification of properties of the form “A G ϕ”, where ϕ can contain arbitrary combinations of “Eα X ” and “Aα X ” modal operators (the α subscript denotes predication over actions). Compared to strategic logics such as ATL and its extensions (e.g., WATL [24]), CHML can express “strategic properties” of the form “in every reachable state, a user (or a group of users) can always reach a desired state in a finite amount of steps” (e.g. liquidity), but it cannot express properties that predicates over users strategies intended as maps from (sequences of) states to actions. Additional differences with the previous logics are that CHML extends propositional logic to first-order (FO) logic, and

that it features a past operator. While temporal logics extended to FO (e.g., FOLTL [33] and FOCTL [14]) and with past operators [35] have already been studied, CHML features a combination of action-based operators, past operator, and first-order logic (plus domain-specific constructs), which is specifically tailored to capture relevant properties of smart contracts while remaining practically addressable by automatic formal verification tools. To the best of our knowledge, no existing logic is equivalent to CHML.

8

Conclusions and Future work

We proposed CHML, a novel logic for expressing complex temporal properties of smart contracts, and KindHML, a tool for verifying CHML properties of smart contracts. Our experiments show that KindHML is capable of verifying or refuting properties that are beyond the reach of existing tools. Several directions remain for future work. In particular, the current version of KindHML is limited to single-contract properties, whereas many relevant properties involve interactions among multiple contracts: for instance, a user must extract tokens from a contract to enable an action on another. A lightweight approach to handle this in KindHML would consist in embedding the functions of multiple contracts into a single one. However, doing this requires some care: e.g., the balances of the embedded contracts must be kept distinct, and the visibility of contract functions must be taken into account. Another research line is extending the Solidity fragment supported by KindHML in order to narrow the gap with the full Solidity language. Along this line, significant extensions would be the treatment of contract-to-contract calls (including those triggered by simple ETH transfers), loops, and the gas mechanism. Another direction for future work is the automatic transformation of the counterexamples produced by KindHML into executable proofs-of-concept (PoCs). In the context of security analysis, PoCs play a crucial role by demonstrating that a reported vulnerability is not merely theoretical but can be concretely exploited in practice. Constructing PoCs typically requires significant manual effort and expertise, as one must derive a sequence of transactions that reproduces the exploit scenario in a realistic execution environment. Recent research has investigated the automatic generation of PoCs for smart contracts, leveraging techniques such as symbolic reasoning over execution traces, and large language models capable of synthesizing exploit scripts from vulnerability descriptions or execution traces [52,25]. Integrating similar techniques into KindHML would enable the automatic synthesis of concrete exploit transactions directly from model-checking counterexamples, producing PoCs that can be executed on a local blockchain or test network. Such functionality would not only facilitate debugging and validation of detected violations, but would also provide actionable artifacts for developers and auditors, bridging the gap between formal verification results and practical security analysis. In our setting, this appears particularly promising because the counterexamples generated by the model checker already encode sequences of contract interactions that violate the

desired temporal property, providing a natural starting point for synthesizing executable exploit transactions. Acknowledgments Massimo Bartoletti and Enrico Lipparini have been partially supported by the projects PRIN 2022 DeLiCE (F53D23009130001) and SERICS (PE00000014) under the MUR National Recovery and Resilience Plan funded by the European Union — NextGenerationEU.

References 1. Smart contract weakness classification (SWC): Transaction order dependence, ht tps://swcregistry.io/docs/SWC-114, accessed on March 23, 2026 2. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press (2007) 3. Alois, J.: Ethereum Parity hack may impact ETH 500,000 or $146 million. https: //www.crowdfundinsider.com/2017/11/124200-ethereum-parity-hack-may-i mpact-eth-500000-146-million/ (2017), accessed on April 1, 2026 4. Alt, L., Blicha, M., Hyvärinen, A.E.J., Sharygina, N.: SolCMC: Solidity compiler’s model checker. In: Computer Aided Verification. LNCS, vol. 13371, pp. 325–338. Springer (2022). https://doi.org/10.1007/978-3-031-13185-1_16 5. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002). https://doi.org/10.1145/585265.585270 6. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability (2021). https://doi.org/10.3233/978-1-586 03-929-5-825 7. Bartoletti, M., Crafa, S., Lipparini, E.: Formal Verification in Solidity and Move: Insights from a Comparative Analysis. In: FMBC. OASIcs, vol. 129, pp. 3:1–3:18. Schloss Dagstuhl (2025). https://doi.org/10.4230/OASIcs.FMBC.2025.3 8. Bartoletti, M., Ferrando, A., Lipparini, E., Malvone, V.: Solvent: Liquidity verification of smart contracts 15234, 256–266 (2024). https://doi.org/10.1007/97 8-3-031-76554-4_14 9. Bartoletti, M., Fioravanti, F., Matricardi, G., Pettinau, R., Sainas, F.: Towards benchmarking of Solidity verification tools. In: FMBC. OASIcs, vol. 118, pp. 6:1– 6:15. Schloss Dagstuhl (2024). https://doi.org/10.4230/OASICS.FMBC.2024.6 10. Bartoletti, M., Lipparini, E., Pompianu, L.: LLMs as verification oracles for Solidity. In: Financial Cryptography (2026). https://doi.org/10.48550/arXiv.2509. 19153 11. Biere, A.: Bounded model checking. Handbook of satisfiability 185(99), 457–481 (2009) 12. Biere, A., Kröning, D.: SAT-Based Model Checking, pp. 277–303. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_10 13. Bliudze, S., Cimatti, A., Jaber, M., Mover, S., Roveri, M., Saab, W., Wang, Q.: Formal verification of infinite-state BIP models. In: ATVA. LNCS, vol. 9364, pp. 326–343. Springer (2015). https://doi.org/10.1007/978-3-319-24953-7_25 14. Bohn, J., Damm, W., Grumberg, O., Hungar, H., Laster, K.: First-order-ctl model checking. In: Arvind, V., Ramanujam, S. (eds.) Foundations of Software Technology and Theoretical Computer Science. pp. 283–294. Springer Berlin Heidelberg, Berlin, Heidelberg (1998). https://doi.org/10.1007/978-3-540-49382-2_27

15. Bose, P., Das, D., Chen, Y., Feng, Y., Kruegel, C., Vigna, G.: SAILFISH: vetting smart contract state-inconsistency bugs in seconds. In: S&P. pp. 161–178. IEEE (2022). https://doi.org/10.1109/SP46214.2022.9833721 16. Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI. pp. 70– 87. Springer (2011). https://doi.org/10.1007/978-3-642-18275-4_7 17. Chahoki, A.Z., Roveri, M., Amyot, D., Mylopoulos, J.: Revisiting formal verification in VeriSolid: An analysis and enhancements. In: OVERLAY. CEUR, vol. 3629, pp. 55–60 (2023) 18. Chaliasos, S., Charalambous, M.A., Zhou, L., Galanopoulou, R., Gervais, A., Mitropoulos, D., Livshits, B.: Smart contract and DeFi security: Insights from tool evaluations and practitioner surveys. In: ICSE. pp. 60:1–60:13. ACM (2024). https://doi.org/10.1145/3597503.3623302 19. Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: CAV. pp. 510–517. Springer (2016). https://doi.org/10.1007/978-3-319-4 1540-6_29 20. De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) Semantics of Systems of Concurrent Processes. pp. 407–419. Springer Berlin Heidelberg, Berlin, Heidelberg (1990). https://doi.or g/10.1007/3-540-53479-2_17 21. Ding, H., Liu, Y., Piao, X., Song, H., Ji, Z.: Smartguard: An LLM-enhanced framework for smart contract vulnerability detection. Expert Syst. Appl. 269 (2025). https://doi.org/doi.org/10.1016/j.eswa.2025.126479 22. Eskandari, S., Moosavi, S., Clark, J.: SoK: Transparent Dishonesty: Front-Running Attacks on Blockchain. In: Financial Cryptography and Data Security. pp. 170– 189. Springer (2020). https://doi.org/10.1007/978-3-030-43725-1_13 23. Feist, J., Grieco, G., Groce, A.: Slither: a static analysis framework for smart contracts. In: WETSEB. pp. 8–15 (2019). https://doi.org/10.1109/WETSEB.201 9.00008 24. Ferrando, A., Kana, B., Malvone, V.: Wallet ATL: Towards reliable smart contract verification. In: AAMAS (2026), to appear 25. Gervais, A., Zhou, L.: AI agent smart contract exploit generation. In: Financial Cryptography and Data Security (to appear) (2026) 26. Hajdu, Á., Jovanovic, D.: solc-verify: A modular verifier for Solidity smart contracts. In: VSTTE. LNCS, vol. 12031, pp. 161–179. Springer (2019). https: //doi.org/10.1007/978-3-030-41600-3_11 27. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language lustre. Proceedings of the IEEE 79(9), 1305–1320 (1991). https://doi.org/10.1109/5.97300 28. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985). https://doi.org/10.1145/2455.2460 29. Holmström, S.: Hennessy-milner logic with recursion as a specification language, and a refinement calculus based on it. In: Rattray, C. (ed.) Specification and Verification of Concurrent Systems. pp. 294–330. Springer London, London (1990). https://doi.org/10.1007/978-1-4471-3534-0_15 30. Jackson, D., Nandi, C., Sagiv, M.: Certora technology white paper. https://docs .certora.com/en/latest/docs/whitepaper/index.html (2022) 31. Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: NDSS. The Internet Society (2018) 32. Kolluri, A., Nikolic, I., Sergey, I., Hobor, A., Saxena, P.: Exploiting the laws of order in smart contracts. In: ACM SIGSOFT Int. Symp. on Software Testing and Analysis. pp. 363–373. ACM (2019). https://doi.org/10.1145/3293882.3330560

33. Kröger, F., Merz, S.: First-Order Linear Temporal Logic, pp. 153–179. Springer Berlin Heidelberg, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-5 40-68635-4_5, https://doi.org/10.1007/978-3-540-68635-4_5 34. Kushwaha, S.S., Joshi, S., Singh, D., Kaur, M., Lee, H.N.: Ethereum smart contract analysis tools: A systematic review. IEEE Access 10, 57037–57062 (2022). https: //doi.org/10.1109/ACCESS.2022.3169902 35. Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 94. pp. 47–58. Springer Berlin Heidelberg, Berlin, Heidelberg (1994). https://doi.org/10.1007/3-540-5 7785-8_130 36. Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM SIGSAC CCS. pp. 254–269 (2016). https://doi.org/10.114 5/2976749.2978309 37. Nelaturu, K., Mavridou, A., Stachtiari, E., Veneris, A.G., Laszka, A.: Correct-bydesign interacting smart contracts and a systematic approach for verifying ERC20 and ERC721 contracts with VeriSolid. IEEE Trans. Dependable Secur. Comput. 20(4), 3110–3127 (2023). https://doi.org/10.1109/TDSC.2022.3200840 38. Nguyen, T.D., Pham, L.H., Sun, J., Lin, Y., Minh, Q.T.: sFuzz: an efficient adaptive fuzzer for Solidity smart contracts. In: ICSE. pp. 778–788. ACM (2020). https: //doi.org/10.1145/3377811.3380334 39. Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: ACSAC. pp. 653–663. ACM (2018). https://doi.org/10.1145/3274694.3274743 40. Permenev, A., Dimitrov, D.K., Tsankov, P., Drachsler-Cohen, D., Vechev, M.T.: VerX: Safety verification of smart contracts. In: S&P. pp. 1661–1677. IEEE (2020). https://doi.org/10.1109/SP40000.2020.00024 41. Ressi, D., Spanò, A., Benetollo, L., Bugliesi, M., Piazza, C., Rossi, S.: Vulnerability detection in solidity smart contracts via machine learning: A qualitative analysis. BCRA p. 100390 (2025). https://doi.org/10.1016/j.bcra.2025.100390 42. Sendner, C., Petzi, L., Stang, J., Dmitrienko, A.: Large-scale study of vulnerability scanners for Ethereum smart contracts. In: EuroS&P. pp. 220–220. IEEE (2024). https://doi.org/10.1109/SP54263.2024.00230 43. Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a sat-solver. In: FMCAD. pp. 127–144. Springer (2000) 44. Stephens, J., Ferles, K., Mariano, B., Lahiri, S.K., Dillig, I.: SmartPulse: Automated checking of temporal properties in smart contracts. In: S&P. pp. 555–571. IEEE (2021). https://doi.org/10.1109/SP40001.2021.00085 45. Tikhomirov, S., Voskresenskaya, E., Ivanitskiy, I., Takhaviev, R., Marchenko, E., Alexandrov, Y.: SmartCheck: Static analysis of Ethereum smart contracts. In: WETSEB. pp. 9–16. ACM (2018). https://doi.org/10.1145/3194113.3194115 46. Tolmach, P., Li, Y., Lin, S., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7), 148:1–148:38 (2022). https://doi.org/10.1145/3464421 47. Torres, C.F., Camino, R., State, R.: Frontrunner Jones and the Raiders of the Dark Forest: An empirical study of frontrunning on the Ethereum blockchain. In: USENIX Security Symp. pp. 1343–1359 (2021) 48. Torres, C.F., Iannillo, A.K., Gervais, A., State, R.: ConFuzzius: A data dependency-aware hybrid fuzzer for smart contracts. In: EuroS&P. pp. 103–119. IEEE (2021). https://doi.org/10.1109/EUROSP51992.2021.00018

49. Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., Bünzli, F., Vechev, M.T.: Securify: Practical security analysis of smart contracts. In: ACM SIGSAC CCS. pp. 67–82. ACM (2018). https://doi.org/10.1145/3243734.3243780 50. Wei, Z., Sun, J., Sun, Y., Liu, Y., Wu, D., Zhang, Z., Zhang, X., Li, M., Liu, Y., Li, C., Wan, M., Dong, J., Zhu, L.: Advanced smart contract vulnerability detection via LLM-powered multi-agent systems. IEEE TSE (2025). https://doi.org/10 .1109/TSE.2025.3597319 51. Wesley, S., Christakis, M., Navas, J.A., Trefler, R.J., Wüstholz, V., Gurfinkel, A.: Verifying Solidity smart contracts via communication abstraction in SmartACE. In: VMCAI. LNCS, vol. 13182, pp. 425–449. Springer (2022). https://doi.org/ 10.1007/978-3-030-94583-1_21 52. Xiao, Z., Li, Y., Wang, Q., Chen, S.: Prompt to Pwn: Automated exploit generation for smart contracts. In: ACISP. pp. 1–28. LNCS, Springer (2026) 53. Zhang, Z., Zhang, B., Xu, W., Lin, Z.: Demystifying exploitable bugs in smart contracts. In: ICSE. pp. 615–627. IEEE (2023). https://doi.org/10.1109/ICSE 48619.2023.00061