Your first specification

Vault records a balance for each address. deposit adds to the caller's balance and withdraw subtracts from it. To keep the focus on specifications, this vault only keeps records; it does not move tokens.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

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

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

    function deposit(uint256 amount) external {
        balances[msg.sender] += amount;
    }

    function withdraw(uint256 amount) external returns (uint256) {
        require(amount <= balances[msg.sender], "insufficient balance");
        balances[msg.sender] -= amount;
        return balances[msg.sender];
    }
}

1. A successful withdrawal reduces my balance by exactly amount.
2. It returns my new balance.
3. It changes nothing except my balance.
4. It fails if, and only if, I ask for more than I have.

1. What changes: ensures and \old

   ensures states a condition that must hold when the function returns successfully. Inside it, \old(e) is the value of e when the call started; a name without \old means its value at the end.

   //@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;

   BeforeMy balance is B

   Callwithdraw(A)

   After successMy balance is B − A

   Specification arithmetic never overflows or wraps: \old(balances[msg.sender]) - amount is the exact mathematical difference. Solidity's own overflow checks still apply to the code.

2. What it returns: \result

   \result is the value the function returns. This clause says the returned number equals the balance left after the withdrawal.

   //@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
   //@ ensures \result == balances[msg.sender];

   Try it

   A wrong return value

   This withdraw remembers the old balance before subtracting. Does it return the right number?

   As writtenFixed code

   Read-onlyRun CertiK Prover

   7//@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
   8//@ ensures \result == balances[msg.sender];
   9function withdraw(uint256 amount) external returns (uint256) {
   10    require(amount <= balances[msg.sender], "insufficient balance");
   11    uint256 previous = balances[msg.sender];
   12    balances[msg.sender] = previous - amount;
   13    return previous;
   14}
   

   Select Run CertiK Prover to check this code against its specification.

3. What may change: assignable

   assignable lists the storage the function may modify; everything else must stay exactly as it was. Naming balances[msg.sender] lets only the caller's entry change, so every other account is protected.

   //@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
   //@ ensures \result == balances[msg.sender];
   //@ assignable balances[msg.sender];

   assignable permits a change; it does not require one. Without an assignable clause, a function that writes state may modify anything. Write assignable \nothing; for a function that changes no storage.

   Try it

   An unexpected change

   This version also keeps a running total of withdrawals. Does the specification allow that?

   As writtenUpdated specification

   Read-onlyRun CertiK Prover

   8//@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
   9//@ ensures \result == balances[msg.sender];
   10//@ assignable balances[msg.sender];
   11function withdraw(uint256 amount) external returns (uint256) {
   12    require(amount <= balances[msg.sender], "insufficient balance");
   13    balances[msg.sender] -= amount;
   14    totalWithdrawn += amount;
   15    return balances[msg.sender];
   16}
   

   Select Run CertiK Prover to check this code against its specification.

