Smart Contract Invariants Protect Against Cybercriminals

Smart Contract Invariants Protect Against Cybercriminals Sofia Bobadilla, Humaira Afrin, Angela Novelli, Martin Monperrus

arXiv:2608.13191v1 [cs.CR] 13 Aug 2026

KTH Royal Institute of Technology Stockholm, Sweden {sofbob, humairaa, anovelli, monperrus}@kth.se

Abstract—Blockchains are among the most adversarial environments in computing. Billions are stolen by cybercriminals who exploit vulnerabilities. This is an open problem and no concept or technique has proven to really make a difference. In this paper, we claim that the classical notion of program invariant is perhaps the most powerful solution to the problem. We devise an original experimental protocol to 1) study how invariants would have protected against past real-world attacks and 2) whether state-of-the-art automated tools can find them. The experimental toolchain is sophisticated. It is based on I NVARIANT E VAL, a benchmark of 28 real Ethereum exploits, each paired with a human-authored invariant that blocks the attack. We validate every invariant with P ON D E R EPLAY, a replay framework that re-executes transactions in order to prove the correctness and soundness of smart contract invariants. We demonstrate that smart contract invariants block all the cybercriminal attacks in I NVARIANT E VAL, fully validated by replaying 108,637 historical transactions. Our large-scale experiments clearly demonstrate that smart contract invariants protect against cybercriminals.

I. I NTRODUCTION Smart contract exploits cause large and irreversible financial losses. More than one billion dollars in on-chain assets have been stolen through vulnerabilities in deployed contracts [6]. A missing access-control guard lets any caller drain funds (e.g., Cork Protocol, $12M 1 ). A missing oracle check opens the door to price manipulation (e.g., Makina, $5.1M 2 ). Smart contract invariants are a powerful defense mechanism. Developers write such invariants, and they are evaluated at runtime for all transactions. The blockchain guarantees are strong: if the invariant is violated, the transaction is reverted, and no side-effect or state change is committed to the chain. Two important questions follow. Could a program invariant have stopped real-world exploits? Can automated invariant generation tools discover those attack-stopping invariants? While important, these are open, unanswered research questions. Prior work evaluates invariant-related tools only against synthetic properties, templates, or mined patterns [4], [16], [25], but none have been confronted with real-world, multimillion dollar loss incidents. In this paper, we answer both questions with a novel protocol and a large-scale experiment. First, we build I NVARI 1 https://dedaub.com/blog/the-11m-cork-protocol-hack-a-critical-lesson-i n-uniswap-v4-hook-security/ 2 https://github.com/SunWeb3Sec/DeFiHackLabs/blob/main/src/test/2026-0 1/makina exp.sol

ANT E VAL , a benchmark of 28 real-world Ethereum exploits, each paired with a human-authored program invariant that blocks the attack. Next, we validate each program invariant with a novel historical verification technique consisting of re-executing 1) the proof-of-concept exploit, 2) the attack transaction, and 3) the contract’s real transaction history. The replay enables us to verify security and functional preservation with guarantees. The hardened contracts block all 28 attacks: every groundtruth invariant causes both the proof-of-concept exploit and the malicious on-chain transaction to fail at the vulnerable step, a 28/28 result. We replay 108,637 historical transactions; of those, 106,815 (98.3% of total replayed) are fully preserved under the hardened bytecode; the 1,526 divergences (1.4%) are each causally attributed to the invariant, not to replay noise. The attack-stopping invariants reduce to eight recurring property families, with price and oracle checks (8 cases), ledger conservation (6), and access control and interaction safety (4 each) as the largest groups. Finally, we study whether the state-of-the-art tools for invariant generation protect against real-world attacks. The publicly available, end-to-end executable tools fall short: FLAMES [11], InvCon [16], and InvCon+ [18] together recover only 2 of the 28 attack-stopping invariants. Our contributions are: • an original, sound methodology for studying smart contract invariant effectiveness, fully grounded on on-chain data. 3 • I NVARIANT E VAL , a benchmark of 28 real Ethereum exploits each paired with a human-authored, attack-stopping program invariant 3 • P ON D E R EPLAY , an on-chain verification framework to test an invariant against both the attack transaction and the contract’s full pre-attack history, providing causal attribution to the protective invariant. Our experimental conclusions are grounded in 108,637 replays. • An evaluation of three state-of-the-art invariant tools against the I NVARIANT E VAL ground truth, showing the fundamental shortcomings of the field. The remainder of the paper is organized as follows. Section II introduces invariants and smart contracts. Section III de3 At the moment, access to I NVARIANT E VAL and P ON D E R EPLAY is available upon request to sofbob@kth.se.

scribes the experimental methodology, the research questions, and the P ON D E R EPLAY replay infrastructure. Section IV reports the results, and Section V discusses related work. II. BACKGROUND A. Blockchain Concepts Smart Contract & Solidity. Smart Contracts are programs deployed on blockchain networks. Contracts are written in high-level smart contract languages, such as Solidity, and then compiled into bytecode for deployment and execution. Solidity is Ethereum’s primary smart contract programming language. The Ethereum Virtual Machine (EVM) is the runtime environment for executing smart contracts on the Ethereum blockchain. Transactions. All operations on the blockchain are initiated via transactions. A transaction is typically sent from a user, signed by their private key, to perform actions such as transferring cryptocurrency or invoking functions on existing contracts. During execution, a called contract may interact with other contracts. Transactions are atomic. If they revert, no sideeffect is written on chain. Smart Contract Security. Before deployment, contracts are typically reviewed through a security audit: a manual and tool-assisted inspection by specialized firms that looks for vulnerabilities in the code [1]. Audits reduce risk but do not eliminate it. Consequently, over one billion dollars in assets have been lost to smart contract exploits [7]. Proof-of-Concept. Once an incident occurs, security researchers reconstruct the attack as a proof-of-concept (PoC) exploit. A proof-of-concept is executable code that reproduces the theft on a fork of the blockchain at the vulnerable block. DeFiHackLabs [6] maintains a public collection of such PoCs for documented exploits. B. Invariants An invariant is a property that holds at a designated point in a program [8]. Three canonical forms are widely recognised: • Preconditions hold at function entry and constrain the inputs or state under which a function may be lawfully called (Listing 1). • Postconditions hold at function exit and capture guarantees about the output or resulting state (Listing 2). • Object invariants (in OOP) hold over the entire lifetime of an object, capturing structural properties of the object’s state that must never be violated. A smart contract deployed on chain is conceptually equivalent to an object (Listing 3). Invariants appear across the software engineering literature under many names: assertions, contracts, properties, runtime checks. They all express the same idea: a logical condition that must hold at a designated program point. Developers rarely write them well [8]. Invariants for Security A security invariant serves a strong purpose: it encodes a property that must hold even under adversarial input. When such an invariant is checked at runtime, a violation basically means that the attack is blocked and the

1 function batchTransfer( 2 address[] _receivers, uint256 _value 3 ) public whenNotPaused returns (bool) { 4 uint256 cnt = _receivers.length; 5 require(_value <= uint256(-1) / cnt); 6 7}

// ... transfer loop ...

