Echidna is a fuzzing tool created by Trail of Bits/Crytic. It is able to operate directly on smart contracts and attempts to disprove various user-defined invariants or assertions. It supports output shrinking and some built-in properties like searching for the ability to selfdestruct a contract.
Echidna in action
### How to use Echidna (Mac)
The Echidna binary can be downloaded directly from [GitHub](https://github.com/crytic/echidna/releases) or alternatively one can use the pre-built Docker container.
To illustrate how Echidna can be used, consider the following contract `Simple.sol`:
```solidity
pragma solidity ^0.8.0;
contract Simple {
uint badNumber = 0;
function reset() external {
badNumber = 0;
}
function bump() external {
badNumber += 1;
}
function echidna_test() external view returns (bool) {
return badNumber < 3;
}
}
```
Any function beginning with `echidna_` is considered an invariant that should never return the value `true`. Echidna will attempt to call other functions in the contract in sequence until the invariant returns `true`.
To run Echidna, use the following command:
```bash
echidna-test Simple.sol
```
This is the kind of output you may get:
Echidna output for Simple.sol
In this case, Echidna has discovered that calling `bump()` three times in a row will result in `echidna_test()` returning true. It also was not able to find a way to `selfdestruct` the contract.
For detailed instructions how to use Echidna, please follow the tutorial at [https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna). This tutorial illustrates other features of Echidna such as test corpuses, filters as well as running a long-term multicore Echidna campaign.
Please note that the tutorial is using the old command syntax and some amendments may be required to work with Echidna Version 2. In particular, if you want to check for assertions, you can use the following code:
```bash
echidna-test Contract.sol --test-mode assertion
```
