Large Language Models for Smart Contract Security: From Property Generation to Attack Detection
Conference proceedings talk, Shonan Meeting No.229, Shonan Village Center, Japan
Recent advances in large language models (LLMs) such as GPT-4 have opened new possibilities for automating smart contract security analysis–traditionally a domain requiring deep program reasoning and formal methods expertise. In this talk, I will introduce our recent efforts to apply LLMs to two key challenges in this space: PropertyGPT, which automatically generates verifiable formal properties (e.g., invariants and pre/post-conditions) for smart contracts, and DeFiScope, which detects complex DeFi price manipulation attacks by reasoning over on-chain price models and high-level protocol semantics. Together, these works demonstrate that LLMs can bridge the gap between human reasoning and formal verification, offering both interpretability and automation.