Invariant-Based Verification of Smart Contract Upgrade Safety on Ethereum

Smart contract upgradeability is widely used in Ethereum to enable postdeployment fixes and feature evolution. However, upgrades can unintentionally violate safety assumptions, leading to storage corruption, interface inconsistencies, access-control regressions, and unsafe execution behavior. Existing analysis tools primarily focus on single-version vulnerabilities and offer limited support for reasoning about correctness across contract upgrades. This paper presents an invariant-based verification approach for smart contract upgrade safety on Ethereum. We formalize the upgrade safety using a set of cross-version invariants and define a global safe-state model that characterizes valid upgrade transitions. Based on this model, we design an automated verification framework that statically analyzes proxy-based upgrade patterns and detects violations related to storage layout evolution, ABI compatibility, initialization safety, delegatecall usage, and access-control preservation. The framework compares compiler-level artifacts from successive contract versions and supports modular, extensible detectors.