Listing 1. Precondition invariant: input bound before batch transfer (BEC)

1 function doExchange(uint256 amount) public returns (bool) { 2 // ... pull tokens, call Curve ... 3 curve.exchange_underlying(1, 2, camount, 0); 4 require(namount >= (camount * 995) / 1000, "slippage too high"); 5} Listing 2. Postcondition invariant: output bound after Curve exchange (ERC20TokenBank)

offending execution is reverted before it commits any effect. Invariants for smart contract security is a promising direction, with active research in the area, see section V. III. E XPERIMENTAL M ETHODOLOGY We study the extent to which program invariants can stop real exploits, how much those invariants modify behavior, and how well current tools can discover them. This research is essential for understanding the current capabilities and steering future research. A. Overview Our experimental methodology answers two main questions: can a single program invariant stop each real exploit, and can automated tools discover it? We build on D E F I H ACK L ABS, a corpus of executable real-world exploits against real on-chain contracts. For each selected exploit, two authors independently write a hardened contract: the original source code augmented with a program invariant inserted at the vulnerable function. Each invariant is then validated by P ON D E R EPLAY, a novel replay framework we built for this purpose. P ON D E R EPLAY re-executes two classes of transactions against the hardened bytecode: the attack transactions (to confirm the invariant stops the exploit) and historical transactions (to confirm normal usage is preserved). An invariant is accepted only when it blocks the attack and leaves legitimate behavior intact or with explained changes.

1 modifier nonReentrant() \{ 2 require(!locked, "reentered"); 3 locked = true; _; locked = false; 4 5 function buyJay(...) public payable nonReentrant { /* ... */ } Listing 3. Object invariant: a reentrancy lock, held across every state-mutating method via a modifier

TABLE I F IVE HIGHEST- LOSS INCIDENTS IN I NVARIANT E VAL , ORDERED BY NORMALIZED USD LOSS . Date

Protocol

Loss

Root Cause

Apr 2018 Apr 2018 Jun 2024 Feb 2021 Sep 2024

BeautyChain (BEC) SmartMesh (SMT) WIFCOIN Yearn yDAI OnyxDAO

˜$900M ˜$140M ˜$13.2M ˜$11M ˜$3.8M

Overflow Overflow Logic Flaw Slippage Logic Flaw

This design grounds every claim we will make in onchain evidence: real calldata, real block state, and real execution outcomes. Figure 1 summarizes the verification pipeline. Section III-B describes our dataset of real-world attacks. Section III-C describes the invariant authoring process, Section III-D the joint security and preservation checks, and Section III-E the P ON D E R EPLAY infrastructure. The four research questions are then evaluated against this validated ground truth. B. Dataset First, we need a dataset of real world attacks, in order to study to what extent invariants can actually protect smart contracts. We do not use toy examples like SmartBugsCurated [12] or synthetic contracts like Iuliano et al. [14]. Our idea is to build our study on the well established D E F I H ACK L ABS benchmark [6]. D E F I H ACK L ABS is an open-source repository of real-world DeFi proof-of-concept exploits (PoCs) implemented in Solidity using the Foundry testing framework. Each exploit comes with a self-contained, executable test that is meant to reproduce a documented past attack against its original on-chain contracts. The full repository contains 871 attacks across multiple blockchains, including Ethereum, BNB Chain, and Polygon. We restrict our study to Ethereum, arguably the largest smart contract platform by total money locked and home base to the majority of high-profile DeFi protocols, such as Uniswap and AAVE. Restricting to one chain keeps our experimental environment uniform. This leaves 359 Ethereum exploits, spanning July 2017 to June 2026. C. Ground Truth: Writing Program Invariants Prior invariant studies evaluate smart contract invariant effectiveness with predefined properties, templates, or mined patterns [4], [16], [25]. Our core novelty is to entirely ground our study of smart contract invariant effectiveness in real-world attacks. Our intuition is that the interesting invariants are attackstopping. If one has had them in the code, the attack would have never succeeded. But what are those attack-stopping invariants? There is no ground truth, since the attack went through and stole real money. We use manual analysis to fill this gap. Manual Analysis We collect the ground-truth program invariants as follows. For each attacked contract, two authors independently write a program invariant, time-boxed to eight

hours per case. For this, they consult all possible public information incl. post-mortem reports, the victim contract source code, and the D E F I H ACK L ABS proof-of-concept exploit. A third author resolves disagreements if any. The goal is that each written invariant 1) stops the attack 2) preserves legitimate behavior. The result is I NVARIANT E VAL, a dataset of 28 entries. Each entry is a triple of 1) a documented exploit transaction 2) a source code proof-of-concept that reproduces the attack path 3) a human-authored invariant. To illustrate that the dataset only involves past incidents where cybercriminals stole real money, Table I lists the five highest-loss incidents in our curated dataset. D. Verification Procedure When one adds an invariant to an existing smart contract, we call the resulting smart contract a “hardened contract”. A hardened contract must satisfy two properties. It must be secure against the exploit that drained the original victim, and it must stay functional for legitimate use. a) Security.: We test security by passing the hardened contract through two independent tests: the I NVARIANT E VAL proof-of-concept and the original malicious on-chain transaction(s). The proof-of-concept validates that the invariant breaks the exploit logic per the community post-mortem and the reproduced attack path. The attack transaction validates that the invariant breaks the attack with the exact calldata, gas, and call path exercised in the real attack. Here, the semantics of blockchain is key: the blockchain gives full guarantees that the on-chain state can be perfectly reproduced at the time of the attack (same block, same transactions before the attack transaction). This is implemented with the mature technique of forking mainnet. To sum up, we verify that the attack transaction reverts on the hardened contract. In the following, the hardened contract is considered secure if and only if both replays fail. We note that a side-effect implication of this protocol is to verify that the proof-ofconcept exploit is faithful to the attack. b) Behavioral Preservation.: In Solidity, an invariant in a require statement can have side-effects if it passes. In other words, the added invariant in the hardened contract may impact the behavior for legitimate cases. Yet, we want invariants that block the attack without changing how the contract behaves for legitimate callers. We need to check for behavioral preservation. To assess behavioral preservation, we collect every historical transaction that 1) happens before the attack transaction and 2) reaches the function(s) containing the program invariant. For each collected historical transaction, we then check its outcome against the hardened contract instead of the vulnerable one. E. Verification Infrastructure As stated in subsection III-D, our entire methodology is based on replaying transactions. The replay is sophisticated; it

Hardened contract original contract + invariant

Security check

I NVARIANT E VAL PoC

Functional-preservation check

Replay Historical txs

Replay Attack tx O ̸= R

blocked

succeeds

Secure Exploit blocked

O ̸= H

O≡H

O ̸= R

Inconclusive O ̸= R

Ineffective Exploit succeeds

R≡H

R ̸= H

Preserved Behavior matches

Not preserved Behavior changes

✓ Valid hardened contract

Manual Root Cause Analysis

Fig. 1. Historical replay verification of a hardened contract. Each transaction yields three traces: the on-chain trace (O), the recompiled trace of the unmodified contract (R), and the hardened-contract trace (H); ≡ denotes trace equivalence per our fidelity criteria (Section III-E2). The security check replays the proofof-concept exploit and the malicious transaction; the functional-preservation check replays historical transactions through the hardened function.

