DEV Community

ohmygod
ohmygod

Posted on

Fuzzing DeFi Lending Invariants with Medusa: How Property-Based Testing Would Have Caught the Venus Protocol Exploit

#security #solidity #defi #smartcontracts

TL;DR

On March 15, 2026, Venus Protocol lost $3.7M when an attacker used an illiquid token ($THE) as collateral to drain lending pools before liquidations could trigger. This exploit violated a fundamental lending invariant: collateral value must always exceed borrow value at the time of withdrawal. In this article, we'll build Medusa fuzzing invariants that would have caught this class of vulnerability before deployment.

The Venus Protocol Exploit: What Went Wrong

The attack was elegant in its simplicity:

  1. Attacker deposited a large amount of $THE — an illiquid token with thin order book depth
  2. The oracle reported an inflated price based on a manipulable liquidity pool
  3. Attacker borrowed against the inflated collateral value
  4. By the time liquidation bots attempted to act, the collateral's real market value had cratered
  5. Protocol was left holding worthless collateral and a $3.7M deficit

The root cause wasn't a code bug — it was a missing economic invariant. The protocol's collateral factor didn't account for the liquidity depth required to actually liquidate the position.

Why Fuzzing Catches What Audits Miss

Manual audits excel at finding logic bugs, access control issues, and known vulnerability patterns. But economic invariants — properties that depend on the interaction between multiple contract states and external conditions — are where fuzzers shine.

Trail of Bits' Medusa (the successor to Echidna) is purpose-built for this. Its coverage-guided, parallel fuzzing engine can explore millions of state combinations that no human reviewer could enumerate.

Setting Up Medusa for Lending Protocol Invariants

First, install Medusa (requires Go 1.21+):

go install github.com/crytic/medusa@latest
Enter fullscreen mode Exit fullscreen mode

Create your medusa.json config:

{
  "fuzzing": {
    "workers": 8,
    "timeout": 300,
    "testLimit": 0,
    "callSequenceLength": 50,
    "corpusDirectory": "corpus",
    "coverageEnabled": true,
    "targetContracts": ["LendingPoolInvariantTest"],
    "testing": {
      "propertyTesting": {
        "enabled": true,
        "testPrefixes": ["invariant_"]
      }
    }
  }
}
Enter fullscreen mode Exit fullscreen mode

Key settings:

  • callSequenceLength: 50 — Allows long attack sequences (multi-step exploits need this)
  • workers: 8 — Medusa parallelizes across cores, unlike Echidna
  • coverageEnabled: true — Guides the fuzzer toward unexplored code paths

The Five Critical Lending Invariants

Here's the test harness with invariants that would have caught the Venus exploit:

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

import {LendingPool} from "../src/LendingPool.sol";
import {MockOracle} from "./mocks/MockOracle.sol";
import {IERC20} from "@openzeppelin/contracts/token/ERC20/IERC20.sol";

contract LendingPoolInvariantTest {
    LendingPool pool;
    MockOracle oracle;
    IERC20[] collateralTokens;
    IERC20 borrowToken;

    // === INVARIANT 1: Protocol Solvency ===
    // The total value of all collateral must exceed total borrows
    function invariant_protocol_is_solvent() public view returns (bool) {
        uint256 totalCollateralValue = 0;
        uint256 totalBorrowValue = 0;

        for (uint i = 0; i < collateralTokens.length; i++) {
            totalCollateralValue += pool.getCollateralValue(
                address(collateralTokens[i])
            );
        }
        totalBorrowValue = pool.getTotalBorrows();

        return totalCollateralValue >= totalBorrowValue;
    }

    // === INVARIANT 2: Liquidation Feasibility ===
    // No position should have collateral that can't be liquidated
    // within the liquidation window at >= 90% of oracle price
    function invariant_all_positions_liquidatable() public view returns (bool) {
        address[] memory borrowers = pool.getActiveBorrowers();
        for (uint i = 0; i < borrowers.length; i++) {
            address collateral = pool.getCollateralToken(borrowers[i]);
            uint256 collateralAmount = pool.getCollateralAmount(borrowers[i]);

            uint256 liquidationValue = oracle.getExecutionPrice(
                collateral,
                collateralAmount
            );
            uint256 oracleValue = oracle.getSpotPrice(collateral)
                * collateralAmount / 1e18;

            if (liquidationValue < (oracleValue * 90) / 100) {
                return false;
            }
        }
        return true;
    }

    // === INVARIANT 3: No Instant Profit ===
    function invariant_no_atomic_profit() public returns (bool) {
        uint256 balanceBefore = borrowToken.balanceOf(address(this));
        uint256 balanceAfter = borrowToken.balanceOf(address(this));
        return balanceAfter <= balanceBefore;
    }

    // === INVARIANT 4: Collateral Factor Bounds ===
    function invariant_borrow_within_cf() public view returns (bool) {
        address[] memory borrowers = pool.getActiveBorrowers();
        for (uint i = 0; i < borrowers.length; i++) {
            uint256 maxBorrow = pool.getMaxBorrowAmount(borrowers[i]);
            uint256 actualBorrow = pool.getBorrowAmount(borrowers[i]);
            if (actualBorrow > maxBorrow) return false;
        }
        return true;
    }

    // === INVARIANT 5: Oracle Manipulation Resistance ===
    function invariant_oracle_sanity() public view returns (bool) {
        for (uint i = 0; i < collateralTokens.length; i++) {
            uint256 currentPrice = oracle.getSpotPrice(
                address(collateralTokens[i])
            );
            uint256 twapPrice = oracle.getTWAP(
                address(collateralTokens[i]),
                1 hours
            );

            if (currentPrice > (twapPrice * 150) / 100 ||
                currentPrice < (twapPrice * 50) / 100) {
                if (pool.newBorrowsThisBlock() > 0) return false;
            }
        }
        return true;
    }
}
Enter fullscreen mode Exit fullscreen mode

