Formally Verifying a Real World Smart Contract

TL;DR

This paper discusses the importance of formal verification for real-world smart contracts written in Solidity, emphasizing the need for higher certainty due to financial risks and the search for effective verification tools.

Contribution

It presents an investigation into tools capable of formally verifying a recent Solidity smart contract, addressing the challenge of ensuring correctness in critical financial applications.

Findings

Identified challenges in verifying Solidity smart contracts.

Evaluated existing formal verification tools for smart contracts.

Highlighted the need for improved verification methods.

Abstract

Nowadays, smart contracts have become increasingly popular and, as with software development in general, testing is the standard method for verifying their correctness. However, smart contracts require a higher level of certainty regarding correctness because they are diffcult to modify once deployed and errors can result in significant financial losses. Therefore, formal verification is essential. In this article, we present our search for a tool capable of formally verifying a real-world smart contract written in a recent version of Solidity.