Introduction

Recon is a tool for automatically scaffolding and running invariant testing in the cloud.

Creating An Account

To get started with Recon, you'll need to create an account using your GitHub account.

Once you've created an account, you'll be redirected to the dashboard where you'll have access to all of the tools in the Recon suite. To run a job you'll need a Recon Pro account. The other tools in the Recon suite are free to use without a Pro account.

Learn Invariant Testing

Most of our guides and documentation are focused on using fuzzing tools, primarily Echidna and Medusa because we use them internally at Recon. However, we also support running other tools on our cloud infrastructure such as Foundry (fuzzing), Halmos (formal verification), and Kontrol (formal verification).

After having chosen a tool best suited to your needs and downloading it locally, you can get started by running jobs directly on the jobs pge.

If you're new to invariant testing, we recommend you start with the following posts before getting started:

If you prefer a full end-to-end video bootcamp, checkout this series on everything you need to know about invariant testing.

Once you've grasped the basics of invariant testing you can setup your first suite and run it on Recon. For a step-by-step guide on how to do this, check out the First Steps guide.

If you have any questions about how to use Recon or invariant testing in general, you can reach out to our team on Discord.

Additional Learning Resources

If you're looking for more resources to help you get started with invariant testing, please see the following:

For more resources on Echidna and Medusa, please see the following:

First Steps

To make getting started with Invariant Testing as easy as possible, we created the create-chimera-app repository which serves as a template that you can use to create a new project with invariant testing built in.

This template uses our Chimera framework to let you run invariant tests with Echidna and Medusa that can be easily debugged using Foundry. We've also incorporated contracts from our Setup Helpers repo which make managing the test suite setup much simpler.

Creating A New Project

If you haven't already, first create a recon account as described in the create an account section and install either Echidna or Medusa.

Next you'll need to create a new project using the create-chimera-app template. You can use the Use this template button on GitHub to do this. This will automatically create a new repository using the create-chimera-app template on your GitHub account.

Create-chimera-app ships with the default foundry project as an example. This is a simple Counter.sol contract that you can use to test the fuzzing capabilities of Echidna and Medusa.

Testing

An example invariant is implemented in the Properties contract and some in-line properties are defined in the TargetFunctions contract.

You can run the default fuzzing tests using the following commands

Echidna


echidna . --contract CryticTester --config echidna.yaml

Medusa


medusa fuzz

Expanding The Example Project

Create-chimera-app is meant to be a starting point for your own project. You can expand the example project by adding your own contracts and properties. See the Chimera Framework section on what the role of each contract is and how to expand the example project.

This substack post walks you through the process of converting invariants from English to Solidity using a ERC4626 vault on an example project using Chimera.

To add new contracts just delete the existing Counter.sol and Counter.t.sol files and add your own.

After adding your new contracts, you can add handlers for the contracts you want to test using invariant testing by using the Build Handlers page on Recon (see this section for how to do this).

Chimera Framework

The Chimera framework lets you run invariant tests with Echidna and Medusa that can be easily debugged using Foundry.

The framework is made up of the following files:

Setup.sol
TargetFunctions.sol
Properties.sol
CryticToFoundry.sol
BeforeAfter.sol
CryticTester.sol

When you build your handlers using Recon these files get automatically generated and populated for you. To use the framework in your project, you just need to download these files that get generated for you and add the Chimera dependency to your project:


forge install Recon-Fuzz/chimera

The Contracts

We'll now look at the role each of the above contracts serve in building an extensible and maintainable fuzzing suite. We'll be looking at examples using the create-chimera-app template project.

`Setup`

This contract is used to deploy and initialize the state of your target contracts. It's called by the fuzzer before any of the target functions are called.

Any contracts you want to track in your fuzzing suite should live here.

In our create-chimera-app template project, the Setup contract is used to deploy the Counter contract:


abstract contract Setup is BaseSetup {
    Counter counter;

    function setup() internal virtual override {
        counter = new Counter();
    }
}

`TargetFunctions`

This is perhaps the most important file in your fuzzing suite, it defines the target function handlers that will be called by the fuzzer to manipulate the state of your target contracts.

Note: These are the only functions that will be called by the fuzzer.

Because these functions have the aim of changing the state of the target contract, they usually only include non-view and non-pure functions.

Target functions make calls to the target contracts deployed in the Setup contract. The handler that wraps the target function allows you to add clamping (reducing the possible fuzzed input values) before the call to the target contract and properties (assertions about the state of the target contract) after the call to the target contract.

In our create-chimera-app template project, the TargetFunctions contract is used to define the increment and setNumber functions:


abstract contract TargetFunctions is
    BaseTargetFunctions,
    Properties
{
    function counter_increment() public {
        counter.increment();
    }

    function counter_setNumber1(uint256 newNumber) public {
        // clamping can be added here before the call to the target contract
        // ex: newNumber = newNumber % 100;

        // example assertion test replicating testFuzz_SetNumber
        try counter.setNumber(newNumber) {
            if (newNumber != 0) {
                t(counter.number() == newNumber, "number != newNumber");
            }
        } catch {
            t(false, "setNumber reverts");
        }
    }

    function counter_setNumber2(uint256 newNumber) public {
        // same example assertion test as counter_setNumber1 using ghost variables
        __before();

        counter.setNumber(newNumber);

        __after();

        if (newNumber != 0) {
            t(_after.counter_number == newNumber, "number != newNumber");
        }
    }
}

`Properties`

This contract is used to define the properties that will be checked after the target functions are called.

