Skip to content

Aave v4: release matched NoFuzz control and restart paired evaluation #531

Closed

Description

@aviggiano

Objective

Release the next stable Ultrafuzz version, construct a matched draft NoFuzz control from that exact release, and restart the blinded Aave v4 Ultrafuzz-vs-NoFuzz comparison.

Scope

  • Close the completed seqLen-100 Aave diagnosis with corrected, evidence-backed conclusions.
  • Prepare and publish Ultrafuzz v0.0.15 from verified origin/main.
  • Create draft-only v0.0.15-nofuzz from the exact paired Ultrafuzz SHA.
  • Run a focused NoFuzz experiment, then fresh blinded paired end-to-end trials.

Issue disposition

Stable release: v0.0.15

  • Fetch origin/main and tags; resolve the exact target SHA and enumerate every merged PR after v0.0.14.
  • Draft complete editorial release notes and require successful remote CI for the exact SHA.
  • Run local release gates.
  • Obtain explicit approval of the exact SHA and notes before publishing.
  • Publish a non-draft, non-prerelease v0.0.15 release and verify its GitHub release and tag resolve to the approved SHA.

Matched NoFuzz draft release

  • Branch from the exact v0.0.15 SHA.
  • Preserve runtime, CLI, dependencies, artifact contracts, model setup, and source snapshot.
  • Limit differences to NoFuzz prompts/guidance, required topology removal, and necessary tests.
  • Produce a diff inventory proving that every non-prompt/topology change is test-only and necessary.
  • Create a draft-only v0.0.15-nofuzz GitHub release that names the paired base SHA.

Restarted evaluation

  • Run a focused NoFuzz experiment on clean Aave v4 source with shared discovery/property artifacts, excluding generated harnesses, corpora, findings, triage, and reports.
  • Require a source-backed violation finding rather than crediting a restated property.
  • Run blinded paired end-to-end trials against Aave commit 6959e3219b5506bf2acae18551cbb2a68a5b8fba with identical GPT-5.5/xhigh settings, budgets, source snapshot, scoring, and reporting.
  • Run at least three pairs; five pairs preferred.
  • Pre-register and report property specification, executable-oracle creation, reachability, counterexample/finding production, triage survival, and semantic benchmark-family credit. Treat invalid/incomplete rows as invalid, not zero.

Explicitly deferred

References

