# PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation

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

## Key facts

- Cited by 37 papers in the map (data through 14 Oct 2026).
- Placed in Privacy and security of RAG, one of 15 directions in Retrieval-augmented generation.
- Builds on 30 of its 67 references that are in the map.
- First posted on arXiv 4 May 2024.

## Placed in

- Retrieval-augmented generation / [Privacy and security of RAG](https://mlsanity.com/rag/privacy-and-security-of-rag/)

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

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Billion-scale similarity search with GPUs](https://mlsanity.com/paper/1702.08734/) (2017)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Keep the Conversation Going: Fixing 162 out of 337 bugs for 0.42 each using ChatGPT](https://mlsanity.com/paper/2304.00385/) (2023)
- [Examining Zero-Shot Vulnerability Repair with Large Language Models](https://mlsanity.com/paper/2112.02125/) (2021)
- [Large Language Models are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Models](https://mlsanity.com/paper/2212.14834/) (2022)
- [Slither: A Static Analysis Framework For Smart Contracts](https://mlsanity.com/paper/1908.09878/) (2019)
- [AutoChip: Automating HDL Generation Using LLM Feedback](https://mlsanity.com/paper/2311.04887/) (2023)
- [On the Effect of Pretraining Corpora on In-context Learning by a Large-scale Language Model](https://mlsanity.com/paper/2204.13509/) (2022)
- [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)
- [LLM4Vuln: A Unified Evaluation Framework for Decoupling and Enhancing LLMs' Vulnerability Reasoning](https://mlsanity.com/paper/2401.16185/) (2024)
- [Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts](https://mlsanity.com/paper/1907.03890/) (2019)
- [ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection](https://mlsanity.com/paper/1807.03932/) (2018)
- [Can Large Language Models Understand Context?](https://mlsanity.com/paper/2402.00858/) (2024)
- [FixMiner: Mining Relevant Fix Patterns for Automated Program Repair](https://mlsanity.com/paper/1810.01791/) (2018)
- [sFuzz: An Efficient Adaptive Fuzzer for Solidity Smart Contracts](https://mlsanity.com/paper/2004.08563/) (2020)
- [Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks](https://mlsanity.com/paper/1812.05934/) (2018)
- [ACFIX: Guiding LLMs with Mined Common RBAC Practices for Context-Aware Repair of Access Control Vulnerabilities in Smart Contracts](https://mlsanity.com/paper/2403.06838/) (2024)
- [A Survey of Smart Contract Formal Specification and Verification](https://mlsanity.com/paper/2008.02712/) (2020)
- [DeFiRanger: Detecting Price Manipulation Attacks on DeFi Applications](https://mlsanity.com/paper/2104.15068/) (2021)
- [Oracle-Supported Dynamic Exploit Generation for Smart Contracts](https://mlsanity.com/paper/1909.06605/) (2019)
- [Formal Analysis of Composable DeFi Protocols](https://mlsanity.com/paper/2103.00540/) (2021)
- [Formal Specification and Verification of Smart Contracts for Azure Blockchain](https://mlsanity.com/paper/1812.08829/) (2018)
- [An Empirical Study of Blockchain System Vulnerabilities: Modules, Types, and Patterns](https://mlsanity.com/paper/2110.12162/) (2021)
- [Automated Invariant Generation for Solidity Smart Contracts](https://mlsanity.com/paper/2401.00650/) (2024)

## Built on by (most cited first, 30 of 37)

- [SelfDefend: LLMs Can Defend Themselves against Jailbreaking in a Practical Manner](https://mlsanity.com/paper/2406.05498/) (2024)
- [ACE: A Security Architecture for LLM-Integrated App Systems](https://mlsanity.com/paper/2504.20984/) (2025)
- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [Measuring and Augmenting Large Language Models for Solving Capture-the-Flag Challenges](https://mlsanity.com/paper/2506.17644/) (2025)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [Incident Response Planning Using a Lightweight Large Language Model with Reduced Hallucination](https://mlsanity.com/paper/2508.05188/) (2025)
- [SCALM: Detecting Bad Practices in Smart Contracts Through LLMs](https://mlsanity.com/paper/2502.04347/) (2025)
- [Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview](https://mlsanity.com/paper/2503.10784/) (2025)
- [Knowledge-Based Multi-Agent Framework for Automated Software Architecture Design](https://mlsanity.com/paper/2503.20536/) (2025)
- [Semia: Auditing Agent Skills via Constraint-Guided Representation Synthesis](https://mlsanity.com/paper/2605.00314/) (2026)
- [Detecting Various DeFi Price Manipulations with LLM Reasoning](https://mlsanity.com/paper/2502.11521/) (2025)
- [Inferring multiple helper Dafny assertions with LLMs](https://mlsanity.com/paper/2511.00125/) (2025)
- [RulePilot: An LLM-Powered Agent for Security Rule Generation](https://mlsanity.com/paper/2511.12224/) (2025)
- [DataGovBench: Benchmarking LLM Agents for Real-World Data Governance Workflows](https://mlsanity.com/paper/2512.04416/) (2025)
- [Agentic Specification Generator for Move Programs](https://mlsanity.com/paper/2509.24515/) (2025)
- [SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models](https://mlsanity.com/paper/2502.07644/) (2025)
- [Towards Secure Program Partitioning for Smart Contracts with LLM's In-Context Learning](https://mlsanity.com/paper/2502.14215/) (2025)
- [Adaptive Plan-Execute Framework for Smart Contract Security Auditing](https://mlsanity.com/paper/2505.15242/) (2025)
- [LISA Technical Report: An Agentic Framework for Smart Contract Auditing](https://mlsanity.com/paper/2509.24698/) (2025)
- [VulnResolver: A Hybrid Agent Framework for LLM-Based Automated Vulnerability Issue Resolution](https://mlsanity.com/paper/2601.13933/) (2026)
- [FTSmartAudit: A Knowledge Distillation-Enhanced Framework for Automated Smart Contract Auditing Using Fine-Tuned LLMs](https://mlsanity.com/paper/2410.13918/) (2024)
- [Towards Automated Formal Verification of Backend Systems with LLMs](https://mlsanity.com/paper/2506.10998/) (2025)
- [ParaVul: A Parallel Large Language Model and Retrieval-Augmented Framework for Smart Contract Vulnerability Detection](https://mlsanity.com/paper/2510.17919/) (2025)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)
- [Hallucination-Resistant Security Planning with a Large Language Model](https://mlsanity.com/paper/2602.05279/) (2026)
- [Knowdit: Agentic Smart Contract Vulnerability Detection with Auditing Knowledge Summarization](https://mlsanity.com/paper/2603.26270/) (2026)
- [Crypto x AI, AI x Crypto: A Survey](https://mlsanity.com/paper/2606.13892/) (2026)
- [IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus](https://mlsanity.com/paper/2606.18098/) (2026)
- [Rethinking and Exploring String-Based Malware Family Classification in the Era of LLMs and RAG](https://mlsanity.com/paper/2507.04055/) (2025)
- [LLMs as verification oracles for Solidity](https://mlsanity.com/paper/2509.19153/) (2025)

## Abstract (arXiv)

With recent advances in large language models (LLMs), this paper explores the potential of leveraging state-of-the-art LLMs,such as GPT-4, to transfer existing human-written properties (e.g.,those from Certora auditing reports) and automatically generate customized properties for unknown code. To this end, we embed existing properties into a vector database and retrieve a reference property for LLM-based in-context learning to generate a new property for a given code. While this basic process is relatively straightforward, ensuring that the generated properties are (i) compilable, (ii) appropriate, and (iii) verifiable presents challenges. To address (i), we use the compilation and static analysis feedback as an external oracle to guide LLMs in iteratively revising the generated properties. For (ii), we consider multiple dimensions of similarity to rank the properties and employ a weighted algorithm to identify the top-K properties as the final result. For (iii), we design a dedicated prover to formally verify the correctness of the generated properties. We have implemented these strategies into a novel LLM-based property generation tool called PropertyGPT. Our experiments show that PropertyGPT can generate comprehensive and high-quality properties, achieving an 80% recall compared to the ground truth. It successfully detected 26 CVEs/attack incidents out of 37 tested and also uncovered 12 zero-day vulnerabilities, leading to 8,256 in bug bounty rewards.