Wallet ATL: Towards Reliable Smart Contract Verification

The exponential growth of Decentralized Finance (DeFi) has underscored the critical need for formal verification methods that can reason about the financial properties of smart contracts. Traditional formal methods such as Alternating-time Temporal Logic (ATL) cannot express liquidity properties-guarantees about users’ ability to access assets based on wallet balances. We introduce Wallet ATL (WATL), an extension of ATL with wallet predicates and financially constrained strategic operators. WATL ensures that actions are both strategically and economically feasible. We formalize the semantics of WATL, provide model checking algorithms within the VITAMIN framework, and address scalability through the Meta-Agent Abstraction, which collapses all non-coalition agents into a single meta-agent with a sum-aggregated wallet. This abstraction preserves liquidity properties while significantly reducing the verification space. Through case studies such as a crowdfunding smart contract, we demonstrate how WATL formally specifies and verifies liquidity guarantees. Our results show that WATL, implemented in the VITAMIN tool, bridges the gap between multi-agent strategic reasoning and financial correctness, providing a practical step towards the formal verification of smart contracts with liquidity-awareness.