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

Computer Science > Artificial Intelligence arXiv:2502.07644 (cs) [Submitted on 11 Feb 2025 (v1), last revised 1 Mar 2026 (this version, v3)] Title:SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models Authors:Shihao Xia, Mengting He, Shuai Shao, Tingting Yu, Yiying Zhang, Nobuko Yoshida, Linhai Song View a PDF of the paper titled SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models, by Shihao Xia and 6 other authors View PDF HTML (experimental) Abstract:To govern smart contracts running on Ethereum, multiple Ethereum Request for Comment (ERC) standards have been developed, each defining a set of rules governing contract behavior. Violating these rules can cause serious security issues and financial losses, signifying the importance of verifying ERC compliance. Today's practices of such verification include manual audits, expert-developed program-analysis tools, and large language models (LLMs), all of which remain ineffective at detecting ERC rule violations. This paper introduces SymGPT, a tool that combines LLMs with symbolic execution to automatically verify smart contracts' compliance with ERC rules. We begin by empirically analyzing 132 ERC rules from three major ERC standards, examining their content, security implications, and natural language descriptions. Based on this study, SymGPT instructs an LLM to translate ERC rules into a domain-specific language, synthesizes constraints from the...