4.2. Basic exercises#


ERC20.sol contains an ERC20 implementation. Write an invariant for ERC20 verifying that address(0) always has zero balance. Run the invariant on ERC20.sol and discover the violation in the contract.


Remember to use the optimistic_loop option, see Important: Optimistic loop.


CVL types

You can use balanceOf(0) in CVL without casting it to address.


A solution is available in zero.spec.

English auction basic exercise#

In EnglishAuction.sol, you will find the implementation of a simple English Auction for selling an NFT. The auction process and additional features are described in the solidity file. Here is a summary of the main details:

  1. The seller of the NFT deploys the contract and sets the NFT and the token to be used.

  2. A participant can bid a certain amount to become the new highest bidder.

  3. Once the bid has ended the highest bidder gets the NFT, and the seller receives the highest bidder’s tokens.


Write a spec for EnglishAuction.sol containing the following two invariants.

  1. The highestBid is higher than or equal to any other bid. You may assume that address(0) cannot place a bid.

  2. The bid of the highestBidder equals the highestBid.


Methods block hint

You will need to define the getters as envfree.

Highest bidder hint

What is the initial value of the highest bidder?


A full solution is available in EnglishAuction.spec.