Wallet Alternating-time Temporal Logic: Towards Reliable Smart Contract Verification

The exponential growth of Decentralized Finance (DeFi) has made the correctness and reli- ability of smart contracts a matter of critical importance. Smart contracts, as autonomous financial programs deployed on blockchains, execute without human intervention or the possi- bility of modification once deployed. Consequently, any design flaw or logical error can lead to irreversible financial loss or systemic failure. This reality underscores the need for formal veri- fication, which provides mathematically rigorous guarantees of correctness through exhaustive reasoning over all possible system behaviors. Traditional model checking techniques and strategic logics such as Alternating-time Tempo- ral Logic (ATL) are insufficient for this task, as they lack the primitives to express and verify liq- uidity properties—guarantees about the ability of users to access and manipulate crypto-assets within a contract based on their wallet balances. In this thesis, we introduce Wallet Alternating- time Temporal Logic (WATL), a novel extension of ATL enriched with wallet predicates and wallet-constrained strategic operators. WATL enables reasoning about agents’ strategies under explicit liquidity constraints, ensuring that actions are not only strategically feasible but also financially executable. We formalize the syntax and semantics of WATL, provide fixed-point characterizations for its model checking algorithm, and implement these within the VITAMIN verification framework. In addition, to address scalability, we propose an abstraction methodology for Wallet Con- current Game Structures (WCGS) based on Meta Agent aggregation: coalition agents are preserved explicitly, while all other agents are collapsed into a single meta-agent with a sum- aggregated wallet. This reduction preserves liquidity-related properties and drastically shrinks the verification space, enabling efficient analysis of systems with hundreds of participants. We illustrate the effectiveness of WATL on canonical smart contract case studies, such as shared energy trading and crowdfunding, demonstrating how liquidity guarantees can be formally spec- ified and automatically verified. Our results show that WATL, implemented in the VITAMIN tool, bridges the gap between multi-agent strategic reasoning and financial correctness, provid- ing a practical step towards the formal verification of smart contracts with liquidity-awareness.