4. When it fails: revert clauses

   ensures describes only successful calls. Three clauses describe when a call reverts. Their condition P is read in the starting state:

   Clause	Meaning
   reverts_when P	If P holds, the call must revert.
   reverts_only_when P	If the call reverts, P held.
   reverts_when_and_only_when P	Both: the call reverts exactly when P holds.

   The vault should fail exactly when the caller asks for more than they have:

   //@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
   //@ ensures \result == balances[msg.sender];
   //@ assignable balances[msg.sender];
   //@ reverts_when_and_only_when amount > balances[msg.sender];
   function withdraw(uint256 amount) external returns (uint256) {

   Revert clauses describe what the code does; they do not add a check. Here the require in withdraw does the reverting. Under Solidity 0.8, arithmetic overflow and underflow revert too, and CertiK Prover accounts for that.

   Try it

   An off-by-one revert

   The specification says a withdrawal fails exactly when it asks for more than the balance. Does the code agree?

   As writtenFixed code

   Read-onlyRun CertiK Prover

   7//@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
   8//@ ensures \result == balances[msg.sender];
   9//@ assignable balances[msg.sender];
   10//@ reverts_when_and_only_when amount > balances[msg.sender];
   11function withdraw(uint256 amount) external returns (uint256) {
   12    require(amount < balances[msg.sender], "insufficient balance");
   13    balances[msg.sender] -= amount;
   14    return balances[msg.sender];
   15}
   

   Select Run CertiK Prover to check this code against its specification.

5. What callers guarantee: requires

   Every clause so far describes the function for all inputs. requires is different: it states a condition the caller must guarantee. CertiK Prover assumes it while checking the function, and proves it at every call. It suits internal helpers such as this one, which trusts its callers to check the balance first:

   //@ requires amount <= balances[user];
   //@ ensures balances[user] == \old(balances[user]) - amount;
   //@ assignable balances[user];
   function _debit(address user, uint256 amount) internal {
       unchecked { balances[user] -= amount; }
   }

   requires adds no runtime check. On an external function, nothing in your code calls it, so a requires there only narrows the claim to callers that satisfy it. To describe input checks the code performs itself, use revert clauses.

   Try it

   An unguaranteed precondition

   _debit requires the balance to cover the amount. Does withdraw guarantee that before calling it?

   As writtenFixed code

   Read-onlyRun CertiK Prover

   7//@ ensures \result == balances[msg.sender];
   8function withdraw(uint256 amount) external returns (uint256) {
   9    _debit(msg.sender, amount);
   10    return balances[msg.sender];
   11}
   12
   13//@ requires amount <= balances[user];
   14//@ ensures balances[user] == \old(balances[user]) - amount;
   15//@ assignable balances[user];
   16function _debit(address user, uint256 amount) internal {
   17    unchecked { balances[user] -= amount; }
   18}
   

   Select Run CertiK Prover to check this code against its specification.

Write deposit's specification before opening the answer: it adds amount to the caller's balance, changes nothing else, and reverts exactly when the new balance would overflow.

//@ ensures balances[msg.sender] == \old(balances[msg.sender]) + amount;
//@ assignable balances[msg.sender];
//@ reverts_when_and_only_when balances[msg.sender] + amount > type(uint256).max;
function deposit(uint256 amount) external {
    balances[msg.sender] += amount;
}

Here is the vault with both functions specified. CertiK Prover proves every clause.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

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

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

    //@ ensures balances[msg.sender] == \old(balances[msg.sender]) + amount;
    //@ assignable balances[msg.sender];
    //@ reverts_when_and_only_when balances[msg.sender] + amount > type(uint256).max;
    function deposit(uint256 amount) external {
        balances[msg.sender] += amount;
    }

    //@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
    //@ ensures \result == balances[msg.sender];
    //@ assignable balances[msg.sender];
    //@ reverts_when_and_only_when amount > balances[msg.sender];
    function withdraw(uint256 amount) external returns (uint256) {
        require(amount <= balances[msg.sender], "insufficient balance");
        balances[msg.sender] -= amount;
        return balances[msg.sender];
    }
}

+-----------------------------+
|  Failure #1: Postcondition  |
+-----------------------------+

The verifier found an execution path that can violate an ensures clause.

  +--- Source Context ---+
  Vault.sol:8
   7 |     //@ ensures balances[msg.sender] == \old(balances[msg.sender]) - amount;
>  8 |     //@ ensures \result == balances[msg.sender];
   9 |     function withdraw(uint256 amount) external returns (uint256) {

[Reason              ]: Postcondition violation
[Failed condition    ]: \result == balances[msg.sender]
…
=== Verification Summary: 1 total, 0 passed, 1 failed, 0 errors ===

1. Find the clause

   The header gives the kind of failure, and the > marker shows the line.

2. Read the failed condition

   This is the exact condition that can be false.

3. Rebuild the scenario

   Choose starting values the code accepts, follow the code, and compare the outcome with the clause, as the playground explanations do.

4. Fix the code or the specification

   Decide which one is wrong. Never weaken a clause only to make it pass.