angeloferrando/solvent repository overview

A tool to formally verify smart contracts through SMT solvers.

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.

Docker image of Solvent ready to be executed on custom smart contracts, or on the available benchmarks.