What the generated Aave v4 invariant suite actually tests, and what it cannot #405

Filed so this is not re-derived later, and so nobody reads the first completed Aave v4 run as a verdict on invariant testing that it cannot support.

The open question behind this benchmark is whether ultrafuzz with invariant testing finds bugs that the no-fuzz release configuration cannot. The strong form of that case is multi-transaction bugs: violations only reachable through a sequence of operations, which no amount of reading a single function surfaces. This note records what the pipeline actually generated when measured against that bar.

Evidence

The R52 suite from stateful-invariant-implement-properties — 13 properties, 33 KB of Properties.sol — classified by what it takes to violate each one:

Twelve of thirteen are single-state or single-call. Those are structural facts about the code, which is the class a no-fuzz agent reading the contracts can derive directly. Fuzzing confirms them; it is not what discovers them.

The math-identity group is weaker still. catalogPreviewRounding asserts hub.previewAddByAssets(...) == _mulDivDown(assets, shares + VIRTUAL_SHARES, ...) — a formula re-derived from the implementation under test. That catches divergence between two code paths; it cannot catch a wrong shared assumption.

The one temporal property is weaker than the reference's

function property_catalogAddedSharePriceNonDecreasing() public view {
    if (!_before.initialized || !_after.initialized) return;
    if (_before.activeAddedShares == 0 || _after.activeAddedShares == 0) return;
    assert(_after.activeAddedAssets * _before.activeAddedShares
        >= _before.activeAddedAssets * _after.activeAddedShares);
}

Against scfuzzbench/aave-v4-scfuzzbench's invariant_supplySharePriceAndDrawnIndexMonotonic:

1. Single-step, not ghost-max. The reference compares against ghost_maxSupplySharePriceAssetsSeen, the maximum observed across the whole sequence. Step-wise checking is equivalent only if every state transition is wrapped in __before/__after; any uninstrumented handler is a hole the reference's form would still catch later.
2. Active-asset only. _snapshot() records assetId = activeAssetIndex % assets.length and the active actor. The reference loops every asset on every check. A handler on asset A that perturbs asset B is invisible — and cross-asset effects through a shared Hub are exactly the multi-transaction class in question.

The generated BeforeAfter.sol is 45 lines with a flat 10-field struct. The reference's is 89 lines with ghost maxima, an Operation enum, and an isAnyUserLiquidatable flag.

What is absent matters most

There is no analogue of invariant_shouldNotBecomeLiquidatable — "no operation other than a price change may make a user liquidatable". That is the strongest example of the thesis: violable only by a sequence, encoding economic intent rather than code structure. The generated BeforeAfter cannot express it — no operation tracking, no liquidatable flag.

Also absent: the reference's deliberate v0/v1/v2 formulations of the solvency invariant, which is how the auditors' and the protocol team's competing definitions were surfaced as a disagreement rather than silently picking one.

What the campaigns did produce

R52's campaign found three, all confirmed with reproducers:

1. catalogInterestRateMath — the finding itself notes the assertion compares a stored drawn rate against a recomputation over view-accrued debt. A harness artifact; it triaged itself correctly.
2. catalogHubSpokeAggregates — getAddedAssets(0)=100000100301 vs Spoke sum 100000100300. One unit. The generated properties use bare exact equality where the reference uses relative difference plus a MIN_TOTAL_SUPPLIED floor. Almost certainly rounding dust.
3. catalogAddedSharePriceNonDecreasing — borrow → 1s accrual → supply, and the exchange ratio decreases. A three-step sequence, and the only finding of the shape the thesis predicts. May still be dust, for the same missing-tolerance reason.

What this does and does not establish

It does not establish that ultrafuzz has no edge over no-fuzz. It establishes that this suite is concentrated in the class with the least edge and thin exactly where the edge would be, on one model, one lane, one target, one run — and with a degraded input, since property-specification-fanin failed on that run, so the catalog feeding implementation was incomplete.

Note also that the target is upstream aave/aave-v4 @ 6959e321, not the scfuzzbench fork, so there is no injected ground truth to score against even with a completed campaign.

To actually answer the question

Three things the current setup lacks:

1. The scfuzzbench fork as target, so ground truth exists.
2. A completed campaign (blocked on The Recon campaign's three findings are discarded on a schema_version literal the contract never states #356 / PR fix(artifacts): stop losing a campaign's findings to a version string #401).
3. A no-fuzz arm on the same commit.

Then compare recall against the known bug set, split by whether each bug requires a sequence. Until then, a completed run tells you the pipeline works — not whether the properties it writes are the ones that matter.

Two cheap improvements independent of all that:

• Add tolerance to the generated conservation properties. Two of R52's three findings look like dust, and triage cost is per-run and recurring.
• Give BeforeAfter ghost state and operation tracking, which is the precondition for the property class that is currently unreachable.