PropertyGPT is an innovative system that leverages large language models (LLMs) to automate the generation of comprehensive properties for smart contracts, enhancing formal verification. The system addresses the challenge of generating invariants, pre-/post-conditions, and rules for smart contracts, which are crucial for security and reliability. PropertyGPT uses a vector database to store existing human-written properties, enabling LLMs to retrieve and generate new properties through in-context learning. The system ensures that the generated properties are compilable, appropriate, and runtime-verifiable by employing compilation feedback, a weighted algorithm for ranking properties, and a dedicated prover for formal verification. Experiments with 623 human-written properties from 23 Certora projects show that PropertyGPT achieves an 80% recall rate and successfully detects 26 CVEs/attack incidents, earning $8,256 in bug bounty rewards. The system's effectiveness is demonstrated through its ability to identify zero-day vulnerabilities in real-world projects, highlighting its potential for practical application in smart contract security.PropertyGPT is an innovative system that leverages large language models (LLMs) to automate the generation of comprehensive properties for smart contracts, enhancing formal verification. The system addresses the challenge of generating invariants, pre-/post-conditions, and rules for smart contracts, which are crucial for security and reliability. PropertyGPT uses a vector database to store existing human-written properties, enabling LLMs to retrieve and generate new properties through in-context learning. The system ensures that the generated properties are compilable, appropriate, and runtime-verifiable by employing compilation feedback, a weighted algorithm for ranking properties, and a dedicated prover for formal verification. Experiments with 623 human-written properties from 23 Certora projects show that PropertyGPT achieves an 80% recall rate and successfully detects 26 CVEs/attack incidents, earning $8,256 in bug bounty rewards. The system's effectiveness is demonstrated through its ability to identify zero-day vulnerabilities in real-world projects, highlighting its potential for practical application in smart contract security.