What Medusa Is and Why It Exists

Medusa is a cross-platform go-ethereum-based smart contract fuzzer inspired by Echidna. It was built by Trail of Bits from the ground up to address architectural limitations that had accumulated in Echidna as protocols grew more complex. Medusa is based on Trail of Bits’ first fuzzer, Echidna, and their experience performing countless security reviews on blockchain systems. With features that make fuzzing more scalable and efficient, Medusa represents a significant leap forward in how developers and security engineers approach smart contract fuzzing.

Trail of Bits has since made their primary focus explicit: while they will continue maintaining Echidna for minor bug fixes, their primary focus now shifts to Medusa’s evolution.

The high-level pitch is straightforward. Medusa’s first major release introduces coverage-guided fuzzing for efficient contract exploration, parallel fuzzing that scales seamlessly with your hardware, smart mutational value generation that leverages runtime values and insights from Slither to optimize fuzzing inputs, on-chain fuzzing that seeds the fuzzing state with values fetched directly from the blockchain, and enhanced debugging capabilities that provide rich execution traces and advanced reporting.


Architecture: How Medusa Differs from Echidna

The most important architectural differences between the two tools are the implementation language, the EVM backend, and the parallelism model.

Language and Runtime

Echidna is a Haskell program designed for fuzzing and property-based testing of Ethereum smart contracts. Haskell’s lazy evaluation and purely functional model make certain algorithmic patterns elegant, but they also impose real constraints on multi-core parallelism and native interoperability with Go-centric tooling ecosystems.

Medusa offers distinct advantages over Echidna. Written in Go, this improves Medusa’s maintainability and allows for a native API, facilitating its integration into other projects. Built on Geth, this ensures strong EVM equivalence and eases code maintenance for Medusa.

This is not a cosmetic difference. Go’s goroutine model maps naturally to the worker-based parallelism that Medusa uses, and the native Go API allows embedding the fuzzer directly into custom toolchains without shell subprocess gymnastics.

EVM Backend

Echidna’s EVM execution layer is hevm, a Haskell-native symbolic EVM. While powerful for certain use cases, hevm can diverge from production Geth behavior in subtle ways involving gas accounting and opcode edge cases. Medusa, by contrast, is powered by a fork of go-ethereum — medusa-geth — which means its execution semantics track mainnet Geth closely. Building on Geth ensures strong EVM equivalence and eases code maintenance for Medusa.

Worker-Based Parallelism

This is where the architecture diverges most sharply from Echidna’s model. Each FuzzerWorker has its own isolated TestChain instance with no shared state. There is no global lock over a single chain instance. Every worker maintains its own in-memory chain, which means additional CPU cores translate directly into additional throughput without coordination overhead.

Workers are periodically destroyed and recreated (WorkerResetLimit) to prevent memory bloat from geth’s state accumulation. This is a practical necessity: go-ethereum’s state trie grows monotonically unless explicitly pruned. The reset cycle allows each worker to shed accumulated state without terminating the campaign.

Eventually, a worker hits the config-defined reset limit for how many sequences it should process, and destroys itself to free all memory, expecting the Fuzzer to respawn another in its place.

The Go-Level Testing API

Medusa provides parallelized fuzz testing of smart contracts through CLI, or its Go API that allows custom user-extended testing methodology. This is a capability Echidna simply does not offer. With the Go API, a security engineer can register custom test functions in Go, plug into the fuzzer’s event lifecycle, and build bespoke reporting pipelines without modifying the fuzzer’s source.

The FuzzerHooks object provides customization points: NewCallSequenceGeneratorConfigFunc for customizing sequence generation strategy, NewShrinkingValueMutatorFunc for customizing shrinking heuristics, ChainSetupFunc for customizing deployment and initialization logic, and CallSequenceTestFuncs[] for registering test functions to run after each sequence.

Echidna’s testing interface is exclusively Solidity-native. Properties must be expressed as on-chain view functions, and the harness is itself a Solidity contract. This is ergonomic for simple invariants but becomes a bottleneck when the test setup requires conditional deployment logic or when the verifier needs data that is not reachable from within the EVM.


The Corpus and Mutation Model

Understanding what Medusa stores in its corpus — and how it mutates those entries — is essential to understanding why it outperforms pure random approaches on complex protocols.