must support replaying 1) the original bytecode 2) the recompiled source code and 3) any modification of the contract, in particular the hardened contract. To the best of our knowledge, there is no tooling for this. The existing solutions cover only half the problem: eth_call state overrides can substitute bytecode but lack sub-block state granularity, forcing a choice between the preexecution state at N −1 (missing same-block prior transactions) and the post-execution state at N ; cast run replays a historical transaction faithfully but provides no mechanism to substitute the bytecode at any address; Foundry fork tests with vm.etch can inject arbitrary bytecode but require a hand-reconstructed scenario rather than the real transaction’s context. No existing tool supports historical replay verification. We build P ON D E R EPLAY to fill this gap. P ON D E R EPLAY can replay a transaction against a different version of the contract bytecode deployed at a certain target address. It answers the counterfactual question Section III-D needs: what would this real transaction have done if the contract had been hardened? 1) Replay Setup: For a transaction in block N , P ON D E R E PLAY forks Ethereum mainnet at block N −1. It injects the new bytecode at the target contract’s on-chain address. If the target transaction is not the first transaction in block N , P ON D E R EPLAY replays the previous transactions in the block before executing the target transaction. This reconstructs the state immediately before the transaction under study. The injected bytecode must be compatible with the deployed

O original literal on-chain data, canonical chain, block N

Reproduction ?

R ≡ O ̸= ⇒ inconclusive

R recompiled unmodified source code, mainnet fork at N −1

Preservation ? H ≡ R ̸= ⇒ not preserved

H hardened invariant installed, mainnet fork at N −1 Both checks compare: transaction status • subcall outcomes • storage diff (ϵ-threshold)

Fig. 2. P ON D E R EPLAY analyzes replay fidelity. Each transaction replay yields three execution traces: the literal on-chain record (O), a recompiled replay of the unmodified contract (R), and a replay of the hardened contract (H). The ?

reproduction check (R ≡ O) validates replay infrastructure; failure renders ?

the transaction inconclusive. The preservation check (H ≡ R) isolates the invariant’s effect; any divergence is causally attributable to the injected guard.

contract. It must be compiled with the same EVM version as the original; otherwise, some opcodes are not yet supported in blocks before the intended EVM upgrade. 2) Replay Fidelity: A replay means re-executing one transaction’s calldata against another version of the target contract. A replay produces three traces, illustrated in Figure 2. The original trace (O) is the literal on-chain data. The recompiled

trace (R) is obtained by re-running the transaction after injecting a recompiled version of the unmodified contract, using the same source and deployment configuration as the on-chain version of the contract; it is used for sanity checking. The hardened trace (H) is obtained by re-running the transaction after injecting the bytecode of the hardened contract. Then, one needs to compare the traces. Transaction status alone is insufficient: the side effects of a passing transaction might be vastly different or a revert can occur deep in a subcall while the top-level call succeeds, so a status-only check would miss the divergence4 . To assess the fidelity of the replay, P ON D E R EPLAY verifies three strong criteria: transaction status fidelity, subcall fidelity, and storage fidelity. Transaction status fidelity is a binary outcome, naturally supported by the EVM. Subcall fidelity means that the set of all contract calls and their status in the transaction is the same. Storage fidelity means that the side effects on chain are identical enough, per numerical semantics. In this case, any divergence is considered as a numerical divergence, and we check that the storage value difference is lower than an arbitrary threshold ϵ. For storage check, P ON D E R EPLAY uses a prestateTracer diff to record which slots changed and by how much. Together the three criteria cover the full observable footprint of a transaction: whether it succeeded, what internal calls change along the way, and what state it ultimately committed. 3) Replay Checks: The reproduction check (O vs. R) asks whether the replay infrastructure faithfully reconstructs the on-chain execution. It is necessary for logically attributing behavioral differences to the invariant. If the recompiled replay cannot match the original on-chain outcome on all three axes, any conclusion later drawn from H on this transaction would be inconclusive: the discrepancy could stem from replay error rather than the invariant. The preservation check (R vs. H) isolates the sole variable that differs between the two executions: the injected invariant. Because R and H share the same block fork, the same pretransaction state, and the same calldata, any divergence on the three axes is exclusively attributable to the invariant. This gives a clean causal guarantee: a divergence is the invariant’s effect, not an artifact of the replay environment. F. Research Questions We organize the study around four research questions: • RQ1. To what extent do program invariants stop real world attacks on smart contracts? • RQ2. To what extent do attack-stopping invariants break existing behavior according to historical replay verification? • RQ3. What are the limitations of historical replay verification? • RQ4. To what extent are the state-of-the-art invariant generation tools able to generate attack-stopping invariants for real world attacks? 4 In Solidity, subcall reverts do not revert the top-level transaction – alas.

1) RQ1: To what extent do program invariants stop real world attacks on smart contracts?: RQ1 studies whether the manually written invariants stop the considered realworld attacks. For each hardened contract, we replay the two attack views from the security check (Section III-D): the I NVARIANT E VAL proof-of-concept and the on-chain attack transaction. The invariant is accepted as effective when both fail at the vulnerable step. Invariant taxonomy. We also want deep qualitative knowledge about the kinds of invariants I NVARIANT E VAL contains. We define a unified taxonomy of eight invariant families, reconciling the properties from Bernardi et al. [2], the templates from Trace2Inv [4], and the D E F I H ACK L ABS root cause metadata: 1) access control & authorization; 2) ledger, supply & conservation; 3) business logic & protocol rules; 4) price, oracle & slippage; 5) input validation & preconditions; 6) arithmetic & precision safety; 7) external call & interaction safety, incl. reentrancy & execution ordering; 8) initialization, storage & configuration. We manually assign each invariant to one family based on the protocol specification and the intent of the hardened function. 2) RQ2: To what extent do attack-stopping invariants break existing behavior according to historical replay verification?: RQ1 shows that I NVARIANT E VAL program invariants stop attacks; RQ2 asks what that protection costs in legitimate usability. For each hardened contract in I NVARIANT E VAL, we replay the contract’s historical transaction history through the functional-preservation check (Section III-D). We count how many transactions are preserved and we record the divergence, if any, between the transaction trace of the recompiled original contract R and the hardened version H. A preserved transaction means that the hardened contract reproduces the original outcome per the three strong properties verified in the verification infrastructure, see subsubsection III-E2. For every transaction that diverges, we manually inspect its call trace and storage diff to understand its root cause. Once the root cause is understood, we assess what the non-preserved behaviour means for those particular transactions, and we record this assessment as the behavioral change reason. 3) RQ3: What are the limitations of historical replay verification?: RQ3 studies the transactions that are inconclusive per our replay algorithm (neither preserved nor non-preserved, O ̸= R). For each inconclusive transaction, we analyze the original on-chain trace and the recompiled replay trace. This enables us to understand what difference in the trace causes this replay to be inconclusive. As an additional check on replay infrastructure, we also test whether the recompiled contract and the hardened one still agree despite the inconclusive verification: agreement here shows that the invariant’s effect is the same and that inconclusiveness stems from the replay infrastructure. 4) RQ4: To what extent are the state-of-the-art invariant generation tools able to generate attack-stopping invariants for real world attacks?: RQ4 evaluates how well the state-ofthe-art of invariant inference is able to identify the ground truth

