# Solvent: liquidity verification of smart contracts

arXiv: https://arxiv.org/abs/2404.17864 · HTML: https://mlsanity.com/paper/2404.17864/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Apr 2024.

## Built on by (most cited first, 1 of 1)

- [LLMs as verification oracles for Solidity](https://mlsanity.com/paper/2509.19153/) (2025)

## Abstract (arXiv)

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.