Model Checking and Runtime Verification of Decentralized Smart Contract Interactions

Abstract

Ensuring the correctness, safety, and reliability of interacting smart contracts across decentralized blockchain platforms remains a persistent challenge due to composability risks, non-deterministic execution environments, and implicit inter-contract dependencies. This paper proposes a hybrid verification framework that integrates model checking with runtime verification to validate communication and behavioral properties in decentralized smart contract ecosystems. The framework employs Linear Temporal Logic (LTL) to specify safety and liveness constraints across token exchange, oracle-based communication, and governance-related contract interactions. Property-based testing and symbolic execution are incorporated to capture hidden state transitions, detect inconsistencies, and validate edge-case behaviors. The proposed methodology is implemented and evaluated using Ethereum smart contracts conforming to ERC-20 and ERC-721 token standards. Experimental analyses demonstrate the framework’s effectiveness in identifying misbehaviors such as inconsistent states, reentrancy-triggered state violations, improper oracle updates, and potential contract deadlocks. Results also show that combining formal verification with runtime monitoring significantly enhances behavioral robustness and reduces vulnerability exposure during decentralized execution. The proposed hybrid verification model offers a scalable and extensible approach for improving trustworthiness and correctness in multi-contract blockchain applications.