VeriChain: A Hybrid Formal Verification Approach Using Control Flow, Symbolic Execution, and Static Analysis for Smart Contract Vulnerability Detection

Abstract

Smart contracts facilitate the trustless and automated execution of agreements on blockchains, however several programming patterns in them (such as re-entrancy, integer overflow/underflow, access control) have led to substantial thefts due to vulnerabilities. Current verification tools (e.g., Mythril, Oyente, and Securify) are essentially based on symbolic execution, taint analysis, and pattern matching with high falsepositives as well as large time cost, poor scalability for complex contracts. This paper develops VeriChain, a hybrid verification framework that combines (i) lexicon/syntax parsing for abstract syntax tree (AST), (ii) Control Flow Graph (CFG) generation for path and dependency representation, (iii) CFG- guided symbolic execution with model checking to search feasible execution paths and (iv) rule-based static analysis towards identifying/characterizing vulnerability patterns. VeriChain was tested on N benchmark smart contracts (including re-entrancy, arithmetic and access-control vulnerabilities) and contrasted with Mythril, Oyente, and Securify. Experiments show that VeriChain enables 98.3% detection accuracy with only 1 false positive (and no false negative in our testing set) and finishes analysis within 2.3 seconds, surpassing state-of-the-art tools in both precision and execution efficiency. VeriChain also outputs a structured security report to categorise detected flaws by severity and to offer developers traces of execution as well as mitigation advice, enabling realistic pre-deployment audit of blockchain smart contract.