Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts.

翻译：智能合约因其长期存在的安全事件而成为攻击者的诱人目标。当前智能合约验证工具的局限性在于，它们无法有效表达和验证涉及加密资产交换的流动性属性：例如，是否在所有可达状态下，用户都能通过触发一系列交易来提取给定数量的加密资产？我们提出了Solvent工具，旨在验证这类现有Solidity验证工具无法处理的属性。我们通过智能合约的通用基准测试评估了Solvent的有效性和性能。