5 Properties Every Smart Contract Auditor Forgets to Test

After running invariant testing campaigns against 40+ DeFi protocols, we keep seeing the same gaps. Not the obvious ones — most teams do check that totalSupply == sum(balances). The gaps that hurt are subtler, and they show up in protocols that already have a solid unit test suite.

1. Token balance vs. internal accounting

The Cream Finance attack in October 2021 broke this one. The attacker manipulated the yUSD vault's price-per-share, inflated their collateral value, and borrowed against it. For a brief but profitable moment, the protocol's tracked collateral exceeded the actual token value on-chain.

The property is simple: for every token the protocol holds, the actual ERC20 balance must be ≥ the tracked liability to depositors.

function property_token_balance_covers_liabilities() public returns (bool) {
    address[] memory tokens = protocol.getTrackedTokens();
    for (uint256 i = 0; i < tokens.length; i++) {
        uint256 actualBalance = IERC20(tokens[i]).balanceOf(address(protocol));
        uint256 trackedLiability = protocol.totalLiability(tokens[i]);
        if (actualBalance < trackedLiability) return false;
    }
    return true;
}

It gets skipped because developers check it implicitly: "if withdrawals work, we're fine." That's not the same as an invariant. The implicit check only fires on the happy path.

One caveat worth writing in: dust amounts from rounding, fee-on-transfer tokens, and rebasing tokens can all trigger a strict >= check when nothing is actually wrong. actualBalance + DUST_TOLERANCE >= trackedLiability is usually the right threshold.

2. Privilege escalation

Unit tests for access control check individual functions. They don't check whether a multi-step sequence of legitimate-looking calls can escalate privileges through composition.

Compound's governance exploit in 2021 is the reference case. A proposal passed that upgraded the comptroller and transferred funds to arbitrary addresses. The access control on each individual function was fine. The vulnerability was in how governance actions composed together.

function property_no_privilege_escalation() public returns (bool) {
    for (uint256 i = 0; i < actors.length; i++) {
        address actor = actors[i];
        if (isInitialAdmin[actor]) continue;

        if (protocol.hasRole(ADMIN_ROLE, actor)) return false;
        if (protocol.hasRole(MINTER_ROLE, actor)) return false;
        if (protocol.owner() == actor) return false;
    }
    return true;
}

Run this after every state-changing handler, not just after governance calls. Escalation bugs are always sequence-dependent; a single call won't grant it, but a specific three-step sequence might. The fuzzer needs to see the full call history to find it.

Get a full invariant audit of your access control

3. Monotonicity on critical counters

Some state variables should only ever move in one direction. totalDebt goes down on repayment, not arbitrarily. totalShares goes down on withdrawal, not on deposits. That sounds obvious, but the property is almost never written down.

A recurring bug class in rebase tokens illustrates why it matters: after an elastic supply adjustment, totalSupply briefly dips below its valid floor before snapping back. If a liquidation fires inside that window, the math uses the dipped value and the result is wrong.

// BeforeAfter struct captures pre-call values
function property_debt_monotone_outside_repayment() public returns (bool) {
    if (!_isRepaymentContext()) {
        return _after.totalDebt >= _before.totalDebt;
    }
    return true;
}

function property_shares_monotone_outside_withdrawal() public returns (bool) {
    if (!_isWithdrawalContext()) {
        return _after.totalShares >= _before.totalShares;
    }
    return true;
}

The BeforeAfter pattern is what makes these testable. Snapshot _before at the start of each handler, check _after at the end, and every non-repayment call triggers the monotonicity check automatically. It's a few lines of boilerplate that catches entire classes of bugs.

4. Oracle staleness

Developers mock oracles in tests. Mock oracles always return fresh prices. Production Chainlink aggregators go stale when gas spikes or aggregator nodes have issues, and the last reported price gets used indefinitely. On a volatile asset, a 20-minute-old price can be 15% off. Liquidations fire incorrectly (or don't fire when they should).

Compound v2 has had documented oracle issues around this. It's a solved problem at the contract level — just check updatedAt against a staleness threshold — but the check doesn't get written if the test suite never exercises a stale oracle.

function property_oracle_prices_are_fresh() public returns (bool) {
    address[] memory collaterals = protocol.getCollateralTokens();
    for (uint256 i = 0; i < collaterals.length; i++) {
        (uint256 price, uint256 updatedAt) = protocol.getPrice(collaterals[i]);
        if (price == 0) return false;
        if (block.timestamp - updatedAt > MAX_PRICE_AGE) return false;
    }
    return true;
}

function property_no_action_succeeds_with_stale_oracle() public returns (bool) {
    vm.warp(block.timestamp + MAX_PRICE_AGE + 1);
    try protocol.borrow(token, 1e18) {
        return false; // borrow succeeded with stale price — bug
    } catch {
        return true;
    }
}

In Recon's campaign runner, time-warp is a first-class fuzz dimension. The fuzzer inserts warp calls between operations automatically, which means you don't need to write explicit staleness scenarios — you just need property_oracle_prices_are_fresh running and the fuzzer finds the sequence that triggers it.

5. Liquidation health

Liquidation tests usually check one thing: did the liquidator receive the right collateral amount? They rarely check whether the borrower's remaining position is actually in a safe zone after the liquidation.

The Aave v2 CRV situation in November 2023 is the closest real-world example. A large CRV short was partially liquidated, but the position was so oversized relative to market liquidity that each liquidation move barely moved the health factor. The protocol let liquidations proceed that didn't materially improve position health. Not a code bug exactly, but an invariant violation that surfaces hidden assumptions about market depth.

For most lending protocols, a health invariant catches more concrete bugs: partial liquidations with wrong bonus calculations that leave health factor at 0.99 (still under 1.0), rounding on collateral seizure that makes health factor slightly worse after liquidation (rare, but I've seen it), or bad oracle prices that make a position appear healthy post-liquidation when it isn't.

function property_liquidation_improves_health() public returns (bool) {
    for (uint256 i = 0; i < liquidatedActors.length; i++) {
        address actor = liquidatedActors[i];
        uint256 postHealthFactor = protocol.healthFactor(actor);

        if (protocol.borrowBalance(actor) > 0) {
            if (postHealthFactor < LIQUIDATION_THRESHOLD) return false;
        }
    }
    return true;
}

Track which actors were liquidated during the sequence rather than checking all actors after every call. Checking all actors every time is expensive and produces false positives when an unrelated actor has a legitimately unhealthy position.

The one property to start with

If you're only going to write one invariant for a protocol that handles multiple users, write this:

function property_sum_of_positions_equals_total() public returns (bool) {
    uint256 sumPositions = 0;
    for (uint256 i = 0; i < actors.length; i++) {
        sumPositions += protocol.positionOf(actors[i]);
    }
    return sumPositions == protocol.totalPositions();
}

It catches reentrancy bugs, rounding errors, off-by-one errors in storage, and silent overflow/underflow — all from one property. The five above are important, but this one is the foundation.

The Recon Book's property design chapter covers all of these in depth with full Chimera examples and BeforeAfter boilerplate. If you want us to write and run a complete suite for your protocol, request an audit and we'll scope it within 24 hours.