What Fuzzing Is — and Why Unit Tests Are Not Enough

Fuzzing is a well-known technique in the security industry to discover bugs in software — invalid, unexpected, or random data is generated automatically and injected into the software to find issues. In a traditional unit test you write a specific input, a specific expected output, and a pass/fail assertion. That model has a fundamental ceiling: you can only discover the bugs you already suspect exist.

Having adequate test coverage using unit tests is essential, but there will always be edge cases you did not test for. It is therefore best practice to extend your testing strategy by using additional security tools, such as static analyzers and fuzzers.

Property-based fuzzing changes the question entirely. Instead of asking “does this function return X for input Y?”, you ask “does this invariant hold for any sequence of calls over any inputs?” Rather than testing specific inputs and outputs, Echidna allows developers to define invariants and properties that should always hold true. For example: “The contract’s total supply should never exceed the maximum cap” or “User balances should never go negative.”

Echidna belongs to a specific family of fuzzer: property-based fuzzing heavily inspired by QuickCheck. In contrast to a classic fuzzer that will try to find crashes, Echidna will try to break user-defined invariants.

This distinction is important in the smart contract context. On-chain bugs rarely manifest as clean crashes. They manifest as silent arithmetic drift, share-price manipulation, or an attacker claiming ownership through a forgotten initializer. Unit tests, by design, only check the scenarios you conceived of when writing them. Echidna is adversarial in a way unit tests can never be.

What Echidna Is

Echidna is a Haskell program designed for fuzzing/property-based testing of Ethereum smart contracts. It uses sophisticated grammar-based fuzzing campaigns based on a contract ABI to falsify user-defined predicates or Solidity assertions.

The core Echidna functionality is an executable called echidna, which takes a contract and a list of invariants (properties that should always remain true) as input. For each invariant, it generates random sequences of calls to the contract and checks if the invariant holds. If it can find some way to falsify the invariant, it prints the call sequence that does so.

Beyond simple property checking, Echidna ships with a rich feature set:

It has features such as: optional corpus collection, mutation, and coverage guidance to find deeper bugs; automatic test case minimization for quick triage; maximum gas usage reporting of the fuzzing campaign; generates inputs tailored to your actual code; and is powered by Slither to extract useful information before the fuzzing campaign.

The Echidna Workflow

1. Write a harness contract

Echidna tests live in Solidity. You create a test contract — typically inheriting or wrapping the target — and expose the invariant functions alongside any setup the fuzzer needs. The invariant functions are the only interface Echidna cares about for pass/fail decisions; everything else is callable fodder.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;

import "./MyToken.sol";

contract EchidnaTokenTest {
    MyToken token;
    address constant USER = address(0x1337);

    constructor() {
        token = new MyToken(1_000_000e18);
        token.transfer(USER, 500_000e18);
    }

    /// @dev Total supply must never exceed the initial cap.
    function echidna_supply_cap() public view returns (bool) {
        return token.totalSupply() <= 1_000_000e18;
    }

    /// @dev No address should hold more than the initial total supply.
    function echidna_no_overflow_balance() public view returns (bool) {
        return token.balanceOf(msg.sender) <= token.totalSupply();
    }
}

2. Write a YAML config file

Most non-trivial campaigns need a config file. A minimal but practical one looks like:

# echidna.yaml
testMode: property
testLimit: 50000
seqLen: 100
shrinkLimit: 5000
corpusDir: "corpus"

deployer: "0x10000"
sender:
  - "0x10000"
  - "0x20000"
  - "0x30000"

coverage: true

Key knobs to understand:

KeyPurpose
testModeproperty, assertion, overflow, optimization, or exploration
testLimitTotal number of call sequences to execute
seqLenMaximum calls per sequence (depth of stateful exploration)
shrinkLimitEffort invested minimizing a found counterexample
corpusDirDirectory for coverage-maximising corpus saves
senderAddresses Echidna will use as msg.sender

You can also assign the RPC provider and block number (indicated by rpcUrl and rpcBlock parameters, respectively) for Echidna to fetch on-chain information. To prevent an indefinite runtime, set an upper limit through the testLimit parameter.

3. Run the campaign

echidna MyContract.sol --contract EchidnaTokenTest --config echidna.yaml

