SECURIFY is a security analyzer for Ethereum smart contracts designed to address the recurring security concerns in smart contract handling of billions of USD. It is scalable, fully automated, and capable of proving contract behaviors as safe or unsafe with respect to given properties. The analysis process involves two steps: symbolically analyzing the contract's dependency graph to extract semantic information and checking compliance and violation patterns to determine if a property holds. SECURIFY uses a domain-specific language (DSL) to specify patterns, enabling extensibility. The system has analyzed over 18,000 contracts and is regularly used for security audits. An extensive evaluation demonstrates its effectiveness in proving correctness and discovering critical violations. Key contributions include a decompiler, a set of compliance and violation patterns, and an end-to-end implementation. The system reduces manual effort by automatically classifying definite violations and reporting all unsafe behaviors. SECURIFY is publicly available and has been used in detailed commercial audits, improving its design and implementation.SECURIFY is a security analyzer for Ethereum smart contracts designed to address the recurring security concerns in smart contract handling of billions of USD. It is scalable, fully automated, and capable of proving contract behaviors as safe or unsafe with respect to given properties. The analysis process involves two steps: symbolically analyzing the contract's dependency graph to extract semantic information and checking compliance and violation patterns to determine if a property holds. SECURIFY uses a domain-specific language (DSL) to specify patterns, enabling extensibility. The system has analyzed over 18,000 contracts and is regularly used for security audits. An extensive evaluation demonstrates its effectiveness in proving correctness and discovering critical violations. Key contributions include a decompiler, a set of compliance and violation patterns, and an end-to-end implementation. The system reduces manual effort by automatically classifying definite violations and reporting all unsafe behaviors. SECURIFY is publicly available and has been used in detailed commercial audits, improving its design and implementation.