What the Corpus Holds

The corpus is a structure that holds “interesting” or “coverage-increasing” call sequences. When Medusa runs, if it finds a call sequence that increased its coverage of the system, it will add it to the corpus.

The corpus directory determines where corpus items should be stored on disk. A corpus item is a sequence of transactions that increased Medusa’s coverage of the system. These corpus items are valuable to store so that they can be re-used for the next fuzzing campaign. Additionally, the directory will also hold coverage reports, which is a valuable tool for debugging and validation.

This persistence model means campaigns compound. A campaign that ran overnight carries its discovered sequences into the next day’s run, and the fuzzer begins from a warmer starting position rather than cold-starting each time.

Coverage Tracking Mechanics

Coverage is a measure of what parts of the code have been executed by the fuzzer. For each target contract, Medusa maintains a byte array where the length of the byte array is equal to the length of that contract’s bytecode. If a certain transaction caused it to execute an opcode that had not been executed before, coverage of that contract increased.

Medusa uses code coverage information to guide the fuzzing process, tracking which branch conditions have been evaluated to true or false (branch coverage), and recording function coverage. Branch coverage is particularly important for DeFi protocols because the interesting state transitions — liquidation thresholds crossed, price deviations exceeding bounds, collateral factors hit — are almost universally guarded by conditional branches.

Mutation Strategies

Sequences are mutated using weighted strategies: corpus head, corpus tail, splice, interleave, and new. These strategies operate at the call-sequence level:

  • Corpus head/tail: Take the first or last portion of an existing high-value sequence and extend it with new calls.
  • Splice: Combine a prefix from one corpus sequence with a suffix from another.
  • Interleave: Merge two corpus sequences, alternating calls from each.
  • New: Generate a completely fresh random sequence.

The reason Medusa re-uses call sequences is that it knows the sequence in question improved coverage. So, it re-uses it, mutates it, and then executes that mutated call sequence in hopes of further increasing coverage. There are a variety of mutational strategies that Medusa employs. For example, Medusa can take a call sequence from the corpus and append a new random transaction at the end of it.

The weighting of these strategies matters. Medusa fixes the weighting of corpus items to use timestamps to favor “hardest-to-discover” inputs. Sequences that were difficult to evolve organically are promoted in the mutation queue, concentrating compute on the edges of the explored state space.

Corpus Pruning

A corpus pruner periodically removes redundant sequences to keep the corpus lean. This prevents the corpus from growing without bound and degrading mutation quality. The pruner is configured via pruneFrequency and ensures that sequences that have become redundant — because their covered paths are now also covered by shorter sequences — are evicted.

Value Generation

Beyond sequence-level mutation, Medusa applies value-level mutation to individual call arguments. Medusa seeds the value set by extracting constants and important values from contracts using both AST analysis and Slither (if available), generates random values of appropriate types for function parameters, mutates previously successful values to explore adjacent states, and uses feedback from execution to solve for values that reach specific code paths.

Smart mutational value generation leverages runtime values and insights from Slither to optimize fuzzing inputs. In practice this means that address literals found in the contract source, magic numbers used as thresholds, and slot values observed during execution all feed back into the value pool that generates future transaction arguments.


Writing Properties in Medusa

Medusa supports three categories of tests, all expressed in Solidity: property tests, assertion tests, and optimization tests.

Property Tests

The PropertyTestCaseProvider calls property test functions (prefix-based naming, and these must be view functions returning bool). If a property returns false, the test fails.

Properties must be prefixed with property_ by default (configurable in medusa.json). The function signature is identical to Echidna’s echidna_ prefix convention, with the sole difference being the prefix string. This makes migrating an existing Echidna harness to Medusa largely a search-and-replace operation.

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

