Can invariant-only Ultrafuzz autonomously rediscover an Aave v4 benchmark bug family? #522

Activity

1. aviggiano

   added

   In ProgressClaimed and actively worked on; has an assignee. Remove if work stops.Claimed and actively worked on; has an assignee. Remove if work stops.

   on Aug 12, 2026
2. aviggiano commented on Aug 12, 2026

   

   aviggiano

   on Aug 12, 2026

   CollaboratorAuthor

   More actions

   Closing as the completed sequence-length experiment

   The sequence-length question this issue was reopened around is answered. The benchmark-rediscovery
   research question is not answered, and it moves to #531 with a matched control and a
   pre-registered protocol. Correcting the record below, because an earlier reading of this evidence
   was wrong in two ways.

   Correction 1: there is no completed seq-len-100 Ultrafuzz run

   The workflow run aave-v4-v056-gpt55-xhigh-invariant-only-20260812-seqlen100-full-timeout is
   canceled, 1m17s in, with project-discovery failed and 24 of 25 nodes still pending. Its
   campaign prompt digest is identical to the seq-len-1 run's, so it was never configured for
   sequence length 100 in the first place.

   The seq-len-100 numbers come from a standalone recon fuzz invocation run by hand inside a git
   worktree of the preserved stateful-invariant-campaign workspace
   (.ultrafuzz/experiments/aave-v4-v056-20260812-seqlen100), between 2026-08-12T01:09:42Z and
   02:09:45Z. Its argv was never recorded in any typed artifact; the effective sequence length is
   provable only from the backend log:

   INFO campaign::campaign: Starting fuzzing campaign with 32 workers
   INFO campaign::campaign: Test limit: 18446744073709551615 (shared across all workers), Sequence length: 100
   

   Every typed artifact under that experiment path (recon-fuzzer-results.json, campaign-plan.json,
   campaign-summary.json, campaign-report.md) actually describes the seq-len-1 baseline: they
   carry run_id: aave-v4-v056-gpt55-xhigh-invariant-only-20260811-full-timeout, an exact_command
   with no --seq-len flag, exact_config.summary.seqLen: 1, and failure_count: 0. The
   experiment's echidna.yaml still says seqLen: 1 and is byte-identical to the config digest
   recorded in recon-fuzzer-results.json, which is how we know the 100 arrived as a CLI override.

   So: no sealed, gated, end-to-end stateful run exists for this target. Any statement that a
   completed seq-len-100 Ultrafuzz campaign produced typed findings here is unsupported.

   What the hand-run campaign did show

   Measure	seq-len 1 (sealed run)	seq-len 100 (hand-run)
   Workers	32	32
   Campaign seconds	3,510.5	3,596.7
   Total calls	11,183,800	85,003,705
   Unique instructions	76,177	94,315
   Corpus retained	63	88
   Failures	0 / 58	1 / 58

   Sequence length is not a marginal knob: 7.6× the calls (seq-len 1 pays a full state reset per
   call), +23.8% unique instructions, and the first falsification landed 0.06 s into the campaign.
   The stock campaign prompt on current origin/main does require --seq-len 100 (verified at
   682d51a3, .ultrafuzz/prompts/strategies/invariants/invariant-testing-campaign.md:111); the
   seq-len-1 inheritance in this project came from its pre-#521 project-local prompt copy, whose
   long-campaign template omitted --seq-len entirely.

   Correction 2: the counterexample is an incomplete-spec counterexample, not a rediscovery

   One property broke: property_hub_spoke_aggregate_conservation()
   (test/foundry/recon/Properties.sol:179), on the assertion at line 191:

   assert(hub.getAddedAssets(assetId) <= aggregate.addedAssets);

   Witness (assetId 0, five spokes), shrunk to a single state-changing call
   target_user_borrow(0):

   • per-spoke getSpokeAddedAssets = [0, 108333333333, 108333333333, 0, 0] → sum 216,666,666,666
   • hub.getAddedAssets(0) = 216,666,666,667
   • violation: exactly 1 wei. hub.getAddedShares(0) equals the aggregate exactly — shares
     conserve; only the asset conversion differs.

   Reproducer: backends/recon-fuzzer/recon-corpus/reproducers/8908329350215675565.txt.

   This is a defect in the generated specification, not a discovery about the protocol:

   1. The assertion is arithmetically unsatisfiable as written. Hub.getSpokeAddedAssets is
      literally toAddedAssetsDown(...) (src/hub/Hub.sol:615) — a per-spoke round-down — while
      getAddedAssets (src/hub/Hub.sol:522) returns the untruncated total. A sum of floors is ≤ the
      true total by construction, so total <= sum_of_floors fails the moment the share price is
      non-integral, which one interest-accruing call guarantees. Two non-empty spokes each lost 0.5 wei
      to truncation.
   2. The benchmark states the same invariant in the opposite direction, with tolerance.
      ScFuzzBench's INVARIANT_3_HUB_ADDED_ASSETS_GREATER_THAN_SPOKE_SUM asserts hub added assets
      ≥ the spoke sum, compares round-down against round-down
      (previewRemoveByShares), and routes the delta through a relative-difference helper, so a 1-wei
      delta on a 2.17e11 base integer-divides to zero and passes. The witness state does not
      violate the benchmark property; family 3 refutes it.
   3. There is no injected bug to rediscover on this target. diff -rq against
      scfuzzbench/aave-v4-scfuzzbench differs in exactly three files, none of them protocol logic:
      WETH9.sol (custom errors), AaveOracle.sol (a setSpoke test hook), and SpokeInstance.sol
      (_disableInitializers() commented out for the fuzzer). Hub.sol, Spoke.sol and every
      library are byte-identical to upstream Aave v4 v0.5.6.
   4. The omission is local and traceable. Two lines above, the same generated file uses a
      rounding-tolerance helper for the same class of aggregation
      (_withinRoundingTolerance(reserveDrawn, aggregate.drawnDebt, aggregate.borrowerCount)).
      Line 191 uses a bare strict inequality with no per-spoke tolerance term. The property faithfully
      transcribes docs/overview.md:57 ("Hub assets <= sum of Spoke assets (converted from shares)")
      as an exact-arithmetic assertion; ScFuzzBench's maintainers read the same doc line and
      deliberately reversed it and added tolerance.

   Residual value, stated plainly: the counterexample is a genuine, reproducible documentation
   defect — docs/overview.md:57 states the inequality in the direction the implementation does not
   satisfy, and the implementation's actual direction (hub total ≥ sum of spoke claims; the hub never
   over-credits) is the protocol-safe one. Informational at most. Zero economic impact, no protocol
   bug, and no semantic benchmark-family credit.

   Disposition

   • The sequence-length experiment is complete: sequence length 100 materially changes campaign
     behaviour, and the requirement is enforced by merged fix(invariants): require stateful Recon sequences #521 on current main.
   • Answer to this issue's research question: still unanswered. No valid, sealed, gated,
     end-to-end stateful invariant-only run exists for this target, and the one counterexample
     produced is an incomplete-spec counterexample rather than a ScFuzzBench family rediscovery.
   • The restarted, matched, blinded paired evaluation that can answer it is tracked in Aave v4: release matched NoFuzz control and restart paired evaluation #531.
   • Property-specification/oracle validity work continues in Validate selected properties against executable backend oracles #524 (executable oracles and
     reachability), Require source-backed rounding tolerances in generated conservation properties #425 (source-backed rounding tolerances — the direct generic lesson of the 1-wei
     assertion), Generate sequence-wide ghost and operation state in BeforeAfter scaffolds #424 (sequence-wide ghost state), and Invariant campaign can report complete when Recon smart-filter drops a generated property #519 (smart-filter omissions). Coverage
     denominator provenance is now Publish the complete coverage denominator instead of a scopeless standardized score #532 and campaign comparability classification is now Classify campaign comparability when required property families are deferred or unreachable #533.

   Closing per #531.