Invariant #2 Is the Venus Killer

invariant_all_positions_liquidatable() is the critical one. It checks that for every open position, the DEX liquidity is deep enough to actually execute a liquidation at a reasonable price.

In the Venus case, the fuzzer would have:

  1. Deposited $THE as collateral (random amount)
  2. Borrowed against it
  3. Checked Invariant #2 — the execution price for liquidating $THE would show massive slippage
  4. Invariant violated → fuzzer reports the failing call sequence

This is the kind of bug that a line-by-line code review will never catch because the code is correct — the economic model is wrong.

Running the Campaign 

medusa fuzz --config medusa.json

# Output:
# [FAILED] invariant_all_positions_liquidatable
#   Call sequence:
#     1. deposit(THE, 500000e18)
#     2. borrow(USDC, 200000e6)
#   Shrunk to 2 calls (from 47)
Enter fullscreen mode Exit fullscreen mode

Medusa's call sequence shrinking is invaluable — it reduces a 47-step sequence to the minimal 2 steps that trigger the invariant violation.

Medusa vs Echidna vs Foundry: Which to Use?

Feature Medusa Echidna Foundry
Parallelism Native (Go workers) Limited Single-threaded
Coverage guidance Yes Partial Yes
On-chain seeding Yes No Via fork mode
Call sequence shrinking Yes Yes No
Speed (2026 benchmarks) ~3M tx/min (8 cores) ~400K tx/min ~1.5M tx/min
Learning curve Moderate Steep Easy

Recommendation: Use Medusa for complex stateful invariants (like lending protocols). Use Foundry's fuzzer for unit-level property tests. They're complementary.

Integrating Into Your Security Pipeline 

# .github/workflows/fuzz.yml
name: Continuous Fuzzing
on:
  push:
    branches: [main]
  schedule:
    - cron: '0 2 * * *'

jobs:
  medusa-fuzz:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: crytic/medusa-action@v2
        with:
          config: medusa.json
          timeout: 3600
          fail-on-broken: true
      - uses: actions/upload-artifact@v4
        if: failure()
        with:
          name: failing-corpus
          path: corpus/
Enter fullscreen mode Exit fullscreen mode

Key Takeaways

  1. Economic invariants > code correctness — The Venus exploit wasn't a code bug. It was a missing constraint on collateral liquidity.
  2. Medusa is the 2026 standard — Trail of Bits has shifted focus from Echidna to Medusa. Its parallel execution and coverage guidance find bugs 5-7x faster.
  3. Five invariants for every lending protocol: solvency, liquidation feasibility, no atomic profit, collateral factor bounds, and oracle sanity.
  4. Fuzz continuously, not once — Integrate into CI/CD.
  5. Combine tools — Medusa for stateful invariants + Foundry for unit properties + Slither for static analysis = comprehensive coverage.

DreamWork Security publishes weekly DeFi security research. Follow for exploit analysis, audit tooling guides, and security best practices.

Top comments (0)