pith. machine review for the scientific record. sign in

arxiv: 2604.14038 · v1 · submitted 2026-04-15 · 💻 cs.CR · cs.LO

Recognition: unknown

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

Massimo Bartoletti , Angelo Ferrando , Enrico Lipparini , Vadim Malvone
Authors on Pith no claims yet

Pith reviewed 2026-05-10 12:54 UTC · model grok-4.3

classification 💻 cs.CR cs.LO
keywords smart contractsformal verificationHennessy-Milner logicSoliditymodel checkingtemporal propertiesblockchain
0
0 comments X

The pith

An automated encoding of a Solidity subset and temporal specifications into Lustre enables the Kind 2 model checker to verify whether smart contracts respect complex properties.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a method to specify and verify temporal properties of smart contracts that unfold across multiple transactions, such as liquidity or front-running attacks. It achieves this by automatically translating an expressive subset of Solidity code along with specifications written in first-order Hennessy-Milner logic into the Lustre language accepted by the Kind 2 model checker. A sympathetic reader would care because empirical studies link many real attacks to business-logic flaws that current tools cannot express or detect. If the translation is faithful, the approach reduces the verification task to an automated model-checking run that reports whether the contract satisfies the given property.

Core claim

Our approach provides a fully automated encoding into Lustre 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 the approach in a toolchain that integrates the translation and verification steps and evaluate it on a benchmark of smart contracts and temporal properties that capture complex attack scenarios.

What carries the argument

The automated encoding from an expressive subset of Solidity together with first-order Hennessy-Milner logic specifications into Lustre, which preserves the semantics required for checking properties that span multiple transactions.

If this is right

  • Non-trivial temporal properties spanning multiple transactions become checkable for smart contracts.
  • Violations corresponding to complex attack scenarios can be detected automatically.
  • The integrated toolchain performs both translation and verification without manual steps in between.
  • The method handles benchmarks that capture real-world attack patterns beyond the reach of prior tools.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same translation strategy could be adapted to other contract languages provided the semantic preservation holds.
  • Verification results could be combined with on-chain monitoring to check live contracts against the same properties.
  • Increasing the handled subset of Solidity would widen the set of verifiable contracts if the encoding remains sound.

Load-bearing premise

The chosen subset of Solidity and its translation into Lustre preserve the original semantics of the temporal properties when the contract runs on a real blockchain.

What would settle it

Running the toolchain on a contract that Kind 2 reports as correct, then observing a violation of the stated property during actual execution on a blockchain.

Figures

Figures reproduced from arXiv: 2604.14038 by Angelo Ferrando, Enrico Lipparini, Massimo Bartoletti, Vadim Malvone.

