# Writing Invariants

ItyFuzz, by default, supports finding [Echidna](https://github.com/crytic/echidna) and [Scribble](https://docs.scribble.codes/) invariant violations. You do not need to change the code if it works for Echidna, Mythril, Harvey, etc. ItyFuzz also supports [`bug()`](#bug-support), which indicates the current code shall not be reached. 

### Echidna Support

Any contracts bearing functions starting with `echidna_` will be treated as invariants and will be tested by ItyFuzz. If it returns `false`, the fuzzer will report a bug.

```solidity
function echidna_test() public {
    assert(false);
}
```

### Scribble Support

Scribble is a tool for writing specifications for Solidity contracts. ItyFuzz supports Scribble annotations after it is compiled by `scribble`.

For example, the following contract has a Scribble annotation that specifies the return value of `inc`:

```bash
contract Foo {
    /// #if_succeeds {:msg "P1"} y == x + 2;
    function inc(uint x) public pure returns (uint y) {
        return x+1;
    }
}
```

You need to compile the contract using `scribble` and pass the compiled contract to ItyFuzz

Note that you must add `--no-assert` to the `scribble` command. Otherwise, ItyFuzz will not detect any bugs.

```bash
scribble test.sol --output-mode flat --output compiled.sol --no-assert
```

Then compile with `solc` and run ItyFuzz:

```bash
solc compiled.sol --bin --abi --overwrite -o build
ityfuzz evm -t "build/*" [More Arguments]
```

### `bug()` Support

You can insert `bug()` or `typed_bug(string message)` in your contract to report a condition when the bug is found.

For instance, a simple case can be written as follows:

```solidity
function buy_token() public {
    if (msg.sender != owner) {
        bug();
    }
}
```

The implementation of `bug()` is as follows:

```solidity
library FuzzLand {
    event AssertionFailed(string message);
  
    function bug() internal {
        emit AssertionFailed("Bug");
    }
  
    function typed_bug(string memory data) internal {
        emit AssertionFailed(data);
    }

}

function bug()  {
    FuzzLand.bug();
}

function typed_bug(string memory data)  {
    FuzzLand.typed_bug(data);
}
```

You can either paste the code above into your contract or import it from [`solidity_utils/lib.sol`](https://github.com/fuzzland/ityfuzz/blob/master/solidity_utils/lib.sol), if you are using `bug` or `typed_bug`.


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.ityfuzz.rs/docs-evm-contract/writing-invariants.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.