# eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts

arXiv: https://arxiv.org/abs/2005.06227 · HTML: https://mlsanity.com/paper/2005.06227/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 May 2020.

## Built on by (most cited first, 11 of 11)

- [Blockchain Large Language Models](https://mlsanity.com/paper/2304.12749/) (2023)
- [SCALM: Detecting Bad Practices in Smart Contracts Through LLMs](https://mlsanity.com/paper/2502.04347/) (2025)
- [Eth2Vec: Learning Contract-Wide Code Representations for Vulnerability Detection on Ethereum Smart Contracts](https://mlsanity.com/paper/2101.02377/) (2021)
- [ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning](https://mlsanity.com/paper/2103.12607/) (2021)
- [MANDO: Multi-Level Heterogeneous Graph Embeddings for Fine-Grained Detection of Smart Contract Vulnerabilities](https://mlsanity.com/paper/2208.13252/) (2022)
- [SmartLLMSentry: A Comprehensive LLM Based Smart Contract Vulnerability Detection Framework](https://mlsanity.com/paper/2411.19234/) (2024)
- [Usenix'23 Extended Version: Smart Learning to Find Dumb Contracts](https://mlsanity.com/paper/2304.10726/) (2023)
- [Vulnerability Detection in Ethereum Smart Contracts via Machine Learning: A Qualitative Analysis](https://mlsanity.com/paper/2407.18639/) (2024)
- [Dual-view Aware Smart Contract Vulnerability Detection for Ethereum](https://mlsanity.com/paper/2407.00336/) (2024)
- [JANUS: A Difference-Oriented Analyzer For Financial Centralization Risks in Smart Contracts](https://mlsanity.com/paper/2412.03938/) (2024)
- [Robust Smart Contract Vulnerability Detection via Contrastive Learning-Enhanced Granular-ball Training](https://mlsanity.com/paper/2603.27734/) (2026)

## Abstract (arXiv)

Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences and, even worse, they can be hardly fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging for a variety of reasons, such as the specific transaction-oriented programming mechanisms, which feature a subtle semantics, and the fact that the blockchain data which the contract under analysis interacts with, including the code of callers and callees, are not statically known. In this work, we present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode and an experimental large-scale evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 95% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%.