Echidna will launch its terminal UI, showing properties, their statuses, the number of calls executed, and live coverage statistics. When a property is violated it switches to shrinking mode — reducing the counterexample to its minimal reproducible sequence — and then prints that sequence.

Testing Modes in Depth

Echidna offers several ways to write properties, which often leaves developers and auditors wondering about the most appropriate testing mode to use.

Property mode (default)

By default, the property testing mode is used, which reports failures using special functions called properties: testing functions should be named with a specific prefix (e.g. echidna_). Testing functions take no parameters and always return a boolean value. Any side effect will be reverted at the end of the execution of the property. Properties pass if they return true and fail if they return false or revert.

This is the right mode when your invariant can be computed purely from on-chain state variables. The no-parameters constraint keeps the property surface small and clean, but it means you must encode all relevant context as state.

Assertion mode

Using the assertion testing mode, Echidna will report an assert violation if the execution reverts during a call to assert(). Technically speaking, Echidna will detect an assertion failure if it executes an assert call that fails in the first call frame of the target contract. An AssertionFailed event (with any number of parameters) emitted by any contract also triggers a failure.

Assertion mode is useful when you want to instrument internal functions or when the property requires parameterised input that you construct inside a function rather than from state alone.

function check_deposit_roundtrip(uint256 amount) public {
    amount = bound(amount, 1, 1e24);
    uint256 before = vault.totalAssets();
    vault.deposit(amount, address(this));
    uint256 after_ = vault.totalAssets();
    assert(after_ >= before); // assets can only grow on deposit
}

Optimization mode

Echidna’s “optimization mode” will automatically discover transaction sequences that maximize or minimize the outcome of a custom function. With a fuzzing contract and a profit function, Echidna can swiftly discover the correct sequence of transactions to reproduce the hack, without needing prior knowledge of the actual contract exploit.

This mode is powerful for reproducing economic exploits: define a echidna_optimize_profit() function returning int256, and Echidna will search for the sequence that makes it as large as possible.

Exploration mode

Exploration mode collects coverage without checking properties. Run it first on a new target to understand how much of the codebase Echidna can reach before you spend cycles writing properties against unreachable code.

Stateful vs. Stateless Fuzzing

When it comes to testing your smart contract with Echidna, you have the option of choosing between two testing modes: stateful and stateless.

By default, Echidna runs in stateful mode, which means that it will keep the state between each function call and try to break the invariants (or properties). In contrast, stateless mode can be activated using the --seqLen 1 command when running Echidna. In this mode, Echidna will discard the state changes during the fuzzing.

The implications are significant:

Stateful mode is more powerful than stateless mode, as it can allow breaking invariants that only exist if the contract reaches a specific state. This means that stateful mode can potentially uncover more bugs and vulnerabilities. On the other hand, stateless tests can be easier to use than stateful tests because they benefit from simpler input generation. However, this ease of use comes at a cost: stateless tests can hide issues that depend on a sequence of operations that is not reachable in a single transaction.

In practice, nearly all DeFi protocol bugs require stateful fuzzing. A reentrancy path, a share-price manipulation, or an accrual accounting error only manifests after a specific sequence of deposit → borrow → repay calls. Single-transaction stateless testing will never reach those states.

Echidna uses property-based testing to verify invariants in smart contracts by executing transactions with randomly generated inputs. Echidna’s stateful fuzzing capability allows it to maintain and manipulate the contract’s state across transactions, making it adept at uncovering complex vulnerabilities that are dependent on specific sequences of actions.

Writing Effective Invariant Properties

The quality of an Echidna campaign is almost entirely determined by the quality of the properties. A weak set of properties gives you a green checkmark and false confidence. Here is a taxonomy to reason from.

System-level solvency invariants

These are the hardest properties to falsify and the most valuable to have. A solvency invariant asserts that the protocol’s liabilities never exceed its assets:

/// @dev The vault can always cover every depositor's claim.
function echidna_vault_solvent() public view returns (bool) {
    return vault.totalAssets() >= vault.convertToAssets(vault.totalSupply());
}

/// @dev Sum of all share balances equals totalSupply (no phantom shares).
function echidna_shares_accounting() public view returns (bool) {
    uint256 sumShares = vault.balanceOf(alice) +
                        vault.balanceOf(bob) +
                        vault.balanceOf(charlie);
    return sumShares <= vault.totalSupply();
}