TABLE II RQ1 ATTACK - STOPPING INVARIANTS IN I NVARIANT E VAL . Loss: AS REPORTED BY D E F I H ACK L ABS ; LOSSES DENOMINATED IN ETH ARE CONVERTED TO USD AT THE ETH/USD MARKET PRICE AT THE ATTACK TRANSACTION ’ S BLOCK TIMESTAMP. Taxonomy: FAMILY FROM THE UNIFIED TAXONOMY (S ECTION III-F1) ASSIGNED FROM THE INVARIANT ’ S SEMANTICS . Hardened fn.: FUNCTION ( S ) WHERE THE INVARIANT WAS INSERTED ( LONG NAMES FOLD OR ABBREVIATE WITH . . . ). Invariant: SOURCE CODE OF THE INVARIANT. Security: THE CORE RQ1 RESULTS , WHETHER THE CONTRACT HARDENED WITH THE ADDED INVARIANT BLOCKS BOTH THE D E F I H ACK L ABS P O C AND THE MALICIOUS ON - CHAIN TRANSACTION (T X ). Security Invariant PoC Tx require(_value<=uint256(-1)/cnt) ✓ ✓ require(total>=_feeSmt&&total>=_value) ✓ ✓ require(msg.value==underlyingRequiredToExercise(oTokensToExer ✓ ✓ cise)) 2021-02 Yearn yDAI $11M Access control earn require(msg.sender==governance,"onlygovernancecancallearn()") ✓ ✓ 2021-09 Nimbus $4.9K Price/oracle swap require(...mul(_reserve0).mul(_reserve1).mul(10_000**2),"Nimb ✓ ✓ us:K") 2022-01 Anyswap $1.4M Interaction safety anySwap...Permit require(returnData.length>0,"Router:permitfunctionmissingforr ✓ ✓ elayer"); 2022-02 TecraSpace $63K Ledger/supply burnFrom require(_allowances[from][msg.sender]>=amount) ✓ ✓ 2022-06 Inverse Finance $1.26M Price/oracle latestAnswer require(crvLPTokenPrice>=lower&&crvLPTokenPrice<=upper,"LPpri ✓ ✓ cedeviates") 2022-09 BadGuysbyRPF $4.1K Ledger/supply WhiteListMint require(_numberMinted(msg.sender)+chosenAmount<=1,"Mintlimite ✓ ✓ xceeded"); 2022-10 N00d $29K Interaction safety enter modifierreentrancy_lock()... ✓ ✓ 2022-10 Uerii $2.4K Ledger/supply _mint require(totalSupply()+amount<=CAP); ✓ ✓ 2022-12 JAY $18K Interaction safety buyJay, sell modifierreentrancy_lock()... ✓ ✓ 2023-01 QTN $3.1K Access control _transfer require(msg.sender==address(uniswapV2Router),"rebasedenied") ✓ ✓ 2023-05 ERC20TokenBank $111K Price/oracle doExchange require(namount>=(camount*995)/1000,"slippagetoohigh") ✓ ✓ 2023-06 VINU $6K Input validation addLiq...ETH require(extcodesize(devaddr)==0,"devaddrnotacontract") ✓ ✓ 2023-08 Uwerx $327K Init/config _transfer require(uniswapPoolAddress!=address(0x1),"uniswapPoolAddressn ✓ ✓ otinitialized"); 2023-09 JumpFarm $3.9K Ledger/supply unstake require(TOKEN.balanceOf(this)<=balanceBefore,"rebasemid-unsta ✓ ✓ ke") 2023-09 Unicly NFT $1.3K Interaction safety deposit, withdraw modifierreentrancy_lock()... ✓ ✓ 2023-10 pSeudoEth $2.3K Price/oracle skim require(balance0-reserve0<=reserve0/10);require(balance1-rese ✓ ✓ rve1<=reserve1/10) 2023-11 grok $55K Price/oracle swap...ForEth require(swapAmount<=taxAmount,"Autoswapexceedsselltax"); ✓ ✓ 2024-04 HoppyFrog $979 Price/oracle _transfer, swap...ForEth require(swapAmount<=maxSwapForSell,"Autoswapexceedstax-scaled ✓ ✓ cap"); 2024-06 APEMAGA $30K Access control family require(msg.sender==account,"Unauthorizedcaller") ✓ ✓ 2024-06 JokInTheBox $34K Business logic unstake require(!currentStake.unstaked,"Stakealreadyunstaked") ✓ ✓ 2024-06 WIFCOIN $13.19M Business logic claimEarned require(_earned>totalRewardsPerWalletPerPlan[...],"Rewardsalr ✓ ✓ eadyclaimed") 2024-08 OMPx $11K Price/oracle purchase, buyBack modifierenforceCooldown... ✓ ✓ 2024-09 Bedrock DeFi $2M Price/oracle mint require(uniBTCAmount*1e10<msg.value,"Exchangerateunsafe") ✓ ✓ 2024-09 OnyxDAO $3.8M Ledger/supply liquidate...Repay require(repayAmount==borrowedAmount) ✓ ✓ 2026-03 AlkemiEarn $89K Access control liquidateBorrow require(msg.sender!=targetAccount,"self-liquidationnotpossibl ✓ ✓ e") Total 28 Total loss $1.07B 28 28 Date 2018-04 2018-04 2020-08

Case BEC SmartMesh Opyn

Loss $900M $140M $370K

Taxonomy Arithmetic Arithmetic Ledger/supply

Hardened fn. batchTransfer transferProxy exercise

invariants. We are able to run end-to-end two state-of-the-art invariant inference tools, InvCon [16] and InvCon+ [18], and one invariant generator, FLAMES [11]. We compare their outputs against the validated invariants from I NVARIANT E VAL. Reapplying our verification protocol is not suitable for this task because the tools do not deliver specific-enough instructions for hardening the contract. Instead, we rely on checking whether the ground-truth invariant appears in the tool output. IV. E XPERIMENTAL R ESULTS A. RQ1: Invariant Effectiveness We check whether the invariants make the considered contracts secure. Table II shows the results. All 28 ground-truth invariants block: 1) the proof-of-concept exploit 2) the actual attack transaction. In both cases, the transaction reverts, it reverts at the expected vulnerable step, and it reverts with the revert message written in the invariant. This perfect result 28/28 (100%) is a consequence of our ground truth protocol. There are 25 attacks for which we did not succeed in writing the securing invariant. This is because of our limited expertise of the target protocol and the time-bound budget.

