SECURIFY is a scalable, automated security analyzer for Ethereum smart contracts that can prove contract behaviors as safe or unsafe with respect to given properties. It uses symbolic analysis of the contract's dependency graph to extract semantic information and checks compliance and violation patterns that capture sufficient conditions for proving properties. SECURIFY is publicly available and has analyzed over 18,000 contracts, regularly used for security audits. It effectively proves the correctness of smart contracts and discovers critical violations. The system uses a domain-specific language (DSL) to define patterns, enabling extensibility. SECURIFY reduces manual effort by automatically classifying violations and warnings, and it reports all unsafe behaviors. It has been used to perform 38 detailed commercial audits of smart contracts. SECURIFY's approach uses semantic facts inferred from the code to check compliance and violation patterns, which are more amenable to automated reasoning than the properties themselves. The system is designed to handle the Turing-completeness of the programming language by focusing on domain-specific properties. SECURIFY's main contributions include a decompiler that symbolically encodes the dependency graph in Datalog, a set of compliance and violation patterns, an end-to-end implementation, and an extensive evaluation showing its effectiveness in proving contract correctness and discovering violations. The system addresses key challenges in smart contract security, including the difficulty of verifying arbitrary properties and the need for precise, scalable analysis. SECURIFY's approach is based on the observation that violations of security properties often violate simpler properties, making them easier to detect. The system uses stratified Datalog to infer semantic facts and check patterns, enabling efficient analysis. It has been applied to real-world examples, such as the Parity wallet vulnerability and the frozen funds issue, demonstrating its effectiveness in identifying critical security issues.SECURIFY is a scalable, automated security analyzer for Ethereum smart contracts that can prove contract behaviors as safe or unsafe with respect to given properties. It uses symbolic analysis of the contract's dependency graph to extract semantic information and checks compliance and violation patterns that capture sufficient conditions for proving properties. SECURIFY is publicly available and has analyzed over 18,000 contracts, regularly used for security audits. It effectively proves the correctness of smart contracts and discovers critical violations. The system uses a domain-specific language (DSL) to define patterns, enabling extensibility. SECURIFY reduces manual effort by automatically classifying violations and warnings, and it reports all unsafe behaviors. It has been used to perform 38 detailed commercial audits of smart contracts. SECURIFY's approach uses semantic facts inferred from the code to check compliance and violation patterns, which are more amenable to automated reasoning than the properties themselves. The system is designed to handle the Turing-completeness of the programming language by focusing on domain-specific properties. SECURIFY's main contributions include a decompiler that symbolically encodes the dependency graph in Datalog, a set of compliance and violation patterns, an end-to-end implementation, and an extensive evaluation showing its effectiveness in proving contract correctness and discovering violations. The system addresses key challenges in smart contract security, including the difficulty of verifying arbitrary properties and the need for precise, scalable analysis. SECURIFY's approach is based on the observation that violations of security properties often violate simpler properties, making them easier to detect. The system uses stratified Datalog to infer semantic facts and check patterns, enabling efficient analysis. It has been applied to real-world examples, such as the Parity wallet vulnerability and the frozen funds issue, demonstrating its effectiveness in identifying critical security issues.