SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models

TL;DR

SymGPT addresses the challenge of verifying Ethereum smart contracts against ERC rules by integrating large language models with symbolic execution. It builds an empirical understanding of 132 ERC rules across ERC20, ERC721, and ERC1155 to inform rule extraction, translation, and constraint synthesis. The system formalizes rules with an EBNF grammar and uses symbolic execution guided by generated constraints to detect violations across thousands of real-world contracts, outperforming static/dynamic baselines and human auditors while remaining cost-efficient. It further demonstrates generalization to a newer standard (ERC3525) with zero false positives in a small test, underscoring the practical impact of combining LLMs with formal methods for scalable ERC compliance verification.

Abstract

To govern smart contracts running on Ethereum, multiple Ethereum Request for Comment (ERC) standards have been developed, each having a set of rules to guide the behaviors of smart contracts. Violating the ERC rules could cause serious security issues and financial loss, signifying the importance of verifying smart contracts follow ERCs. Today's practices of such verification are to manually audit each single contract, use expert-developed program-analysis tools, or use large language models (LLMs), all of which are far from effective in identifying ERC rule violations. This paper introduces SymGPT, a tool that combines the natural language understanding of large language models (LLMs) with the formal guarantees of symbolic execution to automatically verify smart contracts' compliance with ERC rules. To develop SymGPT, we conduct an empirical study of 132 ERC rules from three widely used ERC standards, examining their content, security implications, and natural language descriptions. Based on this study, we design SymGPT by first instructing an LLM to translate ERC rules into a defined EBNF grammar. We then synthesize constraints from the formalized rules to represent scenarios where violations may occur and use symbolic execution to detect them. Our evaluation shows that SymGPT identifies 5,783 ERC rule violations in 4,000 real-world contracts, including 1,375 violations with clear attack paths for stealing financial assets, demonstrating its effectiveness. Furthermore, SymGPT outperforms six automated techniques and a security-expert auditing service, underscoring its superiority over current smart contract analysis methods.

Figures (7)

• Figure 1: An ERC20 rule violation that can be exploited to steal tokens. (Code simplified for illustration purpose.)
• Figure 2: The workflow of SymGPT. (Components with a pattern background are powered by an LLM.)
• Figure 3: EBNF grammar. (The grammar has been simplified for illustration. Terminals highlighted in violet represent utility functions, and more details can be found in Table \ref{['tab:utility']}.)
• Figure 4: The formalization of the rule violated in Figure \ref{['fig:20-high']}.
• Figure 5: An ERC1155 contract contains four high-security impact violations. (Code simplified for illustration purpose.)