diff --git a/.design/basis/09-option-result.md b/.design/basis/09-option-result.md
index f14a151e0..15d1ae787 100644
--- a/.design/basis/09-option-result.md
+++ b/.design/basis/09-option-result.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 3c6a908da157641805a57c3f1ff18215ad79c8cf09a496d3a9d8a1dc043bc0e8 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 607df290746b38714bb16ddb6a651f2b52a23ed0cfdf4f515e7035ef00684a3d (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/ast.rs
 governs: thermite-syntax/src/parser.rs
 governs: thermite-spec/src/validator.rs
diff --git a/.design/basis/11-ergonomics.md b/.design/basis/11-ergonomics.md
index 3ea179af1..849618ec6 100644
--- a/.design/basis/11-ergonomics.md
+++ b/.design/basis/11-ergonomics.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 3c6a908da157641805a57c3f1ff18215ad79c8cf09a496d3a9d8a1dc043bc0e8 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 607df290746b38714bb16ddb6a651f2b52a23ed0cfdf4f515e7035ef00684a3d (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-syntax/src/parser.rs
 governs: thermite-syntax/src/ast.rs
 governs: thermite-lower/src/lower.rs
diff --git a/.design/basis/12-mutual-recursion.md b/.design/basis/12-mutual-recursion.md
index 0cf1a271b..6bee9bed0 100644
--- a/.design/basis/12-mutual-recursion.md
+++ b/.design/basis/12-mutual-recursion.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 5da96b53476e787c3488ff7769ef60bfada0c15797c235683d1fd57937c83946 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: a0626bfbc8c8a2afa354f257fa8d4b788f46cf1e7adfbd3e253ca0ab7a59a914 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: forge/src/check.rs
 governs: thermite-lower/src/lower.rs
 thesis-refs:
diff --git a/.design/forge/check.md b/.design/forge/check.md
index f16c9a62d..90bec1244 100644
--- a/.design/forge/check.md
+++ b/.design/forge/check.md
@@ -3,7 +3,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: a10f679dd2fd4ae2dad1fc8607c93d13413d0d019823f55b85f41b61e1578c7a (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 39db2140160524b596b95cffd085a1c025c06e0b2dd4820f590ee926c9d97198 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: forge/src/check.rs
 thesis-refs:
   - thermite-design.md §5.1
@@ -65,6 +65,46 @@ REQ status table).
 > widening, #101 equivalent-mutant exclusion, #232 struct-inv weave, #237
 > narrowing) extend the pipeline without contradicting the REQs above.
 
+> **Amendment 2026-07-28 (crosslink #92 — the ADT-referrer correction, R-HONEST-4).**
+> The per-item ADT weave (`#68`) seeded `reachable_adt_deps` with `[item] +
+> fn_deps` while every arm of `item_subprogram` wove `item_spec_items` as well, so
+> the referrer set was a strict subset of what the sub-program contained. An ADT
+> reachable only through a woven spec fn was omitted from the emitted Verus, and
+> the run failed closed on an unresolvable type. Three surfaces: a checked
+> `struct`/`enum` landed L0 on `E0425` (`collect_item_adt_refs` is inert on an ADT
+> decl, so `adt_deps` was empty for every ADT item) and dragged `project
+> assurance` to FAILED; a checked `fn` naming no ADT that a woven spec fn takes
+> aborted the run through `vacuity_solver::interpret_summary`'s undetermined-harness
+> refusal; a checked `spec fn` was already correct. A single-ADT file masked all
+> of it, because the only ADT is the checked item, which the ADT arm pushes itself
+> — so no corpus program declaring more than one ADT had ever certified. The seed
+> now extends with `item_spec_items` for every item kind (replaced, not extended,
+> for the `Item::SpecFn` arm — `#71`'s distinct per-spec-fn sub-program), and the
+> ADT arm drops the checked item from `adt_deps` before pushing it, keeping one
+> declaration. REQ-1's per-item pipeline and REQ-5's level rule are unchanged; this
+> corrects their input. Corpus anchor: `conformance/multi_adt.th` +
+> `conformance/multi_adt.cert.json`. Pin:
+> `forge/tests/divergence_multi_adt_subprogram.rs`. Same under-approximated-closure
+> class as the `reachable_spec_fn_deps` body-only omission recorded in
+> `.design/verified/proof-backends.md`'s increment-(i) build-blocker note.
+>
+> The same issue carried a diagnostics defect, corrected alongside. `run_verus`
+> took its scratch stem from `program.items.first()`, and `item_subprogram` weaves
+> ADT decls and spec fns ahead of the checked item, so any item with something
+> woven before it filed its diagnostics under a sibling's name — a failing `enum
+> Unused` reported `E0425` at `forge_is_owner_check_<pid>_<n>/is_owner_check.rs`
+> while `is_owner` itself certified L3. That misattribution is why #92 was first
+> read as two defects, the second being a hole in the L3 refusal path; there is no
+> such hole, and REQ-4's "the failed obligation and its source position" is not
+> satisfied by a position under another item's filename. `run_verus` now takes the
+> checked item's name as a `subject` parameter and no longer receives the
+> sub-program at all, so a harness cannot name a merely-woven member by accident;
+> the equivalence-probe call site's single-item `Program` wrapper, which existed
+> only to feed the old label machinery, is gone with it. Amendment item 6's
+> `<stem>.rs`-inside-`forge_<stem>_<pid>_<n>/` scheme and the AC-4 no-`.` crate-stem
+> property are both unchanged — only the source of `<stem>` moved. Pin:
+> `forge/tests/divergence_harness_names_checked_item.rs`.
+
 The stages, in order, are:
 
 ```
diff --git a/.design/lower/boundary-composition.md b/.design/lower/boundary-composition.md
index bd9b002b3..64cd25a7b 100644
--- a/.design/lower/boundary-composition.md
+++ b/.design/lower/boundary-composition.md
@@ -2,7 +2,7 @@
 <!--
 tier: 3-component
 status: draft
-audited-content-sha256: 5da96b53476e787c3488ff7769ef60bfada0c15797c235683d1fd57937c83946 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: a0626bfbc8c8a2afa354f257fa8d4b788f46cf1e7adfbd3e253ca0ab7a59a914 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
 governs: thermite-lower/src/lower.rs, forge/src/check.rs
 thesis-refs:
   - thermite-design.md §9
diff --git a/.design/verified/proof-backends.md b/.design/verified/proof-backends.md
index 67c0ad748..ea1fb7736 100644
--- a/.design/verified/proof-backends.md
+++ b/.design/verified/proof-backends.md
@@ -3,7 +3,7 @@
 <!--
 tier: 3-component
 status: draft (v-next architecture — the obligation/engine interface; most REQs NOT-STARTED
-audited-content-sha256: 28f745f55a4e7bb8ddf941decb241d4473ed924790c5ddfa3b95711b973e111e (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
+audited-content-sha256: 831c0ced80f6072a740c22b3356cdeccb5cc22def9928431891e4391abf6bfe3 (migrated from legacy audited-sha commit pin to a squash-stable content digest; doc-drift-tripwire.md REQ-2 — content pin is primary, commit pin is a migration fallback)
         behind build blockers. The SHIPPED substrates this builds on are quoted-code-grounded.)
 governs: forge/src/check.rs + forge/src/degrade.rs + forge/src/manifest.rs (the discharge
          pipeline, the ladder, the certificate this interface generalizes) and
diff --git a/conformance/multi_adt.cert.json b/conformance/multi_adt.cert.json
new file mode 100644
index 000000000..7a8e45e86
--- /dev/null
+++ b/conformance/multi_adt.cert.json
@@ -0,0 +1,11 @@
+{
+  "item": "authorize",
+  "level": "L3",
+  "contract_quality": {
+    "tautology": false,
+    "vacuous_precondition": false
+  },
+  "effects": ["pure"],
+  "slag": false,
+  "note": "Stable-subset oracle (goal.md R-CHAR-3): item/level/tautology/vacuous_precondition/effects/slag are hand-derived from .design/forge/check.md REQ-5 (L3 iff verus reports 0 errors) + .design/basis/01-adts.md (REQ-2 enum, REQ-9 enum->Verus + match->Verus match) + thermite-design.md §6 ladder, and are oracle-compared. mutants_killed + solver_time_ms are tool-computed + EXCLUDED (oracle_subset, §5.3). HAND-DERIVATION: `authorize(r, a)` returns true for Owner (either Action), false for Player+Ban, true for Player+Chat. The ens `result == (may_ban(r) || !is_ban(a))` evaluates to: Owner -> may_ban true -> true (both actions); Player+Ban -> false || !true -> false; Player+Chat -> false || !false -> true. Body and contract agree on all four inhabitants of Role x Action, so every obligation discharges -> L3. NON-VACUOUS: a constant-true body fails at Player+Ban, so the ens constrains (R-DEFER-9); req `true` is satisfiable (a total function has no precondition). fx pure -> effects [\"pure\"]; no #[slag] -> slag false. THIS FILE IS THE crosslink #92 CORPUS ANCHOR: it is the first corpus program declaring more than one ADT, the shape that could not certify before #92 (the per-item sub-program omitted the ADTs reachable only through a woven spec fn, so `Role` and `Action` each landed L0 on E0425 and the project verdict was FAILED). The per-item levels of `Role`/`Action` are pinned in forge/tests/divergence_multi_adt_subprogram.rs."
+}
diff --git a/conformance/multi_adt.th b/conformance/multi_adt.th
new file mode 100644
index 000000000..1815aabec
--- /dev/null
+++ b/conformance/multi_adt.th
@@ -0,0 +1,25 @@
+enum Role { Owner, Player }
+enum Action { Ban, Chat }
+
+spec fn may_ban(r: Role) -> bool
+  dec r
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+
+spec fn is_ban(a: Action) -> bool
+  dec a
+{
+  match a { Action::Ban => true, Action::Chat => false }
+}
+
+fn authorize(r: Role, a: Action) -> bool
+  req true
+  ens result == (may_ban(r) || !is_ban(a))
+  fx  pure
+{
+  match r {
+    Role::Owner => true,
+    Role::Player => match a { Action::Ban => false, Action::Chat => true },
+  }
+}
diff --git a/forge/src/check.rs b/forge/src/check.rs
index 92e55b99e..0e4675712 100644
--- a/forge/src/check.rs
+++ b/forge/src/check.rs
@@ -660,17 +660,38 @@ pub fn check_file_with_options(
             Item::SpecFn(_) => reachable_spec_fn_deps(&parsed.program, item.name()),
             _ => spec_items.clone(),
         };
-        // For a checked `Item::SpecFn`, the ADT referrers are its own reachable
-        // spec-fn set (which includes the spec fn itself), so its `enum`/`struct`
-        // decls are present even though the file's full `spec_items` is no longer
-        // woven (#71). The `Item::Fn` path is unchanged — its ADT referrers stay
-        // `[item] + fn_deps` exactly as before (the exec sub-program is byte-stable;
-        // the corpus cert oracle is unperturbed). The Fn arm of `item_subprogram`
-        // still weaves the full `spec_items`.
+        // #92: the referrer set covers everything `item_subprogram` weaves. Every
+        // arm of `item_subprogram` weaves `item_spec_items`, so the spec fns seed
+        // the ADT walk too — an ADT reachable only through a woven spec fn is
+        // otherwise absent from the sub-program and verus cannot resolve it
+        // (`E0425 cannot find type`).
+        //
+        // Before #92 the seed was `[item] + fn_deps`, a strict subset of what is
+        // woven, which surfaced three ways:
+        //   - a checked `struct`/`enum`: `collect_item_adt_refs` is inert on an ADT
+        //     decl (its own field types are followed by the type-graph fixed point
+        //     instead), so `adt_deps` came out empty for every ADT item, while the
+        //     ADT arm weaves the file's whole `spec_items`. A spec fn naming a
+        //     second ADT dangled, so the item landed L0 and the project verdict
+        //     FAILED. A single-ADT file hid this: the only ADT is the checked item,
+        //     which the ADT arm pushes itself.
+        //   - a checked `fn` whose contract and body name no ADT that a woven spec
+        //     fn takes: the solver-vacuity harness failed to elaborate, which
+        //     `vacuity_solver::interpret_summary` refuses as undetermined — a
+        //     `ForgeError` aborting the run (fail-closed, never a silent clean).
+        //   - a checked `spec fn`: already correct via the clear+extend below, which
+        //     is why the single-ADT corpus never exercised the gap.
+        // This is the same under-approximated-closure class the proof-backends
+        // build-blocker note records for `reachable_spec_fn_deps` walking
+        // `decl.body` without `decl.dec`.
+        //
+        // For a checked `Item::SpecFn` the referrers are its own reachable spec-fn
+        // closure alone (which includes the spec fn itself) — #71's distinct
+        // per-spec-fn sub-program — so the seed is replaced rather than extended.
         if matches!(item, Item::SpecFn(_)) {
             referrers.clear();
-            referrers.extend(item_spec_items.iter());
         }
+        referrers.extend(item_spec_items.iter());
         let adt_deps = reachable_adt_deps(&parsed.program, &referrers);
         let sub = item_subprogram(item, &item_spec_items, &fn_deps, &adt_deps);
         let lowered = thermite_lower::lower(&sub).map_err(ForgeError::Lower)?;
@@ -774,7 +795,7 @@ pub fn check_file_with_options(
         // Clean (or a `spec fn`, which carries no contract to check): the solver
         // runs the real L3 proof (REQ-3). Assemble the cert exactly as the
         // non-cached path always has.
-        let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+        let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
         let cert = assemble_certificate(item, &verus);
 
         // #10 automatic degrade ladder (`.design/forge/degrade-ladder.md`, the
@@ -3874,7 +3895,16 @@ fn item_subprogram(
         // `adt_deps`/`spec_items` for an `inv`-free struct keeps the sub-program
         // the item alone (byte-stable for the no-invariant corpus).
         Item::Struct(_) | Item::Enum(_) => {
-            let mut items = adt_deps.to_vec();
+            // #92: since the referrer seed includes the woven `spec_items`, a spec
+            // fn naming the checked ADT puts that ADT in `adt_deps` as well. The
+            // item is pushed below, so drop it here to keep one declaration —
+            // verus rejects a duplicate definition (`E0428`). The other decls a
+            // spec fn reaches stay, which is the point of the fix.
+            let mut items: Vec<Item> = adt_deps
+                .iter()
+                .filter(|d| d.name() != item.name())
+                .cloned()
+                .collect();
             items.extend(spec_items.iter().cloned());
             items.push(item.clone());
             Program { items }
@@ -5152,16 +5182,30 @@ impl Drop for ScratchDir {
 /// with parseable failure → a reported failure cert; unparseable output →
 /// `ForgeError::VerusOutput` (REQ-3).
 fn run_verus(
-    program: &Program,
     lowered: &str,
+    subject: &str,
     seed: u64,
     rlimit: f64,
 ) -> Result<VerusResult, ForgeError> {
-    // Name the scratch dir + `.rs` after the first item (deterministic) so
-    // concurrent runs over different files do not collide; fall back to a fixed
-    // stem. The crate-name gotcha (REQ-2 / AC-4) is unchanged: the `.rs` stem is
-    // still the no-`.` `crate_stem`, so verus's crate-name derivation succeeds.
-    let label = program.items.first().map(|i| i.name()).unwrap_or("forge");
+    // Name the scratch dir + `.rs` after the item this harness is checking
+    // (deterministic) so concurrent runs over different files do not collide.
+    //
+    // #92: the label was `program.items.first()` — the first item of the woven
+    // SUB-program, which is the checked item only when nothing is woven ahead of
+    // it. `item_subprogram` weaves ADT decls and spec fns first and pushes the
+    // checked item last, so a failing `enum Unused` reported its diagnostics under
+    // `forge_is_owner_check_<pid>_<n>/is_owner_check.rs` — naming a sibling that
+    // was merely woven in. The reporter of #92 read that path as the failure
+    // belonging to `is_owner` (certified L3) and concluded the L3 refusal path had
+    // a hole; it did not. A harness names what it checks.
+    //
+    // The sub-program is deliberately not a parameter: taking the label from it
+    // is what went wrong, and a harness that cannot see the woven set cannot name
+    // one of its members by accident.
+    //
+    // The crate-name gotcha (REQ-2 / AC-4) is unchanged: the `.rs` stem is still
+    // the no-`.` `crate_stem`, so verus's crate-name derivation succeeds.
+    let label = if subject.is_empty() { "forge" } else { subject };
     let stem = crate_stem(Path::new(label));
     let scratch = ScratchDir {
         path: unique_scratch_dir(&stem),
@@ -5693,13 +5737,13 @@ fn mutation_score(
             if let Some(stored) = cache::load(cache_dir, &key) {
                 mutant_cert_is_survivor(&stored)
             } else {
-                let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+                let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
                 let cert = assemble_certificate(&item, &verus);
                 let _ = cache::store(cache_dir, &key, &cert);
                 mutant_cert_is_survivor(&cert)
             }
         } else {
-            let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+            let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
             mutant_outcome_is_survivor(&verus.outcome)
         };
 
@@ -5833,11 +5877,10 @@ fn equivalence_proves_equal(
         // carried (never a silent collapse into the proved-distinguishing bucket).
         Err(e) => return Ok(EquivOutcome::Unsupported(e.to_string())),
     };
-    // The obligation is a complete Verus program (the seam emits the frame); run
-    // it as a single-item program for the `run_verus` scratch-dir/label machinery.
-    let label_program = Program {
-        items: vec![Item::Fn(f.clone())],
-    };
+    // The obligation is a complete Verus program (the seam emits the frame), so it
+    // needs no woven sub-program. #92: it used to be wrapped in a single-item
+    // `Program` purely to feed `run_verus`'s label machinery; `run_verus` now takes
+    // the subject name directly, so the wrapper (and its `f.clone()`) is gone.
     let key = cache::cache_key(&obligation, seed, verus_version, THERMITE_VERSION);
     let proved = if use_cache {
         if let Some(stored) = cache::load(cache_dir, &key) {
@@ -5846,7 +5889,7 @@ fn equivalence_proves_equal(
             // mutant kill-check caches — a `Proved` obligation is "survivor"-true).
             mutant_cert_is_survivor(&stored)
         } else {
-            let verus = run_verus(&label_program, &obligation, seed, rlimit)?;
+            let verus = run_verus(&obligation, &f.name, seed, rlimit)?;
             let proved = mutant_outcome_is_survivor(&verus.outcome);
             // Cache the equivalence verdict (REQ-6 determinism): assemble + store
             // the same cert shape the mutant kill-check stores, keyed on the
@@ -5857,7 +5900,7 @@ fn equivalence_proves_equal(
             proved
         }
     } else {
-        let verus = run_verus(&label_program, &obligation, seed, rlimit)?;
+        let verus = run_verus(&obligation, &f.name, seed, rlimit)?;
         mutant_outcome_is_survivor(&verus.outcome)
     };
     // The exclusion fires only on a verus-proved `ensures` (REQ-2/REQ-3/REQ-8):
@@ -5966,12 +6009,12 @@ fn strengthen_certificate(
             if let Some(stored) = cache::load(cache_dir, &key) {
                 return Ok(mutant_cert_is_survivor(&stored));
             }
-            let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+            let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
             let cert = assemble_certificate(&item, &verus);
             let _ = cache::store(cache_dir, &key, &cert);
             Ok(mutant_cert_is_survivor(&cert))
         } else {
-            let verus = run_verus(&sub, &lowered, seed, rlimit)?;
+            let verus = run_verus(&lowered, item.name(), seed, rlimit)?;
             Ok(mutant_outcome_is_survivor(&verus.outcome))
         }
     };
diff --git a/forge/tests/divergence_harness_names_checked_item.rs b/forge/tests/divergence_harness_names_checked_item.rs
new file mode 100644
index 000000000..d930923de
--- /dev/null
+++ b/forge/tests/divergence_harness_names_checked_item.rs
@@ -0,0 +1,180 @@
+//! Divergence pin (crosslink #92, the diagnostics half) — a per-item verus
+//! harness was named after the FIRST item of the woven sub-program rather than
+//! the item it checks, so a failure reported its source location under a
+//! sibling's name.
+//!
+//! `run_verus` took its scratch-dir/`.rs` stem from
+//! `program.items.first().map(|i| i.name())`. `item_subprogram` weaves the ADT
+//! decls and spec fns first and pushes the checked item LAST, so any item with
+//! anything woven ahead of it reported diagnostics under the wrong name:
+//!
+//!   spec fn helper(n: u64) -> u64 { n }
+//!   fn bad(x: u64) -> u64 ens result == helper(x) + 1 { x }   // cannot hold
+//!
+//! `bad`'s sub-program is `[helper, bad]`, so `bad`'s failed postcondition was
+//! reported at `helper_check.rs:13:9` — naming a function that certified L3.
+//!
+//! This is not cosmetic. It is what made #92 look like two bugs instead of one:
+//! the reporter saw `E0425` under `/tmp/forge_is_owner_check_*/is_owner_check.rs`
+//! while `is_owner` certified L3, and reasonably concluded that a harness which
+//! failed to compile could coexist with an L3 on the same item — i.e. that the
+//! L3 refusal path had a hole. It does not. The failing harness belonged to
+//! `Unused` (correctly L0); only its NAME pointed at `is_owner`. A diagnostic
+//! that misattributes its subject sends the next reader hunting a defect that
+//! is not there.
+//!
+//! The fix drops the sub-program from `run_verus` entirely and passes the
+//! checked item's name, so the harness cannot name a merely-woven member even by
+//! accident.
+//!
+//! The authority (R-CHAR-3): `.design/forge/check.md` REQ-4 requires each failing
+//! obligation to carry "the obligation description and the concrete failure
+//! witness … the failed obligation and its source position" — a position under a
+//! sibling's filename does not identify the subject. AC-4 (the crate-name gotcha:
+//! stem has no `.`) is preserved and independently pinned by
+//! `crate_stem_has_no_dot_and_is_valid`. The expected stem `bad_check` is derived
+//! from the fixture's own item name plus the documented `<stem>.rs` scheme
+//! (Amendment item 6), never copied from the toolchain's output.
+//!
+//! Verus check skips with an eprintln when verus is absent (`editor_runs.rs`
+//! precedent). `tests/` is not anti-pattern-gated (R-APG-2).
+
+use std::path::{Path, PathBuf};
+use std::process::Command;
+
+use serde_json::Value;
+
+fn forge_bin() -> PathBuf {
+    PathBuf::from(env!("CARGO_BIN_EXE_forge"))
+}
+
+/// `true` iff verus is reachable (mirrors `divergence_multi_adt_subprogram.rs`).
+fn verus_present() -> bool {
+    if let Ok(p) = std::env::var("VERUS_BIN") {
+        if Path::new(&p).exists() {
+            return true;
+        }
+    }
+    if let Ok(out) = Command::new("which").arg("verus").output() {
+        if out.status.success() && !String::from_utf8_lossy(&out.stdout).trim().is_empty() {
+            return true;
+        }
+    }
+    if let Ok(home) = std::env::var("HOME") {
+        if PathBuf::from(home).join(".local/bin/verus").exists() {
+            return true;
+        }
+    }
+    false
+}
+
+/// A spec fn (woven first) plus an exec fn whose `ens` cannot hold. `bad`'s
+/// sub-program is `[helper, bad]`, so pre-#92 its diagnostics were filed under
+/// `helper_check.rs`.
+const WOVEN_AHEAD_PROGRAM: &str = "\
+spec fn helper(n: u64) -> u64
+  dec n
+{
+  n
+}
+
+fn bad(x: u64) -> u64
+  req true
+  ens result == helper(x) + 1
+  fx  pure
+{
+  x
+}
+";
+
+fn check_program(tag: &str, program: &str) -> Vec<Value> {
+    let fixture = std::env::temp_dir().join(format!(
+        "forge_harness_naming_{tag}_{}.th",
+        std::process::id()
+    ));
+    std::fs::write(&fixture, program).expect("write fixture");
+    let out = Command::new(forge_bin())
+        .arg("check")
+        .arg(&fixture)
+        .arg("--json")
+        .output()
+        .expect("spawn forge check");
+    let _ = std::fs::remove_file(&fixture);
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    serde_json::from_str::<Value>(stdout.trim())
+        .unwrap_or_else(|e| {
+            panic!(
+                "[{tag}] forge check --json stdout must be one JSON doc: {e}\nstdout:\n{stdout}\nstderr:\n{}",
+                String::from_utf8_lossy(&out.stderr)
+            )
+        })
+        .as_array()
+        .unwrap_or_else(|| panic!("[{tag}] forge check --json must emit an array of certs"))
+        .clone()
+}
+
+/// Every `location` string across an item's obligations.
+fn locations_of(certs: &[Value], item: &str) -> Vec<String> {
+    certs
+        .iter()
+        .find(|c| c.get("item").and_then(|v| v.as_str()) == Some(item))
+        .unwrap_or_else(|| panic!("no cert for `{item}` in {certs:#?}"))
+        .get("obligations")
+        .and_then(|o| o.as_array())
+        .unwrap_or_else(|| panic!("cert for `{item}` has no obligations array"))
+        .iter()
+        .filter_map(|o| o.get("location").and_then(|v| v.as_str()))
+        .map(|s| s.to_string())
+        .collect()
+}
+
+#[test]
+fn a_failing_obligation_is_located_in_the_checked_items_harness() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — harness-naming pin not run.");
+        return;
+    }
+    let certs = check_program("woven_ahead", WOVEN_AHEAD_PROGRAM);
+    let locs = locations_of(&certs, "bad");
+    assert!(
+        !locs.is_empty(),
+        "`bad`'s ens cannot hold, so it must carry a located failed obligation \
+         (.design/forge/check.md REQ-4); got {locs:?}"
+    );
+    for loc in &locs {
+        assert!(
+            loc.starts_with("bad_check."),
+            "a failed obligation must be located in the harness of the item under \
+             check (`bad_check.rs`), not in a merely-woven sibling's; got `{loc}`"
+        );
+        // The specific pre-#92 misattribution: `helper` is woven first and
+        // certifies L3, yet lent its name to `bad`'s failure.
+        assert!(
+            !loc.contains("helper"),
+            "the harness must not be named after a woven spec fn; got `{loc}`"
+        );
+    }
+}
+
+#[test]
+fn the_woven_spec_fn_still_certifies_and_owns_its_own_harness() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — harness-naming sibling check not run.");
+        return;
+    }
+    // The other half of the misread: `helper` is fine. Pinning it here makes the
+    // pair explicit — one item failed, a different item was named, and the two
+    // facts were easy to fuse into a phantom "L3 coexisting with a broken
+    // harness" bug.
+    let certs = check_program("sibling", WOVEN_AHEAD_PROGRAM);
+    let level = certs
+        .iter()
+        .find(|c| c.get("item").and_then(|v| v.as_str()) == Some("helper"))
+        .expect("cert for helper")["level"]
+        .as_str()
+        .expect("string level");
+    assert_eq!(
+        level, "L3",
+        "the woven spec fn certifies on its own merits (.design/forge/check.md REQ-5)"
+    );
+}
diff --git a/forge/tests/divergence_multi_adt_subprogram.rs b/forge/tests/divergence_multi_adt_subprogram.rs
new file mode 100644
index 000000000..e611e8251
--- /dev/null
+++ b/forge/tests/divergence_multi_adt_subprogram.rs
@@ -0,0 +1,274 @@
+//! Divergence pin (crosslink #92) — no file declaring more than one ADT could
+//! certify, because `forge::check`'s referrer seed for `reachable_adt_deps` was a
+//! strict subset of what `item_subprogram` weaves.
+//!
+//! Every arm of `item_subprogram` weaves `item_spec_items`, but only the
+//! `Item::SpecFn` arm seeded those spec fns as ADT referrers. An ADT reachable
+//! only through a woven spec fn was therefore absent from the emitted sub-program
+//! and verus could not resolve it. Three surfaces, all live-confirmed:
+//!
+//!   1. a checked `struct`/`enum`: `collect_item_adt_refs` is inert on an ADT decl
+//!      (field types are followed by the type-graph fixed point instead), so
+//!      `adt_deps` came out empty for every ADT item while the arm wove the file's
+//!      whole `spec_items` — a spec fn naming a second ADT dangled, the item landed
+//!      L0 on `E0425 cannot find type`, and `project assurance` was FAILED;
+//!   2. a checked `fn` whose contract and body name no ADT that a woven spec fn
+//!      takes: the solver-vacuity harness failed to elaborate, which
+//!      `vacuity_solver::interpret_summary` refuses as undetermined — a `ForgeError`
+//!      aborting the whole run;
+//!   3. a checked `spec fn`: already correct, which is why a single-ADT corpus
+//!      never exercised the gap.
+//!
+//! One ADT masks all of it: the only ADT is the checked item, which the ADT arm
+//! pushes itself, so the decl is present by construction. This is the same
+//! under-approximated-closure class `.design/verified/proof-backends.md` records
+//! for `reachable_spec_fn_deps` walking `decl.body` without `decl.dec`.
+//!
+//! The authority (R-CHAR-3): expected level L3 is the design contract —
+//! `.design/forge/check.md` REQ-5 (L3 iff verus reports 0 errors) +
+//! `thermite-design.md` §6 (L3 == a fully-discharged real-verus proof) +
+//! `.design/basis/01-adts.md` REQ-2/REQ-9 (enum -> Verus enum, match -> Verus
+//! match). The corpus anchor is `conformance/multi_adt.th` +
+//! `conformance/multi_adt.cert.json` (hand-derived). Adding a declaration that
+//! the rest of the file does not reference cannot change what is provable about
+//! the other items, so the single-ADT twin's levels ARE the oracle for the
+//! two-ADT file. Expected values never copied from the toolchain's output.
+//!
+//! Verus checks skip with an eprintln when verus is absent (`editor_runs.rs`
+//! precedent). `tests/` is not anti-pattern-gated, so `unwrap`/`panic!` are fine
+//! (R-APG-2).
+
+use std::path::{Path, PathBuf};
+use std::process::Command;
+
+use serde_json::Value;
+
+fn forge_bin() -> PathBuf {
+    PathBuf::from(env!("CARGO_BIN_EXE_forge"))
+}
+
+/// `true` iff verus is reachable (mirrors `divergence_struct_inv_spec_fn_subprogram.rs`).
+fn verus_present() -> bool {
+    if let Ok(p) = std::env::var("VERUS_BIN") {
+        if Path::new(&p).exists() {
+            return true;
+        }
+    }
+    if let Ok(out) = Command::new("which").arg("verus").output() {
+        if out.status.success() && !String::from_utf8_lossy(&out.stdout).trim().is_empty() {
+            return true;
+        }
+    }
+    if let Ok(home) = std::env::var("HOME") {
+        if PathBuf::from(home).join(".local/bin/verus").exists() {
+            return true;
+        }
+    }
+    false
+}
+
+/// Run `forge check --json` over an inline program. Panics with the captured
+/// stderr when the run aborts, which is itself surface 2's pre-fix symptom (a
+/// `ForgeError` from the vacuity harness, not a cert array).
+fn check_program(tag: &str, program: &str) -> Vec<Value> {
+    let fixture = std::env::temp_dir().join(format!(
+        "forge_multi_adt_subprog_{tag}_{}.th",
+        std::process::id()
+    ));
+    std::fs::write(&fixture, program).expect("write fixture");
+    let out = Command::new(forge_bin())
+        .arg("check")
+        .arg(&fixture)
+        .arg("--json")
+        .output()
+        .expect("spawn forge check");
+    let _ = std::fs::remove_file(&fixture);
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    serde_json::from_str::<Value>(stdout.trim())
+        .unwrap_or_else(|e| {
+            panic!(
+                "[{tag}] forge check --json stdout must be one JSON doc: {e}\nstdout:\n{stdout}\nstderr:\n{}",
+                String::from_utf8_lossy(&out.stderr)
+            )
+        })
+        .as_array()
+        .unwrap_or_else(|| panic!("[{tag}] forge check --json must emit an array of certs"))
+        .clone()
+}
+
+fn level_of(certs: &[Value], item: &str) -> String {
+    certs
+        .iter()
+        .find(|c| c.get("item").and_then(|v| v.as_str()) == Some(item))
+        .unwrap_or_else(|| panic!("no cert for `{item}` in {certs:#?}"))["level"]
+        .as_str()
+        .unwrap_or_else(|| panic!("cert for `{item}` has no string level"))
+        .to_string()
+}
+
+/// Surface 1, the reported repro: two enums where a spec fn names only the first.
+/// `Unused` is declared and never mentioned again; pre-#92 it certified L0 with
+/// `E0425 cannot find type Role` — the dangling reference belonging to `is_owner`,
+/// which the ADT arm wove into `Unused`'s sub-program without `Role`.
+const SPARE_DECL_PROGRAM: &str = "\
+enum Role { Owner, Player }
+enum Unused { A, B }
+
+spec fn is_owner(r: Role) -> bool
+  dec r
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+
+fn check(r: Role) -> bool
+  req true
+  ens result == is_owner(r)
+  fx  pure
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+";
+
+/// The single-ADT twin of [`SPARE_DECL_PROGRAM`], byte-identical but for the
+/// spare `enum Unused` line. Its levels are the oracle for the two-ADT file.
+const SINGLE_ADT_TWIN: &str = "\
+enum Role { Owner, Player }
+
+spec fn is_owner(r: Role) -> bool
+  dec r
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+
+fn check(r: Role) -> bool
+  req true
+  ens result == is_owner(r)
+  fx  pure
+{
+  match r { Role::Owner => true, Role::Player => false }
+}
+";
+
+/// Surface 2: the checked exec fn `g` names no ADT at all, but the woven
+/// `spec_items` include `p`, whose parameter is an `enum E`. Pre-#92 the
+/// solver-vacuity harness failed to elaborate and the whole run aborted with a
+/// `ForgeError` rather than emitting certs.
+const EXEC_FN_UNMENTIONED_ADT: &str = "\
+enum E { A, B }
+
+spec fn p(e: E) -> bool
+  dec e
+{
+  match e { E::A => true, E::B => false }
+}
+
+fn g(x: u64) -> u64
+  req x < 10
+  ens result == x
+  fx  pure
+{
+  x
+}
+";
+
+#[test]
+fn spare_adt_decl_does_not_break_its_siblings() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — multi-ADT sub-program cert not run.");
+        return;
+    }
+    let certs = check_program("spare", SPARE_DECL_PROGRAM);
+
+    // .design/forge/check.md REQ-5 + thermite-design.md §6: a correct source
+    // certifies L3. `Unused` carries no contract to discharge, exactly as `Role`
+    // does; both are enum decls lowering to a Verus enum (01-adts REQ-9).
+    assert_eq!(
+        level_of(&certs, "Role"),
+        "L3",
+        "the referenced enum must certify"
+    );
+    assert_eq!(
+        level_of(&certs, "Unused"),
+        "L3",
+        "an enum the file never references must certify — its sub-program weaves \
+         the file's spec fns, so it must also weave the ADTs those spec fns name"
+    );
+    assert_eq!(level_of(&certs, "is_owner"), "L3");
+    assert_eq!(level_of(&certs, "check"), "L3");
+}
+
+#[test]
+fn a_spare_adt_decl_changes_no_sibling_level() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — multi-ADT twin comparison not run.");
+        return;
+    }
+    // The oracle: adding a declaration nothing references cannot change what is
+    // provable about the other items, so every shared item's level must match its
+    // single-ADT twin. This is the R-CHAR-3 anchor for the levels above — the twin
+    // is the external truth, not forge's own output on the two-ADT file.
+    let twin = check_program("twin", SINGLE_ADT_TWIN);
+    let spare = check_program("spare_cmp", SPARE_DECL_PROGRAM);
+    for item in ["Role", "is_owner", "check"] {
+        assert_eq!(
+            level_of(&spare, item),
+            level_of(&twin, item),
+            "`{item}`'s level must be invariant under adding an unreferenced decl"
+        );
+    }
+}
+
+#[test]
+fn exec_fn_certifies_when_a_woven_spec_fn_names_an_unmentioned_adt() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — vacuity-harness weave not run.");
+        return;
+    }
+    // Pre-#92 this did not merely mis-level: `forge check` aborted with
+    // "a solver-vacuity harness failed to compile/elaborate before verification".
+    // `check_program` panics on a non-JSON stdout, so reaching the asserts at all
+    // is half the pin.
+    let certs = check_program("exec", EXEC_FN_UNMENTIONED_ADT);
+    assert_eq!(level_of(&certs, "g"), "L3", "the exec fn must certify");
+    assert_eq!(level_of(&certs, "E"), "L3");
+    assert_eq!(level_of(&certs, "p"), "L3");
+}
+
+#[test]
+fn multi_adt_corpus_program_certifies_end_to_end() {
+    if !verus_present() {
+        eprintln!("SKIP: verus not available — multi_adt corpus cert not run.");
+        return;
+    }
+    // The corpus anchor: conformance/multi_adt.th is the first corpus program
+    // declaring more than one ADT. Its golden pins `authorize` (the fn-only
+    // golden convention); the ADT items are pinned here.
+    let corpus = PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("..")
+        .join("conformance")
+        .join("multi_adt.th");
+    let out = Command::new(forge_bin())
+        .arg("check")
+        .arg(&corpus)
+        .arg("--json")
+        .output()
+        .expect("spawn forge check");
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    let certs = serde_json::from_str::<Value>(stdout.trim())
+        .unwrap_or_else(|e| {
+            panic!(
+                "forge check --json on the corpus program must be one JSON doc: {e}\nstdout:\n{stdout}\nstderr:\n{}",
+                String::from_utf8_lossy(&out.stderr)
+            )
+        })
+        .as_array()
+        .expect("array of certs")
+        .clone();
+    for item in ["Role", "Action", "may_ban", "is_ban", "authorize"] {
+        assert_eq!(
+            level_of(&certs, item),
+            "L3",
+            "every item of the multi-ADT corpus program must certify L3"
+        );
+    }
+}