Extending SmartScan: Multi-Language Support and Scalable Formal Verification for Smart Contracts

Abstract

Smart contracts are self-executing programs deployed on blockchain networks, automating trust-based operations in decentralized applications (DApps). At the same time, their transparency and immutability offer significant advantages; these characteristics make them vulnerable to security flaws that, once deployed, cannot be rectified without substantial consequences. Existing verification tools such as Mythril, Slither, Oyente, and Zeus primarily target Solidity contracts using static or symbolic analysis. However, they fall short in supporting diverse blockchain languages like Rust (used in Solana), Michelson (Tezos), and Move (Aptos/Sui). Additionally, these tools lack formal specification using temporal logic, provide limited scalability for large and complex contracts, and often yield high false favorable rates. This paper presents an enhanced SmartScan framework for formally verifying smart contracts across multiple blockchain ecosystems to address these gaps. The framework introduces language-specific parsers and FSM/BIP model generation pipelines for Solidity, Vyper, Rust, Michelson, and Move. These models are translated into SMV format for symbolic model checking using nuXmv. The proposed algorithms incorporate CTL-based specifications to verify key properties such as fund safety, reentrancy prevention, access control compliance, and arithmetic safety. Scalability is achieved through symbolic abstraction, partial-order reduction, and multi-threaded execution, with optional support for distributed verification using cloud platforms. Experimental evaluation on diverse real-world contracts demonstrated a verification accuracy of over 94%, a 40–50% reduction in FSM states after optimization, and speedups of up to 3.2× with parallel execution. The case study on a cross-chain DeFi contract confirmed consistent vulnerability detection across all supported languages. The proposed framework offers a scalable, secure, and language-agnostic solution for trustworthy, intelligent contract verification.