Access control invariants

In smart contracts, invariants are Solidity functions that can represent any incorrect or invalid state that the contract can reach, including: incorrect access control (the attacker became the owner of the contract); incorrect state machine (the tokens can be transferred while the contract is paused); incorrect arithmetic (the user can underflow their balance and get unlimited free tokens).

address constant ATTACKER = address(0x30000);

/// @dev Unprivileged sender must never become the owner.
function echidna_no_ownership_takeover() public view returns (bool) {
    return target.owner() != ATTACKER;
}

/// @dev Withdrawals must be impossible while the protocol is paused.
function echidna_no_transfer_when_paused() public view returns (bool) {
    if (token.paused()) {
        return token.balanceOf(ATTACKER) == initialAttackerBalance;
    }
    return true;
}

Monotonicity invariants

Some values should only ever move in one direction. ERC-4626 vault share prices, for instance, should be monotonically non-decreasing if the protocol charges no withdrawal fee:

uint256 internal lastSharePrice;

function update_share_price_snapshot() public {
    lastSharePrice = vault.convertToAssets(1e18);
}

/// @dev Share price must never decrease (no-loss vault assumption).
function echidna_share_price_monotonic() public view returns (bool) {
    return vault.convertToAssets(1e18) >= lastSharePrice;
}

Note the use of a non-echidna_ helper function. Echidna will call update_share_price_snapshot() as part of the random call sequence, occasionally snapshotting state. The property then checks the direction of drift.

Conservation invariants

Tokens and funds do not appear from nowhere:

/// @dev ETH locked in the contract must match the sum of all deposits.
function echidna_eth_accounting() public view returns (bool) {
    return address(pool).balance >= pool.totalDeposits();
}

Common Invariants for Lending Protocols

Core invariants include: total borrows ≤ total collateral × collateral factor, sum of all debts ≤ sum of all deposits, and individual positions maintain health factor ≥ 1 (or are liquidated). These guarantee: depositors can always withdraw (subject to utilization), borrowers cannot extract unbacked value, and liquidations maintain system health.

Protocol invariants in lending must account for: interest accrual, oracle price changes, and liquidation mechanics.

A practical Echidna harness for a Compound-style lending protocol looks like:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;

import "./LendingPool.sol";
import "./MockOracle.sol";

contract EchidnaLendingTest {
    LendingPool pool;
    MockOracle oracle;

    address constant ALICE  = address(0x10000);
    address constant BOB    = address(0x20000);
    address constant CAROL  = address(0x30000);

    constructor() {
        oracle = new MockOracle();
        pool   = new LendingPool(address(oracle));

        // Give Echidna senders some collateral tokens to work with.
        pool.collateralToken().mint(ALICE, 100_000e18);
        pool.collateralToken().mint(BOB,   100_000e18);
    }

    // ── Invariant 1: Protocol Solvency ────────────────────────────────────
    /// @dev Total supplied assets must always cover total borrows.
    function echidna_protocol_solvent() public view returns (bool) {
        return pool.totalSupplied() >= pool.totalBorrowed();
    }

    // ── Invariant 2: No free money ────────────────────────────────────────
    /// @dev Withdrawing and immediately re-depositing must not increase
    ///      total assets (no value extracted from thin air).
    function echidna_no_free_money() public view returns (bool) {
        uint256 contractBalance = pool.underlyingToken()
                                      .balanceOf(address(pool));
        return contractBalance + pool.totalBorrowed() >= pool.totalSupplied();
    }

    // ── Invariant 3: Healthy positions only ──────────────────────────────
    /// @dev Every open position must maintain health factor >= 1e18.
    function echidna_all_positions_healthy() public view returns (bool) {
        address[3] memory users = [ALICE, BOB, CAROL];
        for (uint i = 0; i < users.length; i++) {
            if (pool.borrowBalanceOf(users[i]) > 0) {
                if (pool.healthFactorOf(users[i]) < 1e18) {
                    return false;
                }
            }
        }
        return true;
    }

    // ── Invariant 4: Interest accrual is non-negative ────────────────────
    uint256 internal lastTotalBorrows;

    function snapshot_borrows() public {
        lastTotalBorrows = pool.totalBorrowed();
    }

    function echidna_interest_non_negative() public view returns (bool) {
        // After interest accrual, total borrows should not decrease.
        if (lastTotalBorrows == 0) return true;
        return pool.totalBorrowed() >= lastTotalBorrows;
    }
}

