Smart Contracts Formal Verification: A Systematic Literature Review

TL;DR

This paper systematically reviews existing methods for formal verification of smart contracts, highlighting current challenges and proposing a new approach based on description logic to improve correctness assurance.

Contribution

It provides a comprehensive survey of verification tools and techniques for smart contracts and introduces an innovative formal verification method using description logic.

Findings

Many smart contracts contain critical errors

Existing verification tools have limitations in coverage and automation

The proposed description logic approach offers a promising alternative

Abstract

Formal verification entails testing software to ensure it operates as specified. Smart contracts are self-executing contracts with the terms of the agreement directly written into lines of code. They run on blockchain platforms and automatically enforce and execute the terms of an agreement when meeting predefined conditions. However, Smart Contracts, as software models, often contain notable errors in their operation or specifications. This observation prompts us to conduct a focused study examining related works published across various sources. These publications detail specifications, verification tools, and relevant experiments. Subsequently, this survey proposes an alternative formal verification based on description logic.