To make the ground truth concrete, we walk through one representative entry of I NVARIANT E VAL, from the vulnerability to the attack-stopping invariant. Case Study: BEC (April 2018, Loss: 900 M USD) BEC is an ERC-20 token. Its batchTransfer() function pays multiple recipients the same amount in one call by computing amount = cnt * value, checking the sender can afford it, then crediting each recipient. However, the multiplication had no safety check. The attacker sent the transaction with 2 receivers and a value of 2255 . Multiplying those together (2×2255 ) caused an overflow, so the balance check passed even though they had no tokens. The inserted program invariant catches such scenario. Taxonomy. We analyze our ground truth invariants. Table II assigns each invariant to a family from the unified taxonomy defined in Section III-F1. Price oracle and slippage are the largest family, with 8/28 cases. Ledger, supply, and conservation checks follow with 6 cases. Access control and authorization account for 4 cases, tied with external call and interaction safety, three of which are reentrancy locks. Business logic guards and arithmetic safety cover 2 cases each; input validation and initialization checks cover 1 case each. All eight families are represented in I NVARIANT E VAL, confirming

1 function batchTransfer( address[] _receivers, uint256 _value ) public whenNotPaused returns (bool) { 2 ... 3 + require(_value <= uint256(-1) / cnt); 4 5 6 7 8 9 10 }

balances[msg.sender] = balances[msg.sender]. sub(amount); for (uint256 i = 0; i < cnt; i++) { balances[_receivers[i]] = balances[ _receivers[i]].add(_value); ... } return true; Listing 4. BEC batchTransfer(): attack-stopping invariant.

that real-world attacks are stopped by a broad spectrum of properties rather than a single dominant pattern. Answer to RQ1: To what extent do program invariants stop real world attacks on smart contracts? Every invariant in I NVARIANT E VAL blocks the attack: all 28 hardened contracts cause both the D E F I H ACK L ABS proof-of-concept and the malicious onchain transaction to fail at the vulnerable step. The eight-family taxonomy shows that no single class of guard dominates. A single require invariant, correctly specifying the protocol’s intended security property, is sufficient to abort past real-world attacks totaling more than one billion dollars of theft. B. RQ2: Behavioral Preservation We evaluate the effect on the hardened version of the contract on historical transactions. We use P ON D E R EPLAY to do so, see subsection III-E. Overall, we replay 108,637 transactions with our fidelity checks. Preserved transactions. 106,815 (98.3% of total replayed) transactions pass the preservation check, indicating equivalent behaviour between the recompiled and hardened contracts; this is presented in column Pres. of Table III. Not-preserved transactions. We observe 1,526 txs (1.4% of total replayed) with a divergence when replayed under the hardened bytecode (Table III, column Not pres.). Divergence Kind In 1,424 cases (93%), the introduced program invariant reverts within the contract directly. In 43 cases, the introduced program invariant reverts in a nested subcall. In the remaining 59 cases, the preservation check fails because of storage drift, which violates storage fidelity. 1) Manual Analysis: We manually analyze all cases in order to identify the reason for non-preservation. This reason is documented in Table IV as column behavioral change reason. a) Past Exploit.: A past transaction is classified as exploit when it reproduces the same vulnerability call pattern as the documented attack. The entry point, and triggering condition match what the proof-of-concept or onchain malicious transaction used to perform the attack.

The transaction reverting in H is intentional and demonstrates soundness. APEMAGA illustrates this: all 10 notpreserved calls invoke family() on the same pair, at block 20175377, 0xcfbc3... (blocks 20175128–20175234) and 0xdbab5d... (blocks 20175265–20175350). The past transactions exercise the same unauthenticated-burn path against the same pair, inflating the token price and ultimately swapping the tokens. Each call reverts with our ground truth invariant (Unauthorized: caller is not the token owner), the same guard that stops the documented attack. Hence, the invariant is correct and the behavioral change is sound. b) Misusage.: A transaction is classified as misusage, if it calls a function in a way the protocol design never envisioned or authorized, while not being malicious. The caller misuses an accounting rule that the vulnerable implementation left open, for example invoking a privileged internal operation through an unauthenticated wrapper. The protective invariant restores the intended protocol rule; consequently the replayed transaction correctly reverts. Nimbus is representative: 449 of the 466 not-preserved calls invoke swap() and revert with the constant-product invariant that also stops the attack. These callers are not attackers; they are ordinary swappers whose trade pushes the pool’s reserves past the protocol rule, a path the vulnerable pool tolerated but the protocol design never intended to expose. c) Whitehat operation.: This label covers cases where the transaction does exercise the same code path as the attack, yet was done by a whitehat hacker. We are able to differentiate exploits from whitehat operations, thanks to Etherscan labels. Whitehat transactions differ in intent, funds are recovered rather than stolen, but are technically equivalent to an exploit, hence are correctly reverted by the protective invariant. The Anyswap case is as such. Etherscan labels 0x636044... as the Whitehat: it calls anySwapOutUnderlyingWithPermit on pools the original attacker had not yet drained, recovering funds before a second attacker could. d) Over-restrictive invariant.: We identify some cases where past transactions revert because the protective invariant is overrestrictive. In this case, the invariant expresses the right security property but its predicate is narrower than the protocol’s actual intended interface. This means that all reverted transactions were done by honest users; those transactions now fail under H because of the over-restrictive invariant, not because they exploit the vulnerability. Yearn yDAI is the clearest case: all 88 not-preserved calls invoke earn() from the same externally owned account, a keeper bot that harvests the vault on a schedule, and each reverts with only governance can call earn(). The perfect invariant should handle protocol access rules for keeper bots. e) Tight numerical envelope.: There is a particularly interesting variation of over-restrictive invariants, which we call “tight numerical envelope”. This category covers invariants whose guard is a numeric bound—a price band, a swap tax, a deviation threshold—rather than an access-control or

TABLE III RQ2 FUNCTIONAL PRESERVATION ON I NVARIANT E VAL . Collected: PRE - ATTACK HISTORICAL TRANSACTIONS SCOPED TO THE HARDENED FUNCTION . Pres.: BEHAVIOR PRESERVED UNDER THE INVARIANT. Not pres.: BEHAVIORAL DIVERGENCE UNDER THE INVARIANT. Incon.: INCONCLUSIVE , THE RECOMPILED REPLAY DOES NOT REPRODUCE THE ON - CHAIN OUTCOME ( ANALYZED IN RQ3). C ASES MARKED “—” HAVE NO REACHABLE PRE - ATTACK HISTORY FOR THE HARDENED FUNCTION . Date Case Collected Pres. Not pres. Incon. 2018-04 BEC 43,952 43,951 0 1 2018-04 SmartMesh 295 295 0 0 2020-08 Opyn 6 3 3 0 2021-02 Yearn yDAI 93 4 88 1 2021-09 Nimbus 862 391 466 5 2022-01 Anyswap 86 9 77 0 2022-02 TecraSpace — — — — 2022-06 Inverse Finance 49 7 41 1 2022-09 BadGuysbyRPF 769 763 0 6 2022-10 N00d 37 37 0 0 2022-10 Uerii — — — — 2022-12 JAY 712 711 0 1 2023-01 QTN 1,406 623 782 1 2023-05 ERC20TokenBank 12 10 0 2 2023-06 VINU 1 1 0 0 2023-08 Uwerx 120 120 0 0 2023-09 JumpFarm 520 506 0 14 2023-09 Unicly NFT 3 3 0 0 2023-10 pSeudoEth — — — — 2023-11 grok 56,847 56,582 4 261 2024-04 HoppyFrog 1,949 1,895 54 0 2024-06 APEMAGA 11 1 10 0 2024-06 JokInTheBox 8 8 0 0 2024-06 WIFCOIN — — — — 2024-08 OMPx 842 839 1 2 2024-09 Bedrock DeFi — — — — 2024-09 OnyxDAO — — — — 2026-03 AlkemiEarn 57 56 0 1 Total (28/28) 108,637 106,815 1,526 296