Common Invariants for AMMs

AMM solvency invariants define reserve relationships. For Uniswap V2, the key solvency invariant is: after any swap operation, the product of the reserves must be greater than or equal to the product before the swap.

Since the constant product should remain (approximately) the same after swaps, this invariant can be tested by comparing the product of reserves before and after a swap operation.

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;

import "./SimpleAMM.sol";

contract EchidnaAMMTest {
    SimpleAMM amm;

    uint256 internal snapshotK;   // product of reserves at last snapshot
    bool    internal initialized;

    constructor() {
        amm = new SimpleAMM();
        amm.addLiquidity(10_000e18, 10_000e18);
    }

    // ── Invariant 1: k never decreases after swaps ────────────────────────
    /// @dev The constant product k = reserveA * reserveB must be non-
    ///      decreasing (fees cause it to strictly increase or stay flat).
    function echidna_k_non_decreasing() public view returns (bool) {
        (uint256 rA, uint256 rB) = amm.getReserves();
        uint256 currentK = rA * rB;
        if (!initialized) return true;
        return currentK >= snapshotK;
    }

    function take_k_snapshot() public {
        (uint256 rA, uint256 rB) = amm.getReserves();
        snapshotK   = rA * rB;
        initialized = true;
    }

    // ── Invariant 2: LP tokens are fully redeemable ───────────────────────
    /// @dev The AMM contract must hold at least as many tokens as the
    ///      sum of all outstanding LP redemption claims.
    function echidna_lp_redeemable() public view returns (bool) {
        (uint256 rA, uint256 rB)  = amm.getReserves();
        uint256 totalLP           = amm.totalSupply();
        if (totalLP == 0) return true;

        uint256 userLP = amm.balanceOf(address(this));
        uint256 claimA = (rA * userLP) / totalLP;
        uint256 claimB = (rB * userLP) / totalLP;

        return amm.tokenA().balanceOf(address(amm)) >= claimA &&
               amm.tokenB().balanceOf(address(amm)) >= claimB;
    }

    // ── Invariant 3: Price impact is bounded ─────────────────────────────
    /// @dev A single swap must never move the price by more than 50%
    ///      (protects against oracle manipulation via single tx).
    function echidna_no_extreme_price_impact() public view returns (bool) {
        (uint256 rA, uint256 rB) = amm.getReserves();
        if (rA == 0 || rB == 0) return true;
        // Price = rB / rA. Check it has not moved >50% from initialisation.
        // This is a simplified example — production invariants use
        // time-weighted averages.
        uint256 price = (rB * 1e18) / rA;
        return price >= 0.5e18 && price <= 2e18;
    }
}

Common vault invariants include: totalSupply of share tokens equals the sum of individual balances; shares can always be redeemed for proportional underlying; and deposits increase shares by the correct amount. ERC-4626 vaults define standard solvency properties. “Total shares = sum of individual shares” is a seemingly obvious invariant — yet violations occur through rounding errors, donation attacks, or inflation attacks.

Corpus Seeding and Coverage Guidance

One of Echidna’s most powerful features — and the one most frequently underused — is its corpus mechanism.

After finishing a campaign, Echidna can save a coverage-maximising corpus in a special directory specified with the corpusDir config option. This directory will contain two entries: (1) a directory named coverage with JSON files that can be replayed by Echidna and (2) a plain-text file named covered.txt, a copy of the source code with coverage annotations.

Using coverage feedback, Echidna evolves test cases to explore new code paths and maximise the testing surface area.

How corpus seeding improves coverage

Cold-start fuzzing is inefficient. If a critical invariant can only be violated after a 10-step sequence beginning with a specific initialisation call, a purely random fuzzer may never find it within a reasonable time budget. Corpus seeding bypasses this:

Use known inputs to generate new inputs. If you have access to a large dataset of valid input, your fuzzer can generate new inputs from them, rather than starting from scratch for each generation. These are usually called seeds.

In practice, the workflow is:

  1. Run a short exploration campaign with testMode: exploration to build an initial corpus.
  2. Inspect covered.txt to identify uncovered branches.
  3. Manually add JSON transaction files to corpus/coverage/ that exercise those branches.
  4. Re-run in property mode with the seeded corpus.