Activity

  1. added
    In ProgressClaimed and actively worked on; has an assignee. Remove if work stops.
    on Aug 12, 2026
  2. aviggiano commented on Aug 13, 2026

    @aviggiano
    CollaboratorAuthor

    Pre-registration: Aave v4 Ultrafuzz vs NoFuzz, default topology, n=1 paired observation

    Registered before any model-authored work in either arm. Amendments after the first launch are
    recorded as dated addenda, never by editing this text.

    Research question

    On clean upstream Aave v4, does Ultrafuzz's fuzzing capability — the stateful invariant campaign,
    coverage expansion, and generated-test authoring — produce a source-backed protocol finding that
    property-guided source analysis alone does not, holding model, budgets, source snapshot, topology
    shape except for fuzzing, scoring and reporting identical?

    Design and its declared limits

    • n = 1 pair. One Ultrafuzz row and one NoFuzz row. Reported as a single observation.
    • No variance estimate, no significance claim, and no rate comparison is derivable from n=1. This is
      an existence check. Aave v4: release matched NoFuzz control and restart paired evaluation #531 asks for at least three pairs and prefers five; running one is a
      deliberate, recorded deviation.
    • A single pair can support only these statements: whether each arm produced any source-backed
      violation finding, and which pre-registered metrics each arm could populate at all.

    Target

    • Repository: aave/aave-v4
    • Commit: 6959e3219b5506bf2acae18551cbb2a68a5b8fba (tag v0.5.6)
    • Clean upstream source. ScFuzzBench's hand-authored tests/recon invariant suite is not
      present, not copied, and not mimicked. Both arms author their own properties. That is the point of
      the experiment: the hand-authored oracle is the capability under test.
    • The ScFuzzBench Aave v4 benchmark injects no protocol mutations; it implements pre-vetted audit
      contest invariants (Sherlock 1209) against this same upstream source. Its broken identities are
      therefore reachable on this commit given an equivalent executable oracle.

    Arms, identified by content

    Both arms run the default audit profile. packages/config/audit-profiles.yml declares
    default: balanced, and balanced declares no topology_path with settings: {}, so the effective
    graph is the editable project topology .ultrafuzz/topology.yml, not invariant-only.yml. The target
    project's ultrafuzz.toml already declares audit_profile = "balanced".

    Ultrafuzz (treatment) NoFuzz (control)
    Release v0.0.15 v0.0.15-nofuzz (draft-only)
    Commit 682d51a3c3107e2830eaae1608bdafa2131e486b 3936963a6eb2da1c4881f2bdc44056db08b7e21a
    Branched from — that exact base SHA
    .ultrafuzz/topology.yml sha256 8a75c4ab0232ef745b9c99781dcbf6b3a3dec912397d9c0603e067fd95a3f0ca f5081f055e8bcc04b4cbfdc5da991248ffa5fcc434d71c4bed0944dd5892cd03
    Nodes 61 total, 50 agentic 54 total, 43 agentic
    Nodes declaring required_commands 2 0
    Model, every model-authored node CodexAgent / gpt-5.5 / xhigh identical
    Runtime, CLI, dependencies, artifact contracts, model setup v0.0.15 identical, unmodified

    The control removes 7 nodes (expand-coverage, the five stateful-invariant-*,
    aggregate-test-files) and the ultrafuzz/generated-tests@1 output from every producer that declared
    it. Control guidance lives in .ultrafuzz/prompts/nofuzz/{setup,review}/, referenced only from the
    control topology, so all 27 prompts shared with invariant-only.yml or smoke.yml are byte-identical
    to the base SHA. Diff inventory and review history: #548.

    Pre-launch checks, required before either arm is trusted

    1. Confirm each arm's resolved config records audit_profile.effective: balanced, gpt-5.5, xhigh,
      and the topology digest above. Any divergence outside the intended difference invalidates the pair.
    2. Confirm every node's executed prompt is the prompt its topology declared. promptEntryForPath
      falls back to a same-logical-id prompt when the declared path is absent (Prompt resolution silently substitutes a same-id prompt when the declared path is missing #556), so a missing
      nofuzz/ file would silently run the treatment arm's guidance inside the control. Verify resolved
      prompt paths and sealed snapshot digests, do not assume.
    3. Confirm the control's report.json carries property_provenance: []. A non-empty array raises
      IMPLEMENTED_PROPERTIES_MISSING because the control declares no
      stateful-invariant-implement-properties node.

    Held constant

    Source snapshot and target commit; model and reasoning effort (CodexAgent / gpt-5.5 / xhigh
    for every model-authored node); the balanced profile's effective settings
    (dynamic_strategies_enumerator = 3, max_parallel_agents = 4, max_parallel_nodes = 8,
    default_timeout_seconds = 1800, workflow_deadline_seconds = 86400,
    invariant_testing_smoke_timeout = 10min, invariant_testing_fuzzer_timeout = 1h, strategy_loops
    at its code default); property_priority_threshold = "high"; the reference catalog and its cache;
    triage quorum and panel size; the severity rubric; the report contract; and the scoring and
    reporting protocol below. Both rows' resolved configs are captured and compared before unblinding;
    any divergence outside the intended difference invalidates the pair.

    Cost basis, stated honestly

    The measured figures available on this host — 5h17m and 6h07m end to end, ~188M tokens, ~$1,092
    estimated spend — are from the 34-node invariant-only profile. They do not transfer to the
    61-node default topology, which additionally runs 20 static strategies, the differential lanes, and
    dynamic strategy generation at enumerator = 3. No measured baseline exists on this host for the
    default topology on this target, so the treatment arm's cost is projected, not known, and expect it
    to exceed the invariant-only figures materially. This is recorded in advance so the eventual number
    is not presented as having been predicted.

    Blinding, and what it can and cannot mean here

    Benchmark comparison is withheld until generation, campaign or analysis, verification, dedupe,
    triage, severity classification, aggregation and final reporting are complete in both arms.
    Unblinding is a single recorded step after both report.md files are final. No benchmark identity,
    invariant name, or expected-finding list is present in either arm's workspace or prompts.

    Arm identity is not concealable, and this protocol does not pretend otherwise. "Blinded" here
    means blind to the benchmark answer key, not blind to which arm produced a run. Five channels in a
    finished report.md identify the arm, and none can be masked without either falsifying an artifact or
    re-adding the capability the control exists to remove:

    1. ## Run summary renders Elapsed time, Tokens used, Estimated spend, Topology digest and
      Prompt digest (packages/runtime/src/final-report-markdown.ts:8-22). Elapsed time and spend differ
      between arms by roughly an order of magnitude, and the two digests differ by construction. This is
      the strongest channel.
    2. ## Property implementation coverage always renders unavailable on the control, because it
      declares no implemented-properties.json producer and
      packages/cli/src/report-artifacts.ts forces that value when the handoff is absent.
    3. The Fuzzer backends column of ## Property provenance always renders unavailable on the control,
      which declares no recon-fuzzer-results.json producer.
    4. ### Proof of Concept never contains a fenced code block on the control, which has no generated
      test or reproducer to minimize.
    5. The ### Strategy detection table can never name the removed nodes on the control.

    Grading instruction, binding on the adjudication step:

    Graders score issue bodies only. For each reported issue, judge only the claim, the cited source
    evidence, the severity rationale, and whether the described behaviour is a real defect in the pinned
    target commit. Do not use report shape or run telemetry as evidence about finding quality.
    Specifically: elapsed time, token counts, estimated spend, topology and prompt digests, an
    unavailable property-implementation-coverage value, an unavailable Fuzzer backends value, the
    presence or absence of a fenced code block under ### Proof of Concept, and the particular strategy
    names in a ### Strategy detection table are all determined by which arm produced the run. They
    carry no information about whether an issue is correct, severe, or well argued, and must not raise or
    lower any score. A grader who believes they have identified the arm must still score issue bodies on
    content alone, and must record that they formed that belief.

    Scoring protocol

    eval score is not usable for this target and is not used. The only Aave label set,
    benchmarks/private-ground-truth/aave-v4-scfuzzbench/findings.yml, binds
    subject: scfuzzbench/aave-v4-scfuzzbench @ edd6c82721512540c8c90e7a36a4a8e19fd7bdf3, and
    assertGroundTruthSubject (packages/evals/src/scoring.ts:650) rejects a private-sensitivity row
    whose target is aave/aave-v4 @ 6959e321. Downgrading sensitivity to bypass that check would void
    the #453 immutable-binding guarantee and is prohibited.

    Metrics are therefore assembled by the manual protocol below from typed run artifacts only, with
    every value citing an absolute artifact path. Semantic benchmark-family credit is a documented
    post-hoc unblinding comparison against the benchmark's family list, adjudicated by the stated rule
    rather than by name matching.

    Pre-registered metrics

    Recorded per arm. Every value cites the artifact path it was read from. A metric that cannot be
    populated is recorded invalid, never zero.

    1. Property specification. Count of properties in property-specification-fanin/properties.json,
      and the count at the selected priority threshold.
    2. Executable-oracle creation. Number of selected properties with an executable oracle that can
      actually falsify — a comparison or revert-selector check reachable from an admitted backend
      entrypoint. A property recorded as implemented whose handler contains no falsifiable assertion
      counts as not an oracle, and the discrepancy is reported. On the control arm this metric
      measures oracle specification rather than executable implementation; that asymmetry is
      intrinsic to the comparison and is reported as such, not as a zero.
    3. Reachability. For each oracle, whether its protocol call and its failure observation were
      reachable, with the blocker named for each that was not. Treatment arm additionally reports
      campaign LCOV.
    4. Counterexample / finding production. Number of source-backed violation findings surviving to
      dedupe-findings. A restated property with no witness, no reproducer, and no source contradiction
      is not a finding and earns no credit. Treatment arm additionally reports falsified test
      identities and shrunk reproducer paths.
    5. Triage survival. Findings surviving triage and severity-classification, with per-finding
      disposition, and the count reaching report.md.
    6. Semantic benchmark-family credit. After unblinding, each surviving finding maps to a
      ScFuzzBench Aave v4 family or to none. Credit requires semantic equivalence of the violated
      property and its direction and tolerance, not name similarity. Explicitly excluded from
      credit: a counterexample against a generated property that the benchmark's own property
      contradicts — an incomplete-spec counterexample, as classified in Can invariant-only Ultrafuzz autonomously rediscover an Aave v4 benchmark bug family? #522 — and post-hoc separation
      of the combined property-24 / property-25 entrypoint, which Aave v4: release matched NoFuzz control and restart paired evaluation #531 places out of scope.

    Validity rules, fixed in advance

    • A row whose workflow did not complete all nodes is invalid, not zero.
    • A row that resumed in a way that repeats a model-backed attempt is classified non-comparable by
      recovery_equivalence.max_repeated_model_executions: 0 and is reported invalid, not zero.
    • A row whose campaign completed but whose required property families were deferred or demonstrably
      unreachable is reported partially comparable, and its zero-finding result is not presented as
      an unqualified negative. Generic mechanism tracked in Classify campaign comparability when required property families are deferred or unreachable #533.
    • A hand-run backend invocation outside the sealed workflow is not evidence for either arm. The
      seq-len-100 episode in Can invariant-only Ultrafuzz autonomously rediscover an Aave v4 benchmark bug family? #522 is the precedent: its numbers came from a manual recon fuzz whose
      argv was never recorded, while every typed artifact at that path described a different run.
    • Effective Recon sequence length is proven from the typed artifact, never from prose. v0.0.15
      requires and records --seq-len 100.

    Disclosed asymmetries

    Every known way the two arms differ beyond the absence of fuzzing. Read these before interpreting any
    result; none is hidden and none is repaired by falsifying an artifact.

    1. Anti-false-positive suppressor, favours the control on precision. Present in 22 control prompts
      against 5 base counterparts. It compensates for losing the failing-test anchor, so any precision or
      F1 advantage the control shows is not a fuzzing result.
    2. boundary-tests findings destination, favours the control on recall at one node. The control
      names the destination through {{output_findings_path}}; base names none at all, which is the
      shipped defect tracked in A node can declare a findings output whose prompt never says where to write findings #539, so base's node cannot report a finding.
    3. Preflight, favours the control. The control declares zero required_commands, so a missing or
      flaky recon/covg-eval can fail the treatment arm and cannot fail the control.
    4. Source-chain citation, favours the treatment arm. The only deliberate asymmetry against the
      control: reachability=public-caller-source-chain must cite source spans for every link of the
      caller chain and for the argument/state admission, standing in for base's generated public wrapper
      PoC, which the control cannot execute.
    5. Stale BENCHMARK_SMOKE_EXCLUDED_NODE_IDS. Unreachable from the shipped lanes; fixing it would
      require a src edit that PRESERVE forbids, so it is encoded as an assert.throws.
    6. Structural report differences. The control always renders unavailable property-implementation
      coverage, No property-derived findings., no fenced code block under ### Proof of Concept, and a
      ### Strategy table that cannot name the removed nodes.

    Reported regardless of outcome

    Both arms' run IDs, elapsed time, token and cost accounting, node completion counts, artifact paths,
    and the full metric table including invalid cells. A well-formed negative result — neither arm
    finding anything — is a reportable outcome and will be reported as such rather than retried until it
    changes.

  3. aviggiano commented on Aug 13, 2026

    @aviggiano
    CollaboratorAuthor

    Addendum 1 (2026-08-13): execution moves to Modal, one arm per VM

    Recorded as a dated addendum rather than by editing the pre-registration, per its own amendment rule.
    This changes execution and reporting, not the research question, the target, the arms, or the metrics.

    Change

    Both arms run on Modal, concurrently, one run per VM, with artifacts on persistent storage, and
    every stopped node is resumed so each run proceeds start to finish reusing completed work. The
    pre-registration as posted described local execution ([execution] mode = "local", which is what both
    prepared checkouts currently declare) and sequential-vs-concurrent as an open choice. Concurrent
    execution is now fixed, which is the better choice for matched host conditions.

    Consequence that must be reported, not buried

    "Always resume" is in direct tension with a clean-attempt reading of either arm. Under
    recovery_equivalence.max_repeated_model_executions: 0 a resume that repeats a model-backed attempt
    classifies a row non-comparable — but that enforcement lives in the eval lane, and this experiment does
    not use eval run or eval score (see the Scoring protocol section: the only Aave ground truth binds
    subject: scfuzzbench/aave-v4-scfuzzbench@edd6c827 and assertGroundTruthSubject rejects a
    private-sensitivity row targeting aave/aave-v4@6959e321). So no automatic comparability gate will fire,
    and the honest-reporting burden shifts entirely onto disclosure.

    Therefore the following are added to the reported quantities, per arm, and will be reported whatever they
    say:

    • number of resumes, and the trigger for each
    • number of repeated model-backed attempts, and which nodes repeated
    • attempts per node from the durable attempt ledger
    • total tokens, estimated spend, and elapsed wall clock, separated into first-attempt and post-resume

    A row that only completed because work was repeated is not equivalent to a row that completed in one
    pass, and the report will say so explicitly rather than presenting a resumed completion as a clean one.

    Cost basis, corrected again

    The pre-registration already warns that the measured 5-6h / ~188M token / ~$1,092 figures come from the
    34-node invariant-only profile and do not transfer to the 61-node default topology. Sizing by agentic
    node count (50 treatment, 43 control, against 23 for invariant-only) projects roughly $2.4k and 11-13h
    for the treatment arm and $1.6-2k and 8-10h for the control, so about $4k for the pair. These are
    projections, recorded before launch so the eventual figures are not presented as having been predicted.

    Integrity precondition, blocking launch

    The control's NoFuzz guidance exists only in .ultrafuzz/prompts/nofuzz/{setup,review}/ (7 files),
    referenced only from its own topology. If those files do not reach the Modal execution environment,
    promptEntryForPath (packages/runtime/src/plan-run.ts:1142) falls back to a same-logical-id entry and
    silently renders the stock prompt — running the treatment arm's guidance inside the control arm and
    voiding the experiment with no error. That hazard is filed as #556.

    Launch is therefore gated on proving prompt carriage into the Modal environment, and on a post-launch
    check that the control's rendered prompt snapshots match its own 7 files rather than the stock ones. If
    carriage cannot be proven, the arms run locally instead; the experiment will not be run on a path where
    this substitution is possible but unverified.

  4. aviggiano commented on Aug 13, 2026

    @aviggiano
    CollaboratorAuthor

    Addendum 2 (2026-08-13): execution stays local, both arms concurrent

    Supersedes Addendum 1's move to Modal. Recorded before launch. The research question, target, arms,
    held-constant list, metrics and validity rules are unchanged.

    Change

    Both arms run locally on the launch host, concurrently, one workflow each, with
    [execution] mode = "local" as both prepared checkouts already declare. The Modal path in Addendum 1 is
    withdrawn and no Modal configuration was applied to either arm.

    Everything Addendum 1 said about resumes still holds and is restated here so it is not lost with the
    withdrawn parts: every stopped node is resumed so each run proceeds start to finish reusing completed
    work, and because this experiment does not use eval run or eval score, no automatic comparability
    gate fires. The following are therefore reported per arm regardless of outcome: number of resumes and
    each trigger, number of repeated model-backed attempts and which nodes repeated, attempts per node from
    the durable attempt ledger, and tokens, estimated spend and elapsed wall clock separated into
    first-attempt and post-resume. A row that completed only because work was repeated is not equivalent to
    one that completed in a single pass, and the report will say so.

    What local concurrent execution costs the comparison, stated in advance

    The two arms share one host and one model gateway. Each declares cpu = 4, memory_mib = 8192 and
    max_parallel_agents = 4, so eight concurrent agents contend for one gateway process and 32 vCPU.
    Consequences to disclose rather than discover:

    • Wall-clock elapsed is not a clean measure of either arm's cost, because each arm's latency is
      affected by the other's load. Token counts and node/attempt counts are the reliable quantities;
      elapsed time is reported but must not be used to compare arm efficiency.
    • Concurrency is what buys matched conditions: both arms see the same host state, the same gateway, and
      the same wall-clock window, which is why they are run together rather than back to back.
    • The gateway is a single point of failure for both arms simultaneously. A gateway fault is an
      operational failure affecting the pair, to be reported as such, and not evidence about either variant.

    Integrity precondition, now satisfied

    Addendum 1 gated launch on proving that the control's 7 nofuzz/ prompts reach the execution
    environment, because promptEntryForPath (packages/runtime/src/plan-run.ts:1142) silently falls back
    to a same-logical-id prompt when a declared path is absent, which would run the treatment arm's guidance
    inside the control (#556).

    Local execution renders prompts directly from each project's own tree, and the gate is now closed by
    direct check: every prompt path declared by each arm's topology exists on disk in that arm — treatment
    50 declared references, 0 missing, 0 under nofuzz/; control 43 declared references, 0 missing, exactly
    7 under nofuzz/ (setup/{project-discovery,prepare-foundry-harness,discover-base-test}.md and
    review/{dedupe-findings,triage,severity-classification,final-report}.md). The fallback therefore cannot
    fire in either arm.

    Post-run verification remains required and will be reported: the control's rendered prompt snapshots
    must match its own 7 files, not the stock ones.

    Prepared state at launch

    treatment control
    project /home/ubuntu/eval-arm-ultrafuzz /home/ubuntu/eval-arm-nofuzz
    package build Ultrafuzz v0.0.15 682d51a3 v0.0.15-nofuzz 3936963a
    source aave/aave-v4@6959e321, clean, submodule pinned identical
    .ultrafuzz/topology.yml sha256 8a75c4ab…95a3f0ca f5081f05…5892cd03
    declared prompt refs 50, 0 missing 43, 0 missing, 7 under nofuzz/
    doctor healthy healthy
    validate 6/6 pass 6/6 pass
    required commands available 9 6
    ultrafuzz.toml byte-identical to the control's byte-identical to the treatment's

    The required-command counts differ by exactly three — recon, recon-generate, covg-eval — derived
    from each topology rather than asserted, which is independent confirmation that the control declares no
    fuzzing backend.

    No --agent or --model flag will be passed at launch: docs/reference/cli.md records that --agent
    clears backend-specific reasoning even when --model also pins a replacement, which would silently drop
    xhigh. Both arms rely on [models.default].

  5. aviggiano commented on Aug 13, 2026

    @aviggiano
    CollaboratorAuthor

    Paired run status — both arms finished

    Both arms of the 2026-08-13 paired run reached a final report. The engine's own view is authoritative here; the on-disk state.json for the treatment arm was stale by roughly an hour and understated progress.

    treatment (ultrafuzz) control (nofuzz)
    engine status done (failed), 264/264 tasks, 8h 0m done (failed), 237/237 tasks, 6h 12m
    final report written written
    production findings 1 low 5 low
    tokens 803,073,878 629,736,537
    estimated spend $4,597.44 $3,632.98

    Both are marked failed because of node-level gate failures, not because work was left undone.

    Two gate defects, now filed

    #582 — campaign command gate rejects the log redirection. The treatment arm's stateful-invariant-campaign ran a complete 3603-second campaign (campaign_outcome: complete, usable_results: true, one reproduced property failure) and was marked failed 191 ms after its artifacts landed. The recorded command satisfies every requirement — --timeout 3600, --test-limit 18446744073709551615, --seq-len 100, and the exact timeout wrapper each appear once, with no --foreground — but constrainedShellTokens bails on the > of the command's own log redirection at character 1179, so all four checks report their flag missing at once. Fix and regression tests are on fix/582-recon-command-redirection.

    The campaign's evidence was not lost: downstream nodes consumed the artifacts and its finding reaches the final report as a harness-defect row crediting recon as the backend. The cost is that a valid campaign and the run containing it are recorded as failed.

    #583 — fan-in markdown parity reports a missing description that is present. property-specification-fanin failed identically in both arms. The gate names 78 properties as missing description; for property-5 the field is present in properties.md and matches the JSON. Mechanism not yet pinned down, so filed separately rather than fixed. This is the third fan-in parity rule to reject compliant artifacts, after #297.

    Effect on the comparison

    The fan-in failure is symmetric and does not bias the arms against each other. The campaign gate failure is treatment-only, but since the artifacts still flowed downstream it does not by itself explain the 1-vs-5 production finding gap — that gap needs to be judged on the reports themselves, not attributed to #582.

    Supervision note

    eval-supervisor.sh logged 10 resumes across the two arms (ledger in /home/ubuntu/eval-supervisor/resumes.jsonl). All were no-ops against live workflows — the v3 stall signal still fired on healthy long-running nodes. The supervisor process died around 16:48 and neither arm needed it to finish. Recorded per Addendum 2; no arm completed only because work was repeated.

  6. aviggiano commented on Aug 14, 2026

    @aviggiano
    CollaboratorAuthor

    Generic follow-up issue disposition after the paired-run audit

    Created:

    Updated existing issues with #531 evidence:

    No new issue was created for these because v0.0.16 now has direct coverage:

    • failed dependency verification is fail-closed through authenticated verification markers, with a passing regression test;
    • property-campaign v3 closes referenced backend evidence over files under the durable artifact directory;
    • lifecycle semantic gates preserve findings through triage, severity classification, and final report disposition.

    This leaves #589 and #590 as the two new generic issues arising from the run.

  7. aviggiano commented on Aug 14, 2026

    @aviggiano
    CollaboratorAuthor

    Completion disposition

    This investigation is complete. The evidence supports a narrower conclusion than the original hypothesis, and the reusable product failures now have explicit follow-ups.

    Answer to the research question

    Stateful fuzzing can reach failures that require dependent state transitions, but this paired experiment did not demonstrate a different confirmed Aave bug found by stateful fuzzing.

    The treatment's autonomous stateful campaign produced only a harness defect. Its sole production finding came from a deterministic shared strategy, not from Recon's sequence search. Conversely, NoFuzz authored several genuinely multi-step deterministic PoCs. The meaningful capability boundary is therefore:

    • stateful fuzzing: autonomously searches transaction sequences and state;
    • NoFuzz in this experiment: the model authors a deterministic scenario, which may itself contain many calls.

    It is not simply “multiple transactions versus one transaction.” The experiment leaves open—and makes more precise—the question of whether autonomous sequence search finds confirmed bugs that source-guided, model-authored multi-call scenarios miss.

    What the two runs showed

    Ultrafuzz treatment NoFuzz control
    Completed tasks 264/264 237/237
    Engine result done (failed) done (failed)
    Tokens 803,073,878 629,736,537
    Cost $4,597.44 $3,632.98
    Production findings 1 Low 5
    Authored tests 26,603 LOC / 112 files 1,751 LOC / 19 files

    Treatment-specific observations:

    • Recon used seqLen=100 and executed 96,751,355 calls.
    • Its sole failure was a retroactive add-cap harness defect, not a production bug, and appeared about 38.5 ms into the campaign.
    • Coverage/corpus growth saturated after 207 seconds and 8,972,029 calls; the remaining ~90.7% of calls added nothing.
    • Recomputed coverage was 59.85%.
    • The one production Low came from deterministic strategy analysis shared in spirit with the control, so it is not evidence for stateful sequence search.

    The control was not limited to one-call attempts. Its authored scenarios included:

    • creating debt, advancing 365 days, then repaying one wei;
    • supplying collateral, borrowing, pausing, then borrowing again;
    • performing 1,000 time advances/premium refreshes.

    There is also a high-risk reentrant collateral-token liquidation PoC that passes, but triage split 2–2 on whether that token behavior is within the support model. It remains unadjudicated, not a confirmed sixth finding.

    Why this experiment cannot isolate the effect of fuzzing

    The comparison was materially confounded:

    • Control prompts asked agents to “find bugs associated with X.”
    • Treatment prompts asked agents to “author focused Foundry tests for X.”
    • Treatment nodes mandated generated-test output; control nodes did not.
    • The resulting 15× difference in test LOC is evidence that the two arms optimized for different deliverables.
    • This was one paired target (n=1).

    Both rows were also invalid under the preregistered success criteria: treatment failed fan-in, campaign verification, and final-report processing; control failed fan-in. The outputs are useful diagnostic and directional evidence, but not a clean causal estimate of stateful fuzzing's incremental bug yield.

    The follow-up #591 will selectively move appropriate strategy nodes to NoFuzz-style bug-search framing. It intentionally does not convert harness/invariant/differential construction nodes wholesale. A bounded blinded/paired A/B should precede broad rollout.

    ScFuzzBench interpretation

    The referenced ScFuzzBench run is evidence that automated stateful exploration can reach assertions requiring multiple dependent transitions. It is not direct evidence of several root-cause-distinct, confirmed Aave bugs: the UI reports assertion identities, includes two canaries and related solvency variants, and has ground-truth mapping disabled.

    Accordingly, ScFuzzBench supports the reachability premise, not the stronger claim that this Ultrafuzz treatment found a bug class unavailable to NoFuzz.

    The separate 2026-08-11 seqLen=100 artifact also does not change the paired result. Its raw trace was a one-wei Hub/Spoke rounding mismatch, metadata labeled it as solvency/property 25, and the final report demoted it to incomplete-spec. It was a detached/manual handoff rather than a sealed end-to-end campaign, so it should be retained as a candidate/lineage lesson, not counted as a confirmed stateful finding here.

    Reusable operational and product learnings

    • Fan-in must not terminate legitimate campaigns. Both arms failed fan-in. The concrete markdown-parity/description failure and repair are tracked in #583; success-path and failure-path regression coverage should prove that valid campaign artifacts continue downstream.
    • Selected properties need executable oracle validation. Tracked in #524.
    • One failing property must not retire unrelated invariant tests. Tracked in #589.
    • A zero-exit coverage tool can still produce vacuous output. Semantic validation is tracked in #590.
    • Lens reference authority remains inconsistent between prompt and gate. Tracked in #285.
    • We did not open duplicate issues for output-shape/JSON failures covered by the v0.0.16 schema-constrained output changes.
    • Strategy-node objective and output contract should match the desired work product. Selective conversion and evaluation are tracked in #591.

    Closing rationale

    The current evidence answers the research question at the resolution this experiment permits: it demonstrates the capability distinction and exposes a better experiment design, but it does not show a different confirmed Aave bug attributable to autonomous stateful fuzzing. The generic defects have been separated into actionable issues, and the prompt/topology follow-up has been created. Closing this investigation as complete does not mean stateful fuzzing is ineffective; it means the present paired run cannot establish its incremental bug yield.

  8. removed
    In ProgressClaimed and actively worked on; has an assignee. Remove if work stops.
    on Aug 14, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions