VerX: Smart contract verifier

What is VerX?

VerX is an automated verifier for custom function requirements of Ethereum contracts. VerX takes as input:

  • Ethereum smart contracts, written in Solidity;

  • functional requirements, written in VerX’s specification language;

  • deployment script, which defines how the contracts are initialized and deployed.

Given these inputs, VerX either verifies that the property holds or outputs a sequence of transactions that may result in violating the property.

Why should I use VerX?

The key advantage of VerX is that it is capable to verify custom properties specified by auditors and developers, which makes VerX an indispensable tool when it comes to verifying the functional correctness of contracts. In contrast, remaining automated tools focus on checking generic vulnerabilities, such as reentrancy or buffer overflows. Moreover, VerX provides formal guarantees, unlike tools based on symbolic execution and fuzzing, which provide bounded guarantees. To learn more, watch our introductory talk on VerX from ETHCC.

How does it work?

VerX first initializes the smart contracts based on the provided deployment script. Then, it uses a novel sound abstraction technique to over-approximate the set of reachable states of the smart contracts while maintaining sufficient precision to prove the target requirement. Finally, it either successfully verifies that the requirement holds or identifies a sequence of transactions that may result in violating the property.

Indices and tables