By modifying a corpus file to call magic(42,129,333,0) and re-running Echidna, the property is violated immediately — where it would have been practically impossible for the random fuzzer to stumble upon those exact values by chance.

Coverage annotations

The covered.txt file uses line markers to signal execution outcomes:

Echidna signals each execution trace in the corpus with the following line markers: * if an execution ended with a STOP, r if an execution ended with a REVERT, o if an execution ended with an out-of-gas error, and e if an execution ended with any other error (zero division, assertion failure, etc).

A branch annotated only with r markers means every execution that reached it reverted — a strong signal that the path leading there is gated by a require that your current seeds never satisfy. This tells you exactly where to focus your manual seeding effort.

Interpreting Echidna Output and Triaging Failures

Reading the terminal UI

During a live campaign, Echidna’s terminal shows:

  • Property name and current status: fuzzing, shrinking, solved, passed, or error
  • Calls/Total calls — useful indicators of the testing process’s intensity and coverage, helping you understand how thoroughly your smart contract is being tested and whether the testing is aligning with your configured parameters.
  • Seed — the specific value of the seed is important for reproducibility. If you encounter a particular bug or issue while testing with Echidna, using the same seed value allows you to reproduce the exact sequence of inputs that led to that issue. This is essential for debugging and fixing vulnerabilities in your contract.

When a property fails

If a boolean property fails due to a revert, Echidna will display “Property X FAILED! with ErrorRevert”; otherwise, it should show “Property X FAILED! with ErrorReturnFalse”.

The distinction matters. ErrorReturnFalse means your invariant function returned false — the condition you asserted is genuinely violated. ErrorRevert can mean the invariant itself panicked, which sometimes indicates a bug in the test harness rather than the contract under test.

Echidna provides automatic test case minimization for quick triage. After identifying a violation, it enters shrinking mode and iteratively removes calls from the sequence until it can no longer do so without making the property pass. What you receive is the minimum reproducible call sequence — often just two or three calls.

A worked triage example

echidna_protocol_solvent: failed!💥
  Call sequence:
    1. deposit(10000000000000000000) from 0x10000
    2. borrow(9500000000000000000) from 0x10000
    3. accrueInterest() from 0x30000
    4. liquidate(0x10000, 9000000000000000000) from 0x20000
  Seed: -4823016740927195938

How to read this:

  1. Alice deposits 10 ETH.
  2. Alice borrows 9.5 ETH (95% utilisation — near the liquidation threshold).
  3. Anyone calls accrueInterest(), which increases the outstanding debt.
  4. Bob liquidates Alice’s position with a partial liquidation.

The solvency invariant breaks after step 4. The trace tells you to look at the accounting inside liquidate(): after a near-max-utilisation partial liquidation following an interest accrual, the protocol’s totalSupplied accounting falls below totalBorrowed. This is a real category of bug in production lending protocols.

Confirming in Foundry

Once Echidna gives you the minimal sequence, reproduce it as a Foundry test:

function test_echidna_repro_solvency() public {
    vm.prank(alice);
    pool.deposit(10e18);

    vm.prank(alice);
    pool.borrow(9.5e18);

    pool.accrueInterest(); // permissionless

    vm.prank(bob);
    pool.liquidate(alice, 9e18);

    assertGe(pool.totalSupplied(), pool.totalBorrowed());
}

This failing Foundry test is now part of your regression suite. The Echidna campaign found the bug; the unit test locks it in permanently.

Combining Echidna with Manual Review

Echidna is not a replacement for manual code review. The two are complementary in ways that are worth being explicit about.

What Echidna does well:

  • Discovers violations of properties you correctly specified.
  • Explores long call sequences that humans would not conceive of.
  • Finds arithmetic edge cases (rounding errors, overflow near boundaries).
  • Reproduces known exploit patterns if given an optimization objective.

What manual review does well:

  • Identifies entire classes of missing properties (the bug Echidna would have found if only you’d thought to write the right invariant).
  • Audits trust assumptions and external call risks (oracle manipulation, callback re-entrancy at the protocol level).
  • Evaluates economic incentive alignment that has no clean Solidity expression.

