🎓 A1Learner
🔍
0 of 45 lessons completed

Solidity Formal Verification Concepts

Solidity formal verification is the practice of proving a property holds in every reachable state of a contract. A test checks a few states, while a proof covers every state the contract can reach.

Supply always equals the sum of balances

SupplyToken states its property in plain words. The proof checks the property after a mint and after a transfer.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

contract SupplyToken {
    address public owner;
    uint256 public totalSupply;
    mapping(address => uint256) public balances;

    constructor() {
        owner = msg.sender;
    }

    function mint(address to, uint256 amount) public {
        require(msg.sender == owner, "not owner");
        totalSupply += amount;
        balances[to] += amount;
    }

    function transfer(address to, uint256 amount) public {
        require(balances[msg.sender] >= amount, "too much");
        balances[msg.sender] -= amount;
        balances[to] += amount;
    }
}

No account withdraws more than it deposited

NoOverdraftVault states its property in plain words. The proof checks the balance after each step of a deposit and withdrawal sequence.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

contract NoOverdraftVault {
    mapping(address => uint256) public balances;

    function deposit() public payable {
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint256 amount) public {
        require(balances[msg.sender] >= amount, "too much");
        balances[msg.sender] -= amount;
        (bool success, ) = payable(msg.sender).call{value: amount}("");
        require(success, "send failed");
    }
}

The fee never exceeds its cap

CappedFee states its property in plain words. The proof checks the fee after a good set, a stranger set, and an over-cap set.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

contract CappedFee {
    address public owner;
    uint256 public feePercent;

    constructor() {
        owner = msg.sender;
    }

    function setFee(uint256 newFee) public {
        require(msg.sender == owner, "not owner");
        require(newFee <= 10, "fee too high");
        feePercent = newFee;
    }
}

Example

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.30;

contract VerifiedToken {
    address public owner;
    uint256 public totalSupply;
    uint256 public feePercent;
    mapping(address => uint256) public balances;

    constructor() {
        owner = msg.sender;
    }

    function mint(address to, uint256 amount) public {
        require(msg.sender == owner, "not owner");
        totalSupply += amount;
        balances[to] += amount;
    }

    function transfer(address to, uint256 amount) public {
        require(balances[msg.sender] >= amount, "too much");
        balances[msg.sender] -= amount;
        balances[to] += amount;
    }

    function setFee(uint256 newFee) public {
        require(msg.sender == owner, "not owner");
        require(newFee <= 10, "fee too high");
        feePercent = newFee;
    }
}

Key points

  • Property: A property is a plain rule about the contract, like total supply equals the sum of balances.
  • Reachable state: A reachable state is any state the contract can reach through its own functions.
  • Fixed sequence: A fixed sequence is a set order of calls that checks the property after each step.
  • Solver: A solver is a tool that checks a property for every reachable state without running each one.
  • Restatement: A property proven for every state is stronger than a property tested in a few states.

In this example, VerifiedToken holds a supply, a fee percent, and a balance mapping. mint adds to the supply and to one balance together. transfer moves value between two balances without changing the supply. setFee is owner only and rejects any fee above ten percent, and the proof checks all three properties after each step.

Note

No solver runs in this lesson, so the proof here is a fixed sequence that checks the property after each step.

Try it Yourself

Edit the code, then press Run.

Running is simulated · Remix IDE

Exercise

A property says total supply always equals the sum of balances. A test mints 100 tokens and transfers 30. What does the property check after the transfer?