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

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 120 references that are in the map.
- First posted on arXiv 11 Feb 2025.

## Builds on (most cited first, 30 of 30)

- [Harnessing the Power of LLMs in Practice: A Survey on ChatGPT and Beyond](https://mlsanity.com/paper/2304.13712/) (2023)
- [GPTScan: Detecting Logic Vulnerabilities in Smart Contracts by Combining GPT with Program Analysis](https://mlsanity.com/paper/2308.03314/) (2023)
- [Securify: Practical Security Analysis of Smart Contracts](https://mlsanity.com/paper/1806.01143/) (2018)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [Combining Fine-Tuning and LLM-based Agents for Intuitive Smart Contract Auditing with Justifications](https://mlsanity.com/paper/2403.16073/) (2024)
- [Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts](https://mlsanity.com/paper/1907.03890/) (2019)
- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection](https://mlsanity.com/paper/1807.03932/) (2018)
- [sFuzz: An Efficient Adaptive Fuzzer for Solidity Smart Contracts](https://mlsanity.com/paper/2004.08563/) (2020)
- [Vandal: A Scalable Security Analysis Framework for Smart Contracts](https://mlsanity.com/paper/1809.03981/) (2018)
- [Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks](https://mlsanity.com/paper/1812.05934/) (2018)
- [solc-verify: A Modular Verifier for Solidity Smart Contracts](https://mlsanity.com/paper/1907.04262/) (2019)
- [FlashSyn: Flash Loan Attack Synthesis via Counter Example Driven Approximation](https://mlsanity.com/paper/2206.10708/) (2022)
- [Demystifying Invariant Effectiveness for Securing Smart Contracts](https://mlsanity.com/paper/2404.14580/) (2024)
- [Demystifying and Detecting Cryptographic Defects in Ethereum Smart Contracts](https://mlsanity.com/paper/2408.04939/) (2024)
- [Turn the Rudder: A Beacon of Reentrancy Detection for Smart Contracts on Ethereum](https://mlsanity.com/paper/2303.13770/) (2023)
- [Enhancing Smart Contract Security Analysis with Execution Property Graphs](https://mlsanity.com/paper/2305.14046/) (2023)
- [How to Save My Gas Fees: Understanding and Detecting Real-world Gas Issues in Solidity Programs](https://mlsanity.com/paper/2403.02661/) (2024)
- [sCompile: Critical Path Identification and Analysis for Smart Contracts](https://mlsanity.com/paper/1808.00624/) (2018)
- [Exploiting The Laws of Order in Smart Contracts](https://mlsanity.com/paper/1810.11605/) (2018)
- [Vulpedia: Detecting Vulnerable Ethereum Smart Contracts via Abstracted Vulnerability Signatures](https://mlsanity.com/paper/1912.04466/) (2019)
- [Rich Specifications for Ethereum Smart Contract Verification](https://mlsanity.com/paper/2104.10274/) (2021)
- [Definition and Detection of Defects in NFT Smart Contracts](https://mlsanity.com/paper/2305.15829/) (2023)
- [Safeguarding DeFi Smart Contracts against Oracle Deviations](https://mlsanity.com/paper/2401.06044/) (2024)
- [DEPOSafe: Demystifying the Fake Deposit Vulnerability in Ethereum Smart Contracts](https://mlsanity.com/paper/2006.06419/) (2020)
- [Extracting Smart Contracts Tested and Verified in Coq](https://mlsanity.com/paper/2012.09138/) (2020)
- [Declarative Smart Contracts](https://mlsanity.com/paper/2207.13827/) (2022)
- [SmartState: Detecting State-Reverting Vulnerabilities in Smart Contracts via Fine-Grained State-Dependency Analysis](https://mlsanity.com/paper/2406.15988/) (2024)
- [Definition and Detection of Centralization Defects in Smart Contracts](https://mlsanity.com/paper/2411.10169/) (2024)

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

- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers](https://mlsanity.com/paper/2605.29059/) (2026)

## Abstract (arXiv)

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 translated rules to model potential rule violations, and performs symbolic execution for violation detection. 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 financial theft. Furthermore, SymGPT outperforms six automated techniques and a security-expert auditing service, underscoring its superiority over current smart contract analysis methods.