Smart Contract Security on Celo with Manticore

Smart Contract Security on Celo with Manticore
none 0.0 0


Smart contracts are self-executing pieces of code that run on distributed ledgers called the “blockchain”. The Ethereum Virtual Machine and other blockchains that are compatible in architecture e.g. Celo are capable of resistance to censorship, downtime, and third-party interference, and have since invented changed how software is perceived. As exciting as smart contracts are, they could introduce high-risk of financial loss especially where exchanging of value (usually monetarily) is involved if not properly scrutinized. It then becomes crucial for developers to analyze contract code before deployment to a live network.


This guide introduces you to working with a security tool called Manticore. I assume you already have experience working with smart contracts using solidity language. If you’re new to this, I recommend reading through Building a Solidity Smart Contract for NFT Royalty Fees - A Step-by-Step Guide - Technical Tutorials - Celo Academy by @Kunaldawar and Best Practices for Writing Smart Contracts with Real World Examples - Technical Tutorials - Celo Academy to get started.


Manticore is a Python-based tool with unusual dependencies such as Z3, protobuf, etc, and performs better on Linux-based operating systems compared to Windows OS. I recommend using WSL if you are on Windows. Follow Install WSL | Microsoft Learn to set up WSL on Windows.

Install the following before proceeding.

  • Python3.7 or later

  • Manticore officially supports the latest LTS version of Ubuntu

  • Editor/IDE. VSCode recommended

  • Python package manager - PIP

    sudo apt update
    sudo apt install python3-pip
    pip3 --version

What is Manticore?

Manticore is a symbolic execution tool for analyzing binaries and smart contracts. It can be used to check and analyze binaries in Linux, for WASM, and EVM using bytecode. With Manticore, developers are able to check for vulnerabilities in smart contracts code written in solidity that are compiled to the EVM bytecode via a technique that uses constraint solving to systematically explore a program’s state space. It is different from other analysis tools because it is property-based i.e. it runs a series of tests on the smart contracts using properties rather than testing a few behaviors.

Usually, as web3 developers, when we write tests, we want to check if our code is correct. We want the test to follow the patterns:

  • Setting or specifying sequences of interactions such as
    • Approve
    • transferFrom
    • the, expected balances should tally
  • Examine the result
  • Iterating the steps on every commit

If we think this way, then we could say writing unit tests for everything is hard and time-consuming.

Why Manticore?

The problem arises from the fact that as developers, we don’t test most behaviors by asking ourselves some unusual questions such as:

  • What if the order of calls changes?
  • What if approval or transferFrom is called twice?

Let’s examine some of the differences between unit and property tests.

1 Most tests devs carried out cover only single input Property test covers any possible inputs
2 Covers cases that you know about Covers cases that you don’t know about
3 Specifies a single transaction sequence. Ex. If Alice calls "r()", it sends Bob 3 ETH. If she then calls "v()", she’ll have 4 ETH Using mathematical models, checks for all possible transaction sequences. Ex. Irrespective of which method is called by Alice, Bob can’t lose money
4 Reasons about a few possible inputs The set of possible inputs are giant: reasons about all of them
5 One test : One-way to check One test : two-way to check
6 - If generates 10000 pairs of units, calls function “f” with all of them, and check the properties on each of them
7 - Executes with any possible initial value
8 - Checks for possibility of failure
9 - Uses solvers for constraints e.g Z3, Yices etc
10 Easy to set up. You could miss stuff Lots of effort to set up. It uses effective formal verification
11 Less assurance Super high assurance

Note: If you need a good test suite or correctness, use Manticore

Installing Manticore

To use Manticore, be sure Python is installed on your machine since we will need the Python package manager - Pip to install the tool. If you need to install it from scratch, please follow the steps I itemized here.

To get the best result and avoid dependency conflict, you could run Manticore in a Virtual box or create a virtual environment.


  1. I assume you have installed the necessary tools and running the Ubuntu OS
  pip3 install manticore

Note: Installing Manticore also installs capstone and Z3 solver But if you need to install is separate, run the command below

sudo pip3 install --no-binary capstone .
sudo apt-get update && sudo apt-get install z3

Open the Ubuntu terminal and type manticore. If the response is negative, then try to install with extra dependencies needed to execute native binaries. Run:

pip install "manticore[native]"

This should globally install Manticore.

  • Check if Manticore is installed
manticore --version

It should return the installed version.

  1. We need a tool called solc-select to manage the solidity compiler. To confirm if solc-select is installed, run:
    solc --version

You should see a version printed in the terminal.

Version: 0.8.19+commit.7dd6d404.Linux.g++

This is the current version of solc installed on my system. If otherwise, install solc-select following these steps.

pip3 install solc-select

Check again if correctly installed. Perform step 2. This time, it should return success.

To use Manticore, we have to install the required compiler version in the contract files and tell solc-select which version to use during compilation. First, let’s check if we have versions of the compiler previously installed.

solc-select install

In my terminal, I got several available versions.

Install a specific version or simply get the latest version.

    solc-select install <version>


    solc-select latest

