A prominent functionality of smart contracts is regulating financial transactions on the blockchain. Flaws in a smart contract could cause funds to be frozen in the contract, resulting in financial losses of honest users. This issue of frozen funds is often considered a violation of liquidity requirements. In this work, we propose a liquidity property for account-based blockchain platforms such as Ethereum. The property captures the situation where the process of claiming funds by the honest users can be disrupted by the strategy of the environment. We formally establish the connection between this property and a strategy-less notion of liquidity under particular conditions, devise sound proof methods for the property, mechanize the theories and proof methods in the Rocq prover, and apply the proof methods to verify or refute the property for example smart contracts. Informative verification and refutation results are obtained for the examples—strategies help reveal how a user may act to ensure the transfer of funds out of a contract or how an attacker may exploit the inherent vulnerabilities of a contract to freeze funds.