Trail of Bits used Echidna in exploration mode to broadly cover the Curvance codebase, and then moved into assertion mode, using anywhere from 10 million to 100 billion iterations during their engagement. The lesson is that fuzzing campaigns should run alongside, not after, manual review — the two feedback loops inform each other. A manual reviewer reading a module will identify invariants worth testing; Echidna breaking those invariants will direct the reviewer back to the specific code paths that deserve deeper scrutiny.

A pragmatic integration looks like:

Manual review phase 1 (architecture + trust boundaries)
    ↓
Write initial Echidna property suite
    ↓
Run exploration mode → inspect covered.txt → seed corpus
    ↓
Run property mode (24h+)
    ↓
Triage any failures → manual root cause analysis
    ↓
Manual review phase 2 (focused on uncovered branches + failure sites)
    ↓
Extend property suite → re-run

Integrate Echidna tests into your regular development workflow to catch vulnerabilities early. Use Echidna in conjunction with other testing and analysis tools for comprehensive contract security.

The introduction of new features in Echidna, such as on-chain contract retrieval and multicore fuzzing, opens up new ways of improving the security of your code in real-world scenarios. Adding fuzz tests into your project improves the security of your code by covering edge cases that may be overlooked by unit or integration tests.

The Limits of Fuzzing

Knowing what fuzzing cannot do is as important as knowing what it can.

Completeness is not guaranteed

Echidna might not find all vulnerabilities. Since fuzz testing can’t guarantee complete coverage, it’s crucial to augment Echidna with other security testing methods like static analysis, formal verification, and even unit testing (e.g., 100% branch coverage, testing for edge cases, positive and negative tests), for a comprehensive analysis.

A passing Echidna campaign means: “I could not find a counterexample within testLimit executions.” It does not mean “no counterexample exists.” The difference matters at the level of security guarantees.

The magic number problem

Some bugs are only reachable through inputs with specific bit patterns — a hardcoded admin address, a specific timestamp, a storage slot aligned to a particular hash. Random mutation has negligible probability of hitting these. For such cases, a symbolic execution tool like Manticore or Halmos is the right complement. This is hard for a pure fuzzer; it is recommended to use a symbolic execution tool like Manticore for such cases.

The property specification problem

The hardest limit is not technical. Echidna can only falsify properties you write. If your mental model of the protocol is wrong — if you believe healthFactor >= 1 is the right solvency condition when the real condition is subtler — then Echidna will dutifully verify that wrong property and tell you everything is fine.

Determining the best amount of time to run a fuzzer is still an open research question; however, monitoring the code coverage of your smart contracts can be a good way to determine if the fuzzing campaign should be extended.

Economic attacks are partially out of scope

Fuzzing explores Solidity state space within one forked chain environment. It does not model multi- chain or cross-contract interactions. Exploits that depend on MEV, timing between blocks, or interaction with live Chainlink oracles at specific prices are outside what Echidna can test in isolation. Testing these scenarios requires a fork-based setup and, ultimately, economic simulation that fuzzing does not replace.

Echidna Audit Checklist

Setup and configuration

  • echidna.yaml is committed with testLimit set to at least 50,000 for pre-audit runs
  • corpusDir is configured to persist interesting sequences across runs
  • workers is set to use available CPU cores
  • seqLen is long enough to reach multi-step exploit paths (≥ 20 for DeFi protocols)

Property design

  • Conservation invariants are defined: totalSupply == sum(balances), totalAssets >= totalDebt
  • Solvency invariants are defined: no position with HF < 1 can exist unliquidated
  • Access control invariants verify that no unprivileged address can reach admin functions
  • Rounding direction invariants confirm the protocol never pays out more than it receives

Testing mode selection

  • assertion mode is enabled for contracts that use assert() defensively in production logic
  • property mode is used for complex invariants that require cross-function state checks
  • optimization mode is used when maximizing attacker profit is a useful signal

Coverage and corpus

  • After the campaign, the coverage report is reviewed — critical branches must be covered
  • Handler functions are used to ensure the fuzzer reaches realistic state transitions
  • Ghost variables track expected aggregate state for conservation checks
  • Seed corpus is seeded with realistic initial states (non-empty pools, outstanding borrows)

Triage and CI

  • All property failures have been investigated before merging
  • Failing call sequences are replayed with verbose output to confirm the violation
  • Echidna runs in CI on every PR touching core protocol logic