After installation, we have to explicitly tell solc which version we want to use for compiling our contracts.

    solc-select use <version>


    solc-select use 0.8.18

or simply use the latest version.

    solc-select use latest

Now that we have told solc-select which version to use, let’s create a project to test if Manticore is working.

Project setup

  • Create a project folder
    mkdir <projectName> && cd <projectName>
  • Create a virtual environment. I call my environment env
python3 -m virtualenv env
  • Navigate to the root folder, then activate the virtual environment
cd <projectRoot> && source env/bin/activate
  • Inside the env folder, or anywhere in the project root, create a Lock.sol file and the code below.
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.9;

// Uncomment this line to use console.log
// import "hardhat/console.sol";

contract Lock {
    uint public unlockTime;
    address payable public owner;

    event Withdrawal(uint amount, uint when);

    constructor(uint _unlockTime) payable {
            block.timestamp < _unlockTime,
            "Unlock time should be in the future"

        unlockTime = _unlockTime;
        owner = payable(msg.sender);

    function withdraw() public {
        // Uncomment this line, and the import of "hardhat/console.sol", to print a log in your terminal
        // console.log("Unlock time is %o and block timestamp is %o", unlockTime, block.timestamp);

        require(block.timestamp >= unlockTime, "You can't withdraw yet");
        require(msg.sender == owner, "You aren't the owner");

        emit Withdrawal(address(this).balance, block.timestamp);


The above code is the usual Lock.sol boilerplate contract. It doesn’t do much. To analyze the contract, we have to invoke Manticore. First,
navigate to the directory where the file resides, then invoke Manticore on the file.

cd <projectRoot>/env
manticore Lock.sol

When you run this command, Manticore will start to run a series of tests on the contract as shown below.

Inspect the log to see the outcome of the process. A folder will be output under the env folder containing the outcome of the analysis. Take your time to inspect the files.


Three test cases were carried out on the contract using three different accounts tagged as:

  1. user_00000001
  2. user_00000002
  3. user_00000003

The summary of the analysis is kept in the "user_0000000<index>.summary" files. Let’s examine the content of thee file.

Message: RETURN
Last exception: RETURN
Last instruction at contract cb37f4304de8d1ca2df2474c6e3a00ab3e720462 offset 63
    8  uint public unlockTime

3 accounts.
* owner::
Address: 0x10000 
Balance: 9999926613 (*)
Storage: STORAGE_10000

* attacker::
Address: 0x20000 
Balance: 9999953097 (*)
Storage: STORAGE_20000

* contract0::
Address: 0xcb37f4304de8d1ca2df2474c6e3a00ab3e720462 
Balance: 0 (*)
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[0] = 0
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
storage[1] = 1
Storage: (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store STORAGE_cb37f4304de8d1ca2df2474c6e3a00ab3e720462 #x0000000000000000000000000000000000000000000000000000000000000000 SVALUE_1) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000) #x0000000000000000000000000000000000000000000000000000000000000001 #x0000000000000000000000000000000000000000000000000000000000010000)
Coverage 44% (on this state)

(*) Example solution given. Value is symbolic and may take other values

Possible Error

While invoking Manticore, you might likely encounter an error as displayed in the image below.

This error is due to a disparity in the version of protobuf on which Manticore depends to run smoothly. Manticore is compatible with the earlier version of protobuf. Most versions greater than 3.20 have conflicts. If your version is higher than v3.20, the error demands that you downgrade the version to v3.20. To downgrade protobuf, follow these steps.

  • pip3 install protobuf==3.20.*
  • Then set the path to be "python".
  • Confirm if this was successful.

After, you may now invoke the command again. This should work fine. The only setback is that the process will be much slower.

The complete code for this tutorial is available at Manticore.


In this guide, we learned :

  • what Manticore is.
  • Why you should use it
  • Its advantage over other tools for unit testing
  • Installation and set up.
  • Invoking Manticore to analyze smart contracts.
  • How to solve common errors.

What next?

Start analyzing your contracts using Manticore to give you more insight into your code. Please leave your comment if you encounter any difficulty while setting up the environment or share with us on Discord.

To learn how to deploy your dream project on the Celo blockchain, visit the Celo documentation

About the Author​

Isaac Jesse , aka Bobelr is a smart contract/Web3 developer. He has been in the field since 2018, worked as an ambassador with several projects like Algorand and so on as a content producer. He has also contributed to Web3 projects as a developer.



I am using this medium to express my sincere gratitude to Celo, especially to the leadership @Celo_Academy for his exceptional coordinating skills, and for the recognition.

Thank you again.

In response to an announcement made at Announcing This Week's Top Proposals and Celebrating this Week's Leading Contributors | 06/01/23, I’d like to get started on this proposal that brings desired value and result to the Celo community.

Thank you for your efforts @Celo_Academy


Thanks so much for your contribution to the community @bobelr. Looking forward to this tutorial!


Hi @bobelr i will be reviewing this


Ok great @thompsonogoyi1t


In this tutorial u used Ubuntu, can I use window system?


Yes, you can run Ubuntu using WSL on Windows. It will work fine.


fixed the manticore links as md.

1 Like

Thank you