/// @dev Medusa property harness for an AMM pool
contract AMMFuzzTest {
    IPool public pool;
    IERC20 public tokenA;
    IERC20 public tokenB;

    uint256 constant INITIAL_LIQUIDITY = 1_000_000e18;

    constructor() {
        // Deploy and seed the pool
        tokenA = new MockERC20("Token A", "TKA", 18);
        tokenB = new MockERC20("Token B", "TKB", 18);
        pool   = new UniswapV2StylePool(address(tokenA), address(tokenB));

        tokenA.mint(address(this), INITIAL_LIQUIDITY);
        tokenB.mint(address(this), INITIAL_LIQUIDITY);
        tokenA.approve(address(pool), type(uint256).max);
        tokenB.approve(address(pool), type(uint256).max);
        pool.addLiquidity(INITIAL_LIQUIDITY, INITIAL_LIQUIDITY);
    }

    // ── Fuzz helpers (callable by Medusa) ────────────────────────────────

    function swap(uint256 amountIn, bool zeroForOne) external {
        amountIn = bound(amountIn, 1, 1e24);
        address tokenIn  = zeroForOne ? address(tokenA) : address(tokenB);
        address tokenOut = zeroForOne ? address(tokenB) : address(tokenA);
        IERC20(tokenIn).mint(address(this), amountIn);
        IERC20(tokenIn).approve(address(pool), amountIn);
        pool.swap(amountIn, zeroForOne, address(this));
    }

    // ── Properties ───────────────────────────────────────────────────────

    /// @notice The constant-product invariant k = reserveA * reserveB must
    ///         never decrease after any swap (fees only increase k).
    function property_k_never_decreases() external view returns (bool) {
        (uint256 rA, uint256 rB) = pool.getReserves();
        return rA * rB >= INITIAL_LIQUIDITY * INITIAL_LIQUIDITY;
    }

    /// @notice No single swap should drain more than 30% of either reserve.
    function property_no_reserve_drain() external view returns (bool) {
        (uint256 rA, uint256 rB) = pool.getReserves();
        return rA >= INITIAL_LIQUIDITY * 70 / 100
            && rB >= INITIAL_LIQUIDITY * 70 / 100;
    }
}

Assertion Tests

The AssertionTestCaseProvider monitors EVM-level panic conditions for each contract method — such as assert(), arithmetic underflow or overflow, divide by zero, and array access violations. Which panic codes trigger test failures is configured via PanicCodeConfig in FuzzingConfig.Testing.AssertionTesting.

Assertion testing is zero-overhead for the property author: simply assert() invariants directly in function bodies, and Medusa will treat any panic as a test failure automatically. This is particularly useful for arithmetic libraries where the invariant is inherent to the computation rather than an external predicate.

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

contract MathFuzzTest {
    using FixedPointMath for uint256;

    uint256 constant WAD = 1e18;

    /// @notice mulWad must be commutative.
    function assertMulWadCommutative(uint256 x, uint256 y) external pure {
        x = bound(x, 0, 1e36);
        y = bound(y, 0, 1e36);
        assert(x.mulWad(y) == y.mulWad(x));
    }

    /// @notice divWad followed by mulWad must recover the original value
    ///         within 1 wei of rounding error.
    function assertDivMulRoundTrip(uint256 x, uint256 divisor) external pure {
        divisor = bound(divisor, 1, 1e36);
        x       = bound(x, 0, 1e36);
        uint256 divided    = x.divWad(divisor);
        uint256 recovered  = divided.mulWad(divisor);
        uint256 delta      = x > recovered ? x - recovered : recovered - x;
        assert(delta <= 1);
    }
}

Optimization Tests

The OptimizationTestCaseProvider tracks optimization targets — such as maximizing gas usage — and shrinks sequences to find minimal paths to those targets. This mode is less commonly used for correctness testing but is invaluable for gas optimization regressions and for modeling attacker profit functions.


Coverage-Guided Fuzzing: The Mechanics

The loop that makes Medusa materially better than black-box random fuzzing at scale is straightforward to describe but deeply consequential in practice.

The reason Medusa re-uses call sequences is that it knows the call sequence in question improved coverage. So, it re-uses it, mutates it, and then executes that mutated call sequence in hopes of further increasing coverage.

At each iteration a FuzzerWorker does one of two things: it either generates a completely random new sequence, or it selects a sequence from the corpus, applies one of the weighted mutation strategies, and executes the result. If the execution touches any bytecode offset that has not been reached before, the sequence is eligible for corpus admission. The worker updates the total CoverageMaps and corpus with the current CallSequence if the most recent call increased coverage.

The fuzzer maintains EVM state for the duration of a call sequence before resetting the state. If a call sequence length of 10 is set, Medusa will execute 10 transactions, maintain state throughout that process, and then wipe the EVM state.

