Revisiting Formal Verification in VeriSolid: An Analysis and Enhancements

While the immutability of smart contracts ensures unparalleled trust and transparency, it is also a doubleedged sword, as any coding errors can lead to substantial financial losses and complex mitigation endeavours. VeriSolid is a security mitigation tool that offers a ‘correct by design’ platform, enabling developers to create and verify smart contracts using predefined property templates. After ensuring the correctness of the design, VeriSolid facilitates the automatic generation of equivalent Solidity code. Our motivational example is a prominent decentralized exchange (DEX), Uniswap, which is responsible for over 82% of DEX transactions. Our experiments uncover and resolve verification issues in two out of four VeriSolid templates. Additionally, we propose seven new templates, enhancing the VeriSolid platform through its open-source project. This research endeavor has yielded a significant enhancement in VeriSolid’s coverage percentage, which represents the percentage of available software requirement specifications that can be formally represented and verified in VeriSolid. This study increased it from 45.6% to 90.5% based on a dataset consisting of 555 requirement specifications, thus enabling the verification of a wider range of property specifications.