[D] We analyzed 4,000 Ethereum contracts by combining an LLM and symbolic execution and found 5,783 issues

Happy to share that our paper “SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models” has been accepted to OOPSLA.

SymGPT combines large language models (LLMs) with symbolic execution to automatically verify whether Ethereum smart contracts comply with Ethereum Request for Comment (ERC) rules. SymGPT 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.

In our evaluation on 4,000 real-world contracts, SymGPT identified 5,783 ERC rule violations, including 1,375 violations with clear attack paths for financial theft. The paper also shows that SymGPT outperforms six automated techniques and a security-expert auditing service.

OOPSLA—Object-oriented Programming, Systems, Languages, and Applications—is one of the flagship venues in programming languages and software engineering. Its scope broadly includes software development, program analysis, verification, testing, tools, runtime systems, and evaluation, and OOPSLA papers are published in the Proceedings of the ACM on Programming Languages (PACMPL).

I’m also exploring how to further improve the tool and apply it to other domains. Discussion and feedback are very welcome.