TABLE IV N OT- PRESERVED HISTORICAL REPLAYS PER CASE . Not pres.: TRANSACTIONS WHERE THE HARDENED TRACE H DIVERGES FROM THE RECOMPILED TRACE R. Trace inv., Sub. inv., AND Tx drift CLASSIFY THE MECHANICAL CAUSE OF DIVERGENCE : THE INVARIANT REVERTS THE TOP - LEVEL CALL , THE INVARIANT REVERTS INSIDE A SUBCALL , OR STORAGE DRIFT. Behavioural change reason: CASE - LEVEL ROOT CAUSE FROM MANUAL ANALYSIS . Behavioural Not Trace Sub. Tx pres. inv. inv. drift Change Reason 3 3 0 0 Past Exploit 88 88 0 0 Over-restrictive Invariant 21-09 Nimbus 466 449 5 12 Misusage 22-01 Anyswap 77 67 8 2 Past Exploit & Whitehat Operation 22-06 Inverse Finance 41 33 8 0 Tight Numerical Envelope 23-01 QTN 782 764 0 18 Over-restrictive Invariant 23-11 grok 4 1 2 1 Tight Numerical Envelope 24-04 HoppyFrog 54 8 20 26 Tight Numerical Envelope 24-06 APEMAGA 10 10 0 0 Past Exploit 24-08 OMPx 1 1 0 0 Misusage Total 1,526 1,424 43 59 Date Case 20-08 Opyn 21-02 Yearn yDAI

structural rule. When the past transaction reverts under replay, this is because the numeric bounds form an envelope too tight for part of the historical traffic. Reverted transactions under replay are then calibration failures: the invariant would preserve all past transactions with wider or context-sensitive bounds. Inverse Finance shows this pattern: 33 of its 41 notpreserved calls to latestAnswer() revert with LP price deviates from Curve VP, the ±10% band the invariant places around the Curve virtual price. Yet these calls are legitimate oracle reads made during ordinary price volatility, not attacks. A wider, volatility-aware, invariant would preserve these reads while still rejecting the flash-loan price spike stopped by the invariant. Answer to RQ2: To what extent do attackstopping invariants break existing behavior according to historical replay verification? The I NVARIANT E VAL invariants preserve behavior on 98.3% of replayed historical transactions. Every divergence is causally traced to the added invariant, not to a replay artifact. Divergences span 10 cases; some reject legitimate calls through over-restrictive invariants or numeric bounds set too tight, while the rest correctly reject exploits, misuses, or whitehatrescue transactions. C. RQ3: Inconclusive Replay We now manually analyze the 296 inconclusive replay verifications (column Incon. of Table III), which span twelve cases; Table V breaks them down. We identify three mechanical causes: original OOG, when the transaction ran out of gas under its original gas limit but the replay was allocated more gas and therefore succeeded; subcall OOG, when the mismatch is confined to an out-of-gas revert inside a subcall on the original trace rather than the top-level outcome; and accumulated drift, when state written by earlier, co-located transactions in the same block differs between real on-chain and the replayed fork. Original OOG (173 cases). The most frequent cause is a gas limit mismatch between the chain and the replay. Onchain, a transaction is submitted with a caller-specified gas limit; if execution exhausts that budget, the EVM reverts the entire call with an out-of-gas error. P ON D E R EPLAY, by design, does not cap the replay exactly at the original gas limit: it allocates sufficient gas to be able to execute the invariant. As a result, a transaction that ran out of gas on-chain succeeds in the recompiled replay R. The reproduction check O vs. R then fails, making the transaction inconclusive. This is a deliberate trade-off: enforcing the original gas cap would require exact gas accounting across a fork, which is unreliable. Subcall OOG (12 cases). A subtler variant occurs when the top-level call succeeds both on-chain and in replay, but an internal subcall exhausts gas and reverts differently in the two executions. In these cases, the transaction status matches between O and R, but the failed-subcall axis diverges: a nested

TABLE V I NCONCLUSIVE HISTORICAL REPLAYS PER CASE . Total Txs: TOTAL NUMBER OF TRANSACTIONS FOR WHICH R DOES NOT REPRODUCE O. Original OOG, Sub. OOG, AND Acc. drift CLASSIFY THE INCONCLUSIVE TXS . Preserved (H≡R): INCONCLUSIVE TRANSACTIONS WHERE R AND H ARE NEVERTHELESS EQUIVALENT, I . E ., THE INVARIANT DOES NOT ALTER THE ON - CHAIN OUTCOME . Total Original Sub. Acc. Preserved Date Case Txs OOG OOG drift (H≡R) 18-04 BEC 1 1 0 0 1 21-02 Yearn yDAI 1 1 0 0 0 21-09 Nimbus 5 2 3 0 3 22-06 Inverse Finance 1 1 0 0 0 22-09 BadGuysbyRPF 6 3 0 3 6 22-12 JAY 1 0 0 1 1 23-01 QTN 1 1 0 0 0 23-05 ERC20TokenBank 2 2 0 0 2 23-09 JumpFarm 14 13 0 1 14 23-11 grok 261 146 9 106 261 24-08 OMPx 2 2 0 0 2 26-03 AlkemiEarn 1 1 0 0 1 Total 296 173 12 111 291

call reverts on-chain but succeeds in the replay, or vice versa. Because the subcall’s revert is swallowed by the caller rather than propagating to the top level, the top-level outcome is unaffected. These 12 cases are confined to contracts with deep call trees where one internal path is close to the gas limit.

Accumulated drift (111 cases). The third cause is state drift introduced by co-located transactions in the same block. P ON D E R EPLAY reconstructs the pre-state of the target transaction by replaying all preceding transactions in block N in order. When any of those prior transactions behaves differently under recompiled bytecode, for example because its own replay is inconclusive, the block state at the point of the target transaction diverges from what actually existed onchain, causing the target transaction’s outcome to change as a consequence. The grok case is the clearest illustration: grok is a high-traffic DEX router through which dozens of other transactions pass in the same block, and small gas or state differences in those co-located calls compound into a state that no longer matches the real chain, accounting for the majority of the 111 accumulated drift cases.

Finally, we run the agreement check announced in Section III-F3: for 291 of the 296 inconclusive transactions (98%), the hardened trace H still matches the recompiled contract outcome R (last column of Table V). This confirms that inconclusiveness stems from the replay infrastructure, not from the invariant.

