2vyper
2vyper is an automated verifier for Ethereum smart contracts written in the external pageVyper, based on the Viper verification infrastructure.
It offers novel specification construct which enable sound and precise verification even in the presence of unlimited re-entrancy. 2vyper can modularly verify applications consisting of multiple collaborating smart contracts, that is, it verifies each contract independently using only an interface description of the other involved contracts, without requiring their source code. Additionally, it offers a novel verification technique that allows specifying the desired contract behavior in terms of resource transactions, which makes specifications more intuitive and can catch typical errors (such as the one that enabled the DAO hack) by default.
2vyper is open source and available on external pageGithub.
Project Members
Publications
- C. Bräm and M. Eilers and P. Müller and R. Sierra and A. J. Summers, Rich Specifications for Ethereum Smart Contract Verification
In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2021. [PDF] [external pagearXiv]
Completed Student Projects
- Christian Bräm, Master's Thesis
Verification of Advanced Properties for Real World Vyper Contracts
- Robin Sierra, Master's Thesis
Verification of Ethereum Smart Contracts Written in Vyper