Figure 1
Figure 1. Figure 1: Syntax of contracts [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Semantics of expressions [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 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 state￾ment s fail, then the evaluation of s gives ⊥, representing an execution error. This makes the premise false, and so the transition does not happen. Th… view at source ↗
Figure 4
Figure 4. Figure 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 syn￾tax in [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Interpretation of contract specifications. [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 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 [PITH_FULL_IMAGE:figures/full_fig_p022_6.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript presents KindHML, a toolchain for the formal verification of an expressive subset of Solidity smart contracts against temporal specifications written in first-order Hennessy-Milner Logic. Contracts and specifications are automatically encoded into Lustre and checked for satisfaction using the Kind 2 model checker; the authors claim this enables detection of multi-transaction attacks (e.g., liquidity and front-running) that lie beyond existing tools. They report an implementation and an evaluation on a benchmark of contracts and properties.

Significance. If the encoding is shown to preserve semantics, the work would be significant: it combines an expressive temporal logic (first-order HML) with a mature synchronous model checker (Kind 2) to address a recognized gap in smart-contract verification. The approach is parameter-free and offers a fully automated translation, which is a strength. However, the absence of any semantic-preservation argument currently limits the strength of the central claim.

major comments (2)
  1. [Abstract / encoding section] Abstract and the description of the encoding (presumably §3): the claim that the translation 'preserves the original semantics for temporal properties across multiple transactions' is load-bearing for the entire contribution, yet no bisimulation, inductive invariant, or even a small hand-checked example is supplied to justify that Lustre streams correctly model Solidity storage, msg.sender, external calls, and HML diamond modalities over transaction traces.
  2. [Evaluation / benchmarks] Evaluation section: the abstract asserts that the approach 'can effectively verify non-trivial temporal properties' and 'detect violations beyond existing tools,' but supplies no tables, concrete verdicts, performance numbers, or comparison against baselines; without these data the effectiveness claim cannot be assessed.
minor comments (2)
  1. [Introduction] The precise definition of the 'expressive subset of Solidity' (e.g., which language constructs are supported and which are excluded) should be stated explicitly early in the paper rather than left implicit.
  2. [Preliminaries / encoding] Notation for first-order HML modalities and their Lustre encoding could be clarified with a small running example that shows both the source formula and the generated Lustre node.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments on our manuscript. We address the major points below, indicating where revisions will be made to improve clarity and support for our claims.

read point-by-point responses

  1. Referee: [Abstract / encoding section] Abstract and the description of the encoding (presumably §3): the claim that the translation 'preserves the original semantics for temporal properties across multiple transactions' is load-bearing for the entire contribution, yet no bisimulation, inductive invariant, or even a small hand-checked example is supplied to justify that Lustre streams correctly model Solidity storage, msg.sender, external calls, and HML diamond modalities over transaction traces.

    Authors: We acknowledge that the manuscript does not supply a formal semantic-preservation argument such as a bisimulation or inductive invariant. Section 3 describes the encoding by mapping Solidity state variables and storage to Lustre streams, transaction sequences to discrete steps, msg.sender and call contexts to auxiliary streams, and first-order HML diamond modalities to Lustre temporal operators. While we maintain that the translation is faithful by construction, we agree an explicit justification is needed. In the revision we will insert a small hand-checked example (a simple contract with a multi-transaction property) that walks through the encoding of storage, sender, and a diamond modality, thereby providing concrete evidence of the correspondence. revision: partial

  2. Referee: [Evaluation / benchmarks] Evaluation section: the abstract asserts that the approach 'can effectively verify non-trivial temporal properties' and 'detect violations beyond existing tools,' but supplies no tables, concrete verdicts, performance numbers, or comparison against baselines; without these data the effectiveness claim cannot be assessed.

    Authors: The evaluation section does describe a benchmark of contracts and properties (including liquidity and front-running scenarios) together with the toolchain's ability to detect violations. However, we accept that the current presentation lacks explicit tables, verdicts, timings, and baseline comparisons. We will revise the section to add tables listing each contract, the encoded property, the Kind 2 outcome (satisfied/violated), verification time, and a short discussion of how the temporal properties go beyond the reach of existing static analyzers. revision: yes

Circularity Check

0 steps flagged

No circularity: translation-based encoding of Solidity subset and HML into Lustre

full rationale

The paper's core contribution is a constructive, automated translation from a Solidity subset plus first-order Hennessy-Milner Logic specifications into Lustre for Kind 2 model checking. No equations, parameters, or derivations are presented that reduce the claimed semantic preservation or verification results to quantities defined inside the paper by construction. The approach is evaluated on external benchmarks of contracts and attack scenarios, providing independent content rather than self-referential fitting or renaming. No self-citation chains or uniqueness theorems are invoked as load-bearing premises. This is a standard formal-methods translation paper whose claims rest on the correctness of the encoding rules themselves, not on any internal circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review yields no explicit free parameters, axioms, or invented entities; the approach rests on standard model-checking assumptions whose details are not supplied.

pith-pipeline@v0.9.0 · 5510 in / 1121 out tokens · 20147 ms · 2026-05-10T12:54:30.977674+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

55 extracted references · 41 canonical work pages

  1. [1]

    Smart contract weakness classification (SWC): Transaction order dependence,ht tps://swcregistry.io/docs/SWC-114, accessed on March 23, 2026

    2026

  2. [2]

    Cambridge University Press (2007)

    Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press (2007)

    2007

  3. [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

    2017

  4. [4]

    In: Computer Aided Verification

    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

    work page doi:10.1007/978-3-031-13185-1_16 2022

  5. [5]

    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM49(5), 672–713 (2002).https://doi.org/10.1145/585265.585270

    work page doi:10.1145/585265.585270 2002

  6. [6]

    In: Handbook of Satisfiability (2021).https://doi.org/10.3233/978-1-586 03-929-5-825

    Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theo- ries. In: Handbook of Satisfiability (2021).https://doi.org/10.3233/978-1-586 03-929-5-825

    work page doi:10.3233/978-1-586 2021

  7. [7]

    In: FMBC

    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

    work page doi:10.4230/oasics.fmbc.2025.3 2025

  8. [8]

    Bartoletti, M., Ferrando, A., Lipparini, E., Malvone, V.: Solvent: Liquidity verifi- cation of smart contracts15234, 256–266 (2024).https://doi.org/10.1007/97 8-3-031-76554-4_14

    work page doi:10.1007/97 2024

  9. [9]

    In: FMBC

    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

    work page doi:10.4230/oasics.fmbc.2024.6 2024

  10. [10]

    Lamb, Jialin Yu, Philip H

    Bartoletti, M., Lipparini, E., Pompianu, L.: LLMs as verification oracles for Solid- ity. In: Financial Cryptography (2026).https://doi.org/10.48550/arXiv.2509. 19153

    work page doi:10.48550/arxiv.2509 2026

  11. [11]

    Handbook of satisfiability185(99), 457–481 (2009)

    Biere, A.: Bounded model checking. Handbook of satisfiability185(99), 457–481 (2009)

    2009

  12. [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

    work page doi:10.1007/978-3-319-10575-8_10 2018

  13. [13]

    In: ATVA

    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

    work page doi:10.1007/978-3-319-24953-7_25 2015

  14. [14]

    In: Arvind, V., Ramanujam, S

    Bohn, J., Damm, W., Grumberg, O., Hungar, H., Laster, K.: First-order-ctl model checking. In: Arvind, V., Ramanujam, S. (eds.) Foundations of Software Technol- ogy and Theoretical Computer Science. pp. 283–294. Springer Berlin Heidelberg, Berlin, Heidelberg (1998).https://doi.org/10.1007/978-3-540-49382-2_27

    work page doi:10.1007/978-3-540-49382-2_27 1998

  15. [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

    work page doi:10.1109/sp46214.2022.9833721 2022

  16. [16]

    In: VMCAI

    Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI. pp. 70–

  17. [17]

    Springer (2011).https://doi.org/10.1007/978-3-642-18275-4_7

    work page doi:10.1007/978-3-642-18275-4_7 2011

  18. [18]

    In: OVERLAY

    Chahoki, A.Z., Roveri, M., Amyot, D., Mylopoulos, J.: Revisiting formal verifica- tion in VeriSolid: An analysis and enhancements. In: OVERLAY. CEUR, vol. 3629, pp. 55–60 (2023)

    2023

  19. [19]

    Knowlog: Knowledge enhanced pre-trained language model for log understanding

    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

    work page doi:10.1145/3597503.3623302 2024

  20. [20]

    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

    work page doi:10.1007/978-3-319-4 2016

  21. [21]

    In: Guessarian, I

    De Nicola, R., Vaandrager, F.: Action versus state based logics for transition sys- tems. 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

    work page doi:10.1007/3-540-53479-2_17 1990

  22. [22]

    Expert Syst

    Ding, H., Liu, Y., Piao, X., Song, H., Ji, Z.: Smartguard: An LLM-enhanced frame- work for smart contract vulnerability detection. Expert Syst. Appl.269(2025). https://doi.org/doi.org/10.1016/j.eswa.2025.126479

    work page doi:10.1016/j.eswa.2025.126479 2025

  23. [23]

    In: Financial Cryptography and Data Security

    Eskandari, S., Moosavi, S., Clark, J.: SoK: Transparent Dishonesty: Front-Running Attacks on Blockchain. In: Financial Cryptography and Data Security. pp. 170–

  24. [24]

    Springer (2020).https://doi.org/10.1007/978-3-030-43725-1_13

    work page doi:10.1007/978-3-030-43725-1_13 2020

  25. [25]

    In: WETSEB

    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

    work page doi:10.1109/wetseb.201 2019

  26. [26]

    In: AAMAS (2026), to appear

    Ferrando, A., Kana, B., Malvone, V.: Wallet ATL: Towards reliable smart contract verification. In: AAMAS (2026), to appear

    2026

  27. [27]

    In: Financial Cryptography and Data Security (to appear) (2026)

    Gervais, A., Zhou, L.: AI agent smart contract exploit generation. In: Financial Cryptography and Data Security (to appear) (2026)

    2026

  28. [28]

    In: VSTTE

    Hajdu, Á., Jovanovic, D.: solc-verify: A modular verifier for Solidity smart con- tracts. In: VSTTE. LNCS, vol. 12031, pp. 161–179. Springer (2019).https: //doi.org/10.1007/978-3-030-41600-3_11

    work page doi:10.1007/978-3-030-41600-3_11 2019

  29. [29]

    Proceedings of the IEEE79(9), 1305–1320 (1991)

    Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language lustre. Proceedings of the IEEE79(9), 1305–1320 (1991). https://doi.org/10.1109/5.97300

    work page doi:10.1109/5.97300 1991

  30. [30]

    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM32(1), 137–161 (1985).https://doi.org/10.1145/2455.2460

    work page doi:10.1145/2455.2460 1985

  31. [31]

    In: Rattray, C

    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 Ver- ification of Concurrent Systems. pp. 294–330. Springer London, London (1990). https://doi.org/10.1007/978-1-4471-3534-0_15

    work page doi:10.1007/978-1-4471-3534-0_15 1990

  32. [32]

    Jackson, D., Nandi, C., Sagiv, M.: Certora technology white paper.https://docs .certora.com/en/latest/docs/whitepaper/index.html(2022)

    2022

  33. [33]

    In: NDSS

    Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: NDSS. The Internet Society (2018)

    2018

  34. [34]

    In: ACM SIGSOFT Int

    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

    work page doi:10.1145/3293882.3330560 2019

  35. [35]

    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

    work page doi:10.1007/978-3-5 2008

  36. [36]

    IEEE Access10, 57037–57062 (2022).https: //doi.org/10.1109/ACCESS.2022.3169902

    Kushwaha,S.S.,Joshi,S.,Singh,D.,Kaur,M.,Lee,H.N.:Ethereumsmartcontract analysis tools: A systematic review. IEEE Access10, 57037–57062 (2022).https: //doi.org/10.1109/ACCESS.2022.3169902

    work page doi:10.1109/access.2022.3169902 2022

  37. [37]

    In: Enjalbert, P., Mayr, E.W., Wagner, K.W

    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

    work page doi:10.1007/3-540-5 1994

  38. [38]

    Deep Learning with Differential Privacy

    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

    work page arXiv 2016

  39. [39]

    IEEE Trans

    Nelaturu, K., Mavridou, A., Stachtiari, E., Veneris, A.G., Laszka, A.: Correct-by- design 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

    work page doi:10.1109/tdsc.2022.3200840 2023

  40. [40]

    In: ICSE

    Nguyen,T.D.,Pham,L.H.,Sun,J.,Lin,Y.,Minh,Q.T.:sFuzz:anefficientadaptive fuzzer for Solidity smart contracts. In: ICSE. pp. 778–788. ACM (2020).https: //doi.org/10.1145/3377811.3380334

    work page doi:10.1145/3377811.3380334 2020

  41. [41]

    In: ACSAC

    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

    work page doi:10.1145/3274694.3274743 2018

  42. [42]

    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

    work page doi:10.1109/sp40000.2020.00024 2020

  43. [43]

    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

    work page doi:10.1016/j.bcra.2025.100390 2025

  44. [44]

    In2024 IEEE Symposium on Security and Privacy (SP)

    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

    work page doi:10.1109/sp54263.2024.00230 2024

  45. [45]

    In: FMCAD

    Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a sat-solver. In: FMCAD. pp. 127–144. Springer (2000)

    2000

  46. [46]

    Stephens, J., Ferles, K., Mariano, B., Lahiri, S.K., Dillig, I.: SmartPulse: Auto- mated checking of temporal properties in smart contracts. In: S&P. pp. 555–571. IEEE (2021).https://doi.org/10.1109/SP40001.2021.00085

    work page doi:10.1109/sp40001.2021.00085 2021

  47. [47]

    In: WETSEB

    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

    work page doi:10.1145/3194113.3194115 2018

  48. [48]

    A survey of smart contract formal specification and verification,

    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

    work page doi:10.1145/3464421 2022

  49. [49]

    In: USENIX Security Symp

    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)

    2021

  50. [50]

    In: EuroS&P

    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

    work page doi:10.1109/eurosp51992.2021.00018 2021

  51. [51]

    Securify: Practical security analysis of smart contracts,

    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

    work page doi:10.1145/3243734.3243780 2018

  52. [52]

    IEEE TSE (2025).https://doi.org/10 .1109/TSE.2025.3597319

    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

    work page arXiv 2025

  53. [53]

    In: VMCAI

    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

    work page doi:10.1007/978-3-030-94583-1_21 2022

  54. [54]

    In: ACISP

    Xiao,Z.,Li,Y.,Wang,Q.,Chen,S.:PrompttoPwn:Automatedexploitgeneration for smart contracts. In: ACISP. pp. 1–28. LNCS, Springer (2026)

    2026

  55. [55]

    In: ICSE

    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

    work page doi:10.1109/icse 2023