Formal Verification Approaches for Solidity-Based Smart Contract Logic Structures

Abstract

Solidity-based smart contracts execute deterministically on decentralized blockchain networks, where deployed logic cannot be modified once on-chain. This immutability creates a strong requirement for correctness and safety prior to deployment. Traditional testing methods are insufficient for capturing the full range of contract execution paths, particularly under adversarial caller inputs and non-sequential transaction ordering conditions. As a result, vulnerabilities such as re-entrancy, timestamp manipulation, arithmetic boundary violations, and access control misconfigurations have historically led to financial loss and state inconsistency. This work presents a formal verification workflow for Solidity contracts that encodes behavioral invariants, preconditions, and postconditions into symbolic and constraint-based representations. Using symbolic execution and SMT-solver reasoning, we evaluate all feasible state transitions and identify counterexample traces that reveal latent logical flaws. A token vesting contract is used as a case study to demonstrate invariant specification, solver-driven vulnerability detection, and corrective refinement of release logic. The results highlight the importance of integrating formal verification techniques into the early stages of smart contract development to ensure reliable and secure decentralized system behavior.