PropertyGPT is an LLM-driven system for formal verification of smart contracts, enabling automated generation of comprehensive properties for unknown code. The system leverages retrieval-augmented property generation, using existing human-written properties from Certora projects to guide LLM-based in-context learning. It generates properties for smart contracts, ensuring they are compilable, appropriate, and runtime-verifiable. PropertyGPT uses a weighted algorithm to rank properties and a dedicated prover to formally verify their correctness. The system was tested on 623 human-written properties from 23 Certora projects, achieving an 80% recall compared to the ground truth. It successfully detected 26 CVEs/attack incidents out of 37 tested and uncovered 12 zero-day vulnerabilities, resulting in $8,256 in bug bounty rewards. PropertyGPT's main contributions include an end-to-end LLM-driven formal verification pipeline, a property specification language (PSL) for smart contracts, and a dedicated prover for property verification. The system was evaluated through extensive experiments and ablation studies, demonstrating its effectiveness in generating comprehensive and high-quality properties. PropertyGPT outperformed existing tools in detecting smart contract vulnerabilities, identifying 9 out of 13 CVEs and 17 out of 24 attack incidents. It also successfully identified zero-day vulnerabilities in real-world projects, generating 22 bug findings, 12 of which were confirmed and fixed. The system's ability to generate and verify properties was validated through a detailed analysis of a vulnerable smart contract function, demonstrating its effectiveness in detecting critical vulnerabilities.PropertyGPT is an LLM-driven system for formal verification of smart contracts, enabling automated generation of comprehensive properties for unknown code. The system leverages retrieval-augmented property generation, using existing human-written properties from Certora projects to guide LLM-based in-context learning. It generates properties for smart contracts, ensuring they are compilable, appropriate, and runtime-verifiable. PropertyGPT uses a weighted algorithm to rank properties and a dedicated prover to formally verify their correctness. The system was tested on 623 human-written properties from 23 Certora projects, achieving an 80% recall compared to the ground truth. It successfully detected 26 CVEs/attack incidents out of 37 tested and uncovered 12 zero-day vulnerabilities, resulting in $8,256 in bug bounty rewards. PropertyGPT's main contributions include an end-to-end LLM-driven formal verification pipeline, a property specification language (PSL) for smart contracts, and a dedicated prover for property verification. The system was evaluated through extensive experiments and ablation studies, demonstrating its effectiveness in generating comprehensive and high-quality properties. PropertyGPT outperformed existing tools in detecting smart contract vulnerabilities, identifying 9 out of 13 CVEs and 17 out of 24 attack incidents. It also successfully identified zero-day vulnerabilities in real-world projects, generating 22 bug findings, 12 of which were confirmed and fixed. The system's ability to generate and verify properties was validated through a detailed analysis of a vulnerable smart contract function, demonstrating its effectiveness in detecting critical vulnerabilities.