Solvent: liquidity verification of smart contracts

TL;DR

This work tackles liquidity verification for smart contracts, addressing the limitation that existing Solidity tools cannot express or verify properties such as: for certain users $a$, there exists a sequence of at most $m$ actions that $a$ can perform to make $p$ hold. Solvent translates a contract and user-defined liquidity properties into SMT constraints and applies bounded-model checking with predicate abstraction, using back-end solvers like Z3 and cvc5. The key contributions are an automated encoding of a Solidity subset and liquidity properties, a toolchain that produces replayable counterexamples when properties fail, and an empirical evaluation on a real-world contract benchmark that reveals liquidity bugs (e.g., frozen funds). The approach has practical impact by helping developers detect and fix liquidity vulnerabilities before deployment, with potential extensions to generate executable proofs and to broaden Solidity coverage and contract-to-contract semantics.

Abstract

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.