Source-linked AI summary
PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, Yang Liu
TL;DR
Automated generation of comprehensive smart-contract properties remains limited, leaving some property types to manual, case-by-case work. PropertyGPT retrieves human-written examples for LLM-based generation, then revises, ranks, and formally verifies candidates. It reports 80% recall against ground-truth properties and findings across tested vulnerabilities and bounty projects.
Problem
Comprehensive automated generation of smart-contract properties remains unmet: prior approaches require historical transactions or generate only invariants, while experts still write properties case by case.
Source: §I · pp. 1–2Method
PropertyGPT retrieves human-written properties from a vector database as in-context examples, then revises candidates using compilation and static-analysis feedback, ranks them, and formally verifies top-K properties.
Source: §I · p. 2Results
80% of equivalent ground-truth properties were covered (64% precision); PropertyGPT detected 9/13 CVEs and 17/24 attack incidents, and 12 bounty findings were confirmed and fixed for $8,256.
Source: §I · p. 2Takeaways & Limitations
PropertyGPT detected vulnerabilities in tested real-world contracts and received $8,256 in vendor bounty rewards for confirmed and fixed findings.
Source: §X · p. 14No automated equivalence checker was available for comparing Certora-style properties with generated PSL-style properties, so authors reviewed equivalence independently.
Source: F. Threats to Validity · p. 13
Abstract
from arXiv · showhide
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.
I. INTRODUCTION
The paper targets the lack of automated, comprehensive smart-contract property generation by adapting human-written examples with LLMs. PropertyGPT retrieves examples, generates and refines properties, ranks them, and verifies selected results.
I. INTRODUCTION
- Automated generation of comprehensive properties remains a gap: earlier approaches require historical transactions, cover only invariants, or leave experts to write properties case by case.The paper notes that this manual work hinders formal verification at scale.Source: §I · pp. 1–2
- PropertyGPT transfers human-written properties to unknown code through retrieval-augmented LLM in-context learning, without error-prone labeling or retraining when data updates.The system also uses compilation and static-analysis feedback to revise candidates, ranks them across similarity dimensions, and formally verifies top-K properties.Source: §I · p. 2
- 80% recall of equivalent ground-truth properties (64% precision); PropertyGPT detected 9/13 CVEs and 17/24 attack incidents, while 12 bounty findings were confirmed and fixed for $8,256.The ground-truth comparison was judged by human experts; the confirmed bounty findings came from four real-world projects.Source: §I · p. 2
II. PRELIMINARY
- The paper uses GPT-4 in-context learning rather than fine-tuning, drawing on existing properties as examples for generation.In-context learning uses examples in the task context to learn a task.Source: §II · p. 2
III. PROPERTYGPT OVERVIEW
- PropertyGPT embeds critical reference code, retrieves associated properties, generates and compiles candidates, ranks the top-K, and sends them to its prover.The system takes subject smart-contract code as input and produces properties with verification results.Source: §III · pp. 2–3
IV. PROPERTY SPECIFICATION LANGUAGE
The paper introduces PSL as a Solidity-like language for specifying smart-contract properties, then describes retrieval-augmented generation, compilation-driven revision, and ranking of candidate properties.
IV. PROPERTY SPECIFICATION LANGUAGE
- PSL extends Solidity with invariants over state, function pre/postconditions, and scenario-based rules under restricted environments; the current prototype supports safety properties, not liveness.The authors describe PSL specifications as easier to write or maintain than CVL and suitable for a self-contained pipeline.Source: §IV · p. 3
V. PROPERTY GENERATION AND REFINEMENT
- PropertyGPT transfers existing human-written properties to generate PSL properties, revises compilation errors using feedback, and ranks compilable candidates with a weighted algorithm for top-K selection.The reference properties need not themselves be written in PSL.Source: §V · pp. 3–4
A. Retrieval-Augmented Property Generation
- The system embeds critical code rather than reference-property text, retrieves associated properties by code similarity, and uses each as a one-shot example for function conditions or cross-function rules.The retrieved property type determines which generation prompt is used.Source: A. Retrieval-Augmented Property… · pp. 4–5
B. Revising Property to Fix Compilation Errors
PropertyGPT iteratively revises properties using compiler feedback, then statically checks compilable properties for target-function execution. A special prompt addresses missing core-function execution, while revision attempts are capped.
B. Revising Property to Fix Compilation Errors
- The PSL compiler provides error locations and reasons, which guide iterative LLM revision until compilation succeeds or the attempt limit is reached.The process uses compiler and static-checking feedback as an external oracle.Source: B. Revising Property to Fix… · p. 5
- 84% of properties were successfully revised within five attempts; 74% compiled with no revisions (63%) or with only one attempt.The maximum-attempt threshold avoids an endless loop.Source: B. Revising Property to Fix… · p. 5
- Compiler success alone is insufficient: static checking catches compilable properties that omit execution of the target subject function.Such a property would be meaningless.Source: B. Revising Property to Fix… · p. 5
- A special revision prompt targets missing core-function execution, aiming to make properties functionally meaningful as well as grammatically correct.The prompt identifies the missing function and includes the contract code.Source: B. Revising Property to Fix… · p. 6
C. Ranking the Top-K Appropriate Properties
PropertyGPT ranks generated properties using weighted code and property similarities, then uses a dedicated prover to check their formal specifications.
C. Ranking the Top-K Appropriate Properties
- Four embedding-based metrics compare raw code, code summaries, raw properties, and high-level property summaries.The algorithm combines these dimensions in a weighted score.Source: C. Ranking the Top-K Appropriate… · p. 6
- High-level natural-language summaries address variation among code with the same functionality and properties with the same semantics.LLMs produce summaries for code and properties.Source: C. Ranking the Top-K Appropriate… · p. 6
- The tuned coefficients were α: 0.134, β: 0.556, γ: 0.141, and η: 0.168, selected using 3,622 generated properties.A linear regression model approximated the actual property score.Source: C. Ranking the Top-K Appropriate… · p. 6
- Properties are ranked by descending score, with higher-ranked properties considered more likely to be important for the prover to verify.Source: C. Ranking the Top-K Appropriate… · p. 6
VI. PROPERTY VERIFICATION
- The prover applies forward symbolic execution and modular verification to PSL specifications, using bounded model checking to assess whether violations persist during execution.Counterexamples support concluding that a property fails, indicating a vulnerability that requires further manual verification.Source: §VI · p. 6, Figure 7 · p. 6
A. Modeling Smart Contract Execution
The paper models smart-contract execution using contract states and transaction information, then verifies properties through source-level symbolic execution. Its verification pipeline combines compiler-aligned semantics with over-approximation, modular verification, and bounded model checking.
A. Modeling Smart Contract Execution
- Unexpected transaction behavior reverts the transaction and leaves contract state unchanged; the analysis excludes reversion because it generally does not threaten safety.Reversion may affect availability, for example through denial of service.Source: A. Modeling Smart Contract Execution · p. 7
B. Verification Technique
- The symbolic executor follows Solidity compiler practices for complex expressions and inheritance, including left-to-right evaluation and resolving polymorphic calls.It uses comprehensive small-step semantics to conduct strongest-postcondition analysis of Solidity contracts.Source: B. Verification Technique · p. 7
- Unknown on-chain calls are assumed to succeed with symbolic return data, while uninterpreted functions model non-linear operations such as sha3.These are over-approximations for behaviors that are difficult to model precisely or fall beyond the research scope.Source: B. Verification Technique · p. 7
- Modular verification makes state variables symbolic; if a property is not thereby established, bounded model checking searches feasible states for counterexamples.The default bound is three, with up to five loop iterations for non-terminated execution.Source: B. Verification Technique · p. 7
VII. IMPLEMENTATION AND SETUP
- PropertyGPT comprises about 3K lines of Python for generation and 38K lines of C++ for grammar support and PSL verification.A converter maps Solidity 0.6.x and 0.7.x contracts into ASTs compatible with Solidity 0.8.x; Z3 4.11.2 discharges symbolic constraints.Source: §VII · p. 7
A. Property Knowledge Collection
- The knowledge base contains 623 human-written properties from 23 Certora projects, collected from 61 audit reports published from 2019 to 2023.All available properties for the selected projects were collected, whether violated or non-violated in their audits.Source: A. Property Knowledge Collection · p. 7
- Embedding-similarity clustering yielded six property clusters, with overlap especially between clusters #3 and #5.The authors further investigated the clusters to classify the collected properties.Source: A. Property Knowledge Collection · pp. 7–8
B. Experimental Setup
The evaluation uses GPT-4-turbo and embedding similarities to generate properties and test vulnerability detection. It evaluates property generation against human-written properties and vulnerability detection on curated attack incidents and CVEs.
B. Experimental Setup
- The experiments used GPT-4-turbo via gpt-4-0125-preview and text-embedding-ada-002, with property-revision attempts capped at nine.Experiments ran in Docker on Ubuntu 20.04 with an Intel Core Xeon 2.2 GHz processor and 2GB RAM.Source: B. Experimental Setup · p. 8
VIII. EVALUATION
- 90 ground-truth properties from nine Certora projects formed the property-generation test set, with remaining projects serving as the knowledge base.PropertyGPT extracts each subject function and queries the knowledge base for in-context learning.Source: §VIII · p. 8
- 24 curated attack incidents and 13 randomly selected CVEs of different types were used to evaluate vulnerability detection.The incident benchmark was curated from SmartInv's benchmark after reviewing duplicates, missing exploits, unavailable source code, incomplete code, and attack types impractical for simple invariant properties.Source: §VIII · p. 9
A. RQ1: Property Generation
PropertyGPT’s property-generation evaluation found 0.80 recall and 0.64 precision against human-written ground truth. In vulnerability detection, it identified 9 of 13 CVEs and 17 of 24 attack incidents, with runtime-context support and reference-property coverage limiting some cases.
A. RQ1: Property Generation
- 0.80 recall, 0.64 precision, and 0.71 F1-score were achieved on 90 ground-truth properties from nine Certora projects.Two experienced authors independently judged equivalence across CVL and PSL, with a third resolving disagreements; 26 of 42 generated properties were true positives and 8 of 10 ground-truth properties were hit.Source: A. RQ1: Property Generation · p. 9, Table III · p. 10
- PropertyGPT’s 11 of 16 false positives for opyn_gamma_protocol were valid properties absent from Certora’s ground truth.OpenZeppelin had the lowest recall and F1-score, which the authors attribute to scarce reliable reference properties because client code rarely reimplements its foundational functionality.Source: A. RQ1: Property Generation · p. 9
B. RQ2: Vulnerability Detection
- 9 of 13 CVEs and 17 of 24 attack incidents were detected by PropertyGPT.It outperformed the compared tools on the CVE set; the attack-incident comparison was qualitative because SmartInv’s instrumented code, ground truth, and raw results were unavailable.Source: Table IV · p. 10, B. RQ2: Vulnerability Detection · pp. 10–11, Table V · p. 10
- PropertyGPT missed four CVEs, including a misuse-of-access-control case that was difficult to distinguish from missing access control.The authors also note that Certora’s studied properties seem to lack access-control support, potentially limiting detection of other access-control vulnerabilities.Source: B. RQ2: Vulnerability Detection · p. 10
- PropertyGPT does not support smart-contract runtime context, which may matter for particular use cases such as deflationary-token abuse.The authors identify this as a root cause among seven undetected projects and leave runtime-context support for future work.Source: B. RQ2: Vulnerability Detection · p. 11
C. RQ3: Generalizability Measurement
PropertyGPT’s indirect similarity measure indicated generalizability to a dataset different from its Certora-derived knowledge base. The influencing-factor study found top-2 retrieval balanced precision and recall, while compiler feedback enabled most generated properties to be repaired within five attempts.
C. RQ3: Generalizability Measurement
- Code similarity averaged cosine similarity and Word Mover’s Distance to indirectly assess transfer-learning generalizability.Lower similarity between tested and retrieved reference code was treated as indicating stronger generalizability.Source: C. RQ3: Generalizability Measurement · p. 11
- 0.68 mean code similarity for 26 successful cases and 0.67 for 11 failed cases supported sufficient generalizability to an entirely different dataset.The authors interpret the small difference between failed and successful cases as evidence that failures were not due to lack of generalizability.Source: C. RQ3: Generalizability Measurement · p. 11
D. RQ4: Influencing Factors
- Top-2 retrieval increased all three metrics over top-1, with precision rising only slightly from 0.64 to 0.65.The authors recommend top-2 properties for efficiency; precision later declined and fluctuated around 0.60 as K increased.Source: Figure 9 · p. 11, D. RQ4: Influencing Factors · p. 11
- 87% success rate was achieved with PropertyGPT’s property repair, versus 63% without revision or repair.Most compilable properties (84%) required no more than five fix attempts; undeclared variables were the main compiler error among 49 properties that remained unfixed.Source: Table VI · p. 11, D. RQ4: Influencing Factors · p. 11
E. RQ5: Real-world Impact
Across four real-world bounty projects, PropertyGPT generated 22 bug findings, 12 of which were confirmed and fixed, earning $8,256 in rewards. Two case studies show generated properties exposing a fee-withdrawal accounting flaw and an envelope-overwrite flaw.
E. RQ5: Real-world Impact
- 12 of 22 bug findings across four bounty projects were confirmed and fixed, yielding $8,256 in vendor rewards.The authors omit the project sources of the two detailed cases to respect anonymity.Source: E. RQ5: Real-world Impact · p. 12
- A generated postcondition exposed that withdrawForwardFee could allow a validator to withdraw more than its allocated forwarding-fee share.The function checked withdrawals against total collected fees, not each validator’s proportionate entitlement; the generated postcondition failed.Source: E. RQ5: Real-world Impact · p. 12
- A generated property detected that addEnvelope could overwrite an existing envelope because the function did not enforce envelope-id uniqueness.The property checked that the same id did not previously exist and that the stored creator matched the caller; the assertion failed on the vulnerable function.Source: E. RQ5: Real-world Impact · p. 13
F. Threats to Validity
The section identifies limits in the equivalence assessment of generated properties and in how broadly vulnerability-detection findings may generalize.
Internal Validity
- Certora-style and PSL-style properties lack an automated equivalence checker, so three authors independently reviewed them.The evaluation used an established Certora property dataset, and the authors released the generated properties and equivalence labels.Source: F. Threats to Validity · p. 13
External Validity
- Findings may not generalize beyond the evaluated contract types and vulnerability types.The evaluation covered 13 representative CVEs and 24 real-world victim projects; 12 of 24 generated findings for high-profile projects were confirmed and fixed.Source: F. Threats to Validity · p. 13
IX. RELATED WORK
Related work spans automated vulnerability detection, property generation, and LLM-based security tools; PropertyGPT combines LLM-based property generation with a source-level symbolic-execution prover. The conclusion presents retrieval-augmented generation as a practical vulnerability-detection technique and identifies richer contract context and property knowledge as future work.
IX. RELATED WORK
- Prior vulnerability analysis includes static pattern-based tools, fuzzers, symbolic execution, and semi-automated verification requiring user-supplied properties.The passage contrasts fuzzers’ higher precision and lower recall with static analyses.Source: §IX · p. 13
- PropertyGPT pairs LLM-based property generation with a source code-level symbolic-execution prover to support detection of a wide range of contract vulnerabilities.The conclusion describes retrieval-augmented generation using LLMs’ in-context learning and reports $8,256 in bounty rewards from real-world vulnerability findings.Source: §IX · p. 13, §X · p. 14
- Earlier property-generation methods target restricted property types or require annotations or transaction histories; PropertyGPT instead uses in-context learning and generates beyond function pre- and postconditions.Cider generates likely invariants, while PropertyGPT verifies generated properties with a prover; SmartInv and PropertyGPT both use LLMs, but SmartInv uses fine-tuning.Source: §IX · p. 13
- LLMs have also been applied to vulnerability detection, fuzzing, protocol analysis, and program repair.The cited examples include GPTScan, TitanFuzz, FuzzGPT, ChatAFL, ACFix, and ChatRepair [63].Source: §IX · pp. 13–14
X. CONCLUSION
- The authors plan to add contract context such as documentation and enrich PropertyGPT’s property knowledge from additional sources.They present the approach as practical for vulnerability detection, reporting $8,256 in bounty rewards.Source: §X · p. 14
APPENDIX
The appendix contrasts CVL’s low-level specification demands with PSL’s Solidity-like approach, describes PSL compiler support, and reports how a regression model ranks generated properties.
B. An Example of CVL
- CVL specifies ERC20Votes checkpoint updates with low-level storage details, while PSL follows Solidity semantics without requiring users to know verification internals.The CVL example states that casting votes updates recorded votes, recalculates total votes, and updates the checkpoint array’s last index.Source: B. An Example of CVL · p. 16, Figure 15 · p. 16
C. Compilation Phase of PSL Specifications
- PSL modifies Solidity compiler v0.8.17 with invariant, rule, precondition, postcondition, and assume constructs, then checks specification syntax.The compiler also restricts invariant, precondition, and postcondition specifications to expression statements.Source: C. Compilation Phase of PSL… · p. 16
D. Learning Optimal Coefficients via Training a Linear Regression Model
- 3,622 generation records were used to train an OLS model that approximates known-property similarity scores from four features.Using fewer features lowered performance metrics, leading the authors to use the four-feature combination for ranking.Source: D. Learning Optimal Coefficients via… · p. 16
- An Ordinary Least Squares (OLS) linear regression model was trained to learn coefficients for ranking top-k appropriate properties; reported performance was MAE 0.0239, MSE 0.0008, RMSE 0.0291, R2 0.1294, MAPE 2.7810, and MDE -0.0022.Source: D. Learning Optimal Coefficients via… · p. 16