TABLE VI OVERALL CAPABILITY OF THE THREE REPRODUCIBLE TOOLS ON I NVARIANT E VAL . Generated: CONTRACTS FOR WHICH THE TOOL PRODUCED AT LEAST ONE INVARIANT FOR THE VULNERABLE FUNCTION . Match: SUBSET OF Generated WHOSE INVARIANT EXACTLY MATCHES THE GROUND TRUTH . Not generated: CONTRACTS FOR WHICH THE TOOL PRODUCED NO INVARIANT FOR THE VULNERABLE FUNCTION ( CRASH , EMPTY OUTPUT, OR WRONG TARGET ).

Tool

Generated

Match

Not generated

InvCon [16]

13

0

15

InvCon+ [18]

24

0

4

FLAMES [11]

28

2

0

Answer to RQ3: What are the limitations of historical replay verification? Inconclusive replays are fully understood and consistent. The dominant cause is out-of-gas changes, either in the called function (173 cases) or in subcalls (12 cases): the gas semantics is fully responsible for the behavioral change. Accumulated drift (111 cases) stems from co-located transactions in the same block that alter shared state before the target transaction executes. Our original historical replay verification is sound and its counterfactual analysis works as expected.

D. RQ4: Automatically Generated Invariants Table VI summarizes the capability of the three reproducible tools to generate effective invariants. Across InvCon [16], InvCon+ [18], and FLAMES [11], only 2 of the 28 groundtruth invariants can be synthesized, both by FLAMES. These two cases correspond to APEMAGA and Inverse Finance. All three tools produce candidates for many contracts (resp. 13, 24, and 28), but the candidates hardly capture the securitycritical property that can block the exploit. Answer to RQ4: To what extent are the stateof-the-art invariant generation tools able to generate attack-stopping invariants for real world attacks? State-of-the-art invariant generation tools are not yet capable of protecting against real-world attacks. Only 3 tools from previous research can be executed in this real-world setup. Only 2 of the 28 ground-truth invariants are synthesized by at least one of them. The considered tools produce many candidates, but almost none capture the securitycritical property that blocks the exploit. This calls for more research on invariant synthesis, evaluated on the real-world attack frontline. V. R ELATED W ORK This paper sits at the intersection of several research lines.

A. Invariant Generation

C. Contract Hardening

Invariant generation can be defined as proposing invariants directly from a program’s implementation, without requiring execution traces. Wang et al. [19] showed that a language model fine-tuned for invariant prediction infers invariants, at a quality comparable to a dynamic detector supplied with several execution traces. SmartInv [25] targets defects whose detection needs semantic reasoning that source code alone does not expose. It reasons jointly over Solidity source code and natural language artefacts such as comments and documentation. PropertyGPT [17] uses GPT-4 with retrievalaugmented generation to produce formal Certora verification properties. FLAMES [11] fine-tunes a language model on real-world invariants extracted from over 500,000 verified onchain contracts in order to generate executable require guards directly from source code, without labels or formal specifications. These tools only report accuracy against synthetic properties, audit reports, or held-out contracts. None measures whether the generated invariants can actually stop real onchain exploits. Our paper closes this gap by studying whether generated invariants actually protect smart contracts. We also note that few of these tools offered replication packages of sufficient quality that we can use in RQ4.

Another line of work studies contract hardening. Sereum [21] protects already-deployed contracts against reentrancy by tracking data flow inside a modified EVM and aborting transactions that violate a fixed reentrancy invariant. ContractGuard [26] introduces a runtime anomaly detection system for Ethereum smart contracts that profiles execution paths and reverts attacks upon detecting abnormal control flows. ÆGIS [24] proposes a runtime protection mechanism for deployed smart contracts that matches transactions against attack patterns. Solythesis [15] transforms Solidity source to insert runtime checks for developer-specified invariants, and reduces the resulting gas overhead through incremental state updates. HCC [13] is a hardening compiler that automatically injects integrity guards against reentrancy and integer bugs. HighGuard [9] detects business-logic violations at runtime by comparing execution against a formal model of intended behavior. BACKRUNNER [22] mitigates attacks by monitoring pending mempool transactions and rescuing funds before an exploit settles. CrossGuard [3] constrains the permitted sequences of external calls to block unexpected interactions. Raven [10] mines defensive patterns from Ethereum by clustering the conditions under which real transactions revert, yielding semantic categories of protective invariants.

B. Invariant Inference Invariant inference infers invariants from execution traces. The best known invariant inference tool is the Daikon dynamic invariant engine [8]. In blockchain, deployed contracts naturally accumulate rich execution histories, and mining these traces is a fundamentally good idea. There exist several invariant inference tools for smart contracts. InvCon [16] adapts the Daikon engine to Ethereum, mining on-chain histories as execution traces in order to flag ERC-20 non-compliance. InvCon+ [18] pairs dynamic trace mining with a Houdini-based static verifier. This filtering yields invariants that are formally sound, unlike the merely likely invariants InvCon reports. Trace2Inv [4] applies dynamic taint analysis to find which variables influence sensitive operations, then instantiates a catalogue of invariant templates as contract-specific require invariants. OpenTracer [5] is Trace2Inv’s trace-analysis engine, released as a standalone dynamic analyzer for invariant generation. SmartOracle [23] mines fine-grained invariants that span function calls, token balances, and state changes within and across transactions. This cross-transaction and cross-contract scope detects violations that single-trace invariants miss. Every inference tool depends on trace availability: underexercised functions accumulate too few data points to yield reliable invariants [4]. By construction, invariant inference tools cannot protect a newly deployed protocol. None of these works quantifies, as we do, how mined invariants are successful at stopping real-world attacks.

D. On-chain Exploit Datasets Empirical studies characterize the attacks themselves. Zhou et al. [28] study real world attacks and their potential mitigations. Zhang et al. [27] mine real front-running attacks to evaluate detectors. A recent systematic review attributes over one billion dollars of losses to recurring vulnerability root causes [20]. These works only document what went wrong. To our knowledge, we are the first to evaluate the extent to which smart contract invariants can protect against real-world attacks. VI. C ONCLUSION In this paper, we studied whether program invariants stop real smart contract exploits and whether automated tools could discover them. We built I NVARIANT E VAL, a benchmark of 28 real Ethereum attacks each paired with a human-authored invariant. We validated every invariant with a novel replay framework that re-executed 108,637 historical transactions. Every invariant blocked its target attack; 98.3% of replayed historical transactions were preserved, and every deviation was traced causally to the invariant rather than to replay noise. Against this ground truth, state-of-the-art generation tools fell short: FLAMES recovered the correct guard in only 2 of 28 cases. A single correctly placed invariant is sufficient to stop a real exploit; finding that invariant automatically remains an open problem.