This design has an important implication for multi-step exploit paths. A sequence that calls deposit, then borrow, then manipulateOracle, then liquidate can only reach the liquidation branch if the first three calls have established the correct preconditions. A purely random fuzzer must stumble on this entire chain by chance. Medusa’s corpus, on the other hand, may have already stored deposit → borrow as a coverage-increasing prefix, and mutation then appends manipulateOracle → liquidate to that warm prefix — dramatically reducing the search space.

Shrinking Failing Sequences

When a property violation is found, Medusa immediately attempts to minimize the reproducing sequence. When a test fails, a ShrinkCallSequenceRequest is generated. The worker iteratively removes and mutates calls while a VerifierFunction confirms the test still fails, producing a minimal reproduction.

The shrunk sequence is what gets presented to the engineer. Instead of a 50-call trace where 40 calls are noise, you receive a 3- or 4-call sequence that precisely isolates the state transition causing the violation. This is the difference between a useful bug report and an inscrutable dump.


Configuring Medusa for Complex DeFi Protocols

Run medusa init to scaffold a medusa.json file. The key configuration surface for a complex DeFi protocol looks like this:

{
  "fuzzing": {
    "workers": 8,
    "workerResetLimit": 50,
    "timeout": 0,
    "testLimit": 0,
    "callSequenceLength": 50,
    "corpusDirectory": "corpus",
    "coverageEnabled": true,
    "targetContracts": ["ProtocolInvariantTest"],
    "deployerAddress": "0x10000",
    "senderAddresses": [
      "0x10000",
      "0x20000",
      "0x30000"
    ],
    "blockNumberDelayMax": 100,
    "blockTimestampDelayMax": 86400,
    "transactionGasLimit": 15000000,
    "testing": {
      "stopOnFailedTest": false,
      "testAllContracts": false,
      "propertyTesting": {
        "enabled": true,
        "testPrefixes": ["property_"]
      },
      "assertionTesting": {
        "enabled": true,
        "panicCodeConfig": {
          "failOnCompilerInsertedPanic": true,
          "failOnAssertion": true,
          "failOnArithmeticUnderflow": true,
          "failOnDivideByZero": true,
          "failOnInvalidShiftOperation": true,
          "failOnOutOfBoundsArrayAccess": true,
          "failOnAllocateTooMuchMemory": true,
          "failOnCallUndefinedPublicFunction": true
        }
      }
    }
  },
  "slither": {
    "useSlither": true,
    "cacheEnabled": true
  }
}

Key Parameters Explained

workers: The number of parallel FuzzerWorker goroutines. Set this to the number of available CPU cores. The Workers field describes the number of parallel fuzzing workers to spawn.

workerResetLimit: The WorkerResetLimit describes how many call sequences a worker should test before it is destroyed and recreated so that memory from its underlying chain is freed. Setting this value too high will result in the in-memory chain’s database growing to a size that is slower to process. Setting it too low may result in frequent worker resets that are computationally expensive for complex contract deployments that need to be replayed during worker reconstruction.

callSequenceLength: Describes the maximum length a transaction sequence can be generated as. For DeFi protocols where exploits require several setup transactions before the vulnerability is triggered, set this to 30–100. After every callSequenceLength function calls, the blockchain is reset for the next sequence of transactions.

blockNumberDelayMax / blockTimestampDelayMax: Defines the maximum block number jump the fuzzer should make between test transactions. The fuzzer will use this value to make the next block’s block.number between 1 and blockNumberDelayMax more than that of the previous block. Jumping block.number allows Medusa to enter code paths that require a given number of blocks to pass. Time-locked governance actions, vesting schedules, and TWAP oracle freshness checks all depend on these parameters.

testLimit / timeout: By default, testLimit is set to 0, which means that Medusa will run indefinitely. For nightly CI runs, set timeout (in seconds) rather than testLimit, so the campaign runs for a fixed wall-clock window regardless of throughput.

On-Chain Fuzzing

Medusa can now run starting with an existing state provided by an external RPC service such as Infura, Alchemy, or a local node. This enables users to speed up the fuzzing setup when using already deployed contracts. For a protocol that has significant on-chain state — liquidity positions, outstanding borrows, accumulated fees — forking from a mainnet block positions the fuzzer in a realistic environment immediately rather than requiring the harness to painstakingly reconstruct that state synthetically.

