PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
Ye Liu
Network and Distributed System Security (NDSS) Symposium 2025 · Day 3 · Blockchain Security 2
The rapid proliferation of smart contracts on blockchain systems has ushered in a new era of decentralized applications, managing billions in digital assets. However, this innovation comes with significant security risks, as smart contracts are frequently targeted by attackers, leading to substantial financial losses—reportedly **$38.7 million in 2024** alone. Traditional formal verification techniques, while powerful in proving program correctness and uncovering deep bugs, often struggle with the unique challenges of smart contract auditing. These methods are typically customized for common vulnerabilities or demand extensive manual input from users, hindering their scalability and adaptability to application-specific security flaws.
AI review
Competent systems research that combines RAG with formal verification for smart contract property generation — a real problem, a real contribution, and actual bug bounties to show for it. The work is legitimate but not groundbreaking; the core insight (LLMs are better at generating specs in a Solidity-like DSL than in an alien formal language) is sensible engineering rather than a paradigm shift, and the evaluation numbers, while solid, leave meaningful gaps unaddressed.