ACKNOWLEDGEMENTS This work was supported by the WASP program funded by Knut and Alice Wallenberg Foundation, and by the Swedish Foundation for Strategic Research (SSF). Some computation was enabled by resources provided by the National Academic Infrastructure for Supercomputing in Sweden (NAISS). We thank Dwellir for giving us access to their RPC infrastructure under an academic license. R EFERENCES [1] Vivi Andersson, Sofia Bobadilla, Harald Hobbelhagen, and Martin Monperrus. Poco: Agentic proof-of-concept exploit generation for smart contracts. ACM Trans. Softw. Eng. Methodol., May 2026. Just Accepted. [2] Thomas Bernardi, Nurit Dor, Anastasia Fedotov, Shelly Grossman, Neil Immerman, Daniel Jackson, Alexander Nutz, Lior Oppenheim, Or Pistiner, Noam Rinetzky, et al. Wip: Finding bugs automatically in smart contracts with parameterized invariants. Retrieved July, 14:2020, 2020. [3] Zhiyang Chen, Sidi Mohamed Beillahi, Pasha Barahimi, Cyrus Minwalla, Han Du, A. Veneris, and Fan Long. Enforcing control flow integrity on defi smart contracts. 2025. [4] Zhiyang Chen, Ye Liu, Sidi Mohamed Beillahi, Yi Li, and Fan Long. Demystifying Invariant Effectiveness for Securing Smart Contracts. Proceedings of the ACM on Software Engineering, 8(FSE):Article 79, July 2024. [5] Zhiyang Chen, Ye Liu, Sidi Mohamed Beillahi, Yi Li, and Fan Long. Opentracer: A dynamic transaction trace analyzer for smart contract invariant generation and beyond. 2024 39th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 2399– 2402, 2024. [6] Defihacklabs. https://github.com/SunWeb3Sec/DeFiHackLabs/. [7] Defillama hacks dashboard. https://defillama.com/hacks. [8] Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants. Science of Computer Programming, 69(1):35–45, 2007. Special issue on Experimental Software and Toolkits. [9] Mojtaba Eshghie, Cyrille Artho, H. Stammler, Wolfgang Ahrendt, T. Hildebrandt, and Gerardo Schneider. Highguard: Cross-chain business logic monitoring of smart contracts. 2024 39th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 2378– 2381, 2023. [10] Mojtaba Eshghie, Melissa Mazura, and Alexandre Bartel. RAVEN: Mining Defensive Patterns in Ethereum via Semantic Transaction Revert Invariants, December 2025. arXiv:2512.22616. [11] Mojtaba Eshghie, Gabriele Morello, Matteo Lauretano, Alexandre Bartel, and Martin Monperrus. FLAMES: Fine-tuning LLMs to Synthesize Invariants for Smart Contract Security, October 2025. arXiv:2510.21401. [12] João F. Ferreira, Pedro Cruz, Thomas Durieux, and Rui Abreu. Smartbugs: a framework to analyze solidity smart contracts. In Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, ASE ’20, page 1349–1352, New York, NY, USA, 2021. Association for Computing Machinery. [13] Jens-Rene Giesen, Sébastien Andreina, Michael Rodler, Ghassan O. Karame, and Lucas Davi. Hcc: A language-independent hardening contract compiler for smart contracts. In International Conference on Applied Cryptography and Network Security, 2022. [14] Gerardo Iuliano, Luigi Allocca, Matteo Cicalese, and Dario Di Nucci. Automated vulnerability injection in solidity smart contracts: A mutation-based approach for benchmark development. In Proceedings of the 29th International Conference on Evaluation and Assessment in Software Engineering, EASE ’25, page 91–101, New York, NY, USA, 2025. Association for Computing Machinery. [15] Ao Li, Jemin Andrew Choi, and Fan Long. Securing smart contract with runtime validation. Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020. [16] Ye Liu and Yi Li. InvCon: A Dynamic Invariant Detector for Ethereum Smart Contracts. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, pages 1–5, Rochester MI USA, October 2022. ACM.

[17] Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, and Yang Liu. PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation. In Proceedings of the 32nd Network and Distributed System Security Symposium (NDSS). Internet Society, 2025. Distinguished Paper Award. [18] Ye Liu, Chengxuan Zhang, and Yi Li. Automated Invariant Generation for Solidity Smart Contracts. IEEE Transactions on Dependable and Secure Computing, 22(6):7172–7188, 2025. [19] Kexin Pei, David Bieber, Kensen Shi, Charles Sutton, and Pengcheng Yin. Can large language models reason about program invariants? In Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett, editors, Proceedings of the 40th International Conference on Machine Learning, volume 202 of Proceedings of Machine Learning Research, pages 27496–27520. PMLR, 23–29 Jul 2023. [20] Hadis Rezaei, Mojtaba Eshghie, Karl Anderesson, and Francesco Palmieri. Sok: Root cause of $1 billion loss in smart contract realworld attacks via a systematic literature review of vulnerabilities. ArXiv, abs/2507.20175, 2025. [21] Michael Rodler, Wenting Li, Ghassan O. Karame, and Lucas Davi. Sereum: Protecting existing smart contracts against re-entrancy attacks. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019, San Diego, California, USA, February 24-27, 2019. The Internet Society, 2019. [22] Chaofan Shou, Yuanyu Ke, Yupeng Yang, Qi Su, Or Dadosh, Assaf Eli, D. Benchimol, Doudou Lu, Daniel Q Tong, Dex Chen, Z. Tan, Jacob Chia, Koushik Sen, and Wenke Lee. Backrunner: Mitigating smart contract attacks in the real world. ArXiv, abs/2409.06213, 2024. [23] Jianzhong Su, Jiachi Chen, Zhiyuan Fang, Xingwei Lin, Yutian Tang, and Zibin Zheng. SmartOracle: Generating Smart Contract Oracle via Fine-Grained Invariant Detection. IEEE Transactions on Software Engineering, 51(4):947–959, 2025. [24] C. F. Torres, Mathis Baden, Robert Norvill, Beltran Borja Fiz Pontiveros, H. Jonker, and S. Mauw. Ægis: Shielding vulnerable smart contracts against attacks. Proceedings of the 15th ACM Asia Conference on Computer and Communications Security, 2020. [25] Sally Junsong Wang, Kexin Pei, and Junfeng Yang. SmartInv: Multimodal Learning for Smart Contract Invariant Inference. In 2024 IEEE Symposium on Security and Privacy (SP), pages 571–589. IEEE, May 2024. [26] Xinming Wang, Jiahao He, Z. Xie, Gansen Zhao, and S. Cheung. Contractguard: Defend ethereum smart contracts with embedded intrusion detection. IEEE Transactions on Services Computing, 13:314–328, 2019. [27] Wuqi Zhang, Lili Wei, S. Cheung, Yepang Liu, Shuqing Li, Luanqi Liu, and Michael R. Lyu. Combatting front-running in smart contracts: Attack mining, benchmark construction and vulnerability detector evaluation. IEEE Transactions on Software Engineering, 49:3630–3646, 2022. [28] Shunfan Zhou, Zhemin Yang, J. Xiang, Yinzhi Cao, Min Yang, and Yuan Zhang. An ever-evolving game: Evaluation of real-world attacks and defenses in ethereum ecosystem. In USENIX Security Symposium, 2020.

Related documents

• Equipment, Systems, and Network Information Security Protection#512285
• SoK: When Safe Agents Fail Together: The Security of Multi Agent LLM Systems#627632
• Contextual Integrity and EU Data Protection Law: Towards a More Informed and Transparent Analysis#461754
• The Dark Side of LLMs: Agent-based Attack Vectors for System-level Compromise#617839
• The Dark Side of LLMs: Agent-based Attack Vectors for System-level Compromise#617339