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 \emph{SymGPT\xspace},
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\xspace instructs an LLM to translate ERC rules into a domain-specific language,
synthesizes constraints from the translated rules to model potential rule violations,
and performs symbolic execution for violation detection.
Our evaluation shows that SymGPT\xspace identifies 5,783 ERC rule violations
in 4,000 real-world contracts, including 1,375 violations with
clear attack paths for financial theft.
Furthermore, SymGPT\xspace outperforms six automated techniques
and a security-expert auditing service, underscoring its superiority over current
smart contract analysis methods.