Pass --rpc-url and --rpc-block on the CLI or configure them in the chain section of medusa.json.


Interpreting Medusa Output and Triaging Failures

Reading the Terminal Output

Medusa emits a live status line showing calls per second, corpus size, unique coverage points, and the number of failing tests found. When a property violation occurs, it prints the failing sequence with configurable verbosity:

  • -v: Shows only top-level transactions in the execution trace.
  • -vv: Shows nested calls with standard detail and is the default behavior.
  • -vvv: Shows all call sequence elements with maximum detail, attaching traces to every call in the sequence.

For DeFi triage, start with -vvv. Multi-hop delegate calls and token callbacks are invisible at lower verbosity levels and are exactly where the interesting state mutations tend to occur.

The HTML Coverage Report

Medusa generates an HTML coverage report in the corpusDirectory after each campaign. The report maps covered and uncovered bytecode back to source lines. The directory will also hold coverage reports, which is a valuable tool for debugging and validation. If an entire branch of your liquidation logic is uncovered after a 24-hour campaign, the issue is almost always in the harness — the fuzzer cannot reach that branch because no function in the harness sets up the preconditions that enable it.

Triage Workflow

  1. Examine the shrunk sequence first. The minimizer has already removed noise. Each call in the shrunk sequence is load-bearing.
  2. Replay with -vvv. Inspect the return values and storage slots touched at each step.
  3. Add emit statements to the harness. Solidity events are visible in the trace and are the recommended debugging mechanism.
  4. Check corpus health. If coverage has plateaued and no violations are found, the corpus may need seeding. Add harness helper functions that explicitly navigate to the unexplored state.
  5. Verify the property itself. A property that always returns true regardless of state is not a useful property. Medusa cannot falsify a tautology.
A campaign that finds no violations is only meaningful if the coverage report shows that all critical branches were reached. Zero violations with low coverage is not a clean bill of health — it is an incomplete test run.

Combining Medusa with Echidna in a Dual-Fuzzer Workflow

No single fuzzer catches everything. Medusa and Echidna have complementary strengths, and the most rigorous fuzzing engagements run both.

Medusa, the geth-based fuzzer, complemented Echidna in its coverage efforts for falsifying invariants on Curvance. In that real-world engagement, immediately after Medusa started running, it found a medium-severity bug in the code that Echidna had missed. Echidna eventually found this bug after the block time delay was changed, likely due to the fuzzer’s non-determinism. The first Medusa run of 48+ hours resulted in a medium-severity bug.

A practical dual-fuzzer CI pipeline looks like this:

# ── Stage 1: Smoke test on every commit ──────────────────────────────────
forge test --fuzz-runs 10000

# ── Stage 2: Deep Medusa campaign (nightly, pre-audit) ───────────────────
medusa fuzz \
  --workers $(nproc) \
  --timeout 28800 \
  --corpus-dir corpus/ \
  --use-slither

# ── Stage 3: Targeted Echidna run on specific invariant classes ──────────
echidna . --config echidna.yaml --test-limit 500000

Why Keep Echidna?

Echidna uses sophisticated grammar-based fuzzing campaigns based on a contract ABI to falsify user-defined predicates or Solidity assertions. Its grammar-based approach can sometimes surface violations that Medusa’s corpus-mutation strategy misses, because it explores the ABI input space with a different prior. Running both ensures that neither tool’s blind spots become yours.

Without Medusa’s key features matured to full parity, some teams recommend using Foundry and Medusa alongside Echidna rather than as a complete replacement. The guidance is pragmatic: use Medusa as the primary workhorse for stateful, long-horizon campaigns, and retain Echidna for targeted invariant falsification where its ABI-grammar model performs well.

Shared Harness Architecture

The most friction-reducing approach is to write a single Solidity harness that both tools can target. The only differences are:

  • Property function prefixes (echidna_ vs property_).
  • The configuration file (echidna.yaml vs medusa.json).
  • Constructor argument passing syntax.

By keeping all the setup logic, helper functions, and ghost state tracking in a shared base contract, you get independent coverage signals from two fuzzers with minimal duplication:

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

