# Debugging Smart Contract's Business Logic Using Symbolic Model-Checking

## TL;DR

This paper introduces a symbolic model-checking approach for verifying the correctness of smart contract business logic, addressing a critical gap left by existing tools that focus only on implementation bugs.

## Contribution

It presents a novel formal verification method for Solidity smart contracts that can verify both state and trace properties, including business logic correctness.

## Key findings

- Detected a non-trivial business logic error in MiniDAO smart contract within seconds
- Demonstrated effectiveness of the approach on real-world smart contract example
- Addresses a significant gap in existing smart contract verification tools

## Abstract

Smart contracts are a special type of programs running inside a blockchain. Immutable and transparent, they provide means to implement fault-tolerant and censorship-resistant services. Unfortunately, its immutability causes a serious challenge of ensuring that a business logic and implementation is correct upfront, before publishing in a blockchain. Several big accidents have indeed shown that users of this technology need special tools to verify smart contract correctness. Existing automated checkers are able to detect only well known implementation bugs, leaving the question of business logic correctness far aside. In this work, we present a symbolic model-checking technique along with a formal specification method for a subset of Solidity programming language that is able to express both state properties and trace properties; the latter constitutes a weak analogy of temporal properties. We evaluate the proposed technique on the MiniDAO smart contract, a young brother of notorious TheDAO. Our Proof-of-Concept was able to detect a non-trivial error in the business logic of this smart contract in a few seconds.