At Recon our preference is to define these as Echidna/Medusa assertion properties but they can also be defined as boolean properties.

In our create-chimera-app template project, the Properties contract is used to define a property that states that the number can never be 0:


abstract contract Properties is BeforeAfter, Asserts {
    // example property test
    function invariant_number_never_zero() public {
        t(counter.number() != 0, "number is 0");
    }
}

`CryticToFoundry`

This contract is used to debug broken properties by converting the breaking call sequence from Echidna/Medusa into a Foundry unit test. When running jobs on Recon this is done automatically for all broken properties using the fuzzer logs.

If you are running the fuzzers locally you can use the Echidna and Medusa tools on Recon to convert the breaking call sequence from the logs into a Foundry unit test.

This contract is also useful for debugging issues related to the setup function and allows testing individual handlers in isolation to verify if they're working as expected for specific inputs.

In our create-chimera-app template project, the CryticToFoundry contract doesn't include any reproducer tests because all the properties pass.

The test_crytic function demonstrates the template for adding a reproducer test:


contract CryticToFoundry is Test, TargetFunctions, FoundryAsserts {
    function setUp() public {
        setup();

        targetContract(address(counter));
    }

    function test_crytic() public {
        // TODO: add failing property tests here for debugging
    }
}

`BeforeAfter`

This contract is used to store the state of the target contract before and after the target functions are called in a Vars struct.

These variables can be used in property definitions to check if function calls have modified the state of the target contract in an unexpected way.

In our create-chimera-app template project, the BeforeAfter contract is used to track the counter_number variable:


// ghost variables for tracking state variable values before and after function calls
abstract contract BeforeAfter is Setup {
    struct Vars {
        uint256 counter_number;
    }

    Vars internal _before;
    Vars internal _after;

    function __before() internal {
        _before.counter_number = counter.number();
    }

    function __after() internal {
        _after.counter_number = counter.number();
    }
}

`CryticTester`

This is the entrypoint for the fuzzer into the suite. All target functions will be called on an instance of this contract since it inherits from the TargetFunctions contract.

In our create-chimera-app template project, the CryticTester contract is used to call the counter_increment and counter_setNumber1 functions:


// echidna . --contract CryticTester --config echidna.yaml
// medusa fuzz
contract CryticTester is TargetFunctions, CryticAsserts {
    constructor() payable {
        setup();
    }
}

Assertions

When using assertions from Chimera in your properties, they use a different interface than the standard assertions from foundry's forge-std.

The following assertions are available in Chimera's Asserts contract:


abstract contract Asserts {
    // greater than
    function gt(uint256 a, uint256 b, string memory reason) internal virtual;

    // greater than or equal to
    function gte(uint256 a, uint256 b, string memory reason) internal virtual;

    // less than
    function lt(uint256 a, uint256 b, string memory reason) internal virtual;

    // less than or equal to
    function lte(uint256 a, uint256 b, string memory reason) internal virtual;

    // equal to
    function eq(uint256 a, uint256 b, string memory reason) internal virtual;

    // true
    function t(bool b, string memory reason) internal virtual;

    // between uint256
    function between(uint256 value, uint256 low, uint256 high) internal virtual returns (uint256);

    // between int256
    function between(int256 value, int256 low, int256 high) internal virtual returns (int256);

    // precondition
    function precondition(bool p) internal virtual;
}

Setup Helpers

These contracts were created with the intention of speeding up the setup process for an invariant testing suite.

For an example implementation of these contracts in use see the create-chimera-app repo.

ActorManager

The ActorManager contract serves as the source of truth for actors that are being used in the fuzzing suite setup.

The primary functions of interest when setting up a suite are:

_addActor - allows adding a new address as an actor that can be tracked
_switchActor - this should be exposed in a target function that can be called by the fuzzer to randomly switch between actors

To use the actors stored in the ActorManager, add the asActor modifier on all of your target function handlers which pranks as the currently set actor.

For privileged functions you can use the asAdmin modifier which calls the target functions as the tester contract (address(this)). The tester contract is typically set as the default admin address by convention.

AssetManager

The AssetManager allows tracking all assets being used in the fuzz suite setup. Similar to the ActorManager this serves as the source of truth for all assets used in the test suite and therefore no target function should be called that may transfer an asset not tracked in the AssetManager.

The primary functions of interest when setting up a suite are:

_newAsset - deploys an instance of the MockERC20 contract and adds it to tracking so it can be accessed as needed
_getAsset - used to clamp values used for tokens in calls to target functions
_finalizeAssetDeployment - a utility for minting tokens added via _newAsset to all actors that have been setup and approving it to all contracts in the the system that may need to call transferFrom on it

Utils

Provides utilities for invariant testing

checkError - allows checking if a revert reason from a function call is equivalent to the reason passed in as the expected argument

Panic

A library that provides named variables corresponding to compiler panic messages. Used to more easily access these messages when using the checkError utility.


library Panic {
    // compiler panics
    string constant assertionPanic = "Panic(1)";
    string constant arithmeticPanic = "Panic(17)";
    string constant divisionPanic = "Panic(18)";
    string constant enumPanic = "Panic(33)";
    string constant arrayPanic = "Panic(34)";
    string constant emptyArrayPanic = "Panic(49)";
    string constant outOfBoundsPanic = "Panic(50)";
    string constant memoryPanic = "Panic(65)";
    string constant functionPanic = "Panic(81)";
}

MockERC20

A minimal MockERC20 contract that lets you mock any standard ERC20 tokens that will be interacting with the system without requiring external dependencies.

Recon Docs