3. aviggiano

   closed this as completedon Aug 12, 2026
4. aviggiano commented on Aug 12, 2026

   

   aviggiano

   on Aug 12, 2026

   CollaboratorAuthor

   More actions

   Correction to the closing comment

   Point 3 of my closing comment ("There is no injected bug to rediscover on this target") is
   misleading and should not be read as written.

   The ScFuzzBench Aave v4 benchmark does not inject mutations into the protocol source. Its
   tests/recon/Properties.sol header states its method directly: it implements a pre-vetted list of
   Audit Contest invariants (Sherlock contest 1209) against upstream Aave v4. Its 10 non-canary broken
   identities are therefore genuine invariant violations observable in unmutated v0.5.6, not
   artificial defects planted in a fork.

   Consequences for how this issue should be read:

   • The byte-identical diff against the fork (3 harness-compatibility files, protocol logic
     unchanged) shows the two source trees are the same unit under test. It does not show there is
     nothing to find on 6959e321. The benchmark families are reachable on the clean upstream commit,
     given equivalent executable oracles.
   • What the fork supplies that the clean target does not is the hand-authored oracle. That is
     exactly the capability Ultrafuzz's invariant group is supposed to produce autonomously, so
     running against clean aave/aave-v4@6959e321 and letting Ultrafuzz author its own properties is
     the correct experiment — not a weaker substitute for running against the fork.
   • The conclusion of the closing comment is unchanged, and rests on points 1, 2 and 4: the 1-wei
     property_hub_spoke_aggregate_conservation counterexample is an incomplete-spec counterexample
     because the generated assertion compares an untruncated total against a sum of per-spoke
     round-downs and is unsatisfiable as written, and because the benchmark's own family-3 property
     states the inequality in the opposite direction with a relative tolerance, so the witness state
     does not violate it. Neither of those arguments depends on the presence or absence of injected
     bugs.

   The restarted evaluation in #531 will run against aave/aave-v4@6959e3219b5506bf2acae18551cbb2a68a5b8fba
   with Ultrafuzz authoring its own invariants, and will not mimic ScFuzzBench's hand-authored suite.