Pith. sign in

REVIEW 8 cited by

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2405.02580 v2 pith:VZHEKXTY submitted 2024-05-04 cs.SE cs.AI

Ye Liu , Yue Xue , Daoyuan Wu , Yuqiang Sun , Yi Li , Miaolei Shi , Yang Liu This is my paper · ORCID
classification cs.SEcs.AI
keywords propertiespropertygenerategeneratedllmspropertygptcodeexisting
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
abstract

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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 8 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis

    cs.SE 2026-07 conditional novelty 6.0 of 10

    VeriSynth synthesizes executable Z3 verification models from zkEVM Rust source via LLM-guided translation with solver-backed checking, detecting 91.6% of 95 injected opcode bugs versus 46.3% for a direct LLM baseline ...

  2. TrapHunter: Exposing Covert Pathways in Trap Token Contracts

    cs.SE 2026-07 conditional novelty 6.0 of 10

    TrapHunter detects six categories of malicious ERC-20 'trap token' logic by combining Abstract Behavior Trees, Augmented Path Graphs, LLM intent reasoning, and fork-based validation, reaching 81.8% precision / 85.4% recall.

  3. Knowdit: Agentic Smart Contract Vulnerability Detection with Auditing Knowledge Summarization

    cs.CR 2026-03 conditional novelty 6.0 of 10

    Knowdit links abstract DeFi semantics to vulnerability patterns in a knowledge graph and drives an agentic specify–harness–fuzz–reflect loop that finds all high-severity and most medium-severity bugs on held-out Code4...

  4. TraceLLM: Security Diagnosis Through Traces and Smart Contracts in Ethereum

    cs.CR 2025-09 conditional novelty 6.0 of 10

    TraceLLM automatically generates human-readable security reports for Ethereum hacks by feeding LLMs a mix of execution traces, decompiled code, and balance changes.

  5. Do AI models help produce verified bug fixes?

    cs.SE 2025-07 conditional novelty 6.0 of 10

    Programmers with LLM access solved fewer formally verified debugging tasks than a no-AI control group, though complete novices and strong language experts gained some benefit.

  6. RISKTAGGER: Evidence-Guided LLM Agent for Post-Incident Forensic Analysis of Money Laundering in Web3

    cs.CR 2025-10 conditional novelty 5.0 of 10

    An LLM-driven agent automatically extracts clues from incident reports, traces laundering paths on-chain, and labels accounts as high/medium/low risk, with evaluation on the Bybit hack.

  7. A Systematic Classification of Vulnerabilities in MoveEVM Smart Contracts (MWC)

    cs.CR 2025-05 reject novelty 5.0 of 10

    The paper introduces the MoveEVM Weakness Classification (MWC), a 37-code, six-frame taxonomy for Move-EVM hybrid smart contract vulnerabilities, but its empirical validation and internal consistency are lacking.

  8. Towards LLM-assisted High-Quality Property Generation for Solidity Smart Contracts

    cs.SE 2026-07 conditional novelty 4.0 of 10

    LLM-generated Solidity test properties catch most of the mutants that human-written properties catch on average, and match human quality on the LibBit contract.

Pith tools