/// @dev Shared base harness — both Echidna and Medusa inherit from this.
abstract contract LendingFuzzBase {
    LendingPool   public pool;
    PriceOracle   public oracle;
    MockERC20     public collateral;
    MockERC20     public debt;

    uint256 constant INITIAL_PRICE    = 1e18;   // 1:1
    uint256 constant MAX_LTV          = 75e16;  // 75%
    uint256 constant LIQUIDATION_BONUS = 5e16;  // 5%

    // Ghost variable: tracks total deposited collateral by this harness.
    uint256 internal _totalDeposited;

    constructor() {
        collateral = new MockERC20("WETH", "WETH", 18);
        debt       = new MockERC20("USDC", "USDC", 6);
        oracle     = new PriceOracle();
        pool       = new LendingPool(address(oracle));

        oracle.setPrice(address(collateral), INITIAL_PRICE);
        collateral.mint(address(this), 1_000_000e18);
        debt.mint(address(pool), 10_000_000e6);
        collateral.approve(address(pool), type(uint256).max);
    }

    // ── Fuzz actions ─────────────────────────────────────────────────────

    function deposit(uint256 amount) public {
        amount = _bound(amount, 1e15, 1_000e18);
        pool.deposit(address(collateral), amount);
        _totalDeposited += amount;
    }

    function borrow(uint256 amount) public {
        amount = _bound(amount, 1, 100_000e6);
        pool.borrow(address(debt), amount);
    }

    function repay(uint256 amount) public {
        uint256 outstanding = pool.debtOf(address(this));
        if (outstanding == 0) return;
        amount = _bound(amount, 1, outstanding);
        debt.mint(address(this), amount);
        debt.approve(address(pool), amount);
        pool.repay(address(debt), amount);
    }

    function shiftOracle(int256 bps) public {
        // Shift price by at most ±50%
        bps = int256(_bound(uint256(bps < 0 ? -bps : bps), 0, 5000)) * (bps < 0 ? -1 : int256(1));
        uint256 current = oracle.getPrice(address(collateral));
        uint256 next = bps < 0
            ? current * uint256(10000 + bps) / 10000
            : current * uint256(10000 + bps) / 10000;
        oracle.setPrice(address(collateral), next);
    }

    // ── Shared invariants (internal) ──────────────────────────────────────

    function _invariant_solvency() internal view returns (bool) {
        uint256 totalBorrowed  = pool.totalBorrowed();
        uint256 totalReserves  = pool.totalReserves();
        return totalReserves >= totalBorrowed;
    }

    function _invariant_no_underwater_without_liquidation() internal view returns (bool) {
        uint256 collateralValue = pool.collateralValueOf(address(this));
        uint256 debtValue       = pool.debtValueOf(address(this));
        if (debtValue == 0) return true;
        // If the position is underwater, it must be liquidatable.
        if (debtValue > collateralValue) {
            return pool.isLiquidatable(address(this));
        }
        return true;
    }

    function _bound(uint256 x, uint256 lo, uint256 hi) internal pure returns (uint256) {
        if (lo >= hi) return lo;
        return
lo + (x % (hi - lo));
    }
}

The _bound helper mirrors Foundry’s bound() cheatcode, giving Medusa the same input-bounding capability without any framework dependency. Once the corpus has accumulated meaningful coverage, switching _bound parameters to tighter ranges focuses the fuzzer on the most financially sensitive region of the input space.


Medusa Audit Checklist

Setup and configuration

  • medusa.json is committed to the repository with testLimit set to at least 100,000
  • corpusDir is configured so that seed coverage persists across CI runs
  • assertionTesting and propertyTesting are both enabled
  • forkConfig is set if the protocol interacts with deployed mainnet contracts

Property design

  • Conservation invariants are implemented as property_* functions returning bool
  • Solvency invariants (total assets ≥ total liabilities) are explicitly tested
  • 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

Handler and corpus

  • All state-mutating protocol functions are reachable from the fuzzer’s call sequence
  • Input parameters are bounded with _bound() to exclude impossible states
  • Ghost variables track aggregate state for conservation checks
  • Seed corpus includes edge cases: zero amounts, maximum amounts, single-user pools

Triage and CI

  • All property failures have been investigated before merging
  • Medusa runs on every PR touching core arithmetic or state-transition logic
  • Counterexamples are stored as regression tests in the test suite
  • Coverage reports are reviewed to confirm all critical code paths are exercised