Pith. sign in

REVIEW 11 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
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). Sign in to comment.

Forward citations

Cited by 11 Pith papers

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

  1. From Exploration to Specification: LLM-Based Property Generation for Mobile App Testing

    cs.SE 2026-04 unverdicted novelty 7.0 of 10

    PropGen automates property generation for Android app testing via LLM synthesis from guided exploration and feedback refinement, yielding 912 valid properties and 25 previously unknown bugs across 12 apps.

  2. 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 ...

  3. 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.

  4. Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming

    cs.SE 2026-07 unverdicted novelty 6.0 of 10

    VLP adds an NL documentation layer with trace-linked mismatch detection and derived formal checks to make human validation of LLM code feasible, lifting pass@1 from 28.7-73.2% to 65.4-93.5%.

  5. SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification

    cs.SE 2026-04 unverdicted novelty 6.0 of 10

    SpecSyn generates formal specifications with over 90% precision and 75% recall, successfully verifying 1071 out of 1365 target properties on open-source programs.

  6. 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...

  7. 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.

  8. V2E: Validating Smart Contract Vulnerabilities through Profit-driven Exploit Generation and Execution

    cs.SE 2026-04 unverdicted novelty 5.0 of 10

    V2E automates PoC generation, triggerability and profitability validation, and iterative refinement using LLMs to confirm exploitable smart contract vulnerabilities, outperforming baselines on 264 labeled contracts.

  9. 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.

  10. 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.

  11. IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus

    cs.AI 2026-06 unverdicted novelty 4.0 of 10

    Improved IsabeLLM adds RAG, error tracing, and Isabelle compatibility updates and is tested on verifying Bitcoin Proof of Work consensus.

Pith tools