Abstract
Smart contracts deployed on the Ethereum Virtual Machine (EVM) govern high-value decentralized finance (DeFi) protocols, rendering them prime targets for malicious exploitation. Despite the proliferation of static analysis tools, existing techniques frequently suffer from high false-positive rates or computational intractability when analyzing complex inter-procedural data flows and arithmetic edge cases. In this paper, we introduce a hybrid verification framework that synergizes abstract interpretation with Satisfiability Modulo Theories (SMT) solving to enable scalable and precise vulnerability detection in Solidity source code. Our approach first employs interval and octagon numerical abstract domains to rapidly compute over-approximated variable bounds, prune provably safe execution paths, and isolate suspicious control-flow subgraphs. Subsequently, path conditions and semantic constraints from these reduced subgraphs are translated into first-order logic formulas encoded in the Bitwuzla and Z3 SMT solvers to verify deep semantic invariants, including reentrancy, integer overflow/underflow under varying compiler semantics, and unhandled external call exceptions. We evaluated our prototype on a benchmark suite of 4,250 verified smart contracts alongside historical exploit datasets. The empirical results demonstrate that our dual-phase method achieves a 94.2% detection precision with an 88.6% recall rate, reducing false-positive rates by 41.3% compared to baseline static analyzers while maintaining an average verification latency of under 4.8 seconds per contract. These findings highlight the viability of combining fast abstract domain approximations with constraint solving for automated security auditing in high-assurance blockchain environments.
