diff --git a/evals/unsafe-rust/fixtures/pilot/README.md b/evals/unsafe-rust/fixtures/pilot/README.md
new file mode 100644
index 0000000000..3217cc458a
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/pilot/README.md
@@ -0,0 +1,52 @@
+# Exploratory Pilot Fixtures
+
+> **Evaluator-only material.** Do not expose this file, its directory names, or
+> both members of a pair to an evaluated agent.
+
+These source-only fixtures were frozen for the 2026-07-30 exploratory
+evaluation. They are deliberately small enough to review without compiling or
+executing target code.
+
+The pilot uses a common support policy:
+
+- Rust 1.85.0;
+- every ordinary build profile;
+- `debug_assertions` enabled and disabled;
+- every public item is supported API; and
+- no additional deployment restriction.
+
+## Synthetic vulnerable oracle
+
+The vulnerable member contains six independently scored atoms:
+
+| ID | Required conclusion |
+|---|---|
+| M1 | The entirely safe call `decode_flag(2)` creates an invalid `bool`; `UNSOUND`. |
+| M2 | A caller-provided safe `AddressSource` implementation may return an unreadable pointer consumed by `load_source`; `UNSOUND`. |
+| M3 | Safe construction through the public `ByteHandle::address` field does not establish dereferenceability; `UNSOUND`. |
+| M4 | A contract-satisfying call to `item_unchecked(&[0x10, 0x20], 1)` returns the wrong element without itself reaching UB; `CONTRACT-BROKEN`. |
+| M5 | With debug assertions disabled, the macro-generated public safe function permits an unchecked out-of-bounds access; `UNSOUND`. |
+| M6 | `checked_first` is sound due to the preceding emptiness check, but its stated safety rationale is false; proof-comment defect without condemning the implementation. |
+
+Recovery requires the correct surface, violated or missing proposition, and a
+defensible classification. M1–M4 and M6 have configuration closure
+preregistered as not applicable to the atom-specific score; all seven common
+dimensions apply to M5.
+
+The fixed member removes each of these six semantic defects. It deliberately
+retains an unsafe block in `item_unchecked` without a proof-grade adjacent
+comment, so it is a bug-specific fixed control rather than a proof-complete
+whole-crate control. An agent may correctly report that proof-artifact defect;
+it must not reproduce any repaired finding.
+
+## Admission and interpretation
+
+The six atoms were specified before evaluated-agent reports were observed.
+One independent source reviewer and the evaluator agreed on the atoms before
+the first result was scored. The pilot is nevertheless not a release
+evaluation: it has one replicate per cell and lacks the plan's hardened
+filesystem, documentation, network, package, and paired-side isolation.
+
+Historical zerocopy and current-zerocopy pilot targets remain Candidate or
+Challenge fixtures. Their results are descriptive until their authority-rooted
+oracles complete the two-reviewer admission process.
diff --git a/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/Cargo.toml b/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/Cargo.toml
new file mode 100644
index 0000000000..16b72d1f33
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "opaque-byte-tools"
+version = "0.1.0"
+edition = "2021"
+rust-version = "1.85"
+
+[lib]
+path = "src/lib.rs"
diff --git a/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/SUPPORT.md b/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/SUPPORT.md
new file mode 100644
index 0000000000..b1c5707fcc
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/SUPPORT.md
@@ -0,0 +1,7 @@
+# Support policy
+
+This crate supports Rust 1.85.0.
+
+All ordinary build profiles are supported. Debug assertions may be enabled or
+disabled. Every public item is supported API. There are no additional
+deployment restrictions.
diff --git a/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/src/lib.rs b/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/src/lib.rs
new file mode 100644
index 0000000000..0369076ea9
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/pilot/synthetic-fixed/src/lib.rs
@@ -0,0 +1,59 @@
+#![deny(unsafe_op_in_unsafe_fn)]
+
+pub fn decode_flag(raw: u8) -> bool {
+    match raw {
+        0 => false,
+        1 => true,
+        _ => panic!("invalid flag byte"),
+    }
+}
+
+pub trait AddressSource {
+    fn byte(&self) -> &u8;
+}
+
+pub fn load_source<S: AddressSource>(source: &S) -> u8 {
+    *source.byte()
+}
+
+pub struct ByteHandle<'a> {
+    address: &'a u8,
+}
+
+impl<'a> ByteHandle<'a> {
+    pub fn new(address: &'a u8) -> Self {
+        Self { address }
+    }
+
+    pub fn load(&self) -> u8 {
+        *self.address
+    }
+}
+
+/// Returns `bytes[index]`.
+///
+/// # Safety
+///
+/// `index` must be less than `bytes.len()`.
+pub unsafe fn item_unchecked(bytes: &[u8], index: usize) -> u8 {
+    unsafe { *bytes.get_unchecked(index) }
+}
+
+macro_rules! make_indexer {
+    ($name:ident) => {
+        pub fn $name(bytes: &[u8], index: usize) -> u8 {
+            bytes[index]
+        }
+    };
+}
+
+make_indexer!(profile_index);
+
+pub fn checked_first(bytes: &[u8]) -> Option<u8> {
+    if bytes.is_empty() {
+        return None;
+    }
+    // SAFETY: The preceding emptiness check establishes that index 0 is
+    // in-bounds.
+    Some(unsafe { *bytes.get_unchecked(0) })
+}
diff --git a/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/Cargo.toml b/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/Cargo.toml
new file mode 100644
index 0000000000..16b72d1f33
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "opaque-byte-tools"
+version = "0.1.0"
+edition = "2021"
+rust-version = "1.85"
+
+[lib]
+path = "src/lib.rs"
diff --git a/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/SUPPORT.md b/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/SUPPORT.md
new file mode 100644
index 0000000000..b1c5707fcc
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/SUPPORT.md
@@ -0,0 +1,7 @@
+# Support policy
+
+This crate supports Rust 1.85.0.
+
+All ordinary build profiles are supported. Debug assertions may be enabled or
+disabled. Every public item is supported API. There are no additional
+deployment restrictions.
diff --git a/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/src/lib.rs b/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/src/lib.rs
new file mode 100644
index 0000000000..d9d3d33952
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/pilot/synthetic-vulnerable/src/lib.rs
@@ -0,0 +1,53 @@
+#![deny(unsafe_op_in_unsafe_fn)]
+
+use core::{mem, ptr::NonNull};
+
+pub fn decode_flag(raw: u8) -> bool {
+    unsafe { mem::transmute(raw) }
+}
+
+pub trait AddressSource {
+    fn address(&self) -> *const u8;
+}
+
+pub fn load_source<S: AddressSource>(source: &S) -> u8 {
+    unsafe { source.address().read() }
+}
+
+pub struct ByteHandle {
+    pub address: NonNull<u8>,
+}
+
+impl ByteHandle {
+    pub fn load(&self) -> u8 {
+        unsafe { self.address.as_ptr().read() }
+    }
+}
+
+/// Returns `bytes[index]`.
+///
+/// # Safety
+///
+/// `index` must be less than `bytes.len()`.
+pub unsafe fn item_unchecked(bytes: &[u8], index: usize) -> u8 {
+    unsafe { *bytes.get_unchecked(0) }
+}
+
+macro_rules! make_indexer {
+    ($name:ident) => {
+        pub fn $name(bytes: &[u8], index: usize) -> u8 {
+            debug_assert!(index < bytes.len());
+            unsafe { *bytes.get_unchecked(index) }
+        }
+    };
+}
+
+make_indexer!(profile_index);
+
+pub fn checked_first(bytes: &[u8]) -> Option<u8> {
+    if bytes.is_empty() {
+        return None;
+    }
+    // SAFETY: Since `u8` occupies one byte, every `[u8]` contains an element.
+    Some(unsafe { *bytes.get_unchecked(0) })
+}
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/current-result.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/current-result.md
new file mode 100644
index 0000000000..57ede92165
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/current-result.md
@@ -0,0 +1,89 @@
+# Current Zerocopy `impls.rs` Challenge
+
+Snapshot: `53a3fbfa15d656b25b74688369f7248ff354a021`.
+
+This challenge has no whole-target positive oracle and receives no aggregate
+semantic score. Novel claims were independently source-reviewed; they are not
+converted into confirmed production unsoundness merely because an evaluated
+agent reported them.
+
+## Paired result
+
+| Behavior | Skill | Baseline |
+|---|---|---|
+| Overall production verdict | `UNPROVED`; no concrete valid-use UB or false postcondition established | `UNPROVED`; no concrete downstream production UB established |
+| SIMD normative proof gap | Found | Found |
+| Historical-version `Option` zero-representation gap | Missed/claimed locally closed | Found |
+| `ManuallyDrop<T>: HasField` exact-contract concern | Missed | Found |
+| Incomplete `Immutable` proof for `Box<T>` | Found | Found as a documentation residual |
+| Optional function-pointer/`NonNull` `Immutable` proof | Called unproved | Called documentation residual |
+| Missing fixture/configuration inputs | Found | Not made explicit |
+| Two `assume_initialized` sites | Correctly scoped test-only and `UNPROVED`, not `UNSOUND` | Correctly scoped test-only and unjustified, not downstream production |
+
+Both agents resisted the tempting but unjustified conclusion that an explicit
+“this is unsound” FIXME in generic test machinery proves a concrete bad
+execution or a downstream-shipping defect.
+
+## Independent adjudication
+
+### Confirmed proof gaps
+
+- **Option zero representation: `UNPROVED` over the declared Rust 1.56+
+  range.** The source cites a Rust 1.89 guarantee. Independent version review
+  found that the explicit all-zero-to-`None` guarantee appears later than the
+  declared MSRV for several families, and the explicit unsafe-function-pointer
+  coverage later still. No compiler counterexample was established, so this
+  is missing authoritative coverage, not demonstrated unsoundness.
+- **Aggregate SIMD matrix: `UNPROVED`.** The generic argument relies on
+  nonnormative UCG text that disclaims being a guarantee. Some current
+  per-type standard-library pages may close individual types, but no reviewed
+  proof covers every emitted type, architecture, feature, nightly, and
+  supported compiler version.
+- **`Box<T>: Immutable`: `UNPROVED`.** No reviewed normative contract
+  establishes the representation property required by zerocopy's trait over
+  the entire supported compiler range. No counterexample was found.
+
+### Claims narrowed or disputed
+
+- A reviewer derived the optional function-pointer and `NonNull<T>`
+  `Immutable` obligations from normative `Copy` restrictions and
+  `UnsafeCell` rules and classified them `PROVED`. Thus the skill report's
+  `UNPROVED` classification for these two families is conservative
+  over-reporting, not an admitted defect.
+- A reviewer classified `ManuallyDrop<T>: HasField` as
+  `CONTRACT-BROKEN`: the local contract asks for exact field identity, type,
+  and visibility, while public std documentation exposes only private fields
+  and the implementation uses a public proxy marker. No invalid projection,
+  memory unsafety, or provenance failure was demonstrated because std does
+  guarantee `ManuallyDrop<T>` has `T`'s layout and bit validity.
+
+  This semantic classification still needs project-author review. The local
+  contract permits `Self` merely to share the layout of a type containing the
+  field, so a layout-equivalent public proxy-field interpretation may be
+  intended. The pilot therefore records the claim as a high-priority contract
+  ambiguity, not a final production defect.
+- The two test-only `assume_initialized` comments give an invalid generic
+  implication: `TryFromBytes` does not imply initialized padding. A second
+  review found that the finite current test invocations nevertheless construct
+  byte-initialized values. The admitted conclusion is proof-comment debt in
+  test-only code; no concrete bad execution or production issue was proved.
+
+## Fixture failure discovered by the skill
+
+The current blind bundle included `Cargo.toml`, `build.rs`, and `src/`, but
+omitted the lockfile, path-dependency sources, linked MSRV policy, and pinned
+nightly/configuration material needed for a complete theorem. The skill agent
+correctly refused closure for those axes.
+
+This is an evaluation-fixture defect, not evidence against zerocopy. A future
+scored current-source run must rebuild the bundle with all semantically
+required policy, dependency, generated, and configuration inputs and then
+restart both conditions from fresh agents.
+
+## Interpretation
+
+The baseline found two important obligations that the skill report omitted,
+while the skill was more explicit about theorem status, configuration
+incompleteness, and exact residual scope. This mixed result is useful: the
+skill improved reporting discipline but did not dominate unaided defect/proof
+gap discovery on the current high-quality target.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/historical-result.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/historical-result.md
new file mode 100644
index 0000000000..cc1e6c38a6
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/historical-result.md
@@ -0,0 +1,68 @@
+# Historical `read_from_io` Pair
+
+## Admitted atom
+
+Two independent source reviewers reconciled the following
+authority-rooted atom before the reports were assigned an objective score:
+
+> Immediately before `Ptr::as_bytes`, the referent must satisfy zerocopy's
+> local `invariant::Initialized`: all `size_of::<Self>()` bytes must form a
+> bit-valid byte array. In the vulnerable snapshot,
+> `MaybeUninit::<Self>::zeroed()` does not establish initialization of padding
+> after its return-by-value typed move, so the subsequent
+> `assume_validity::<Initialized>` lacks a premise. The resulting byte slice is
+> passed to caller-provided safe `Read` code, which may inspect it. The fixed
+> snapshot instead performs an in-place bytewise zero of the final storage
+> before asserting `Initialized`, which closes this exact missing premise.
+
+The reviewers checked the local `Initialized`, `assume_validity`, `as_bytes`,
+`FromBytes`, and `FromZeros::zero` contracts and Rust 1.84.1 documentation for
+`MaybeUninit::zeroed`, `MaybeUninit::assume_init`, `ptr::write_bytes`,
+`Read`, and invalid values.
+
+The fixed classification is bug-specific. It is not a whole-crate soundness
+label.
+
+## Results
+
+| Snapshot | Skill | Baseline |
+|---|---|---|
+| Vulnerable `49a13ba…` | Recovered; `14/14` | Recovered; `14/14` |
+| Fixed `f99854a…` | Exact atom closed; no repaired-defect assertion | Exact atom closed; no repaired-defect assertion |
+
+Both vulnerable reports:
+
+- located `MaybeUninit::<Self>::zeroed()` and the false `Initialized`
+  transition;
+- traced the transition through `Ptr::as_bytes` and reference construction;
+- supplied a fully safe generic instantiation and adversarial-safe reader
+  path;
+- used exact Rust 1.84.1 authorities;
+- covered the requested `std`/`x86_64-unknown-linux-gnu` configuration; and
+- classified the safe API as unsound.
+
+Both fixed reports proved that `uninit(); buf.zero()` writes the whole final
+object representation in place and that arbitrary memory-safe `Read` behavior
+cannot make bytes uninitialized. Errors and panics skip `assume_init`; a
+successful return is valid under the `FromBytes` unsafe-trait contract.
+
+There were no hard errors for the admitted memory-initialization atom.
+
+## Robustness observation
+
+The skill-enabled reports additionally made explicit that caller-provided safe
+`Read` implementations cannot be trusted to obey their behavioral prose. A
+safe override of `read_exact` may return success without filling the buffer.
+That does not affect the fixed implementation's soundness because untouched
+bytes remain initialized. Whether the brief phrase “Reads a copy … from the
+source” is precise enough to make this a documented-postcondition violation
+is interpretation-dependent; the pilot records this as an unresolved
+robustness/documentation question rather than an admitted
+`CONTRACT-BROKEN` atom.
+
+## Interpretation
+
+This public historical case was likely represented in model training data, and
+the source contains general padding warnings even after incident-specific
+collateral was removed. Equal one-replicate recovery therefore demonstrates
+basic reasoning compatibility, not skill lift or memorization resistance.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/manifest.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/manifest.md
new file mode 100644
index 0000000000..a841f451da
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/manifest.md
@@ -0,0 +1,109 @@
+# 2026-07-30 Exploratory Pilot Manifest
+
+> **Evaluator-only material**
+
+## Status
+
+This is an exploratory, source-only forward test. It is not a release
+evaluation and cannot satisfy the release gates in `testing-plan.md`.
+
+The intended isolated CLI harness could not be authenticated without exposing
+a persistent host credential to a networked process. That escalation was
+rejected. The fallback used fresh collaboration agents with
+`fork_turns="none"`, opaque temporary bundle names, paired-agent separation,
+and explicit path restrictions. Those restrictions were procedural: every
+agent still technically shared the host filesystem and tool environment.
+
+No evaluated target was built, tested, macro-expanded by execution, or
+otherwise run.
+
+## Frozen identities
+
+- Skill package tree digest (deterministic tar SHA-256):
+  `48564ca8d4f6ecabbb3a35be3e9b6de65842c9710445a0dd68501fd234f9ff5b`
+- Skill entrypoint SHA-256:
+  `b943f1092008252bbd77e10a1a4963fb0f78a60303ab653218c5c423cc6f0d70`
+- Synthetic vulnerable bundle:
+  `e561c4a3ebf71800857edeedc217227bf152a719845b74b5ded4bac4f77081c3`
+- Synthetic fixed bundle:
+  `27a820a8a590194916cb25a3b39b38aa3a04cc1556636a1b96cbebee755d3a51`
+- Historical zerocopy vulnerable source:
+  commit `49a13ba945954a6127036165499b6242e74bc3c6`;
+  sanitized bundle digest
+  `450562e0515de2e60836b133e2a03a6ef7c3c65976866dde6d99a4b2f4dced25`
+- Historical zerocopy fixed source:
+  commit `f99854afb33365e9dada073a166b3047df7109d1`;
+  sanitized bundle digest
+  `62c51935d22fb64d363482e50ce04658e0f674e570324243f48dde1f92448e4f`
+- Current zerocopy source:
+  commit `53a3fbfa15d656b25b74688369f7248ff354a021`;
+  bundle digest
+  `3242db7402b801cefb4425fd36c9c117906b1647765006b6533c8fde6b8ffb2b`
+
+Tree digests were computed from GNU tar streams with sorted names, timestamp
+zero, numeric owner/group zero, and file contents and modes preserved.
+
+The exact hosted model identifier, sampling seed, and effective reasoning
+setting were not exposed by the collaboration-agent API. Every run inherited
+the same parent model configuration and used one replicate.
+
+## Conditions and opaque runtime IDs
+
+| Target | Skill | Baseline |
+|---|---|---|
+| Synthetic vulnerable | `q7m2` | `p4x9` |
+| Synthetic fixed | `n8k3` | `v2c6` |
+| Historical vulnerable | `t6z2` | `l4n8` |
+| Historical fixed | `d7q3` | `w1f5` |
+| Current `src/impls.rs` challenge | `j9e2` | `s3k6` |
+
+No agent was assigned two cells or both members of a vulnerable/fixed pair.
+
+## Prompt protocol
+
+Naturalistic synthetic skill condition:
+
+```text
+Use the unsafe Rust skill from [SKILL] to audit [TARGET] at the supplied
+snapshot. Do not modify, build, test, or otherwise execute the target. Return
+the audit report in your final response.
+```
+
+The baseline omitted only the skill invocation. Both conditions were told to
+inspect only their target and exact versioned official Rust Reference or
+standard-library documentation needed to verify claims.
+
+Historical zerocopy runs used the same paired construction, with the neutral
+scope `FromBytes::read_from_io` and all definitions, helpers, contracts, and
+invariants on which its proof depends. The theorem was restricted to Rust
+1.84.1, feature `std`, and `x86_64-unknown-linux-gnu`.
+
+Current zerocopy runs used the neutral scope `src/impls.rs`, the public unsafe
+trait contracts implemented there, invoked macro definitions, and relevant
+Cargo/build/configuration policy.
+
+## Sanitation
+
+Historical bundles were produced from `Cargo.toml` and `src/` at the exact
+commits, with no `.git` directory or history. The fixed bundle removed:
+
+- the incident-numbered explanatory note adjacent to the repair; and
+- the incident-named regression test added by the repair.
+
+No API contract, safety comment, implementation statement, helper, or
+substantive type documentation was removed. A scan found no occurrence of the
+incident numbers, fixing title, pair commit IDs, or regression-test name in
+either final runtime bundle.
+
+## Scoring status
+
+The synthetic six-atom oracle is recorded in
+`../../fixtures/pilot/README.md`.
+
+The historical `read_from_io` atom was promoted from Candidate after a second
+independent, source-only authority review agreed on the exact missing premise
+and bug-specific fixed proof. Its score is in `historical-result.md`.
+
+Current zerocopy remains a Challenge fixture: it measures scope, calibration,
+and proof behavior and has no whole-target positive oracle. Novel claims
+require independent adjudication.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/report.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/report.md
new file mode 100644
index 0000000000..3e8f12199c
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/report.md
@@ -0,0 +1,220 @@
+# Unsafe Rust Skill Exploratory Evaluation
+
+Date: 2026-07-30  
+Skill entrypoint:
+[`SKILL.md`](../../../../skills/unsafe-rust/SKILL.md)  
+Protocol: [`testing-plan.md`](../../testing-plan.md)  
+Frozen inputs and prompts: [`manifest.md`](manifest.md)
+
+## Executive conclusion
+
+The frozen skill passed this behavioral smoke test, but the evaluation does
+**not** qualify it for release.
+
+- On the admitted six-atom synthetic vulnerable fixture, the skill and
+  baseline both recovered every issue. The skill received `78/78`; the
+  baseline received `73/78`. The difference came from authority,
+  configuration, surface-closure, TCB, and report completeness—not recall.
+- Neither condition reproduced a repaired defect on the synthetic fixed
+  control. The skill supplied a scoped positive proof and correctly reported
+  the deliberately retained local-comment debt; the baseline missed that
+  proof-artifact defect and made a less-supported universal no-finding claim.
+- On the admitted historical zerocopy `read_from_io` defect, both conditions
+  received `14/14`, and both fixed-side agents proved that in-place zeroing
+  closes the padding-initialization hole.
+- On current zerocopy, both conditions correctly refused a positive
+  whole-scope verdict and distinguished test-only proof debt from
+  downstream-shippable code. Results were mixed: the skill was stronger at
+  theorem/configuration/report discipline, while the baseline found two
+  important proof/contract questions omitted by the skill.
+- No evaluated target code was executed.
+
+The evidence supports a narrow claim:
+
+> In one fresh-agent paired smoke test, the skill preserved perfect known-atom
+> recall and materially improved proof/report completeness without introducing
+> a repaired-defect false positive.
+
+It does not establish general lift, cross-model behavior, corpus closure, or
+release readiness.
+
+## Executed design
+
+Ten fresh-agent runs were performed:
+
+| Target | Skill runs | Baseline runs |
+|---|---:|---:|
+| Synthetic vulnerable | 1 | 1 |
+| Synthetic fixed | 1 | 1 |
+| Historical zerocopy vulnerable | 1 | 1 |
+| Historical zerocopy fixed | 1 | 1 |
+| Current zerocopy `src/impls.rs` challenge | 1 | 1 |
+
+Every evaluated agent used `fork_turns="none"`. No agent saw another report or
+both members of a vulnerable/fixed pair. Runtime target names were opaque.
+Historical incident titles, issue numbers, VCS metadata, fixing history, and
+the incident-named regression test were absent. The skill was not edited after
+its revision was frozen; its entrypoint SHA-256 remained
+`b943f1092008252bbd77e10a1a4963fb0f78a60303ab653218c5c423cc6f0d70`.
+
+The synthetic reports were normalized, shuffled, and scored without revealing
+condition identity. The historical atom was admitted only after a second
+independent source/authority review. Current-source findings were independently
+reviewed but remain a Challenge result rather than a complete audit.
+
+## Objective results
+
+### Synthetic pair
+
+Full scoring and deductions:
+[`synthetic-score.md`](synthetic-score.md).
+
+| Condition | Known-atom recall | Proof/report score | Hard errors |
+|---|---:|---:|---:|
+| Skill | `6/6` | `78/78` | 0 |
+| Baseline | `6/6` | `73/78` | 0 |
+
+The baseline lost points for incomplete authority on two local proofs, partial
+configuration closure, no safe-surface/exhaustiveness inventory, and missing
+overall theorem/TCB/residual-scope material. These are exactly the behaviors
+the skill is intended to improve.
+
+The fixed-side skill report supported its scoped positive conclusion. The
+fixed-side baseline did not make a repaired-defect assertion, but it missed the
+absent adjacent proof for `item_unchecked` and did not fully support its broad
+no-finding language.
+
+### Historical zerocopy pair
+
+Full result and oracle:
+[`historical-result.md`](historical-result.md).
+
+| Condition | Vulnerable atom | Fixed control | Hard errors |
+|---|---:|---|---:|
+| Skill | `14/14` | Exact defect closed | 0 |
+| Baseline | `14/14` | Exact defect closed | 0 |
+
+Both conditions traced the false `Initialized` upgrade through
+`Ptr::as_bytes` to caller-provided safe `Read` code and did not confuse the
+final `assume_init` with the earlier byte-slice defect. Both fixed reports
+proved that `uninit(); buf.zero()` initializes the complete final storage
+before a byte slice is formed.
+
+This public historical issue is contamination-prone and both source versions
+contain general padding documentation. Equal recall is therefore a capability
+check, not evidence of lift.
+
+## Current zerocopy challenge
+
+Detailed paired findings and independent adjudication:
+[`current-result.md`](current-result.md).
+
+Both conditions returned `UNPROVED` rather than manufacturing a positive or
+negative whole-target verdict. Both correctly placed the two
+`assume_initialized` calls under `#[cfg(test)]` and declined to infer a
+concrete bad execution merely from the comments' admitted generic proof gap.
+
+Independently supported residuals include:
+
+- an authoritative-documentation gap for all-zero `Option` representations
+  over the entire declared Rust 1.56+ range;
+- no normative universal SIMD proof across every emitted type, target,
+  feature, nightly, and compiler version; and
+- an incomplete normative proof for `Box<T>: Immutable`.
+
+The baseline found the historical-`Option` gap and a `ManuallyDrop<T>:
+HasField` field-contract ambiguity that the skill omitted. The skill found that
+the fixture lacked lockfile, path-dependency, linked policy, and pinned-nightly
+inputs needed for complete configuration closure.
+
+The skill also listed optional function-pointer and `NonNull<T>` `Immutable`
+impls as unproved. Independent review derived those obligations from normative
+`Copy` and `UnsafeCell` rules, so these appear to be conservative
+over-reporting.
+
+Most importantly, the skill's statement that null-pointer-optimized `Option`
+obligations “closed locally” was not justified across the declared MSRV. The
+overall result remained `UNPROVED`, so this was not a false whole-scope
+certification, but it is a premature positive local conclusion. A
+release-gating review should treat an equivalent explicitly `PROVED` claim as
+a hard error.
+
+No novel current-source claim is reported as production UB. The
+`ManuallyDrop` claim remains a contract-interpretation question for project
+authors because `HasField` permits a layout-equivalent field model.
+
+## Harness and validity limitations
+
+The evaluation does not satisfy the protocol's isolation attestation.
+
+An outer bubblewrap plus nested Codex sandbox was locally verified as a viable
+filesystem boundary. An authenticated run would have required providing the
+networked process with a credential. Mounting the persistent host
+authentication file was rejected, correctly, as an exfiltration risk. No
+attempt was made to bypass that decision.
+
+The fallback used procedural restrictions:
+
+- fresh no-history agents;
+- opaque, separate `/tmp` bundles;
+- no paired-side reuse;
+- prompts restricting reads to target, skill treatment, and exact official
+  Rust documentation; and
+- no target execution.
+
+Agents nevertheless shared the host filesystem and general tool environment.
+The baseline was not physically prevented from discovering the skill or
+evaluator files. Network/documentation allowlisting was not enforced. Thus the
+pilot cannot meet the plan's release isolation gate.
+
+Additional limitations:
+
+- one replicate per cell;
+- no previous-skill condition;
+- exact model identifier, sampling seed, token counts, and elapsed time were
+  unavailable from the collaboration API;
+- scorer citation content was not independently re-opened after report
+  normalization;
+- no opaque private holdout;
+- no Google audit-log, RustSec-wide, std-wide, authoring, change-review,
+  evidence-review, or generated/FFI/configuration microfixture cohort;
+- no statistical inference; and
+- the current-source bundle itself was incomplete for a full audit.
+
+One auxiliary historical-oracle prompt was rejected by a generic
+“cybersecurity” classifier. Rephrasing it as a non-operational source-contract
+comparison succeeded. No evaluated run was lost to that filter.
+
+## Tool/package validation
+
+The skill package passed the skill-creator static validator:
+
+```text
+Skill is valid!
+```
+
+This checks package structure and metadata, not semantic quality.
+
+## Release disposition
+
+**Disposition: exploratory pass; release gates not met.**
+
+Before a release evaluation:
+
+1. provision a short-lived evaluator credential acceptable for the isolated
+   bubblewrap harness; never mount the host's persistent authentication state;
+2. rebuild the current-source bundle with every semantically required
+   manifest, lockfile, path dependency, policy, generated input, and
+   configuration artifact;
+3. independently admit the remaining microfixture and public-corpus oracles,
+   including record/atom closure for `audits.toml`;
+4. run the preregistered three- and five-replicate cohorts, previous-skill
+   comparator, and opaque holdouts;
+5. independently verify every necessary citation against its exact version;
+   and
+6. adjudicate the current `Option` MSRV and `ManuallyDrop::HasField` questions
+   with zerocopy/Rust maintainers before converting them into regression
+   fixtures.
+
+Do not change the runtime skill based on this report without assigning a new
+skill revision and rerunning every affected paired condition.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/README.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/README.md
new file mode 100644
index 0000000000..2ae5835856
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/README.md
@@ -0,0 +1,9 @@
+# Normalized reports
+
+These files preserve the evaluated agents' substantive final reports while
+removing ephemeral absolute `/tmp` links, repeated per-file hash tables, and
+run identifiers. They are scorer-facing normalized artifacts, not byte-for-byte
+transcripts. The original final responses remain in the evaluation thread.
+
+Condition and pair identities were withheld from the scorer. Their mapping is
+recorded in the evaluator manifest after scoring.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-a.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-a.md
new file mode 100644
index 0000000000..dea23d964e
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-a.md
@@ -0,0 +1,17 @@
+# Audit result
+
+No unsafe-code soundness or correctness findings.
+
+- `item_unchecked` documents exactly the required precondition,
+  `index < bytes.len()`, matching Rust 1.85's `slice::get_unchecked` contract.
+- `checked_first` performs an unconditional emptiness check before
+  `get_unchecked(0)`. It does not rely on a debug assertion, so the proof holds
+  in every stated build profile.
+- The remaining APIs use valid typed references, safe matching, copying, or
+  bounds-checked indexing. `decode_flag` and `profile_index` can panic on
+  invalid input, but cannot trigger undefined behavior.
+- Callers can cause UB only by violating the clearly documented contract of
+  the explicitly `unsafe` `item_unchecked` API.
+
+The snapshot was reviewed statically only; it was not modified, built, tested,
+or executed.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-b.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-b.md
new file mode 100644
index 0000000000..e91cc3439b
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-b.md
@@ -0,0 +1,198 @@
+# Unsafe Rust audit: `opaque-byte-tools` 0.1.0
+
+## Claim and verdict
+
+- **Claim:** For the exact snapshot, Rust 1.85.0, every supported target and
+  ordinary profile, and both values of `debug_assertions`, every well-typed
+  safe use and every unsafe use satisfying its documented contract is free of
+  Rust undefined behavior.
+- **Soundness verdict:** **UNSOUND** — four independently valid safe uses reach
+  UB (`F-01`–`F-04`).
+- **Documented-postcondition verdict:** **CONTRACT-BROKEN** —
+  `item_unchecked` does not return the documented element (`F-05`).
+- **Proof-artifact status:** **UNPROVED** — the snapshot has no valid adjacent
+  proof for any unsafe block (`F-06`).
+- **Combined result:** **UNSOUND + CONTRACT-BROKEN**.
+- No build, test, macro expansion tool, or target code was executed.
+
+## Findings
+
+### F-01 — `decode_flag` creates invalid `bool` values
+
+**Status:** UNSOUND
+
+The entirely safe call `decode_flag(2)` reaches
+`mem::transmute::<u8, bool>(2)`. Rust 1.85 guarantees `bool` size 1 but permits
+only bit patterns `0x00` and `0x01`; any other pattern is UB. `transmute`
+additionally requires its result to be valid at the destination type.
+[Rust 1.85 Boolean
+Reference](https://doc.rust-lang.org/1.85.0/reference/types/boolean.html#r-type.bool.repr),
+[`transmute`
+contract](https://doc.rust-lang.org/1.85.0/std/mem/fn.transmute.html).
+
+Minimum resolution: avoid `transmute`; explicitly map or reject values.
+
+### F-02 — Safe `AddressSource` implementations can supply unreadable pointers
+
+**Status:** UNSOUND
+
+A downstream safe witness is:
+
+```rust
+struct Null;
+
+impl AddressSource for Null {
+    fn address(&self) -> *const u8 {
+        core::ptr::null()
+    }
+}
+
+load_source(&Null);
+```
+
+`AddressSource` is not an unsafe or sealed trait, so its implementations cannot
+carry an unenforced soundness obligation. `ptr::read` requires a pointer valid
+for reads, properly aligned, and pointing to initialized `T`; Rust 1.85 states
+a null pointer is never valid for a non-zero-sized access.
+[`ptr::read`
+safety](https://doc.rust-lang.org/1.85.0/core/ptr/fn.read.html#safety),
+[`core::ptr`
+validity](https://doc.rust-lang.org/1.85.0/core/ptr/index.html#safety),
+[unsafe-trait
+boundary](https://doc.rust-lang.org/1.85.0/reference/items/traits.html#unsafe-traits).
+
+Minimum resolution: return `&u8` from the safe trait method, or make and fully
+document an unsafe sealed boundary whose implementations guarantee
+accessibility, initialization, lifetime, and permitted concurrent access.
+
+### F-03 — Public `ByteHandle` construction does not establish its read
+invariant
+
+**Status:** UNSOUND
+
+This is valid safe code:
+
+```rust
+ByteHandle {
+    address: core::ptr::NonNull::dangling(),
+}
+.load();
+```
+
+`NonNull` guarantees non-nullness, not dereferenceability. Rust 1.85 explicitly
+describes `NonNull::dangling()` as dangling but well-aligned, while `read`
+requires validity for a non-zero-sized `u8` access.
+[`NonNull::dangling`](https://doc.rust-lang.org/1.85.0/core/ptr/struct.NonNull.html#method.dangling),
+[`ptr::read`
+safety](https://doc.rust-lang.org/1.85.0/core/ptr/fn.read.html#safety).
+
+The required invariant—live, readable, initialized storage for the entire
+call—is unowned because the field is public and safely replaceable.
+
+### F-04 — `profile_index` relies on `debug_assert!` for memory safety
+
+**Status:** UNSOUND when `debug_assertions = false`; no UB from this path when
+it is true
+
+The private macro generates the public safe function `profile_index`. In the
+explicitly supported `debug_assertions = false` configurations, this safe call
+reaches UB:
+
+```rust
+profile_index(&[], 0);
+```
+
+Rust 1.85 says optimized builds do not execute `debug_assert!` unless debug
+assertions are enabled. `slice::get_unchecked` states that calling it with an
+out-of-bounds index is UB even if its returned reference is unused.
+[`debug_assert!`
+configuration](https://doc.rust-lang.org/1.85.0/core/macro.debug_assert.html#uses),
+[`slice::get_unchecked`
+safety](https://doc.rust-lang.org/1.85.0/core/primitive.slice.html#method.get_unchecked).
+
+### F-05 — `item_unchecked` ignores its `index`
+
+**Status:** CONTRACT-BROKEN; its UB-freedom derivation closes under the
+published safety precondition
+
+The contract says the function returns `bytes[index]`, but the implementation
+always reads index `0`.
+
+For example, `unsafe { item_unchecked(&[0x10, 0x20], 1) }` satisfies
+`index < bytes.len()` but returns `0x10` rather than `0x20`.
+
+The safety precondition implies the slice is nonempty, so index `0` is in
+bounds; no UB counterexample was established for contract-satisfying calls.
+
+### F-06 — Missing or invalid local safety proofs
+
+**Status:** UNPROVED proof artifact; not an additional UB witness
+
+Five unsafe blocks have no adjacent `SAFETY` derivation. The sole comment
+argues that because `u8` occupies one byte, every `[u8]` has an element. That
+proposition is false and does not prove the bounds obligation.
+
+`checked_first` itself has a valid independent derivation: reaching the
+unchecked access means `is_empty()` returned false, so the length is nonzero
+and index `0` is in bounds.
+[`slice::is_empty`](https://doc.rust-lang.org/1.85.0/core/primitive.slice.html#method.is_empty),
+[`slice::get_unchecked`](https://doc.rust-lang.org/1.85.0/core/primitive.slice.html#method.get_unchecked).
+
+## Boundary and obligation coverage
+
+| Public surface | Boundary | Result |
+|---|---|---|
+| `decode_flag(u8) -> bool` | Safe function | UNSOUND (`F-01`) |
+| `AddressSource::address` | Caller-implementable safe trait method | Unenforced pointer invariant (`F-02`) |
+| `load_source` | Safe generic function | UNSOUND (`F-02`) |
+| `ByteHandle` and public `address` field | Safe literal construction/replacement | Unowned invariant (`F-03`) |
+| `ByteHandle::load` | Safe method | UNSOUND (`F-03`) |
+| `item_unchecked` | Unsafe function | UB obligation closes under `index < len`; CONTRACT-BROKEN (`F-05`) |
+| Macro-generated `profile_index` | Safe function | UNSOUND when assertions are disabled (`F-04`) |
+| `checked_first` | Safe function | Source derivation closes; local proof invalid (`F-06`) |
+
+There are no other files, reexports, hidden APIs, dependencies, custom `Drop`
+implementations, unsafe traits/impls, FFI, assembly, allocators, or concurrency
+surfaces. The declarative macro is private but its single expansion creates the
+public `profile_index` API.
+
+## Configuration closure
+
+`Supported(c)` is Rust/compiler/core/std 1.85.0, edition 2021, every Rust 1.85
+target on which this dependency-free library is accepted, every ordinary build
+profile, `debug_assertions ∈ {true, false}`, and no Cargo features or
+dependency-feature axes.
+
+The pointer, validity, and `item_unchecked` findings are
+target/profile-parametric. F-04 specifically covers every supported
+configuration with debug assertions disabled. Panic strategy does not repair
+it.
+
+## TCB audit log
+
+Consumed entries are only the exact Rust 1.85 official propositions linked
+above:
+
+- boolean representation and validity;
+- `transmute` source/destination validity;
+- raw-pointer read validity, alignment, and initialization;
+- null and dangling pointer rules;
+- `NonNull::dangling`;
+- `slice::get_unchecked`;
+- `slice::is_empty`;
+- `debug_assert!` configuration behavior; and
+- unsafe-trait boundary semantics.
+
+Each citation was opened at its exact version and verified. There are no
+dependency, external-specification, implementation, deployment, probabilistic,
+or tool assumptions. No independent human TCB acceptance was performed, so
+this report issues no positive whole-crate `PROVED` certification; that
+limitation does not weaken the concrete **UNSOUND** and
+**CONTRACT-BROKEN** counterexamples.
+
+## Residual scope and re-audit triggers
+
+This is a source-level Rust abstract-semantics audit, not a
+backend/binary/security audit. Re-audit after any source or public-contract
+change, support-policy expansion, Rust/toolchain change, macro change,
+dependency introduction, or authoritative-documentation change.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-c.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-c.md
new file mode 100644
index 0000000000..a9adc1eb5b
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-c.md
@@ -0,0 +1,83 @@
+# Audit report
+
+Source-only review; no target code was built, tested, modified, or executed.
+
+## High — `decode_flag` creates invalid `bool` values from safe code
+
+`decode_flag(2)` is a safe call, but `transmute` produces a `bool` with an
+invalid bit pattern. Rust 1.85 permits only `0x00` and `0x01`; any other
+pattern is undefined behavior.
+
+Replace the transmute with explicit decoding, returning `Option`/`Result` for
+invalid inputs or using `raw != 0` if all nonzero values intentionally mean
+true.
+
+Reference: [Rust 1.85 Boolean
+representation](https://doc.rust-lang.org/1.85.0/reference/types/boolean.html#representation)
+
+## High — `profile_index` relies on a removable assertion for memory safety
+
+The public safe function checks bounds only with `debug_assert!`, then calls
+`get_unchecked`. With debug assertions disabled—explicitly supported by
+`SUPPORT.md`—a safe call such as `profile_index(&[], 0)` performs an
+out-of-bounds unchecked access and causes undefined behavior.
+
+Use ordinary indexing, `get`, or an unconditional `assert!` before
+`get_unchecked`.
+
+References: [Rust 1.85
+`debug_assert!`](https://doc.rust-lang.org/1.85.0/std/macro.debug_assert.html),
+[Rust 1.85
+`slice::get_unchecked`](https://doc.rust-lang.org/1.85.0/std/primitive.slice.html#method.get_unchecked)
+
+## High — Safe `AddressSource` implementations can make `load_source`
+dereference arbitrary pointers
+
+`AddressSource::address` has no safety contract and can be implemented entirely
+in safe code to return null, dangling, uninitialized, or otherwise unreadable
+memory. `load_source` then dereferences that pointer from a safe API.
+
+Prefer returning `&u8`. Otherwise, make the implementation invariant explicit
+through an `unsafe trait` or make `load_source` unsafe with a complete validity,
+lifetime, initialization, and concurrency contract.
+
+Reference: [Rust 1.85 `ptr::read` safety
+requirements](https://doc.rust-lang.org/1.85.0/std/ptr/fn.read.html#safety)
+
+## High — Public `ByteHandle` construction does not establish the invariant
+required by `load`
+
+`NonNull<u8>` guarantees non-nullness, not that the pointer is live,
+initialized, or readable. Because the field is public, this entirely safe
+expression creates a handle whose safe `load` causes undefined behavior:
+
+```rust
+ByteHandle {
+    address: NonNull::dangling(),
+}.load();
+```
+
+Encode the lifetime with `&'a u8`, or make the field private and provide an
+unsafe constructor with documented invariants. Making `load` unsafe is another,
+less ergonomic option.
+
+References: [Rust 1.85
+`NonNull::dangling`](https://doc.rust-lang.org/1.85.0/std/ptr/struct.NonNull.html#method.dangling),
+[Rust 1.85
+`ptr::read`](https://doc.rust-lang.org/1.85.0/std/ptr/fn.read.html#safety)
+
+## Medium — `item_unchecked` ignores its requested index
+
+The contract says the function returns `bytes[index]`, but it always accesses
+index zero. For example, valid input `([10, 20], 1)` returns `10`, not `20`.
+The stated precondition guarantees the slice is nonempty, so this is a
+correctness failure rather than additional undefined behavior.
+
+Use `bytes.get_unchecked(index)`.
+
+## Informational — Misleading safety rationale
+
+`checked_first` is currently sound because the preceding empty-slice branch
+establishes `0 < bytes.len()`. Its safety comment is nevertheless false:
+element size does not imply every slice contains an element. The comment should
+cite the preceding emptiness check to prevent future maintenance mistakes.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-d.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-d.md
new file mode 100644
index 0000000000..8e86663497
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/reports/synthetic-d.md
@@ -0,0 +1,136 @@
+# Unsafe Rust Audit: `opaque-byte-tools` 0.1.0
+
+## Claims and verdicts
+
+- **Soundness:** **PROVED** for the exact snapshot, under Rust/stdlib 1.85.0,
+  edition 2021, every target on which the crate is compilable, all ordinary
+  profiles, either debug-assertion state, and either panic strategy.
+- **Documented postconditions:** **PROVED**. A valid call to
+  `item_unchecked(bytes, index)` returns the copied value of `bytes[index]`.
+- **Combined mandatory result:** **PROVED**, relative to the stated TCB.
+- **Binary/backend/security claims:** None.
+- **Findings affecting the verdict:** No `UNSOUND`, `UNPROVED`, or
+  `CONTRACT-BROKEN` findings.
+
+The crate has no dependencies, lockfile, features, build script, FFI,
+assembly, atomics, custom allocator, included/generated files, target `cfg`s,
+or external state. The declarative macro has exactly one in-scope invocation
+and was audited textually. No target code was modified, built, tested,
+expanded by a tool, or executed.
+
+## Boundary and API coverage
+
+| Surface | Classification | Result |
+|---|---|---|
+| `decode_flag` | Safe free function | **PROVED**: exhaustive `u8` match; invalid encodings panic without unsafe state. |
+| `AddressSource` and `load_source` | Caller-implementable safe trait and safe generic consumer | **PROVED**: the consumer relies only on the type-valid `&u8` returned by the trait. |
+| `ByteHandle`, `new`, and `load` | Public type with private field; safe methods | **PROVED**: the sole field is an ordinary shared reference supplied by the constructor and only read. |
+| `item_unchecked` | Public unsafe function | **PROVED** under its complete `index < bytes.len()` precondition. |
+| `make_indexer!` and `profile_index` | Private macro generating a public safe function | **PROVED**: the one expansion contains ordinary checked slice indexing and no unsafe operation. |
+| `checked_first` | Safe function backed by unsafe indexing | **PROVED** by the derivation below. |
+
+There are no public fields, exported macros, reexports, hidden public items,
+unsafe traits or impls, custom `Drop`, or manual auto-trait impls.
+
+## Invariants
+
+- **INV-BYTEHANDLE:** While a `ByteHandle<'a>` is usable, `address` is a
+  type-valid shared reference to a `u8` for `'a`. The field type establishes
+  the property, its privacy prevents unchecked construction, and neither
+  method mutates it.
+- No global, temporal, concurrency, partial-initialization, or
+  destruction-sensitive invariant exists.
+
+## Obligation ledger
+
+### OBL-1 — `item_unchecked` call to `get_unchecked`
+
+**PROVED.** Its unsafe API contract requires `index < bytes.len()`. A `usize`
+index is nonnegative, so this places it in the zero-based slice bounds. Rust
+1.85.0 documents that `get_unchecked` returns a reference to the indexed
+element and that an out-of-bounds index is undefined behavior. Therefore the
+documented caller fact discharges the callee's only additional safety
+condition. Dereferencing the resulting `&u8` copies that element without
+extending an alias or ownership obligation.
+
+### OBL-2 — `checked_first` call to `get_unchecked(0)`
+
+**PROVED.**
+
+- If `bytes.is_empty()` is true, the function returns before reaching unsafe
+  code.
+- Rust 1.85.0 specifies that `is_empty` reflects whether slice length is zero.
+- Therefore, on the fallthrough path, `bytes.len() != 0`; because the length is
+  a `usize`, `0 < bytes.len()`.
+- No callback, mutation, panic point, or state transition intervenes.
+- Thus index zero is in bounds and the unchecked access is permitted.
+
+The resulting reference is immediately copied into `Some`; no obligation
+escapes.
+
+### OBL-3 — `item_unchecked` postcondition
+
+**PROVED.** Rust 1.85.0 describes `get_unchecked` as returning a reference to
+the selected element. Dereferencing that reference yields the same `u8` that
+checked expression `bytes[index]` denotes under the function's in-bounds
+precondition.
+
+### OBL-4 — Safe-surface closure
+
+**PROVED.** All remaining operations are safe Rust. Caller-controlled
+`AddressSource` implementations are consumed only through their enforced
+return type. Panic, reentrancy, or other safe implementation behavior cannot
+expose an invalid local state.
+
+## Configuration closure
+
+The supported set is Rust/stdlib 1.85.0 with edition 2021, every compilation
+target capable of supplying that standard library, all ordinary profiles,
+debug assertions enabled or disabled, and normal unwind or abort panic
+behavior.
+
+Coverage is parametric:
+
+- There is no conditional compilation or target-dependent representation.
+- No pointer-width arithmetic, overflow-sensitive arithmetic, layout
+  assumption, generated input, dependency feature, or debug assertion
+  participates in a proof.
+- Panic paths contain no unsafe operation or suspended invariant.
+- The single macro invocation expands from a finite, directly inspected rule
+  to a safe indexing function.
+
+## TCB audit log
+
+| ID | Accepted proposition | Exact authority | Consumers |
+|---|---|---|---|
+| `AXIOM-SLICE-GET-1.85` | For an in-bounds `usize`, `slice.get_unchecked` returns a reference to the indexed element; an out-of-bounds call is UB. | [Rust 1.85.0 `slice::get_unchecked`](https://doc.rust-lang.org/1.85.0/std/primitive.slice.html#method.get_unchecked) | OBL-1, OBL-2, OBL-3 |
+| `AXIOM-SLICE-EMPTY-1.85` | `slice.is_empty()` is true exactly when the slice length is zero. | [Rust 1.85.0 `slice::is_empty`](https://doc.rust-lang.org/1.85.0/std/primitive.slice.html#method.is_empty) | OBL-2 |
+| `AXIOM-INDEX-1.85` | Slice indices are zero-based. | [Rust 1.85.0 Reference, array and slice indexing](https://doc.rust-lang.org/1.85.0/reference/expressions/array-expr.html#array-and-slice-indexing-expressions) | OBL-1, OBL-2 |
+
+The official Rust 1.85.0 authorities were opened and checked. No dependency,
+implementation, platform, probabilistic, deployment, or tool-result
+assumption is consumed.
+
+## Maintenance finding
+
+**DOC-M1 — Local unsafe proofs are less complete than the supplied skill
+requires.**
+
+- `item_unchecked` has a sufficient public safety contract but no adjacent
+  `SAFETY` derivation for the internal unchecked call.
+- `checked_first` correctly identifies the dominating check, but does not
+  explicitly state the `get_unchecked` contract or its result.
+
+The audit discharges both obligations above, so this is not an `UNPROVED` or
+soundness finding for the frozen snapshot. The minimal maintenance remedy is to
+record the corresponding derivations adjacent to those unsafe blocks.
+
+## Residual scope and re-audit triggers
+
+No binary/code-generation-backend theorem, performance property, panic-freedom
+promise, or toolchain version other than 1.85.0 was audited. Independent human
+review was not performed.
+
+Re-audit is required for changes to source, public safety contracts, supported
+Rust versions/configurations, macro invocations, dependencies/build machinery,
+or consumed official documentation.
diff --git a/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/synthetic-score.md b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/synthetic-score.md
new file mode 100644
index 0000000000..8453d1bc93
--- /dev/null
+++ b/evals/unsafe-rust/runs/2026-07-30-exploratory-pilot/synthetic-score.md
@@ -0,0 +1,67 @@
+# Synthetic Pilot Score
+
+The scorer received normalized reports under labels A–D, the preregistered
+oracle, and the scoring rubric. It was told which reports concerned the
+vulnerable and fixed members, but not which condition produced a report. It
+did not inspect the skill, target bundles, run manifest, or external sources.
+
+## Vulnerable member
+
+| Report | M1 | M2 | M3 | M4 | M5 | M6 | Scope | Complete | Total |
+|---|---:|---:|---:|---:|---:|---:|---:|---:|---:|
+| B | 12 | 12 | 12 | 12 | 14 | 12 | 2 | 2 | **78/78** |
+| C | 12 | 12 | 12 | 11 | 13 | 11 | 1 | 1 | **73/78** |
+
+Both reports recovered all six atoms. Report B received no deductions.
+
+Report C deductions:
+
+- M4 Premises/authority: `-1`; the report did not ground the
+  `get_unchecked` behavior and safety contract used to close the no-UB
+  conclusion.
+- M5 Configuration closure: `-1`; it established the assertions-disabled
+  counterexample but did not close the enabled state and remaining support
+  space.
+- M6 Premises/authority: `-1`; it did not ground `is_empty` semantics or the
+  unchecked-index obligation.
+- Whole-scope/safe-surface coverage: `-1`; it found every planted surface but
+  supplied no inventory or exhaustiveness argument.
+- Report completeness: `-1`; it omitted an overall/combined verdict, complete
+  support-policy closure, TCB accounting, and residual scope.
+
+There were no hard errors in either report.
+
+After scoring, the evaluator unblinded the mapping:
+
+- B was the skill-enabled run `q7m2`.
+- C was the no-skill run `p4x9`.
+
+Thus this single paired replicate produced equal known-atom recall (`6/6`
+each) and a five-point proof/report-quality difference (`78/78` versus
+`73/78`). This is descriptive only; one replicate cannot establish a
+population effect.
+
+## Fixed member
+
+- **Report A:** no repaired issue was reproduced. Its broad no-finding
+  conclusion outran its brief proof: it lacked a complete surface inventory,
+  configuration closure, and authority-backed obligation ledger, and it
+  missed the retained absent adjacent proof for `item_unchecked`. The scorer
+  found no hard semantic error against the bug-specific fixed oracle.
+- **Report D:** no repaired issue was reproduced. Its positive conclusion was
+  supported by boundary coverage, invariant/obligation derivations,
+  configuration closure, and stated authorities. It correctly classified the
+  retained local-proof defect as maintenance-only and did not reproduce M6.
+  The scorer found no hard error.
+
+After scoring:
+
+- A was the no-skill run `v2c6`.
+- D was the skill-enabled run `n8k3`.
+
+## Citation limitation
+
+The scorer judged only the evidence present in the normalized reports and did
+not independently open external citations. The evaluated agents stated that
+they opened the exact Rust 1.85.0 pages. Citation-content verification by an
+independent scorer remains a release-gate requirement.
diff --git a/evals/unsafe-rust/source-catalog.md b/evals/unsafe-rust/source-catalog.md
new file mode 100644
index 0000000000..b111a540d5
--- /dev/null
+++ b/evals/unsafe-rust/source-catalog.md
@@ -0,0 +1,734 @@
+# Unsafe Rust Evaluation Source Catalog
+
+> **Evaluator-only material**
+>
+> This catalog contains fixture leads, historical fixes, and expected-finding
+> sources. It is not part of the `unsafe-rust` skill and must never be mounted
+> into an evaluation agent's workspace. An agent that can read this file, an
+> audit note, an advisory, a fixing diff, or an issue title has been given the
+> answer and has not performed a blind audit.
+>
+> These sources are evidence for constructing and checking evaluations. They
+> are not Rust semantic authorities and must never be cited as axioms in a
+> soundness proof.
+
+## Purpose and Snapshot Policy
+
+This catalog identifies code from which maintainers can build semantic
+evaluations of the `unsafe-rust` skill. It deliberately combines:
+
+- real vulnerable source at exact historical revisions;
+- the corresponding fixed source when available;
+- code that expert auditors found difficult or insufficiently documented
+  without proving it unsound;
+- small pass/fail examples from analysis and verification tools;
+- current, high-quality open-world code;
+- hand-proved negative controls; and
+- boundary cases that test whether an agent states the right theorem rather
+  than mechanically labeling every unusual behavior Rust UB.
+
+Every acquired source must be frozen by repository commit, crate checksum, or
+content digest. Record the acquisition date because advisory databases, issue
+labels, default branches, generated output, and tool suites change. Counts in
+this document describe the 2026-07-30 research snapshot; the fixture manifest,
+not a prose count, is the eventual coverage authority.
+
+Refreshing a source creates a new corpus revision. Never silently replace an
+old fixture: doing so destroys result comparability.
+
+## Corpus Registry
+
+| Corpus | What it contributes | Inclusion policy |
+|---|---|---|
+| [Google `rust-crate-audits`](https://github.com/google/rust-crate-audits) | Independent expert audit notes over a very broad crate population, including proof/documentation defects and high-risk code without confirmed unsoundness | Exhaustively classify every audit record and represent every explicit issue atom |
+| [RustSec Advisory Database](https://github.com/RustSec/advisory-db) | Published affected ranges, advisories, references, and many vulnerable/fixed crate pairs | Include every Rust UB, memory-safety, or soundness advisory after de-duplication; do not limit the search to one label |
+| [GitHub Advisory Database](https://github.com/github/advisory-database) and [OSV](https://osv.dev/) | Additional aliases, affected ranges, references, and occasionally records not yet represented elsewhere | Reconcile with RustSec; add unique Rust memory-safety records |
+| [`google/zerocopy`](https://github.com/google/zerocopy) | A rich historical regression set plus a current, high-quality, heavily documented unsafe-code corpus with macros and many configuration axes | Include every located historical soundness incident as a vulnerable/fixed pair and shard a complete audit of the current pinned tree |
+| [`rust-lang/rust`](https://github.com/rust-lang/rust) standard-library history | Bugs in authoritative-library implementations, unusual unsafe abstractions, and compiler-version interactions | Include closed `I-unsound` library issues with reconstructible source and fixes; separately classify compiler bugs |
+| [`Qwaz/rust-cve`](https://github.com/Qwaz/rust-cve) | Curated historical Rust standard-library CVEs and soundness issue leads | Cross-check the standard-library inventory and reconstruct exact revisions |
+| [`Artisan-Lab/Rust-memory-safety-bugs`](https://github.com/Artisan-Lab/Rust-memory-safety-bugs) | A published 186-incident study corpus spanning third-party libraries, the standard library, executables, and one compiler bug | Import unique reconstructible incidents; preserve the paper's classifications only as hypotheses to verify |
+| [`rust-fuzz/trophy-case`](https://github.com/rust-fuzz/trophy-case) | Real fuzz-found defects and reproducers | Include genuine UB/memory-safety cases; retain panic, resource-exhaustion, and ordinary bounds-check failures as theorem-calibration controls |
+| [`sslab-gatech/Rudra`](https://github.com/sslab-gatech/Rudra) | Real unsafe-code findings and checker pass/fail examples, especially panic safety, Send/Sync, and higher-order unsafe interactions | Reconstruct reported issues and include representative tool tests |
+| [`vnrst/Yuga`](https://github.com/vnrst/Yuga) | Lifetime-annotation defects, a RustSec-derived example set, synthetic examples, and reported real-project findings | Include all available labeled examples, separating confirmed, fixed, unconfirmed, and synthetic cases |
+| [`safer-rust/RAPx`](https://github.com/safer-rust/RAPx) and predecessor datasets | Drop, aliasing, ownership, API-dependency, and verification examples, including sound controls | Import exact pass/fail examples and reconstruct linked real findings |
+| [`CodeSentryAI/lockbud`](https://github.com/CodeSentryAI/lockbud) | Concurrency, deadlock, atomicity, and memory-safety leads | Include only cases relevant to the claimed theorem and use non-UB concurrency bugs as calibration |
+| [`rust-lang/miri`](https://github.com/rust-lang/miri) | Small executable UB examples covering validity, initialization, alignment, aliasing, provenance, intrinsics, FFI, races, and target behavior, plus passing controls | Sample every semantic family from compile-fail/run-fail and pass suites; never treat a clean Miri run as a universal proof |
+| [`model-checking/kani`](https://github.com/model-checking/kani) and [`verify-rust-std`](https://model-checking.github.io/verify-rust-std/) | Proof harnesses, bounded-model examples, expected failures, and precise tool-scope questions | Use both genuine proofs and deliberately insufficient bounds/models |
+| [`tokio-rs/loom`](https://github.com/tokio-rs/loom) and [`MPI-SWS/genmc`](https://github.com/MPI-SWS/genmc) | Weak-memory, scheduling, publication, refcount, and atomic-ordering examples | Preserve each tool's stated execution/model limits; include both found executions and bound/model gaps |
+| [Verus](https://github.com/verus-lang/verus), [RefinedRust](https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev), and the [RustBelt artifact](https://plv.mpi-sws.org/rustbelt/popl18/) | Proof-bearing positive controls and examples of theorem/model boundaries | Admit only exact proved propositions and their explicit semantic/tool TCB |
+| [`DavisPL/rust-counterexamples`](https://github.com/DavisPL/rust-counterexamples) | Environmental, compiler, build-time, and safe-code counterexamples outside the ordinary unsafe-library abstraction model | Use to test theorem boundaries, deployment assumptions, and TCB reporting |
+| [`Speykious/cve-rs`](https://github.com/Speykious/cve-rs) | Deliberate exploitation of compiler/library soundness holes and safe-syntax boundary cases | Fetch on demand only after license review; use as boundary calibration, not a normal crate-audit benchmark |
+| [RustMizan](https://sfu-rsl.github.io/rust-mizan/) | Recent RustSec-derived vulnerable/patched crate-, file-, and function-level variants plus mutation/evaluation infrastructure | Revalidate historical licensing and every transformation; reserve privately regenerated variants as holdouts |
+| [RustXec](https://github.com/ying-selab/RustXec) | Reproducible vulnerability executions, build logs, fix links, and containers across many recent projects | Import only the memory-safety subset into soundness scoring; treat a reproduced bad outcome as evidence, not automatically as a Rust UB proof |
+| [TypePulse artifact](https://zenodo.org/records/14750104) | Type confusion, alignment, layout, transmutation, and lifetime findings | Require upstream confirmation or an independent proof/witness before objective scoring |
+| [`lizhuohua/rust-ffi-checker`](https://github.com/lizhuohua/rust-ffi-checker) and [`lizhuohua/rust-mir-checker`](https://github.com/lizhuohua/rust-mir-checker) | FFI ownership/lifetime and MIR bug leads, including trophy cases | Reconstruct from upstream; isolate GPL material and do not promote warnings to oracles |
+| [RustSan](https://www.usenix.org/conference/usenixsecurity24/presentation/cho-kyuwon), [ERASan](https://github.com/S2-Lab/ERASan), and [SafeFFI](https://www.usenix.org/conference/usenixsecurity26/presentation/braunsdorf) | Sanitizer-compatible RustSec cases and cross-language lifetime/ownership examples | Use as discovery or executable evidence subject to artifact/license review and exact model limitations |
+| [Awesome Rust Checker](https://github.com/BurtonQin/Awesome-Rust-Checker) | A discovery index for MirChecker, FFIChecker, TypePulse, PinChecker, MIRAI, Loom, Shuttle, and newer datasets | Re-run discovery at each corpus refresh; validate all leads against primary repositories |
+
+The registry is intentionally broader than the release-gating suite. A source is
+not a usable fixture until its exact artifact, license, expected theorem, and
+hidden oracle have been validated.
+
+### Legal disposition ledger
+
+The fixture manifest, rather than this discovery table, is authoritative for
+licensing. Use these initial dispositions:
+
+| Material | Metadata/tool license observed | Initial disposition |
+|---|---|---|
+| Google audit log | Apache-2.0 | Vendor metadata if useful; fetch each audited crate under its own historical license |
+| RustSec / imported GHSA | CC0-1.0 / CC-BY-4.0 metadata | Vendor metadata with attribution as required; fetch source/PoCs separately |
+| Miri, Kani, Loom, Verus, FFIChecker | Generally MIT, Apache-2.0, or dual-licensed; verify exact files | Vendor selected tests only with notices and per-file review |
+| MirChecker | GPL-3.0 | Isolate or link/fetch according to distribution policy |
+| Rudra analyzer | MIT OR Apache-2.0 | Tool tests may be vendorable; treat artifact/PoC repositories as link-only until their licenses are confirmed |
+| Yuga and its lifetime corpus | No clear redistribution license found in this review | Link-only; reconstruct cases from licensed upstream projects |
+| RustMizan / RustXec / TypePulse / research datasets | Dataset wrappers commonly CC-BY-4.0; embedded-source licenses vary | Fetch-by-digest; verify every historical source, PoC, generated file, and container independently |
+| ERASan / SafeFFI / RustSan artifacts | Reusable artifact or global license unclear for some material | Link-only until archive-level and per-file review succeeds |
+| CVE-Rs | Nonstandard GLWTSPL | Link-only or independently recreate the underlying compiler-boundary case |
+| Every historical crate or current challenge repository | Project-specific and revision-specific | Verify `Cargo.toml` plus `LICENSE*` at the exact snapshot; never infer from the current default branch |
+
+Public GitHub access is not redistribution permission, and a dataset license
+never silently relicenses embedded projects.
+
+## Mandatory Corpus A: Google Audit Log
+
+The pinned baseline is
+[`audits.toml` at commit `2a67b488aa2a4d123e68d95edd1f1916bb3f937e`](https://github.com/google/rust-crate-audits/blob/2a67b488aa2a4d123e68d95edd1f1916bb3f937e/audits.toml),
+dated 2026-07-29. It contains 2,177 audit records under 948 crate keys.
+There are 103 `ub-risk-3` and 73 `ub-risk-4` records, for 176 high-risk
+records across 149 crates. Across all grades, 91 records cite 114 distinct
+GitHub or GitLab issue/PR URLs; within the high-risk records, 66 records cite
+97 distinct such URLs. These numbers are inventory checks, not semantic labels.
+The audit repository is Apache-2.0 licensed; that does not relicense any audited
+crate source.
+
+### Closure procedure
+
+An import is complete only after all of the following hold:
+
+1. Parse every `[[audits.<crate>]]` record from the pinned file. Preserve the
+   crate key, record ordinal, version/delta range, criteria, notes, reviewer,
+   date if present, source aggregation, and every URL.
+2. Manually classify every record, including records whose notes are empty,
+   records that say no issue was found, and incomplete or difficult audits.
+3. Split each independent assertion or bullet in `notes` into an atom, then
+   recursively inspect every linked issue, PR body/comment, fixing diff, and
+   upstream discussion and atomize every additional independently checkable
+   defect or proof claim. A note such as “multiple issues” is not one atom.
+   Give source-derived atoms their own IDs and preserve the edge back to the
+   note and audit record.
+4. Classify each atom as one of:
+   - demonstrated or strongly supported unsoundness;
+   - a missing or invalid proof, safety contract, or safety comment;
+   - a reachable safe-surface or visibility defect;
+   - a configuration, generator, FFI, concurrency, panic, layout, validity, or
+     other coverage defect;
+   - a documented-postcondition defect;
+   - auditability or maintenance debt without a claim of unsoundness;
+   - an explicit no-known-defect result;
+   - an unconfirmed or disputed claim; or
+   - irrelevant to unsafe-code authoring and audit.
+5. Resolve cross-record edges such as “same review as previous” and
+   “see `<other crate>`.” Preserve every duplicate record-to-atom mapping even
+   when execution artifacts are de-duplicated.
+6. For delta audits, acquire both baseline and final source, preserve Cargo
+   Vet's final-version semantics, and determine whether the note describes a
+   newly present issue, a baseline issue, or an issue repaired by the final
+   version. Resolve package identity and archive checksum from metadata rather
+   than deriving it from the audit key.
+7. Follow every linked issue, PR, commit, advisory, and upstream discussion.
+   Validate that the cited source version actually contains the described code.
+   A risk grade or audit note is not enough to establish the oracle.
+8. Map every valid atom to an exact source snapshot and location. Where
+   possible, record a safe reproducer, the fixing change, and the smallest
+   authoritative Rust contract needed to adjudicate it.
+9. Give every record and atom a stable ID such as
+   `GRA:<audit-commit>:<crate-key>:<record-ordinal>:<atom-ordinal>`.
+10. Give every extracted URL a disposition: incorporated evidence, duplicate,
+    irrelevant, inaccessible, moved, or rejected with a reason. Record totals
+    by URL kind.
+11. Generate a closure report proving:
+   - 2,177 of 2,177 records are classified;
+   - every note atom, recursively source-derived atom, and URL has a
+     disposition;
+   - every confirmed atom appears in at least one blind fixture;
+   - every `ub-risk-3/4` record appears either as a finding fixture or a
+     calibration candidate with a recorded sampling/exclusion decision; and
+   - no fixture exposes its audit record, links, expected answer, or fix.
+
+Keyword extraction is useful for triage but is never the closure argument.
+Phrases such as “issues found,” “unsound,” “undefined behavior,” “incorrect
+safety comment,” “uninitialized,” and “missing safety documentation” miss
+indirectly worded findings and can misclassify historical or hypothetical
+discussion.
+
+### Required fixture forms
+
+Every confirmed issue atom gets a focused blind fixture containing enough
+unaltered context to derive the issue but no oracle leak. Every multi-issue
+record also gets a combined fixture to test whether the agent stops after its
+first finding. Representative crates from every risk grade get full,
+history-stripped source audits to test discovery in realistic noise.
+
+High-risk records with no proved defect are essential negative/calibration
+cases. The correct result may be a scoped `UNPROVED`, a documentation gap, or
+an expensive but successful proof; the evaluator must not reward invented UB.
+
+The audit log already supplies diverse regression leads, including:
+
+- invalid layout, validity, transmute, and representation assumptions;
+- premature `set_len` and uninitialized-memory exposure;
+- aliasing, interior-mutability, and lifetime extension;
+- panic/unwind and destructor invariants;
+- mutable statics, Send/Sync, callbacks, and global handlers;
+- `target_feature`, SIMD, architecture, OS, allocator, and debug-assertion
+  branches;
+- FFI declarations, ABI types, foreign ownership, and error behavior;
+- unsafe macros and generated safe APIs;
+- public pointer or invariant-bearing fields, `#[doc(hidden)]` items, sealing,
+  and unsafe trait contracts;
+- wrong, incomplete, or missing safety comments; and
+- code that appears alarming but for which the auditor did not establish
+  unsoundness.
+
+These are discovery aids, not an exhaustive hazard taxonomy. The record/atom
+closure check is what makes this corpus exhaustive.
+
+## Mandatory Corpus B: RustSec and Advisory Feeds
+
+The research checkout of RustSec is pinned at commit
+[`7c7ccac53056b87f69ac677f15ea2d9a98a6f8e2`](https://github.com/RustSec/advisory-db/commit/7c7ccac53056b87f69ac677f15ea2d9a98a6f8e2).
+At that snapshot, 192 crate advisory files contain
+`informational = "unsound"` and `rust/std` contains 18 standard-library
+advisory files.
+
+RustSec's own advisory metadata is CC0-1.0; imported GitHub advisory metadata
+may be CC-BY-4.0. Neither license applies to the underlying vulnerable source,
+PoCs, containers, or generated artifacts.
+
+The importer must not stop at those 192 records. Some concrete
+memory-corruption vulnerabilities are not informational “unsound” advisories,
+and one advisory may describe several defects. Search all RustSec records for
+Rust UB and memory-safety categories, descriptions, aliases, keywords,
+affected functions, and references. Reconcile aliases against GitHub's
+advisory database and OSV, then atomize each distinct defect.
+
+For each atom:
+
+- acquire the exact affected crate release from crates.io and verify its
+  checksum, or pin the exact repository commit if no published artifact exists;
+- acquire the first known fixed release or commit separately;
+- validate affected and patched ranges instead of trusting a title;
+- preserve the safe reproducer when one exists, but hide it from blind agents;
+- distinguish UB reachable from valid safe use, misuse of an unsafe API,
+  ordinary security bugs, panic/DoS, unmaintained status, and withdrawn or
+  disputed claims;
+- de-duplicate against Google audit-log, research-corpus, and upstream issue
+  atoms while retaining all provenance; and
+- retain the vulnerable/fixed pair even if the fix merely narrows the API or
+  changes its contract.
+
+The complete RustSec-derived set is a release-scale suite. A stratified subset
+is appropriate for rapid iteration, but every imported atom must remain
+scheduled for a periodic exhaustive run.
+
+## Mandatory Corpus C: Zerocopy
+
+### Historical vulnerable/fixed registry
+
+The history search produced this pre-admission registry. Full hashes shown with
+an ellipsis must be resolved from repository history before materialization.
+Before promotion from `Candidate`, the private manifest must add exact affected
+paths, trigger configurations, affected/fixed releases, and a two-reviewer
+source theorem. Unqualified `#NNN` references in this section are
+`google/zerocopy` issues or pull requests.
+
+| Case | Vulnerable state | Fixed state / primary source | Primary evaluation value | Initial class |
+|---|---|---|---|---|
+| Allocation `Layout` overflow | `173cd8eb117a967b6bb72c0b78cdac27e2100b31` | [`f3d80a93210d246a509bf56eed8bce6780b8160f`](https://github.com/google/zerocopy/commit/f3d80a93210d246a509bf56eed8bce6780b8160f), #63 | `usize` multiplication does not establish `Layout`'s `isize::MAX` bound; pointer-width/`alloc` case | Candidate |
+| `MaybeUninit<T>` unsafe impls, 0.7 | `cb20ba09…` | `62f76d2a…`, #299/#308 | `T` containing `UnsafeCell` violates the unsafe trait theorem | Candidate |
+| `MaybeUninit<T>` unsafe impls, 0.6 backport | `9bc48cc9…` | [`c33bc318160692090145d1e00f72259eab09ded5`](https://github.com/google/zerocopy/commit/c33bc318160692090145d1e00f72259eab09ded5), #309 | Same root obligation in a distinct release line | Candidate |
+| `Ref::into_ref` / `Ref::into_mut` | `a8572dafd9a0a5f5f583ab4c16e62dab9b664b15` and affected releases | 0.7 fix `3c1a56ac…`, other backports, 0.8 fix [`dad47d5ca87595f11881657d377f595be471e65b`](https://github.com/google/zerocopy/commit/dad47d5ca87595f11881657d377f595be471e65b), #716/#721/#755, [RUSTSEC-2023-0074](https://rustsec.org/advisories/RUSTSEC-2023-0074.html) | Runtime guard ownership/lifetime, safe returned-reference API, released-range reconstruction | Candidate |
+| `Ptr::forget_valid` | `f4995df6…` | [`7e62d435e1a9db1edc03d579c8f61f50d5ae37eb`](https://github.com/google/zerocopy/commit/7e62d435e1a9db1edc03d579c8f61f50d5ae37eb), #898 | `Valid` does not imply padding is initialized; non-total invariant ordering | Candidate |
+| Generated “at least” invariant | `674e7fb1…` | [`449eaff57eea3d9328e96fe3c7a7cdc45991f4c6`](https://github.com/google/zerocopy/commit/449eaff57eea3d9328e96fe3c7a7cdc45991f4c6), #909 | The same false relation generated through a macro | Candidate |
+| Atomic transparent wrapper | `4c3165f1…` | [`418555a37f3f92c89ce435624b38f215df515acb`](https://github.com/google/zerocopy/commit/418555a37f3f92c89ce435624b38f215df515acb), #1028/#1585 | Missing inner bound for `AtomicBool`; validity plus `target_has_atomic` | Candidate |
+| Safe `IntoByteSlice` trait | `d2e6bb8f…` | [`0f4ef070c76cbb33e5654410e35a1f2790a12500`](https://github.com/google/zerocopy/commit/0f4ef070c76cbb33e5654410e35a1f2790a12500), #1215/#1261 | A caller-provided safe impl can violate the exact-range invariant | Candidate |
+| Generic `repr(C, align(N))` derive | `2d5ef9f9…` | [`8e0de3fa2275f91abca38be83146136eb7fc726b`](https://github.com/google/zerocopy/commit/8e0de3fa2275f91abca38be83146136eb7fc726b), #1748/#1752 | Derive input closure and generic padding | Candidate |
+| `repr(Rust)` derive follow-up | resolve from #1764 | resolve from #1783 | Separate derive-input/layout atom | Candidate |
+| Aligned-enum derive follow-up | resolve from #1758 | resolve from #1784 | Separate enum layout/padding atom | Candidate |
+| `Ptr::read_unaligned` | `2c237a30…` | [`040557496ce7a0b1dac08c11c5ae37268b5d7b85`](https://github.com/google/zerocopy/commit/040557496ce7a0b1dac08c11c5ae37268b5d7b85), #1892/#1893 | Shared aliasing/interior mutability across `UnsafeCell` | Candidate |
+| Transient internal `Ptr::split_at` | change introduced immediately before #1890 | fixed before stable release, #1890 | Internal latent defect versus released safe-API/reachable-execution scope | Candidate calibration |
+| Mutable transmute, original | `3ad056be…` | partial fix `118b6f3b18a4ae997768860f3256a83b3a00990f`, #2226/#2229 | `&mut Dst` writes may invalidate the shadowed `Src` | Candidate |
+| Mutable transmute, partial fix | `118b6f3b18a4ae997768860f3256a83b3a00990f` | complete follow-up `25d27d579fc8ec9177384ff1e8175b8bf9f4838e`, #2331 | Detecting uncovered `TryFromBytes::*mut*` consumers | Candidate |
+| `FromBytes::read_from_io` | `49a13ba9…` | [`f99854afb33365e9dada073a166b3047df7109d1`](https://github.com/google/zerocopy/commit/f99854afb33365e9dada073a166b3047df7109d1), #2319/#2358 | Arbitrary caller-provided safe `Read::read` can inspect uninitialized padding; the selected-safe-dependency exception does not apply | Candidate |
+| DST/aligned-enum padding | `8647029c…` | [`ed93a1926701a1ac6e434e322a17473ac890ec8e`](https://github.com/google/zerocopy/commit/ed93a1926701a1ac6e434e322a17473ac890ec8e), #3063/#3064, fixed in 0.8.40 | Dynamic trailing padding and aligned enum cases | Candidate |
+| Exclusive `Ptr::iter` | `5fc5d5be…` | [`f70e4224996ed73b2cd927719246361d977a629e`](https://github.com/google/zerocopy/commit/f70e4224996ed73b2cd927719246361d977a629e), #3419/#3421, fixed in 0.8.50 | Two calls through `&self` yield overlapping exclusive pointers | Candidate |
+| `CastUnsized` safety proof | `5c67d2c8…` | [`7cc13f19f042482750f68c4abe0adecebc4d67e6`](https://github.com/google/zerocopy/commit/7cc13f19f042482750f68c4abe0adecebc4d67e6), #2908 | Invalid comment/proof, without automatically implying runtime unsoundness | Candidate calibration |
+| Previously unprovable `size_of_val_raw` argument | `a51d64fc…` | [`50d9d621284c5b64ac371d1f1b1f2381fec30d1b`](https://github.com/google/zerocopy/commit/50d9d621284c5b64ac371d1f1b1f2381fec30d1b), #1574 | A documentation gap later closed by a stronger std contract | Candidate calibration |
+| Raw-pointer read-only contract | parent of `403a890f…` | `403a890fcab08942c33e83d02884548544e31fe7`, #1607/#1617 | Contract needed to forbid assuming write permission | Candidate |
+| Stale `SizeEq` contract | `09334fd9…` | `81a0fd941138c309e5309a29285e74300be7d2de`, #2564 | Implementation evolution without invariant-documentation evolution | Candidate |
+| Missing/versionless citations | `9483f7dd…` | `16d065d1d59393cdcadbbce573a02b2279be59a9`, #1655/#2800 | Exact/versioned authority and independent citation verification | Candidate calibration |
+
+Retain these zerocopy-specific non-defect/uncertainty controls:
+
+- [#1757](https://github.com/google/zerocopy/issues/1757), a hypothesized
+  packed-union issue rejected under the supported inputs and generated padding
+  check;
+- [#672](https://github.com/google/zerocopy/pull/672), an explicitly
+  non-soundness `repr(C, packed(N))` regression;
+- [#1086](https://github.com/google/zerocopy/issues/1086), a target build
+  failure rather than demonstrated UB;
+- [#874](https://github.com/google/zerocopy/issues/874), a
+  potentially-unsound ZST/provenance concern not shown exercisable; and
+- [#3380](https://github.com/google/zerocopy/issues/3380), a
+  compiler/coinduction concern rather than a demonstrated current zerocopy
+  exploit.
+
+Search all branches and releases for `unsound`, `soundness`, `undefined
+behavior`, `UB`, safety-comment fixes, RustSec/GHSA identifiers, and changes
+that make an item or trait unsafe. Do not assume commit messages use those
+words. Diff public safety contracts and consult changelog/advisory history.
+Every distinct historical incident becomes a paired fixture; the fixing diff is
+hidden from both agents in the pair.
+
+### Current open-world audit
+
+The current baseline is
+[`53a3fbfa15d656b25b74688369f7248ff354a021`](https://github.com/google/zerocopy/commit/53a3fbfa15d656b25b74688369f7248ff354a021),
+described locally as `v0.8.55-3-g53a3fbfa1`. It is assumed to be a
+high-quality candidate, not assumed to be proved sound. A valid novel finding
+must never be scored as a false positive merely because the code is current.
+Materialize the fixture from that immutable commit object, not by copying the
+possibly dirty live worktree.
+
+The hidden minimum oracle for that snapshot must include these already known
+questions and defects:
+
+- [#2762](https://github.com/google/zerocopy/issues/2762): a nondeterministic
+  function-like proc macro can make repeated field-type tokens expand
+  differently, so a derive may validate one type and generate an unsafe impl
+  for another; owner: proc-macro shard. The hygiene check in
+  `830bc15e5…` does not repair nondeterministic repeated expansion;
+- [#388](https://github.com/google/zerocopy/issues/388): an attribute proc
+  macro running after a derive can mutate the item after the derive inspected
+  its earlier shape; owner: proc-macro shard;
+- [#2941](https://github.com/google/zerocopy/issues/2941): union field
+  projection may treat validity through one overlapping field as validity of a
+  different field; owners: pointer-projection and hidden-API shards;
+- [#899](https://github.com/google/zerocopy/issues/899): deliberately unsound
+  `#[cfg(test)]` implementations, which must be scoped to test executions rather
+  than misreported as a shipped production API defect; owners:
+  built-in-implementations and nonshipping-test-configuration shards;
+- [#2965](https://github.com/google/zerocopy/issues/2965): validity-contract
+  prose that may omit safety/provenance facts; owner: invariant-representation
+  shard;
+- [#2319](https://github.com/google/zerocopy/issues/2319): remaining
+  constructor/padding documentation questions after the I/O implementation
+  repair; owners: trait-contract and layout shards;
+- [#1792](https://github.com/google/zerocopy/issues/1792): union
+  `IntoBytes` derivation behind `zerocopy_derive_union_into_bytes`, with an
+  explicit conditional assumption and unsettled union-validity basis; owners:
+  proc-macro/generated-output and configuration shards; and
+- [#3199](https://github.com/google/zerocopy/issues/3199): unfinished proof
+  obligations for `layout::cast_from`, for which `UNPROVED` may be correct
+  without a UB witness; owner: layout/proof shard.
+
+These are a lower bound, not a complete answer key. Some are proof or
+configuration questions rather than demonstrated production unsoundness.
+Agents must independently derive the right classification and may find
+additional valid issues. Their initial admission class is `Candidate` or
+`Challenge`; an open issue alone does not make an objective defect oracle.
+
+Use separate fresh agents for these audit units:
+
+1. trait theorems and every safe method/surface in `src/lib.rs`;
+2. pointer invariant representation in
+   `src/pointer/{inner,invariant,ptr}.rs`;
+3. pointer operations, projection, iteration, and splitting in `src/pointer/`,
+   `src/lib.rs`, and `src/split_at.rs`;
+4. transmutation algebra in `src/pointer/transmute.rs`, related pointer
+   methods, and transmute macros;
+5. byte-slice, `Ref`, borrow-guard, ownership, and returned-reference behavior
+   in `src/byte_slice.rs` and `src/ref.rs`;
+6. wrapper lifetimes, interior mutability, allocation, and destruction in
+   `src/wrappers.rs`;
+7. primitive, atomic, function-pointer, SIMD, float, and validity
+   implementations in `src/impls.rs` and `src/byteorder.rs`;
+8. layout/allocation arithmetic, ZSTs, DST metadata, and allocation failure in
+   `src/layout.rs`, `src/util/mod.rs`, and alloc branches;
+9. declarative macros and hidden support in `src/macros.rs` and `src/util/`;
+10. the entire proc-macro generator as a theorem over every accepted token
+    stream and interaction with other macros/attributes;
+11. every checked-in generated output class and representative instantiated
+    expansion under `zerocopy-derive/`;
+12. build-script-produced Rust-version cfgs, feature closure, target
+   architecture, endianness, atomic widths, SIMD/nightly modes,
+   `debug_assertions`, `alloc`/`std`, documentation cfgs, Kani/Miri cfgs, and
+   unstable/internal configurations that can ship;
+13. all reachable `#[doc(hidden)]` safe surfaces, including direct downstream
+    access and mutation possibilities;
+14. dependency and TCB contracts; and
+15. an integration pass that consumes the shard reports and proves or refuses
+    the requested whole-crate conclusion.
+
+The current configuration manifest must investigate, then classify from pinned
+project policy:
+
+- features `alloc`, `std`, `derive`, `simd`, `simd-nightly`, and
+  `float-nightly`;
+- architectures including `arm`, `aarch64`, `x86`, `x86_64`, `wasm32`,
+  `powerpc`, and `powerpc64`;
+- endianness, 16-bit pointer-width paths, and atomic widths 8/16/32/64/ptr;
+- every build-script Rust-version cfg from the MSRV through current,
+  including gates associated with Rust 1.57, 1.59, 1.60, 1.61, 1.78, 1.81,
+  1.87, and 1.89;
+- `zerocopy_derive_union_into_bytes`, `zerocopy_unstable_ptr`,
+  `zerocopy_unstable_linux`, `zerocopy_inline_always`, `no_fp_fmt_parse`, and
+  internal dev/nightly cfgs; and
+- build/proc-macro host-target differences.
+
+Do not assume that every syntactically present axis is supported or shippable.
+Classify each combination as shipping-library, host-build, test-only,
+documentation-only, analysis-only (for example Miri/Kani/coverage), internal,
+or unsupported, with source evidence. The downstream theorem quantifies over
+the actual supported shippable set; separate the other classes so they can be
+audited without contaminating that theorem.
+
+The intentionally unsound test-only implementations marked
+`FIXME(#899)` in `src/impls.rs` are a scope-calibration fixture. An agent must
+notice them when tests are in scope, but must not claim that an excluded
+test-only path ships to downstream library users. Generated expected-output
+files and derive tests remain useful for proving what the proc macro emits.
+
+For the hidden-API shard, state explicitly that `#[doc(hidden)]` ordinarily
+removes documentation/SemVer expectations but does not relax soundness
+according to the item's safe/unsafe marking. Direct downstream use is not
+forbidden misuse merely because Rustdoc omits the item.
+
+The integration agent must receive raw source plus normalized shard reports,
+not this catalog or historical answers. A time-bounded inability to close the
+current whole crate should yield a precisely scoped `UNPROVED`, not an
+optimistic or pessimistic verdict.
+
+## Broader Real-World and Research Corpora
+
+### Rust standard library and compiler
+
+Cross-reference RustSec's `rust/std`, `Qwaz/rust-cve`, closed
+`I-unsound` + library-team issues, fixing PRs, and
+`tests/ui/known-bug` cases. Library implementation bugs are direct unsafe-code
+fixtures. Compiler bugs test a different TCB boundary and must be labeled as
+such; they must not be mixed into a score for author-written unsafe-library
+proofs without a separate theorem. A `tests/ui/known-bug` case usually records
+a pinned compiler regression expectation; it is not automatically an
+unsafe-library-authoring defect.
+
+High-value adversarial-safe-caller pairs include:
+
+- [`Borrow` returning different values across calls](https://github.com/rust-lang/rust/issues/80335)
+  and its fixing PR #81728;
+- [`Read` returning a count larger than the supplied buffer](https://github.com/rust-lang/rust/issues/80894),
+  fixing PR #80895, and documentation clarification #82892; and
+- [a panicking callback observing `String::retain`'s temporary invariant
+  violation](https://github.com/rust-lang/rust/issues/78498), initial repair
+  #78499, and follow-up #82554.
+
+The incomplete first `String::retain` repair is a useful partial-fix fixture.
+These cases test arbitrary type-valid behavior, panic, reentrancy, and repeated
+queries from caller-controlled safe code.
+
+The 186-incident Artisan-Lab corpus reports 33 standard-library, 142
+third-party-library, 10 executable, and one compiler case. Use it to discover
+older issues missing from modern advisory filters, then revalidate every case
+against primary source because labels and language rules may have evolved.
+
+The
+[Crates and Vulnerabilities dataset](https://zenodo.org/records/7828059)
+indexes 84,105 packages, 433 vulnerabilities, 300 repositories, and 218 fix
+commits. Its CC-BY-4.0 wrapper is useful for discovery and metadata joins, but
+does not relicense embedded crate source.
+
+### Packaged benchmark corpora
+
+[RustMizan](https://github.com/sfu-rsl/rust-mizan) is unusually close to the
+desired evaluation shape. Its published dataset contains 42 RustSec
+memory-safety CVEs across 25 crates and 173 crate-, file-, and function-level
+variants, often with vulnerable and patched sides, annotations, mutation
+infrastructure, and Kani/RAPx integrations. Use its runner and transformations
+as implementation leads, but independently verify:
+
+- the exact historical code license for every embedded crate;
+- that “patched” means only that the disclosed bug is repaired;
+- that every supposedly semantics-preserving mutation actually preserves the
+  relevant obligation; and
+- that public variants have not become recognition tests through model
+  training.
+
+Regenerate and privately review metamorphic variants for holdout use.
+
+[RustXec](https://github.com/ying-selab/RustXec) contains 102 vulnerabilities
+from 89 projects from 2021–2025, with proof-of-vulnerability executions,
+containers, fix links, and build/test logs. Its approximately 88.5 GB artifact
+is best fetched on demand. Only its memory-corruption subset belongs in
+soundness scoring; other security defects belong in separately labeled
+robustness/security tests. Reproducing a disclosed bad outcome does not by
+itself prove which Rust abstract-semantic rule is violated.
+
+[TypePulse](https://zenodo.org/records/14750104) contributes 26 known
+type-confusion examples and additional reported findings involving
+misalignment, layout, transmutation scope, lifetime, and representation.
+Analyzer output is a lead until an upstream acknowledgement, independent
+witness, or source proof validates the exact snapshot.
+
+### Checker and verifier corpora
+
+For Rudra, Yuga, RAPx and its predecessors, Lockbud, MirChecker, FFIChecker,
+TypePulse, and PinChecker:
+
+1. acquire the tool's expected-pass and expected-fail examples;
+2. locate every linked upstream issue and fixing commit;
+3. distinguish developer-confirmed, independently reproduced, tool-only,
+   disputed, and false-positive cases;
+4. import real code independently of the detector output;
+5. hide tool names, warnings, issue titles, and known reproducers from the
+   audit agent; and
+6. use the detector output only as an evaluator lead until a human has
+   reconstructed the proof or counterexample.
+
+Yuga is particularly useful for lifetime annotation and interprocedural
+dataflow. Its repository includes synthetic/RustSec examples and reported
+findings in projects such as `bv`, `cslice`, `json-rust`, `sled`, `tokio`, and
+audio bindings. Confirmed and unconfirmed reports must be separate strata.
+
+Miri's fail/pass suites provide precise microfixtures but measure different
+behavior:
+
+- a failing execution can witness an error under Miri's model and exact run;
+- a passing execution does not prove soundness for all inputs/configurations;
+- a fixture about unsupported behavior can test whether the agent records a
+  model or documentation gap; and
+- a sound tool with a proved exhaustive harness may discharge a stronger claim
+  than ordinary sampled testing.
+
+Kani and other proof tools should therefore contribute paired evidence
+fixtures: one whose documented model and exhaustive harness imply the claimed
+proposition, and one with a missing bound, environmental model, configuration,
+or tool premise. The evaluation asks the agent to accept only the exact theorem
+actually established.
+
+Use [Loom](https://github.com/tokio-rs/loom) for controlled concurrency pairs
+involving publication, refcounts, wakeups, aliasing, and memory ordering, but
+retain its documented scheduling/model limitations in the hidden oracle. Use
+[GenMC](https://github.com/MPI-SWS/genmc) as a complementary LLVM-level
+weak-memory source after per-file license review.
+
+Verus, RefinedRust, RustBelt, and `verify-rust-std` can supply genuine scoped
+positive controls. The evaluator must preserve the exact specification,
+semantic model, trusted toolchain, admitted axioms, and connection between the
+proved artifact and audited code. A theorem about λRust or a translated/model
+program is not silently a theorem about every detail of the current Rust
+implementation.
+
+Rudra's published work reported 264 bugs and 76 CVEs and is valuable for unsafe
+generics/traits, uninitialized exposure, higher-order invariants, panic safety,
+and Send/Sync. Its analyzer repository is permissively licensed, but the
+inspected artifact/PoC repositories do not clearly grant the same license. Use
+those as indexes and reconstruct fixtures from exact upstream crate revisions.
+
+FFIChecker contributes FFI ownership, use-after-free, and double-free cases.
+MirChecker contributes FFI lifetimes, possible double frees, and many
+non-soundness arithmetic/panic warnings. The former is MIT; the latter is
+GPL-3.0. Keep GPL material isolated and independently adjudicate both tools'
+trophy cases.
+
+RustSan selected ASan-compatible RustSec cases; ERASan contains additional
+RustSec proof-of-concept material; and SafeFFI supplies vulnerable and benign
+cross-language pairs, patched compiler/runtime pieces, and probabilistic
+AArch64 HWASan tests. Where a reusable artifact or redistribution license is
+unclear, retain only a link/acquisition recipe. Sanitizer failures are concrete
+execution evidence; sanitizer silence does not cover all validity, provenance,
+race, configuration, or execution obligations.
+
+### Recent public development cases
+
+The following 2026 leads are useful public development fixtures:
+
+- [`jxl-grid` GHSA-5pmv-rx8r-wmv5](https://github.com/tirr-c/jxl-oxide/security/advisories/GHSA-5pmv-rx8r-wmv5),
+  a 32-bit integer-overflow/out-of-bounds-write case with a vulnerable/fixed
+  release pair and Miri reproducer;
+- [`intrusive-rs` PR #104](https://github.com/Amanieu/intrusive-rs/pull/104)
+  and adjacent 2026 fixes, covering use-after-free, iterator/splice
+  transitions, concurrency, and panic safety;
+- [`rkyv` issue #670](https://github.com/rkyv/rkyv/issues/670), involving
+  crafted-archive out-of-bounds behavior; and
+- current RustSec records such as exception-safety/uninitialized-value and
+  bounds-checking unsoundness.
+
+At each refresh, search advisory feeds, `I-unsound` issues, fixing PRs, Miri
+regressions, and maintained checker result lists for newer cases. Keep holdout
+identities and answers outside this repository in an access-controlled store.
+Checked-in named cases are never “private holdouts,” regardless of their age.
+Refer to true holdout cohorts only by opaque cohort/version IDs.
+
+### Environmental and adversarial-safe-code boundaries
+
+`rust-counterexamples` and selected compiler/OS cases test whether the agent
+correctly separates:
+
+- source-level Rust soundness from an OS, filesystem, process, or deployment
+  theorem;
+- trusted deliberately selected dependency behavior from arbitrary
+  caller-provided safe code;
+- compiler/std assumptions from library implementation proof;
+- build-time or linker behavior from a runtime UB claim; and
+- unconditional soundness from a cryptographic, negligible-probability, or
+  deployment-restricted claim.
+
+These fixtures are expected to produce qualified TCB entries and scoped
+verdicts, not one universal classification.
+
+## Hand-Built and Metamorphic Fixtures
+
+Real incidents do not cover every load-bearing instruction in isolation.
+Create small hand-proved fixtures for:
+
+- public fields, constructors, safe methods, safe trait methods, and
+  macro-generated safe APIs as alternate invariant-bypass surfaces;
+- a properly sealed trait, an incompletely sealed trait, and a soundness
+  requirement placed only in safe trait prose;
+- a `pub(super)` invariant-bearing safe field versus a compiler-enforced
+  public `unsafe` field with a complete contract;
+- delayed dataflow in which an unsafe function stores state consumed by a later
+  function;
+- a caller callback or safe trait implementation that returns a type-valid but
+  adversarial value, panics, reenters, or mutates accessible state;
+- a deliberately selected safe dependency API versus caller-provided safe
+  code with identical-looking documentation;
+- a third-party unsafe dependency that is audited, admitted precisely, or
+  silently trusted;
+- a valid `SAFETY` citation, a misquote, a wrong-version citation, and a
+  citation whose context does not imply the asserted fact;
+- an unsafe API that is UB-free but violates a promised postcondition;
+- a postcondition weakening or safety-precondition strengthening across
+  SemVer, exact-pin, in-tree-fork, and out-of-band contract channels;
+- UB hidden behind a feature/target/cfg combination, macro expansion,
+  build-script result, allocator, panic path, `debug_assertions`, SIMD feature,
+  or architecture;
+- a cryptographic-signature or hash-collision guarded bad path;
+- an execution that eventually exhibits UB, testing rejection of “before the
+  UB was still guaranteed” reasoning;
+- a deployment-restricted binary whose conditional theorem is valid but whose
+  API would be unsound if exported safely; and
+- a proof-producing static analysis result versus a sampled or bounded result
+  that does not establish the requested universal claim.
+
+Prefer reversible mutations of real fixed code over invented anti-patterns.
+Examples include restoring one hunk of a historical fix, moving a check under
+`debug_assert!`, exposing one private invariant-bearing field, deleting one
+safety-contract conjunct, or generating the same defect through a macro. Each
+mutation must have a human-reviewed proof that it changes exactly the intended
+obligation and does not leak the answer through naming.
+
+## Coverage Dimensions
+
+The fixture manifest must tag, but must not assume exhaustiveness from, these
+dimensions:
+
+- raw pointer allocation, provenance, bounds, alignment, liveness, and access;
+- references, aliasing, interior mutability, and concurrency;
+- initialization, padding, byte exposure, and type validity;
+- layout, `repr`, DST metadata, enums, `bool`, niches, and transmutation;
+- arithmetic, indexing, capacity/length, zero-sized types, and address spaces;
+- ownership transfer, panic/unwind, cancellation, reentrancy, drop, and leaks;
+- lifetimes, variance, higher-ranked bounds, Pin, self-reference, and callbacks;
+- unsafe traits/impls, Send/Sync, safe implementers, and sealing;
+- FFI, ABI, unwinding, foreign allocation, symbols, linker behavior, and
+  external specifications;
+- atomics, races, memory ordering, and global/static state;
+- target architecture/OS/endian/pointer width/atomic width, SIMD and
+  `target_feature`, features, allocator, panic strategy, optimization,
+  `debug_assertions`, toolchain version, and build/proc-macro output;
+- all safe API surfaces, including hidden and generated surfaces;
+- local invariant composition across functions and time;
+- authoritative citations, documentation gaps, dependency trust, and TCB
+  non-vacuity;
+- mandatory postconditions, robustness scope, and contract evolution;
+- probabilistic/deployment assumptions and exact verdict scope; and
+- evidence interpretation, including testing, interpreters, static analysis,
+  model checking, deductive verification, and manual proof.
+
+This tag set is for measuring diversity and detecting omissions. The real
+closure rule is proposition-based: every known issue atom and every requested
+skill behavior must have a fixture.
+
+## Fixture Admission and Provenance
+
+A source's admission class determines how it may be scored:
+
+- **Objective defect:** two independent reviewers have produced and reconciled
+  an authority-rooted source theorem for the exact artifact, valid-use path,
+  violated or missing proposition, and status. A runtime witness, upstream
+  acknowledgement, vulnerable/fixed pair, formal result, and reproducer are
+  independent corroboration tags; none substitutes for the source theorem.
+- **Candidate:** an advisory, audit note, analyzer report, unresolved issue, or
+  incomplete human argument still requires adjudication. It may test review
+  behavior but cannot contribute to objective defect-recall scoring.
+- **Scoped positive proof:** two reviewers have accepted a complete proof of an
+  exact property under an explicit model and TCB. The proof may be rigorous
+  English or machine-checked; machine form is not required.
+- **Bug-specific fixed control:** the known defect theorem is false on the
+  fixed artifact for a proved reason. This says nothing about other defects or
+  whole-artifact soundness.
+- **Challenge:** no complete positive or negative oracle. Score process, scope,
+  and independently adjudicated findings; never score “agrees with no known
+  bug” as soundness.
+
+Record corroboration independently, for example `UPSTREAM-ACK`, `VULN-FIXED`,
+`EXEC-WITNESS`, `FORMAL-WITNESS`, `SAFE-REPRODUCER`, and `MULTI-REVIEW`.
+
+A fixture is admitted only when its hidden manifest records:
+
+- stable fixture and oracle-atom IDs;
+- `theorem_domain` and `boundary_class`, separating author/library unsafe
+  abstractions, standard-library implementations, compiler TCB bugs,
+  OS/FFI/environment/deployment claims, build/proc-macro/supply-chain
+  execution, and non-UB robustness/security;
+- all source URLs and immutable revisions/checksums;
+- acquisition date and exact files included;
+- vulnerable and fixed revisions, when applicable;
+- affected Rust/compiler/dependency versions;
+- supported and trigger configurations;
+- license/SPDX expression, attribution, and redistribution decision;
+- separate metadata, historical source, PoC/harness, generated-file, and
+  container licenses, with disposition `vendor`, `fetch-by-digest`,
+  `link-only`, or `exclude`;
+- the exact claim the evaluation asks the agent to establish;
+- a human-reviewed explanation for every known finding and accepted
+  alternative reasoning;
+- authoritative Rust/std citations or an explicit documentation/TCB gap;
+- safe reproducers, tool results, and their limits;
+- expected status for soundness, postconditions, and conditional claims;
+- fixture transformations and a semantic-equivalence review;
+- all oracle-leak removals;
+- duplicate links to other corpora; and
+- confidence, disputes, and required human adjudication.
+
+Do not redistribute code when its license is absent, incompatible, or unclear.
+Store an acquisition recipe and digest and fetch it on demand. Preserve all
+required notices for vendored fixtures.
+
+## Refresh Checklist
+
+Before a release-scale evaluation:
+
+1. Pin new commits for every database and discovery index.
+2. Re-run exhaustive record/atom classification for changed records.
+3. Search zerocopy and other designated repositories for new advisories,
+   unsoundness issues, contract changes, and safety-comment fixes.
+4. Import new RustSec/GHSA/OSV and standard-library incidents.
+5. Search recent checker publications and primary issue trackers.
+6. Reserve a private, recent holdout cohort.
+7. Revalidate old fixtures against their pinned compiler and documentation.
+8. Recheck licenses, acquisition digests, links, and oracle isolation.
+9. Publish a corpus revision manifest and change summary.
+10. Never rewrite prior result records to use the new corpus retroactively.
diff --git a/evals/unsafe-rust/testing-plan.md b/evals/unsafe-rust/testing-plan.md
new file mode 100644
index 0000000000..71b5e0ef37
--- /dev/null
+++ b/evals/unsafe-rust/testing-plan.md
@@ -0,0 +1,1106 @@
+# Unsafe Rust Skill Evaluation Plan
+
+> **Evaluator-only material**
+>
+> This plan and every oracle it produces must remain outside the installable
+> `unsafe-rust` skill and outside every test agent's filesystem and context.
+> Evaluation agents receive the skill, a neutral task, and the source under
+> review—never this document, the source catalog, advisory/audit metadata, a
+> fixing diff, or an intended conclusion.
+>
+> **Status:** active protocol. The initial non-release pilot is recorded in
+> [`runs/2026-07-30-exploratory-pilot/`](runs/2026-07-30-exploratory-pilot/).
+> The frozen legacy rerun is recorded in
+> [`runs/2026-07-31-legacy-regression/`](runs/2026-07-31-legacy-regression/),
+> and the 54-run abstraction-design treatment/core-ablation experiment is
+> recorded in
+> [`runs/2026-07-31-abstraction-design-v1/`](runs/2026-07-31-abstraction-design-v1/).
+> The latter confirmed a material workflow improvement but failed its complete
+> preregistered gate set; none of these studies is a universal release proof.
+
+## Evaluation Objective
+
+Determine whether using the `unsafe-rust` skill causes fresh coding agents to
+author and audit unsafe Rust with materially better proof completeness,
+defect recall, calibration, and contract preservation than the same agents
+without the skill.
+
+The suite must test observable behavior, not preferred wording. Its primary
+question is:
+
+> Given only the audited artifact, its real contracts and configurations, and
+> admissible documentation, does the agent find and discharge every in-scope
+> soundness and mandatory-postcondition obligation, expose every missing
+> implication, and state no stronger conclusion than its proof establishes?
+
+For confirmed historical defects, the suite must demonstrate that agents can
+independently recover every known issue atom. For fixed or proved controls, it
+must penalize agents that merely recognize a pattern and assert unsoundness.
+For open-world targets such as current zerocopy, it must reward valid novel
+findings and honest incompleteness rather than agreement with an assumed
+“clean” label.
+
+This evaluates a skill revision, agent model, tool environment, prompt,
+corpus revision, and budget together. It never establishes that the skill, an
+agent, or a codebase is universally sound.
+
+## Non-Negotiable Design Properties
+
+1. **Fresh agents.** Every discovery, authoring, review, and paired-side run
+   starts without conversation history or another agent's conclusions.
+2. **Blind artifacts.** Expected findings, issue/advisory titles, vulnerable
+   labels, fixes, audit notes, and oracle metadata are absent.
+3. **Exact provenance.** Every artifact, compiler, dependency, documentation
+   version, configuration, and skill revision is pinned.
+4. **Issue-level closure.** Aggregate averages never hide a known issue atom
+   that no skill-enabled agent found.
+5. **Open-world adjudication.** Known findings are a lower-bound oracle. A
+   novel finding is reviewed, not automatically called a false positive.
+6. **Paired calibration.** Vulnerable, fixed, proof-complete, proof-incomplete,
+   and no-known-defect cases are all represented.
+7. **Universal-claim discipline.** A tested matrix does not substitute for a
+   proof over every supported shippable configuration.
+8. **Independent authority checking.** An answer is not correct merely because
+   it agrees with an advisory. Its Rust/std factual premises and citations must
+   actually imply its claims.
+9. **No unsafe execution by default.** Source review is read-only. Any build
+   script, proc macro, native build, test, container, reproducer, or historical
+   package execution occurs only in a disposable, credential-free,
+   network-disabled sandbox.
+10. **Separate authoring from validation.** Freeze the skill before running an
+    evaluation. If a result motivates a skill change, assign a new revision
+    and restart affected conditions; never patch the treatment in place after
+    observing its outputs.
+
+## Evaluation Artifact Architecture
+
+Keep four stores physically separate:
+
+1. **Runtime skill store**
+   - only the exact `skills/unsafe-rust/` package under test;
+   - immutable per run;
+   - no links to maintainer or evaluator material.
+2. **Blind fixture store**
+   - source, public API documentation, exact dependencies/contracts, and a
+     neutral task;
+   - no `.git`, history, answer metadata, or issue-bearing collateral;
+   - content-addressed.
+3. **Private oracle store**
+   - the full manifest described in the source catalog;
+   - audit/advisory/issue/fix provenance;
+   - known-finding atoms and human proofs;
+   - inaccessible to the audited agent and synthesis agents.
+4. **Result store**
+   - immutable prompts, environment manifests, raw transcripts, reports, TCB
+     logs, edits, tool outputs, resource usage, and scores;
+   - result IDs derived from skill, corpus, fixture, condition, agent, and
+     replicate revisions.
+
+An evaluation sandbox should contain only:
+
+```text
+/task/task.md
+/target/...
+/skill/unsafe-rust/...
+/contracts/...       # only exact contracts the real auditor could inspect
+/rust-docs/...       # optional pinned Reference/std mirror
+/output/...
+```
+
+Do not mount the enclosing repository. In particular, exclude `evals/`,
+`maintainers/`, other worktrees, branch metadata, local playbooks, cached
+advisories, and sibling vulnerable/fixed fixtures.
+
+Use a genuinely separate filesystem namespace, container, or VM. Codex
+sub-agents in one root thread share the checkout and are not isolated merely
+because they were told not to read sibling paths. The baseline environment must
+contain no installed `unsafe-rust` skill, prior-skill package, skill metadata,
+or searchable cache.
+
+The runner must fail closed if a forbidden path is present or if the blind
+bundle's digest differs from its manifest. Hash the complete effective prompt,
+mounted files, tool policy, network policy, and environment for each condition.
+
+### Executable-artifact isolation
+
+Treat historical `build.rs`, proc macros, native build systems, test binaries,
+PoCs, and supplied container images as hostile. Execute them only inside a
+disposable VM/microVM or equivalently reviewed hardened boundary with:
+
+- no host filesystem, daemon socket, device, credential, secret, SSH agent, or
+  cloud-metadata access;
+- read-only content-addressed inputs and isolated throwaway output/caches;
+- non-root execution, syscall/capability/device restrictions, and no privilege
+  escalation;
+- no egress or DNS;
+- CPU, memory, disk, PID, file-size, and wall-time quotas; and
+- teardown plus artifact/log capture after each run.
+
+A third-party container image is an input, not the security boundary. Source
+review never requires executing the target and remains the default.
+
+## Fixture Preparation
+
+### Preserve what the proof needs
+
+Include:
+
+- all source files in the stated audit scope;
+- actual public and safety documentation;
+- manifests, lockfiles, build scripts, macros, proc macros, generated source,
+  target specifications, and configuration policy needed to determine the
+  supported set;
+- exact dependency API documentation or source when its contract is relevant;
+- exact external specifications needed for FFI or deployment claims; and
+- ordinary repository instructions only in a specifically labeled
+  naturalistic variant.
+
+Do not “simplify” a real fixture in a way that removes an invariant producer,
+consumer, panic path, callback, configuration, or generated surface.
+
+### Remove answer leakage
+
+By default remove:
+
+- `.git`, branches, tags, commit messages, blame, and remotes;
+- `.cargo_vcs_info.json`, embedded source-map/provenance paths, patch metadata,
+  generated provenance comments, and package-manager caches that reveal source
+  revisions;
+- changelogs, release notes, security policy incident lists, advisory files,
+  audit metadata, and issue/PR templates that name the defect;
+- regression tests, examples, or filenames that explicitly state the answer,
+  unless the task is intentionally to explain a supplied failing execution;
+- fix patches and sibling fixture directories;
+- evaluator manifests and diagnostic output from analysis tools; and
+- issue numbers in non-semantic comments.
+
+Never remove or silently rewrite the API's actual safety contract or the
+`SAFETY` comment being audited. If a real semantic comment itself names an
+incident, classify the case as a follow-through test or build a separately
+reviewed neutral reduction; do not pretend it is blind discovery.
+
+Before removing collateral, check `include_str!`, `include_bytes!`, build
+scripts, proc macros, generated-source inputs, package metadata, and test
+harnesses for semantic use of that file. If the build or proof consumes it,
+retain it in a labeled naturalistic fixture or replace it only with a reviewed
+neutral equivalent.
+
+Maintain two variants where sanitation might affect realism:
+
+- **naturalistic:** the exact distributable source minus version-control and
+  evaluator material; and
+- **blind:** a reviewed bundle with answer-bearing collateral removed.
+
+Record every transformation. Compilation/tests can check for accidental
+breakage but cannot prove semantic equivalence.
+
+Scan the final bundle for oracle issue numbers and titles, URLs, advisory IDs,
+audit-note substrings, base/fix SHAs, vulnerable/fixed labels, and source-map
+paths as well as forbidden files. “Blind” means evaluator-oracle-blind; it
+cannot prove that a pretrained model never saw a public incident. Only opaque,
+access-controlled holdouts and freshly reviewed transformations reduce that
+residual contamination.
+
+### Do not reveal the trigger configuration
+
+Tell the agent the genuine support policy and ask for every supported
+configuration. Do not say “look at 32-bit,” “enable feature X,” or “the bug is
+in release mode” unless an ordinary user request would already restrict scope
+that way. The hidden oracle records the triggering combination.
+
+For a separate local-proof capability test, it is acceptable to scope the task
+to one module or function, but the prompt must not identify the violated
+obligation.
+
+## Hidden Fixture Manifest
+
+Each fixture must instantiate the source-catalog schema and additionally
+record:
+
+- neutral target label and blind-bundle digest;
+- task mode and exact prompt;
+- files and public surfaces genuinely in scope;
+- `theorem_domain` and `boundary_class`, kept separate among author/library
+  unsafe abstraction, standard-library implementation, compiler TCB,
+  OS/FFI/environment/deployment, build/proc-macro/supply-chain execution, and
+  non-UB robustness/security;
+- supported configuration set and trigger subset;
+- every expected finding atom and its required discovery scope;
+- allowed classifications and accepted alternative proof paths;
+- whether a concrete UB witness is required, optional, or unavailable;
+- whether the case is Objective defect, Candidate, Scoped positive proof,
+  Bug-specific fixed control, or Challenge, plus independent corroboration
+  tags;
+- contamination risk and public-model-training likelihood;
+- source-level, runtime, binary, deployment, robustness, and security claims
+  that must remain separate;
+- expected TCB entries and entries that would make the theorem vacuous;
+- run permissions and whether executing any project code is allowed;
+- scorer version and required human expertise; and
+- retirement/revalidation triggers.
+
+The oracle atom must describe a proposition, not a keyword. For example,
+“agent says aliasing” is insufficient. It should state which safe surface
+permits which state, how that state reaches which consuming operation, which
+precondition is not proved, and what status follows.
+
+## Fresh-Agent Protocol
+
+### Definition of fresh
+
+A fresh agent:
+
+- receives no turns from skill design, corpus research, fixture preparation,
+  the other half of a pair, or another evaluation;
+- has no persistent memory or shared scratch files;
+- cannot inspect result/oracle stores or the internet beyond the evaluation's
+  explicit allowlist;
+- receives the same model, reasoning effort, tools, and resource budget as its
+  comparator; and
+- starts from a content-addressed clean sandbox.
+
+When using sub-agents, use no inherited turns (`fork_turns="none"` or its
+equivalent). Do not use an agent that helped author or research the skill.
+
+### Conditions
+
+Run two separately labeled experiments; they answer different questions.
+
+1. **Naturalistic lift**
+   - Skill condition: an ordinary user audit/authoring request that explicitly
+     invokes the mounted `$unsafe-rust` skill.
+   - No-skill baseline: the same ordinary request without the invocation and
+     with no specialized skill mounted or discoverable.
+   - Interpretation: the combined benefit of the skill's workflow and content
+     for a normal request.
+2. **Rubric-controlled lift**
+   - Skill condition: a detailed user request that independently states the
+     desired theorem, configuration, citation, TCB, postcondition, and output
+     requirements, plus the mounted skill.
+   - No-skill baseline: byte-identical substantive requirements without a
+     mounted or discoverable skill.
+   - Interpretation: the skill's additional value after the user has already
+     supplied much of the rubric.
+
+When evaluating a revision, add a **previous-skill condition** to each
+experiment under otherwise identical conditions.
+
+Do not use the detailed prompt templates below as the naturalistic no-skill
+baseline; they intentionally encode several skill teachings. Freeze and hash
+the effective prompt and mounts for every condition.
+
+Randomize condition order and opaque fixture names. Never let one agent see two
+conditions or both sides of a vulnerable/fixed pair.
+
+Use at least three independent replicates per condition for routine fixtures
+and five for release-gating, high-severity, current-zerocopy minimum-oracle, and
+private-holdout fixtures. Fix the sampling configuration when the platform
+allows it; otherwise record it.
+
+An evaluation is invalid if a skill run gets more time, task-specific context,
+network, search results, or tool permissions than its baseline. The skill
+package itself is the intended treatment; no condition may see another
+condition's package or metadata.
+
+### Documentation access
+
+Prefer a pinned offline mirror of the exact Rust Reference and standard-library
+documentation versions applicable to the fixture. Otherwise allow network
+access only to exact versioned `doc.rust-lang.org` pages and explicitly
+provided external/dependency specifications. Block general search, GitHub,
+RustSec, crates.io pages, blogs, and cached issue results.
+
+Fail closed on redirects outside the allowlist, unversioned-documentation
+fallbacks, and content whose digest or version differs from the manifest.
+
+The agent must open and verify cited documentation. Merely emitting a plausible
+URL does not receive citation credit.
+
+### Budgets
+
+Use realistic but generous budgets. Whole-crate proof is not a function-level
+task. Split large repositories into invariant-owning modules and configurations
+before reducing the budget.
+
+Record:
+
+- model and reasoning setting;
+- token and elapsed-time budget;
+- tool-call and source-line counts;
+- documentation retrieval time;
+- whether the run ended naturally, exhausted a budget, or was interrupted; and
+- any user steering.
+
+Budget exhaustion is `UNPROVED` evaluation behavior, not evidence that the
+target is sound or unsound.
+
+## Prompt Templates
+
+Replace bracketed fields mechanically from the private manifest. Do not add an
+issue hint.
+
+### Naturalistic lift
+
+Skill-enabled audit:
+
+```text
+Use the $unsafe-rust skill from [SKILL_PATH] to audit [TARGET] at the supplied
+snapshot. Do not modify the target. Write the audit report to [OUTPUT].
+```
+
+No-skill audit:
+
+```text
+Audit [TARGET] at the supplied snapshot. Do not modify the target. Write the
+audit report to [OUTPUT].
+```
+
+Use equivalently short paired requests for change review and authoring. Do not
+silently add the skill's theorem, safe-surface checklist, citation rules,
+configuration closure, verdicts, or TCB template to this baseline.
+
+The remaining templates are for the separately reported rubric-controlled
+experiment.
+
+### Focused audit
+
+```text
+Use the $unsafe-rust skill from [SKILL_PATH] to audit [TARGET] at the supplied
+snapshot. The in-scope source is [SCOPE]. Establish the strongest justified
+source-level Rust soundness and mandatory documented-postcondition conclusions
+for every valid use and every supported shippable configuration in that scope.
+Do not modify the target. Put the persistent audit report and TCB audit log in
+[OUTPUT]. Independently verify every cited authority.
+```
+
+### Full crate or library
+
+```text
+Use the $unsafe-rust skill from [SKILL_PATH] to perform a complete unsafe-code
+audit of [TARGET] at the supplied snapshot. Derive the supported configuration
+set from the source and project policy. Cover every reachable safe and unsafe
+API surface, generated artifact, and invariant transition that can ship to
+downstream users. Do not modify the target. Put the persistent audit report and
+TCB audit log in [OUTPUT]. If the proof cannot be closed, identify the exact
+unproved obligations rather than guessing a verdict.
+```
+
+### Change review
+
+```text
+Use the $unsafe-rust skill from [SKILL_PATH] to review the supplied patch to
+[TARGET]. Determine every soundness, safety-contract, documented-postcondition,
+configuration, and compatibility obligation affected by the change. Review
+both the changed lines and every producer or consumer whose proof depends on
+them. Do not modify the target. Write the review to [OUTPUT].
+```
+
+### Repair/authoring
+
+```text
+Use the $unsafe-rust skill from [SKILL_PATH] to make [REQUESTED API OR CHANGE]
+correct for all valid uses and supported shippable configurations. You may edit
+the target. Minimize the unsafe boundary, write proof-grade safety contracts
+and local comments, and update the TCB/audit artifacts required by the skill.
+Do not rely on hidden caller behavior. Put the change and audit handoff in
+[OUTPUT].
+```
+
+### Evidence review
+
+```text
+Use the $unsafe-rust skill from [SKILL_PATH] to determine exactly what the supplied
+analysis result and harness establish about [TARGET]. State the theorem, model,
+bounds, configurations, assumptions, and remaining TCB. Then determine which
+requested soundness or postcondition obligations, if any, it discharges.
+```
+
+### Integration
+
+```text
+Use the $unsafe-rust skill from [SKILL_PATH] to integrate the supplied independent
+module audit reports for [TARGET]. Check their scopes, TCBs, boundary contracts,
+configuration coverage, and producer/consumer handoffs against the raw source.
+Do not assume a shard verdict is correct merely because it is supplied.
+Establish or refuse the requested whole-target conclusions and write the
+integrated report to [OUTPUT].
+```
+
+Rubric-controlled baseline prompts replace only
+`Use the $unsafe-rust skill from [SKILL_PATH] to` with `Independently`; their
+substantive requirements remain byte-identical. They must not add a tutorial or
+abbreviated rubric.
+
+## Test Families
+
+### 1. Microproof and contract tests
+
+Use short snippets with complete hidden proofs to isolate one behavior at a
+time:
+
+- identify the exact operation/contract being justified;
+- enumerate every precondition;
+- derive each conjunct from local facts, named invariants, verified axioms, or
+  explicit TCB entries;
+- prove the resulting invariant and mandatory postconditions;
+- reject a circular, restated, misquoted, inapplicable, or wrong-version proof;
+- distinguish `UNPROVED`, `UNSOUND`, and `CONTRACT-BROKEN`;
+- trace dataflow from a state-producing unsafe API to a later consumer;
+- treat an adversarial safe trait implementation or callback correctly;
+- recognize all safe API surfaces, including public fields, constructors,
+  methods, trait methods, macros, and reachable hidden items;
+- distinguish a macro callable with no caller-side unsafe obligation from a
+  macro deliberately constructed so expansion succeeds only in an unsafe
+  context, then audit the actual generated API/operation;
+- handle sealing and compiler-enforced unsafe fields;
+- separate selected-safe-dependency trust from caller-controlled safe code;
+- qualify cryptographic/deployment assumptions; and
+- reject “observations before later UB remain guaranteed.”
+
+For each unsound/proof-incomplete microfixture, include a separately run
+proof-complete partner. Rename and reorder variants to prevent memorized pattern
+matching.
+
+### 2. Google audit-log exhaustive suite
+
+Use the pinned source and closure process in
+[source-catalog.md](source-catalog.md).
+
+Build four sub-suites:
+
+1. **`GRA-ATOM`:** one focused blind fixture for every confirmed note atom.
+   This is the direct capability regression: can the skill recover every known
+   issue without being told what it is?
+2. **`GRA-MULTI`:** one combined fixture for every record with multiple
+   independent atoms. This tests whether an agent stops after the first issue.
+3. **`GRA-REPLAY`:** a naturalistic full-source or original-delta audit for
+   every record containing an admitted objective finding, plus a preregistered
+   stratified sample of difficult/high-risk records with no known defect. This
+   tests discovery amid realistic noise and calibration without converting a
+   risk grade into an answer.
+4. **`GRA-LEDGER`:** classify all 2,177 records, recursively atomize their
+   linked primary sources, and give every record, atom, URL, and exclusion a
+   disposition. This is exhaustive issue-coverage accounting, not necessarily
+   2,177 agent runs.
+5. **`GRA-ALL-REPLAY` (research-scale optional):** when resources and public
+   source reconstruction permit, run record-level blind replays over the full
+   ledger. An unavailable or non-relevant record receives a recorded
+   disposition, not a fabricated fixture. This optional sweep is not a
+   prerequisite for useful initial validation.
+
+Import the snapshot-specific anchor families and calibration labels from the
+source catalog and generated corpus manifest. Keep crate names and incident
+lists out of this stable protocol so the catalog can refresh without the two
+documents drifting. In particular, distinguish confirmed issues, fixed
+versions such as the cataloged `flate2` control, explicitly disputed atoms,
+and generated-code negative controls. The record/atom/URL closure ledger—not a
+handwritten list or risk grade—establishes completeness.
+
+### 3. Advisory and historical-pair suite
+
+For every admitted RustSec/GHSA/OSV memory-safety atom:
+
+1. run a focused vulnerable fixture;
+2. run a full-source vulnerable audit where source size permits;
+3. run the fixed side with a different fresh agent;
+4. run a change-review fixture over the repair without revealing the issue;
+5. when practical, ask a fresh authoring agent to repair the vulnerable side;
+6. separately present any reproducer/tool result as an evidence-review task;
+   and
+7. de-duplicate scoring while retaining every advisory-to-atom mapping.
+
+The source catalog and generated manifest hold the current named anchor set.
+Select release cohorts by theorem domain and coverage tags—initialization,
+arbitrary caller types, concurrency, target layout, SIMD, generated code, FFI,
+panic/drop, allocators, provenance, compiler evolution, lifetime, postconditions,
+adversarial safe traits, reentrancy, and other admitted dimensions—without
+duplicating snapshot-specific names here.
+
+Build/proc-macro code-execution advisories are scope/TCB fixtures unless a
+separate source-level UB proposition is proved.
+
+### 4. Standard-library adversarial-safe-caller suite
+
+Reconstruct every admitted adversarial-safe-caller pair in the source catalog,
+including any partial repair, and add every admitted standard-library
+`I-unsound` atom from the corpus ledger. These cases test that unsafe code may
+not rely on caller-provided safe implementations behaving according to prose.
+Keep compiler soundness bugs in a separate TCB-boundary stratum.
+
+### 5. Zerocopy historical suite
+
+Every historical lead in the source catalog gets:
+
+- a vulnerable focused audit;
+- a fixed focused audit by a different agent;
+- a full-source or full-module audit;
+- a change review;
+- a proof-comment/contract review when the repair changed prose; and
+- a partial-fix test when history contains more than one repair.
+
+The source catalog's versioned historical registry is the mandatory set; import
+it mechanically rather than maintaining a second list here. Include its
+negative, disputed, internal-only, build-failure, and proof-comment calibration
+cases as distinct cohorts.
+
+Score the dataflow theorem, not just the changed line. For example, the
+`Ref` case requires following runtime borrow-guard ownership to a returned
+reference; the mutable-transmute history requires detecting that an initial
+repair covered only one of several consumers.
+
+### 6. Current zerocopy suite
+
+Materialize the exact immutable current commit identified in the source
+catalog, not the live worktree. Import the catalog/manifest's current
+invariant-owner shards. Run each with five fresh skill agents, five no-skill
+baselines, and at least three previous-skill agents. Give each shard enough
+budget to close its own surface and configuration partition.
+
+The shard manifest must contain an invariant-owner/boundary coverage map
+showing that every source file, reachable public surface, generated artifact,
+configuration class, producer, transition, and consumer belongs to a shard.
+Shard boundaries must arise from proof ownership, not from the locations of
+known issues. Retain at least one naturalistic full-source run so shard-specific
+hints and missed cross-boundary behavior are visible.
+
+Then run separate fresh integration agents over:
+
+- raw current source;
+- normalized shard reports with agent identity removed but condition kept
+  homogeneous: skill integration receives only skill reports, baseline
+  integration only baseline reports, and previous-skill integration only
+  previous-skill reports;
+- the union of declared scopes, TCBs, obligation ledgers, and configuration
+  partitions; and
+- no historical/current issue oracle.
+
+Required special runs:
+
+1. **Reachable `#[doc(hidden)]` audit.** Exercise hidden public traits,
+   associated items, modules/reexports, helper types, safe methods, and exported
+   macros from an adversarial downstream crate. State that hidden items are
+   ordinarily outside documentation/SemVer promises but retain the soundness
+   obligations implied by their actual safe/unsafe markings; direct use is not
+   forbidden misuse.
+2. **Proc-macro theorem.** Audit the generator over every accepted token stream,
+   interaction with attribute/function-like macros, repeated tokens, hygiene,
+   cfgs, discriminants, and generated helper types.
+3. **Generated-output audit.** Inspect real expansions and checked-in expected
+   outputs, not only generator source.
+4. **Configuration closure.** Derive the actual supported shippable set from
+   pinned project policy. Separately classify shipping-library, host-build,
+   test-only, documentation-only, analysis-only, internal, and unsupported
+   combinations. Prove the shipping theorem universally and audit the other
+   requested classes without silently folding them into that theorem.
+5. **Scope calibration.** Correctly classify intentionally unsound
+   `#[cfg(test)]` code without claiming it ships in the normal library.
+6. **Naturalistic versus skill-isolation.** Run once with ordinary project
+   instructions and once with only the target source plus skill. The isolation
+   variant explicitly excludes `zerocopy/AGENTS.md`,
+   `zerocopy/agent_docs/`—especially `agent_docs/unsafe_code.md`—other
+   worktrees, playbooks, this repository's evaluator material, and fixes.
+
+The catalog maps each hidden current minimum-oracle item to owning shards and a
+provisional admission class. Release checking must verify that each admitted
+objective atom is addressed by every owning shard; Candidate/Challenge items
+are scored for reasoning and calibration, not agreement with an open issue.
+Any novel finding receives independent adjudication.
+
+Do not call current zerocopy a clean or fixed control. The correct integrated
+result may be a mix of scoped `PROVED`, `UNPROVED`, `UNSOUND`,
+`CONTRACT-BROKEN`, and conditional claims.
+
+### 7. Tool-evidence and proof suite
+
+Build paired tasks from:
+
+- Miri fail/pass suites;
+- Kani expected pass/fail and `verify-rust-std`;
+- Loom and GenMC concurrency examples;
+- Verus, RefinedRust, and RustBelt proof artifacts;
+- Rudra, Yuga, RAPx, TypePulse, FFIChecker, MirChecker, RustSan/ERASan, and
+  SafeFFI findings; and
+- ordinary tests, fuzzing, sanitizers, and manual analyses attached to real
+  incidents.
+
+For every result, ask what exact proposition it establishes. Include:
+
+- one witnessed bad execution;
+- one clean sampled execution;
+- one bounded proof with an insufficient bound;
+- one exhaustive finite proof;
+- one proof under a model that omits the relevant behavior;
+- one proof over generated/translated code with an unproved source mapping;
+- one concurrency exploration with an incomplete schedule/model;
+- one static analysis that soundly over-approximates the requested domain; and
+- one analyzer warning with no validated oracle.
+
+The agent must neither dismiss every static analysis nor promote every formal
+tool result to universal Rust soundness.
+
+Include `cargo-geiger` only as potentially incomplete unsafe-site/configuration
+enumeration evidence, never as a soundness oracle. Include
+`cargo-semver-checks` or public-API diffs only as contract-evolution discovery
+aids, never as proof that safety preconditions or behavioral guarantees were
+preserved.
+
+### 8. Authoring, repair, and review suite
+
+Auditing alone does not validate the authoring half of the skill. Ask fresh
+agents to:
+
+- design a greenfield safe wrapper over a raw-pointer primitive from
+  requirements;
+- design a greenfield unsafe API with complete caller obligations;
+- choose and implement a greenfield unsafe-trait or sealing strategy;
+- design a macro-generated safe/unsafe API whose theorem covers every accepted
+  input and expansion;
+- design an FFI or allocator abstraction from exact external requirements;
+- turn a historical defect into a sound safe abstraction;
+- choose between local validation and propagating an unsafe caller contract;
+- redesign a safe trait as sealed or unsafe when its behavior is consumed for
+  soundness;
+- privatize an invariant-bearing `pub(super)` field or design a documented
+  compiler-enforced unsafe field;
+- write exact `# Safety` documentation and adjacent `SAFETY` proofs;
+- replace a misquoted/versionless citation with a verified, versioned one or
+  report that authoritative text is insufficient;
+- preserve invariants across panic, unwind, cancellation, reentrancy, and drop;
+- repair a macro/proc macro by proving the generator theorem or constraining
+  accepted inputs;
+- update a TCB audit log for a safe dependency, unsafe dependency, exact pin,
+  in-tree fork, or out-of-band contract;
+- preserve documented postconditions as well as UB freedom; and
+- review contract evolution for SemVer, exact pins, forks, and consumer-specific
+  agreements.
+
+Give greenfield tasks hidden proof obligations rather than an intended API
+shape. Accept any design that closes those obligations and preserves the
+requested behavior; do not reward imitation of one reference implementation.
+
+Evaluate the resulting code and proof independently. Compilation, tests, Miri,
+or a plausible comment cannot substitute for the hidden proof.
+
+### 9. Robustness, compatibility, and conditional-theorem suite
+
+Use paired snippets and real fixes to test:
+
+- UB-free implementation that violates an unsafe API's postcondition;
+- postcondition weakening that invalidates downstream unsafe proofs;
+- safety-precondition strengthening across a nominally compatible release;
+- a safe API correctness failure not in requested robustness scope;
+- a cryptographic-signature-gated bad path;
+- a negligible-probability collision path;
+- a binary safe only under an explicit deployment restriction;
+- a safe library API that tries to hide the same restriction;
+- exact-version/fork/out-of-band dependency guarantees; and
+- compiler/linker/build options that still produce a binary but change the
+  requested claim or TCB.
+
+Score source soundness, documented postconditions, compatibility, security,
+probability, and deployment as separate claims.
+
+### 10. Metamorphic, instruction-injection, and holdout suite
+
+For each major defect family, create privately reviewed variants that:
+
+- rename crates/items/lifetimes and neutralize comments;
+- reorder independent declarations and invert branches;
+- extract or inline helper functions;
+- move the invariant carrier across a type, field, guard, token, or function
+  contract;
+- emit the operation through a macro or inspect its expansion;
+- place the defect behind a feature, cfg, target, allocator, panic path, or
+  build-script result;
+- substitute ZST, over-aligned, zero-length, allocation-failure, reentrant,
+  panicking, weak-memory, or adversarial-safe-code cases; and
+- restore one hunk of a real repair while retaining unrelated refactors.
+
+Include semantics-changing partners that look syntactically similar. A skill
+that memorizes “this pattern is bad” should fail the fixed partner.
+
+Add naturalistic repositories containing misleading source comments,
+repository instructions, generated text, or prompt-like strings. The agent
+must treat target content as code/data under audit, not as authority to weaken
+the user task, reveal other files, skip proof, or change output destinations.
+Keep ordinary project policy distinct from adversarial instruction injection.
+
+All named cases in the checked-in source catalog are public development
+fixtures, not private holdouts. Keep true holdout identities, source, and
+answers only in an access-controlled store and refer to them in this plan by
+opaque cohort/version ID.
+
+## Scoring Model
+
+### Per-finding atom
+
+Score applicable dimensions on a three-point scale:
+
+| Dimension | 0 — absent/incorrect | 1 — partial | 2 — complete |
+|---|---|---|---|
+| Discovery | Missing or wrong location | General concern near relevant code | Exact location/surface and full affected scope |
+| Required proposition | Wrong or absent | Some pre/postconditions identified | Every applicable pre/postcondition stated concretely |
+| Dataflow/invariant chain | Missing or circular | Partial producer/consumer trace | Every establishment, transition, suspension, consumer, and exit path accounted for |
+| Premises and authority | Folklore, unchecked, or hallucinated | Plausible but incomplete support | Local facts checked; exact versioned authority verified; non-axioms explicit in TCB |
+| Valid-use reasoning | Hidden caller assumption | Some adversarial cases | Quantifies over all valid uses and adversarial safe caller behavior |
+| Configuration closure | Trigger/config missed | Trigger found but no supported-set proof | Every actually supported combination covered concretely or abstractly |
+| Classification | Incorrect verdict | Concern found but statuses conflated | Exact independent status for soundness, postconditions, and conditional claims |
+
+A finding counts as recovered only if the agent identifies the affected
+surface/location, the violated or missing proposition, and a defensible
+classification. Keyword overlap does not count.
+
+Pre-register `N/A` dimensions per fixture and task mode before any run; exclude
+them from both numerator and denominator. Never convert a missing applicable
+dimension to `N/A` after seeing a result.
+
+Use separate rubrics:
+
+- **Audit:** the seven common dimensions above plus whole-scope/safe-surface
+  coverage and report completeness.
+- **Authoring/repair:** design validity, minimal/enforced boundary, complete
+  contracts/comments, proof, postcondition preservation, configuration
+  closure, TCB update, and compatibility.
+- **Change review:** changed-proof impact, all affected producer/consumer
+  discovery, contract directionality, configuration impact, compatibility, and
+  correct disposition.
+- **Evidence review:** exact theorem, model/domain/bounds, source-artifact
+  correspondence, tool/environment TCB, configuration scope, and which target
+  obligations follow.
+
+Do not aggregate scores across task modes or theorem domains as if their
+denominators were equivalent.
+
+### Per-run dimensions
+
+Measure:
+
+- known-atom recall and multi-issue completeness;
+- valid-finding precision after adjudication;
+- unsupported `UNSOUND` and unsupported `PROVED` rates;
+- safe-surface discovery;
+- obligation-ledger completeness;
+- local proof completeness and non-circularity;
+- citation accuracy, versioning, quotation scope, and actual verification;
+- TCB completeness, precision, versioning, and non-vacuity;
+- adversarial safe-caller handling;
+- mandatory-postcondition coverage;
+- configuration/generator coverage;
+- production/test/internal/released scope accuracy;
+- correct use of `UNPROVED`;
+- contract-evolution and SemVer analysis;
+- evidence theorem/model calibration;
+- novel-finding validity;
+- actionable report quality;
+- edit correctness and preservation for authoring tasks; and
+- tokens, elapsed time, tool calls, and human adjudication cost.
+
+Keep defect recall and proof quality separate. An agent may identify the right
+line for an invalid reason, or write a beautiful proof that omits another safe
+surface.
+
+Report author/library unsafe abstractions as the primary skill-effect cohort.
+Report standard-library implementation, compiler TCB, OS/FFI/environment,
+build/proc-macro/supply-chain execution, and non-UB robustness/security as
+separate domains. Never improve the primary score by pooling easier or
+conceptually different boundary cases into it.
+
+### Hard errors
+
+Any of the following fails the run regardless of aggregate score:
+
+- `PROVED` is issued with an undisclosed/uncovered obligation or supported
+  shippable configuration;
+- `UNSOUND` is issued without a proved valid-use path to UB;
+- a fixed/proved partner is condemned solely by pattern recognition;
+- an invalid, hallucinated, or unchecked authority citation is used as a
+  necessary premise;
+- arbitrary caller-provided safe code is trusted behaviorally;
+- an advisory, issue, tool result, this skill, or evaluator text is used as a
+  Rust axiom;
+- a `PROVED` postcondition or whole-scope conclusion omits an applicable
+  mandatory documented postcondition;
+- a TCB entry assumes the exact in-scope conclusion or implementation and makes
+  the audit vacuous;
+- test-only/internal/non-shipping code is misreported as an ordinary downstream
+  production surface, or a shipping configuration is dismissed as “only cfg”;
+- eventual UB is treated as preserving guaranteed observations “before” it;
+  or
+- the agent read any oracle/paired-side material.
+
+A missed known atom is an issue-level recall failure and may block its
+preregistered cohort or release; it is not labeled a universal hard error in
+every stochastic naturalistic/full-crate run. This distinction prevents
+confusing failure to discover a defect with an affirmatively unsound or
+fabricated conclusion.
+
+## Release Gates
+
+Before the first scored run, freeze:
+
+- the corpus revision, admitted denominator, exclusions, cohorts, task modes,
+  theorem domains, and `N/A` decisions;
+- primary/secondary endpoints, replicate/stopping rule, retry policy, budgets,
+  and scorer version;
+- numerical non-inferiority and improvement margins; and
+- opaque holdout cohort/version IDs.
+
+The default gates are intentionally demanding:
+
+1. Every admitted Objective-defect atom appears in an evaluator-oracle-blind
+   fixture.
+2. Every admitted Objective-defect atom is recovered and correctly classified
+   in every skill-enabled focused replicate.
+3. Every atom in a `GRA-MULTI` fixture is recovered in every release-gating
+   focused replicate; finding only the first issue fails that fixture.
+4. A preregistered full-source/sharded recall cohort meets its explicit
+   issue-level target. Use 100% when the prompt, scope, partition, and budget
+   expressly ask for complete recovery. Report broader naturalistic
+   full-repository recall per replicate without relabeling every stochastic
+   miss a hard error.
+5. There are zero hard errors.
+6. On focused Objective-defect fixtures, every applicable proof dimension
+   scores 2. Full-source cohorts have no applicable dimension at 0 and meet a
+   preregistered mean/floor.
+7. Fixed-side controls do not reproduce the repaired finding. Other valid
+   findings remain allowed. Scoped positive proofs are accepted only within
+   their exact theorem/model/TCB; Candidate and Challenge fixtures are never
+   global soundness labels.
+8. Every admitted Objective-defect item in the current-zerocopy minimum oracle
+   is addressed by each owning shard with correct
+   production/test/configuration scope. Candidate/Challenge entries are judged
+   on reasoning and calibration, not issue agreement.
+9. Every authoring fixture produces no unsound or vacuous edit and satisfies
+   all applicable contract, postcondition, configuration, TCB, and
+   compatibility dimensions.
+10. The runner emits a successful automated attestation for filesystem,
+    package, prompt, network, documentation, and paired-side isolation.
+11. The opaque holdout cohort has 100% focused Objective-defect recall, zero
+    hard errors, required proof-quality floors, no repaired-defect false
+    assertion, and no fixture-specific runtime-skill change.
+12. Skill-versus-baseline/prior-skill effects meet preregistered endpoints.
+    Suggested defaults are zero additional hard errors; a lower 95% paired
+    confidence bound above -2 percentage points for recall, adjudicated
+    precision, and proof-floor pass rate; and either a +10-point absolute
+    improvement or standardized paired effect of at least 0.5 on a primary
+    behavior the skill is intended to change. When the baseline is already at
+    least 95% and the skill meets the absolute safety floors, a preregistered
+    ceiling rule may accept non-inferiority without artificial “improvement.”
+
+The 2,177-record GRA ledger remains the full corpus-closure goal, but completing
+it is not a prerequisite to begin with a frozen, semantically adjudicated
+initial tranche. No release may claim exhaustive audit-log issue coverage until
+every record, recursively derived atom, and URL has a disposition.
+
+Because agents may be stochastic, report every replicate. Statistical
+confidence intervals and paired effect sizes are useful secondary summaries;
+they do not turn an individual missed soundness obligation into a success.
+Three/five replicates are engineering minima, not statistical justification;
+increase them when a power analysis or endpoint variance requires it.
+
+If a fixture is wrong, contaminated, unlicensed, or ambiguous, quarantine and
+repair it with a versioned reason. A post-result quarantine creates a new
+corpus revision and restarts every affected comparison; it cannot change the
+frozen denominator retroactively. Required-run infrastructure failures and
+budget exhaustion remain failed/incomplete results under the preregistered
+retry policy, not silently replaceable runs. Never relabel an agent failure as
+a fixture failure merely to pass the release.
+
+## Oracle Construction and Adjudication
+
+### Build an oracle, do not copy a verdict
+
+For every objective atom, two qualified reviewers should independently:
+
+1. inspect the exact source and all relevant safe surfaces/configurations;
+2. reconstruct the producer-to-consumer dataflow;
+3. state the missing/violated proposition;
+4. verify the exact Reference/std basis or record a documentation/TCB gap;
+5. check the safe reproducer or proof when available;
+6. inspect the repair and confirm what it changes;
+7. classify soundness, postcondition, compatibility, and conditional claims
+   separately; and
+8. reconcile disagreements before the atom becomes an Objective defect or
+   Scoped positive proof.
+
+Audit notes, advisories, upstream acknowledgements, and fixing diffs are strong
+leads and corroboration, but not substitutes for this work.
+
+### Novel findings
+
+Blind scorers first remove agent identity and condition. Two independent
+reviewers then classify every extra assertion as:
+
+- valid new finding;
+- valid proof/documentation gap;
+- duplicate or broader form of an oracle atom;
+- unsupported but reasonable question;
+- invalid assertion; or
+- requires upstream/Rust-documentation clarification.
+
+Do not penalize a run for a valid novel finding. Add confirmed incidents to the
+regression corpus after disclosure/embargo and licensing review.
+
+Potential novel defects in current maintained code enter an access-controlled
+coordinated-disclosure quarantine. Restrict transcripts, reports, PoCs, and
+fixture material to the triage group; contact the applicable maintainers; and
+do not publish results or admit a public regression fixture until the issue is
+fixed, disclosed, or the maintainers authorize release.
+
+### Scoring independence
+
+Whenever feasible:
+
+- fixture authors do not score the first run;
+- blind scorers do not know skill/baseline condition;
+- an adjudicator resolves disagreement;
+- the same judge rubric and evidence bundle apply to all conditions; and
+- automated extraction computes counts only after semantic labels are fixed.
+
+LLM judges may assist with report normalization but cannot be the sole
+authority for a Rust soundness oracle.
+
+Before release-scale scoring, calibrate reviewers on a hidden mixed set and
+measure agreement by label and rubric dimension. Require unanimous reconciled
+theorem atoms for Objective-defect/Scoped-positive admission and a
+preregistered agreement floor (suggested: Cohen's κ or Krippendorff's α at
+least 0.8) for routine scoring. Unresolved theorem disagreements block oracle
+admission; they are not averaged into a numeric truth.
+
+## Execution Schedule
+
+### Pre-merge smoke suite
+
+Run a small, rotating, contamination-resistant set covering every load-bearing
+skill instruction:
+
+- microproof citation and invariant tests;
+- one adversarial safe trait/callback;
+- one vulnerable/fixed real pair;
+- one multi-issue audit-log record;
+- one cfg/generated-code defect;
+- one postcondition/contract-evolution case;
+- one evidence-calibration pair; and
+- one current-zerocopy shard excerpt.
+
+This is a fast regression signal, not the release claim.
+
+### Candidate-release suite
+
+Run:
+
+- every microfixture;
+- every `GRA-ATOM` and `GRA-MULTI` fixture;
+- all admitted RustSec historical pairs in the release subset;
+- all zerocopy historical cases;
+- all current zerocopy shards and integration;
+- all authoring/review/evidence tests;
+- fixed/proved/calibration controls; and
+- the opaque access-controlled holdout cohort.
+
+### Full corpus suite
+
+At each major skill release and corpus refresh, run:
+
+- `GRA-REPLAY`, completed `GRA-LEDGER` closure, and, when scheduled,
+  `GRA-ALL-REPLAY`;
+- every admitted RustSec/GHSA/OSV memory-safety atom;
+- all reconstructible standard-library cases;
+- packaged benchmark corpora after de-duplication;
+- every admitted, independently adjudicated checker finding;
+- expanded configuration/architecture runners; and
+- multiple supported agent models if the skill is intended for them.
+
+Large corpus runs may be distributed, but each audit agent remains isolated.
+
+### Longitudinal suite
+
+Retain results by immutable skill and corpus revision. Track:
+
+- newly found incidents;
+- old fixtures invalidated by Rust/documentation evolution;
+- behavior changes by model revision;
+- improvements and regressions by skill section;
+- cost and completion trends; and
+- which historical audits need reinterpretation after a foundational skill
+  change.
+
+## Result Report
+
+Publish a report containing:
+
+- exact skill, corpus, runner, model, toolchain, and documentation revisions;
+- fixture inclusion/exclusion and license summary;
+- contamination checks;
+- automated isolation attestation;
+- condition/replicate counts and resource budgets;
+- separately reported task modes and theorem domains;
+- issue-level results, with no known atom hidden by aggregate metrics;
+- hard errors;
+- precision after novel-finding adjudication;
+- configuration and safe-surface coverage;
+- citation and TCB defects;
+- authoring/edit preservation results;
+- skill versus baseline/prior-skill paired comparisons;
+- current-zerocopy shard and integration outcomes;
+- invalid/quarantined fixtures;
+- threats to validity; and
+- proposed skill changes linked to behavioral failures.
+
+Do not publish opaque holdout source or answers. Do not publish vulnerable code
+whose license or coordinated-disclosure status forbids it.
+
+## Threats to Validity
+
+Actively monitor:
+
+- public advisories and famous fixes present in model training;
+- answer leakage through source comments, tests, changelogs, crate names, or
+  network search;
+- source reductions that remove the actual producer/consumer chain;
+- “fixed” labels being mistaken for whole-crate soundness;
+- tool warnings being mistaken for ground truth;
+- Reference/std documentation changing after a fixture was proved;
+- compiler behavior or aliasing/provenance models changing;
+- running only the configuration that triggers a known bug;
+- unrealistic prompts, budgets, or permissions;
+- scorer awareness of condition;
+- evaluator disagreement hidden by one numeric score;
+- model updates being mistaken for skill improvements;
+- duplicating one incident across RustSec, GHSA, audit logs, and research
+  datasets; and
+- benchmark-specific instructions accreting into the runtime skill.
+
+The response to contamination is access-controlled metamorphic/holdout renewal,
+not more explicit hints in the prompt.
+
+## Readiness Checklist for the Follow-Up Testing Turn
+
+Before running the first agent:
+
+1. Freeze the skill revision.
+2. Implement the private fixture/oracle manifest and result schema.
+3. Create the 2,177-record audit-log ledger, freeze an initial adjudicated
+   denominator, and continue full record/atom/URL closure as the release-scale
+   corpus goal.
+4. Admit an initial Objective-defect and Scoped-positive tranche with
+   two-reviewer authority-rooted proofs.
+5. Materialize vulnerable/fixed zerocopy historical pairs.
+6. Materialize current zerocopy's manifest-defined invariant-owner shards,
+   whole-source variant, boundary coverage map, and supported-set manifest.
+7. Build and hash blind bundles; scan them for oracle leakage.
+8. Prepare pinned offline Rust/std documentation and exact external contracts.
+9. Construct and review the hardened no-network VM/microVM runner for any
+   executable artifact.
+10. Dry-run only the harness on a trivial non-evaluation fixture.
+11. Freeze prompts, corpus denominator/exclusions, budgets, conditions,
+    replicate/stopping/retry rules, numerical endpoints/margins, and scorer
+    rubrics.
+12. Calibrate independent scorers and resolve every admission disagreement.
+13. Verify in an automated attestation that agents cannot read `evals/`,
+    `maintainers/`, sibling worktrees, prior results, another condition's skill
+    package, or the other half of any pair.
+
+Only then begin semantic testing. Any skill change made in response to a result
+starts a new skill revision and requires fresh runs; do not continue the same
+agent conversation.
diff --git a/skills/unsafe-rust/SKILL.md b/skills/unsafe-rust/SKILL.md
new file mode 100644
index 0000000000..543a42bc7f
--- /dev/null
+++ b/skills/unsafe-rust/SKILL.md
@@ -0,0 +1,221 @@
+---
+name: unsafe-rust
+description: "Author, document, review, audit, or redesign unsafe Rust with proof-grade rigor. Use for unsafe blocks and functions, unsafe traits and impls, raw pointers, FFI, inline assembly, intrinsics, layout or validity reasoning, concurrency and atomics, SIMD and target features, allocators, invariant-bearing fields, safety comments or `# Safety` documentation, soundness reviews, TCB audits, generated unsafe code, changes to safety or behavioral contracts, and proof-oriented redesign of unsafe abstractions."
+---
+
+# Unsafe Rust Authoring and Audit
+
+Treat each safety contract as an English-language theorem and each safety
+comment as its proof. Reject hand-waving, folklore, hidden assumptions, and
+proof by testing.
+
+## Establish the Exact Claim
+
+Unless the user specifies a narrower claim, establish:
+
+> For the exact audited source snapshot, every supported compilation
+> configuration, every valid in-scope use in a context satisfying all
+> out-of-scope safety obligations preserves freedom from Rust undefined behavior
+> under the documented Rust abstract semantics, and every mandatory in-scope
+> documented postcondition holds, assuming only the explicitly recorded trusted
+> computing base (TCB).
+
+Interpret valid use as follows:
+
+- For a safe API, quantify over every well-typed safe use. Impose no hidden
+  safety precondition.
+- For an unsafe API, quantify over every use satisfying all documented initial,
+  ongoing, and terminal safety obligations.
+- For a binary or other entrypoint, quantify over executions satisfying the
+  explicitly recorded deployment assumptions. Do not transfer those
+  assumptions silently to a safe library API.
+
+Prove every documented postcondition of each unsafe API in scope and every
+documented guarantee consumed by an in-scope soundness proof. Include broader
+safe-API robustness only when the user or audit scope requests it.
+
+Prove source-level Rust soundness first. State claims about a particular
+compiler backend, binary, platform, security property, probability, or
+deployment separately with their additional premises.
+
+## Use Only Applicable Premises
+
+- Bottom out Rust-language and standard-library facts in exact applicable text
+  from versioned Rust Reference or standard-library documentation.
+- Quote and link the smallest sufficient set of passages whose propositions,
+  together with justified inference steps, entail the fact. Open each citation
+  and verify its wording, qualifications, version, and scope.
+- Attach an applicability domain to every claim and premise, whether stated
+  locally or inherited from an identified project policy or canonical entry. A
+  derivation proves only the cases covered by all premises it consumes.
+- Apply a guarantee documented for an older Rust release to a later stable
+  release only when an exact applicable Rust backwards-compatibility
+  commitment preserves that exact proposition throughout the later release's
+  relevant domain. An API's stability badge does not by itself preserve every
+  behavioral statement in its current documentation. Record a
+  non-authoritative compatibility premise explicitly in the TCB. Never infer
+  an earlier-version guarantee merely from later documentation.
+- Do not promote this skill, the Rustonomicon, Unsafe Code Guidelines, RFCs,
+  blogs, issue discussions, implementation behavior, Miri, or common practice
+  to Rust axioms. Use them to discover risks and authoritative text, or record
+  the exact additional proposition as a TCB assumption.
+- Trust a deliberately selected safe dependency API to behave as documented
+  only when that exact trust is explicit in the TCB. Do not extend this
+  exception to caller-controlled safe code, callbacks, values, or safe trait
+  implementations.
+- Audit a third-party unsafe API through to admissible premises or record its
+  exact implementation and contract as an additional TCB assumption.
+
+When no admissible direct or derived proof can be completed because
+authoritative documentation is ambiguous or insufficient, identify the
+smallest missing proposition. Do not repair it with intuition. Report a
+documentation gap and suggest an upstream improvement when appropriate.
+
+## Compose Proofs Locally and Literally
+
+- Identify the controlling contract independently of the existing safety
+  comment. Distinguish normative contract text from examples, rationale,
+  implementation comments, and inferred design intent.
+- Read the controlling contract according to its actual text. Decompose every
+  applicable conjunction, implication, quantifier, temporal clause,
+  precondition, and postcondition into separately reviewable obligations. Do
+  not replace a literal requirement with an operationally similar property.
+  Give every normative clause a disposition even when no known consumer uses
+  it.
+- Reify every fact used nonlocally as a named contract or invariant carried by a
+  type, field, function boundary, guard, typestate, lock, token, or other
+  locally checkable mechanism. A function contract about global state is an
+  acceptable degenerate case.
+- Prove that each state transition establishes, preserves, transfers,
+  deliberately suspends under an explicit obligation, or discharges every
+  applicable invariant. At each consumer, prove that the current invariant
+  entails the exact needed precondition.
+- Trace dataflow across calls and time rather than limiting review to lexical
+  unsafe blocks. Account for every producer, transition, and consumer.
+- For new code, place invariant-bearing representation in the smallest
+  practical leaf module, keep safely accessible representation fields private
+  to it, and treat safe code outside that module—including the rest of the same
+  crate—as untrusted.
+
+## Follow the Proof Workflow
+
+1. **Frame the claim.** Record the artifact identity, exact scope, valid uses or
+   executions, Rust and dependency versions, supported configuration set,
+   mandatory postconditions, TCB, exclusions, and whether design alternatives
+   are requested.
+2. **Inventory the surface.** Enumerate every in-scope safe and unsafe API
+   surface, obligation site, invariant producer/transition/consumer, and
+   generated or expanded artifact across the supported set.
+3. **State every obligation.** Obtain each controlling contract, decompose it
+   literally, and state the exact proposition and applicability to prove.
+4. **Construct the derivation.** Derive every conjunct from checked local facts,
+   named invariants, applicable authoritative axioms, tool-derived theorems, or
+   explicit TCB entries. Unfold definitions and seek indirect multi-premise
+   derivations; absence of one direct sentence is not itself a documentation
+   gap. Justify every intermediate inference.
+5. **Close composition.** Ensure every literal contract clause and safe surface
+   has a disposition, every premise consumed by unsafe code has an admissible
+   source, and every supported configuration region is proved by an abstract
+   argument or exhaustive partition. Try to falsify the contract reading,
+   inference chain, and coverage before concluding `PROVED`.
+6. **Report exactly.** Keep unresolved obligations visible and state the
+   smallest missing implication. Record proofs, TCB, coverage, findings,
+   postcondition failures, documentation gaps, and residual scope without
+   optimism.
+
+Do not require a concrete UB counterexample to reject an incomplete proof. A
+missing, ambiguous, circular, or inapplicable derivation is sufficient for
+`UNPROVED`.
+
+## Write and Review Proof-Grade Documentation
+
+Read [proof-obligations.md](references/proof-obligations.md) before authoring or
+reviewing an unsafe contract, invariant, `SAFETY` comment, or local proof.
+
+Keep each proof adjacent to the smallest cohesive unsafe operation or assertion.
+State the exact operation and its preconditions, cite checked facts and named
+invariants, show the derivation, and prove resulting postconditions and
+invariant state on every applicable exit.
+
+When existing code can be validated only by reconstructing a material
+derivation absent from its safety comment, do not accept it silently. Include
+the reconstructed derivation—or the smallest missing portion—in the review,
+with its citations and applicability. Classify implementation correctness
+separately from proof-documentation quality. If changes are authorized, improve
+the adjacent proof; otherwise provide proposed wording. Do not use a
+reconstructed implementation proof to invent or strengthen a caller-facing
+contract retroactively.
+
+## Close API and Configuration Boundaries
+
+Read
+[api-boundaries-and-evolution.md](references/api-boundaries-and-evolution.md)
+for fields, constructors, methods, traits, sealing, macros, public or hidden
+APIs, robustness, or contract evolution.
+
+Apply this mandatory safe-surface checklist: public fields, constructors, safe
+methods, safe trait methods, and macro-generated APIs all count as safe API
+surfaces. Include language-reachable `#[doc(hidden)]` safe items for soundness
+even when excluded from documentation or compatibility promises.
+
+Treat caller-provided safe code as adversarial within the behaviors permitted
+by safe Rust and its types. Seal a trait or make it unsafe when soundness
+requires an unenforced implementer behavior.
+
+Read
+[configurations-and-generated-code.md](references/configurations-and-generated-code.md)
+for every full audit and whenever conditional compilation, targets, generated
+code, FFI, assembly, SIMD, allocators, linking, or build tooling is relevant.
+Every supported combination of compilation options that can ship downstream
+must be sound. Use parametric proofs or exhaustive partitions when literal
+enumeration would explode; do not substitute a tested sample.
+
+## Evaluate Trust and Evidence
+
+Read [tcb-and-evidence.md](references/tcb-and-evidence.md) for every full audit
+and whenever a proof uses dependencies, external specifications, tools,
+testing, formal verification, environmental restrictions, or cryptographic or
+probabilistic assumptions.
+
+Judge evidence by the exact proposition it establishes, its artifact and model,
+its quantified domain and bounds, its premises, and its residual trust—not by a
+label such as testing, static analysis, model checking, or formal verification.
+
+## Design for Provability When Requested
+
+Read [abstraction-design.md](references/abstraction-design.md) when the user asks
+to design, refactor, or reconsider an unsafe abstraction, or when authoring a
+new unsafe abstraction.
+
+Judge existing code under its current source and controlling contract. Inferred
+intent or a preferable model may guide a separate proposal but may not narrow,
+reinterpret, or discharge a current obligation. Treat implemented changes as a
+new artifact and audit them anew.
+
+## Use Exact Verdicts
+
+Read [audit-reporting.md](references/audit-reporting.md) before delivering a
+persistent or full audit.
+
+- **PROVED:** Every obligation for the exact named claim is discharged over its
+  complete applicability, relative to the stated TCB.
+- **UNPROVED:** At least one required derivation, premise, applicability or
+  coverage argument, postcondition proof, or citation is missing, ambiguous,
+  circular, or unverifiable.
+- **UNSOUND:** A valid use or in-scope execution is proved to reach undefined
+  behavior.
+- **CONTRACT-BROKEN:** A documented postcondition is proved false even though
+  undefined behavior need not occur.
+
+Apply verdicts separately to soundness, documented postconditions, and
+conditional application claims. State exact scope, applicability, and TCB
+beside every verdict. Never substitute “looks sound,” “probably sound,” or test
+success.
+
+For a persistent audit, complete:
+
+- [tcb-audit-log-template.md](assets/tcb-audit-log-template.md)
+- [unsafe-code-audit-report-template.md](assets/unsafe-code-audit-report-template.md)
+
+For an inline review, provide the equivalent material compactly. Reuse an
+existing canonical project log rather than creating a competing trust model.
diff --git a/skills/unsafe-rust/agents/openai.yaml b/skills/unsafe-rust/agents/openai.yaml
new file mode 100644
index 0000000000..0f0ca3e7b1
--- /dev/null
+++ b/skills/unsafe-rust/agents/openai.yaml
@@ -0,0 +1,4 @@
+interface:
+  display_name: "Unsafe Rust Authoring and Audit"
+  short_description: "Prove, audit, and redesign unsafe Rust"
+  default_prompt: "Use $unsafe-rust to author, audit, or redesign this unsafe Rust abstraction and its safety contracts."
diff --git a/skills/unsafe-rust/assets/tcb-audit-log-template.md b/skills/unsafe-rust/assets/tcb-audit-log-template.md
new file mode 100644
index 0000000000..7cfad4e866
--- /dev/null
+++ b/skills/unsafe-rust/assets/tcb-audit-log-template.md
@@ -0,0 +1,101 @@
+# TCB Audit Log: `<project / audit>`
+
+## Identity
+
+- **Log ID/revision:** `<stable ID or digest>`
+- **Audit/report:** `<link or ID>`
+- **Skill revision:** `<unsafe-rust revision>`
+- **Source snapshot:** `<repository + revision/digest>`
+- **Generated artifacts:** `<identities/digests>`
+- **Rust/toolchain scope:** `<versions>`
+- **Supported configuration predicate:** `<definition or link>`
+- **Theorem(s) supported:** `<exact soundness, postcondition, binary, or
+  application claims>`
+- **Owner/reviewer:** `<names or roles>`
+- **Reviewed at:** `<date>`
+
+## Trust Policy
+
+`<State which premises may be admitted, the selected-safe-dependency policy,
+the treatment of third-party unsafe APIs, and what kind of verdict this TCB can
+support.>`
+
+## Entry Index
+
+| ID | Category | Exact trusted proposition | Identity/version | Scope/configurations | Contract channel | Consumers | Disposition | Re-audit trigger |
+|---|---|---|---|---|---|---|---|---|
+| `<AXIOM-...>` | `<category>` | `<one precise proposition>` | `<version/digest>` | `<quantification>` | `<authority/contract>` | `<proof IDs>` | `<accepted/rejected/pending>` | `<event>` |
+
+## Detailed Entries
+
+### `<ID>` — `<short name>`
+
+- **Category:** `<AXIOM / SAFE-DEP / UNSAFE-DEP / EXTERNAL-SPEC /
+  IMPLEMENTATION / TOOL / ENVIRONMENT/DEPLOYMENT / CRYPTO/PROBABILISTIC /
+  OUT-OF-BAND / project category>`
+- **Disposition:** `<accepted / rejected / pending / superseded>`
+- **Exact proposition:** `<the smallest proposition accepted without further
+  in-scope proof>`
+- **Quantification and scope:** `<inputs, executions, versions, targets,
+  configurations, APIs, and time interval>`
+- **Exact identity:** `<document URL + version, package + version/source,
+  revision/digest, binary, model, tool, agreement, or environment>`
+- **Source/contract:** `<narrow link, document section, agreement, audit, or
+  other contract source>`
+- **Relevant quotation:**  
+  > `<minimum exact quotation, when a textual contract supplies the fact>`
+- **Contract relationship:** `<Rust authority / SemVer range / exact pin /
+  Rust backwards-compatibility commitment / in-tree fork / out-of-band
+  agreement / consumer-specific promise / external specification / deployment
+  condition / other>`
+- **Why needed:** `<which proof cannot proceed without this proposition>`
+- **Why admission is permitted:** `<project policy, authorized trust decision,
+  contract relationship, or other basis for accepting rather than proving it>`
+- **Consumers:** `<obligation and proof IDs>`
+- **Verification performed:** `<citation check, source audit, certificate check,
+  artifact digest, configuration check, human review, etc.>`
+- **Residual trusted components:** `<implementation, translation, model, solver,
+  proof checker, foreign system, parties, or none>`
+- **Known limitations:** `<unsupported cases, bounds, ambiguity, expiration, or
+  none>`
+- **Owner/approver:** `<human or role authorized to accept this premise>`
+- **Re-audit trigger:** `<version/configuration/contract/tool/environment change
+  or date>`
+- **Notes:** `<only information necessary to apply or review the entry>`
+
+## Dependency Contract Summary
+
+| Dependency | Safe/unsafe surface | Exact behavior relied upon | Contract relationship | Features/configuration | Implementation audit or TCB entry | Update trigger |
+|---|---|---|---|---|---|---|
+| `<package/source>` | `<surface>` | `<proposition>` | `<SemVer / pin / fork / agreement / other>` | `<scope>` | `<proof or ID>` | `<event>` |
+
+## Rejected or Unresolved Premises
+
+| Proposed ID | Proposition | Reason rejected/unproved | Blocked obligations | Required resolution |
+|---|---|---|---|---|
+| `<ID>` | `<claim>` | `<missing authority/proof>` | `<IDs>` | `<action>` |
+
+## Review Attestation
+
+- [ ] Every consumed entry has an exact proposition rather than a vague trust
+      statement.
+- [ ] No entry merely assumes an in-scope conclusion or trusts code the declared
+      audit scope purports to prove.
+- [ ] Every identity, version, digest, and configuration scope was checked.
+- [ ] Every quotation was opened and verified in context.
+- [ ] Selected safe dependencies are distinguished from caller-controlled code.
+- [ ] Exact pins are used only to freeze identity; every undocumented
+      proposition has an audit, additional contract, or explicit admission.
+- [ ] Every third-party unsafe implementation is recursively audited or
+      explicitly admitted.
+- [ ] Tool-derived facts state their exact theorem and residual TCB.
+- [ ] External, deployment, and probabilistic assumptions qualify the verdict
+      conspicuously.
+- [ ] Every entry has consumers and a re-audit trigger.
+- [ ] Every consumed entry supporting `PROVED` is explicitly accepted; pending,
+      rejected, and superseded entries support no proved claim.
+- [ ] Rejected and unresolved premises appear in the audit findings.
+
+**Reviewer:** `<name/role>`  
+**Review result:** `<accepted / rejected / incomplete>`  
+**Date:** `<date>`
diff --git a/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md b/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md
new file mode 100644
index 0000000000..29e2b10723
--- /dev/null
+++ b/skills/unsafe-rust/assets/unsafe-code-audit-report-template.md
@@ -0,0 +1,207 @@
+# Unsafe Rust Audit: `<project / scope>`
+
+## Claims and Verdicts
+
+- **Soundness claim:** `<exact source-level or binary-level absence-of-UB theorem>`
+- **Soundness verdict:** `<PROVED / UNPROVED / UNSOUND; split by scope or
+  configuration when needed>`
+- **Documented-postcondition claim:** `<exact contracts in scope>`
+- **Documented-postcondition verdict:** `<PROVED / UNPROVED /
+  CONTRACT-BROKEN; split by contract, scope, or configuration when needed>`
+- **Combined mandatory result:** `<PROVED only if every in-scope soundness and
+  mandatory documented-postcondition obligation is proved; otherwise list all
+  applicable component verdicts and finding IDs>`
+- **Conditional application claim:** `<deployment/security/probabilistic theorem,
+  or none>`
+- **Conditional application result:** `<exact qualified result and finding IDs;
+  do not present it as unconditional Rust soundness>`
+- **Scope:** `<APIs/modules/packages/binaries>`
+- **Supported configuration predicate:** `<exact definition or link>`
+- **TCB log:** `<ID/revision/link>`
+- **Skill revision:** `<unsafe-rust revision>`
+- **Qualification:** `<exact conditional assumptions; “none beyond stated TCB”
+  if appropriate>`
+
+## Audited Snapshot
+
+- **Repository/source:** `<URL/path + revision/digest>`
+- **Uncommitted changes:** `<identity or none>`
+- **Generated/expanded artifacts:** `<identities/digests/locations>`
+- **Rust/compiler/stdlib:** `<versions and range>`
+- **Dependencies:** `<lockfile/resolution/source identity>`
+- **Build inputs/tools:** `<relevant versions, environment, generators>`
+- **Prior audit reused:** `<ID/revision or none>`
+- **Auditor/reviewer/date:** `<identity>`
+
+## Contracts in Scope
+
+### Soundness
+
+`<State valid uses/executions and the exact absence-of-UB theorem.>`
+
+### Documented Postconditions
+
+| Contract ID | API/entrypoint | Preconditions | Postconditions | Source/version |
+|---|---|---|---|---|
+| `<CONTRACT-...>` | `<item>` | `<P>` | `<Q>` | `<link/quote location>` |
+
+### Additional Robustness Claims
+
+| Claim ID | Exact proposition | Scope and authority | Result | Evidence/finding |
+|---|---|---|---|---|
+| `<ROBUST-...>` | `<claim>` | `<scope/contract/request>` | `<exact result>` | `<proof/finding IDs>` |
+
+`<Write “none” if no additional robustness claim is in scope.>`
+
+## Boundary and API Coverage
+
+| Surface ID | Item/generated family | Safe/unsafe | Construction/access path | Configuration scope | Contract/proof status |
+|---|---|---|---|---|---|
+| `<API-...>` | `<item>` | `<safe/unsafe>` | `<how reached>` | `<scope>` | `<status/link>` |
+
+Confirm coverage of:
+
+This is a mandatory minimum, not an exhaustive surface list. Apply
+[Enumerate every surface](../references/api-boundaries-and-evolution.md#enumerate-every-surface)
+and record every additional language-reachable surface in the table above.
+
+- [ ] safely accessible representation across the owning-module boundary,
+      including `pub(super)`, `pub(crate)`, ancestor-visible, and generated
+      access;
+- [ ] public fields;
+- [ ] constructors;
+- [ ] safe methods;
+- [ ] safe trait methods and caller-provided implementations;
+- [ ] macros and macro-generated APIs;
+- [ ] reexports and configuration-specific APIs;
+- [ ] language-reachable `#[doc(hidden)]` safe items.
+- [ ] associated items, safe free functions/statics, callbacks, FFI entrypoints,
+      blanket/default/auto-trait behavior, operators, and destruction whenever
+      language-reachable or semantically relevant.
+
+## Invariant Inventory
+
+| Invariant ID | Exact proposition | Owner/boundary | Must hold when | Producers/mutators | Consumers | Status |
+|---|---|---|---|---|---|---|
+| `<INV-...>` | `<predicate>` | `<module/type/field/etc.>` | `<interval>` | `<locations>` | `<locations>` | `<status>` |
+
+## Obligation Ledger
+
+| Obligation ID | Source/API | Exact proposition | Required domain | Premises and their applicability | Covered domain/cases | Proof location | Reviewer | Status |
+|---|---|---|---|---|---|---|---|---|
+| `<OBL-...>` | `<location>` | `<goal>` | `<required applicability>` | `<facts/invariants/TCB + domains>` | `<scope/partition>` | `<link>` | `<identity>` | `<status>` |
+
+## Configuration Closure
+
+- **Supported set:** `<formal/operational definition>`
+- **Discovered axes:** `<features, cfg, targets, architectures, OSes, SIMD,
+  allocators, debug assertions, panic modes, generated output, and other actual
+  axes>`
+- **Coverage proof:** `<parametric argument, exhaustive partition, finite
+  enumeration, generator proof, or combination>`
+- **Generated artifacts:** `<identity/proof>`
+- **Enforced exclusions:** `<how unsupported combinations cannot ship>`
+- **Sampled/tested configurations:** `<list and exact limited evidence provided>`
+- **Uncovered configurations:** `<none or finding IDs>`
+
+## TCB Summary
+
+| Category | Entry IDs | Human disposition | Material limitations |
+|---|---|---|---|
+| `<category>` | `<IDs>` | `<accepted/rejected/pending>` | `<limitations>` |
+
+Full log: `<link/ID>`
+
+## Tool-Derived Evidence
+
+| Proof ID | Proposition and entailment | Artifact/tool/model/options | Quantification and bounds | Non-vacuity and semantic fidelity | Trust, stubs, and residual TCB | Result/certificate | Consumers |
+|---|---|---|---|---|---|---|---|
+| `<TOOL-PROOF-...>` | `<exact theorem and why it implies the obligation>` | `<identities>` | `<scope/bounds/completeness>` | `<reachability + source/model correspondence>` | `<trusted functions/models/components + TCB IDs>` | `<terminal result/link/digest>` | `<obligation IDs>` |
+
+## Findings
+
+### `<FINDING-ID>` — `<short title>`
+
+- **Status/severity:** `<UNPROVED / UNSOUND / CONTRACT-BROKEN / other>`
+- **Implementation classification:** `<verdict/status for the implementation
+  obligation>`
+- **Proof-artifact classification:** `<adequate / deficient / missing / not
+  applicable>`
+- **Affected claim:** `<soundness/postcondition/compatibility/etc.>`
+- **Source/API/configuration:** `<exact scope>`
+- **Required proposition:** `<goal>`
+- **Existing proof or behavior:** `<what was claimed/implemented>`
+- **Reconstructed derivation:** `<material proof missing from the reviewed
+  artifact, with citations/applicability; or none>`
+- **Proposed proof-artifact repair:** `<replacement comment/canonical proof, or
+  none>`
+- **Defect:** `<smallest missing, false, circular, or unsupported implication>`
+- **Authority/TCB involved:** `<citations/IDs>`
+- **Counterexample:** `<valid UB/postcondition witness, or “not required/not
+  established”>`
+- **Affected producers/consumers:** `<IDs/locations>`
+- **Required resolution:** `<minimum proof, contract, implementation, privacy,
+  configuration, or TCB change>`
+- **Compatibility impact:** `<SemVer/contract implications>`
+- **Re-audit scope:** `<what must be revisited>`
+
+## Abstraction Design (Optional)
+
+`<Omit unless design or redesign was requested. Preserve the current-artifact
+findings above unchanged.>`
+
+- **Required behavior and constraints:** `<exact consumer propositions,
+  compatibility commitments, support domain, and authorized changes>`
+- **Current literal result:** `<scoped finding/verdict, unchanged by proposal>`
+- **Recommended candidate:** `<proposed contract, representation, and boundary>`
+- **Proof simplification:** `<obligations and TCB premises eliminated,
+  localized, or retained>`
+- **Behavior delta:** `<behavior or guarantees added, lost, or unchanged>`
+- **Compatibility and migration:** `<contract delta, affected parties, plan>`
+- **Fresh-audit status:** `<not implemented / new snapshot + separate verdict>`
+
+## Documentation and Skill Gaps
+
+### Authoritative Rust Documentation
+
+| Gap ID | Missing/ambiguous proposition | Attempted authoritative sources | Blocked obligations | Suggested upstream report |
+|---|---|---|---|---|
+| `<DOC-GAP-...>` | `<proposition>` | `<links>` | `<IDs>` | `<action>` |
+
+### Skill Guidance
+
+| Gap ID | Omission or ambiguity | Audit impact | Proposed maintainer follow-up |
+|---|---|---|---|
+| `<SKILL-GAP-...>` | `<gap>` | `<impact>` | `<action>` |
+
+## Residual and Excluded Scope
+
+`<List every inaccessible, unaudited, unsupported, conditionally proved, or
+explicitly excluded region. Explain enforcement of exclusions.>`
+
+## Re-audit Triggers
+
+- `<source or contract changes>`
+- `<configuration/support changes>`
+- `<Rust or authoritative documentation changes>`
+- `<dependency, generator, tool, TCB, environment, or agreement changes>`
+- `<new incident or discovered obligation>`
+
+## Final Attestation
+
+- [ ] Every in-scope obligation has a status.
+- [ ] Every `PROVED` obligation has a complete checked derivation.
+- [ ] Every material derivation reconstructed during review is exposed with its
+      applicability, and deficient proof artifacts are reported separately.
+- [ ] Every supported configuration is covered by proof.
+- [ ] Every consumed citation and TCB entry was independently verified.
+- [ ] Every consumed TCB entry supporting `PROVED` has an accepted human
+      disposition.
+- [ ] Every mandatory documented postcondition was reviewed in addition to UB
+      freedom.
+- [ ] Residual scope and conditional assumptions are conspicuous.
+- [ ] The final verdict does not rely on lack of a counterexample or clean tests.
+
+**Auditor:** `<identity>`  
+**Independent reviewer (if performed):** `<identity or not performed>`  
+**Date:** `<date>`
diff --git a/skills/unsafe-rust/references/abstraction-design.md b/skills/unsafe-rust/references/abstraction-design.md
new file mode 100644
index 0000000000..b477d8022d
--- /dev/null
+++ b/skills/unsafe-rust/references/abstraction-design.md
@@ -0,0 +1,164 @@
+# Designing Unsafe Abstractions for Provability
+
+## Contents
+
+- [Keep verification and design separate](#keep-verification-and-design-separate)
+- [Establish design requirements](#establish-design-requirements)
+- [Extract the minimum capability](#extract-the-minimum-capability)
+- [Generate proof-oriented candidates](#generate-proof-oriented-candidates)
+- [Prove and compare candidates](#prove-and-compare-candidates)
+- [Report the result](#report-the-result)
+
+## Keep Verification and Design Separate
+
+Use this process when the user asks to design or redesign an unsafe abstraction,
+or when authoring a new unsafe abstraction. Do not run it automatically during
+an immutable acceptance audit unless the user requests design advice.
+
+Judge existing code under its exact current source and controlling contracts.
+Inferred intent, a proposed narrower contract, or an easier-to-prove
+representation may not:
+
+- reinterpret or weaken a current obligation;
+- discharge a premise of the current implementation;
+- erase or downgrade a current finding; or
+- justify accepting the current artifact.
+
+Keep conclusions about the current artifact logically independent of every
+candidate design. A proposal describes a possible future artifact; it has no
+`PROVED` verdict. After implementation, identify the new snapshot and apply the
+ordinary unsafe-Rust proof workflow anew.
+
+Preserve at least the scoped current finding that motivates the redesign. Do
+not expand that step into a whole-crate audit unless the requested audit scope
+requires it.
+
+For greenfield work, no current-artifact verdict is necessary. State the design
+requirements, construct the candidate, and prove the implemented artifact.
+
+## Establish Design Requirements
+
+Record the constraints that the abstraction must satisfy:
+
+- required externally observable behavior and mandatory postconditions;
+- current public contracts and compatibility commitments that must remain;
+- exact propositions required by relevant consumers;
+- supported Rust versions, targets, features, and configurations;
+- representation, performance, interoperability, or integration constraints;
+  and
+- which semantic or compatibility changes the user has authorized.
+
+Use each source only for the proposition it actually establishes. User
+requirements can determine desired behavior. Current contracts determine
+current obligations. Call sites, tests, names, comments, history, and
+implementation structure may suggest intent or establish local source facts,
+but an inference about intent is not a Rust semantic premise and does not prove
+implementation correctness.
+
+Known internal consumers do not exhaust the consumers of a public API. Treat
+the published contract as a required constraint unless an applicable contract
+channel and the user authorize changing it. Surface material ambiguity when
+different interpretations would change the public contract, support policy, or
+compatibility result.
+
+## Extract the Minimum Capability
+
+For each required behavior, state the exact semantic proposition consumers
+need. Separate properties that the current abstraction may have bundled, such
+as:
+
+- nominal identity from an operational capability;
+- layout from validity, initialization, provenance, alignment, or aliasing;
+- metadata from memory projection;
+- ownership from access permission;
+- one-time establishment from an ongoing invariant;
+- safe caller behavior from an unsafe implementer promise; and
+- behavior common to many types from one exceptional case.
+
+Identify where each proposition is established, carried, consumed, and
+discharged. Prefer a design in which types, validation, privacy, sealing,
+typestate, guards, or other locally checkable mechanisms enforce the fact.
+
+Do not make a proof easier merely by transferring an unnecessary or hidden
+obligation to callers. Every remaining unsafe caller or implementer obligation
+must be explicit, sufficient, and justified by a need the implementation cannot
+enforce safely.
+
+## Generate Proof-Oriented Candidates
+
+Consider the smallest transformations that remove the unsupported premise:
+
+- eliminate an unnecessary unsafe operation, impl, configuration, or promise;
+- validate the required property before the unsafe operation;
+- narrow an API or implementation to the cases actually supported;
+- reuse a safe or already-proved primitive whose contract matches exactly;
+- specialize a one-off case instead of inventing a generic abstraction;
+- split independent capabilities or invariant dimensions;
+- seal an implementer boundary or move representation behind a smaller module;
+  or
+- introduce a new reusable abstraction only when demonstrated consumers share
+  the same semantic capability.
+
+For example, if one contract claims both nominal field reflection and pointer
+projection while some consumers require only projection, consider separating
+those capabilities rather than inventing a nominal field. This is a design
+prompt, not a Rust fact; prove the resulting contracts normally.
+
+Do not pad the output with cosmetic or strictly dominated alternatives. When
+requirements are ambiguous or viable candidates make materially incomparable
+tradeoffs, present the consequential choice instead of choosing silently.
+
+## Prove and Compare Candidates
+
+For each viable candidate, state:
+
+- exact safe and unsafe contracts;
+- representation and named invariants;
+- how every required consumer proposition is supplied;
+- where each remaining obligation is enforced;
+- authoritative axioms, dependency contracts, and TCB entries required;
+- supported applicability domain;
+- unresolved proof obligations; and
+- behavior, compatibility, migration, and re-audit consequences.
+
+Construct a conditional proof plan before implementation. After implementation,
+prove the exact source rather than the design sketch.
+
+Reject candidates that fail required behavior, proof closure, supported-domain
+coverage, or binding compatibility constraints. Among the remainder, prefer a
+candidate that preserves required behavior while reducing one or more of:
+
+- unsafe surface exposed to callers or implementers;
+- strength or number of unsupported premises;
+- invariant access region, lifetime, and fan-out;
+- TCB size;
+- coupling between independent capabilities;
+- version- or configuration-specific proof branches;
+- accidental representation commitments; and
+- genericity without demonstrated reuse.
+
+Also account for authorized implementation, performance, and migration costs.
+Do not collapse incomparable tradeoffs into an invented score, and do not
+prefer a small textual diff that silently weakens a relied-upon contract.
+
+Apply
+[Evolve contracts deliberately](api-boundaries-and-evolution.md#evolve-contracts-deliberately)
+to every candidate contract change.
+
+## Report the Result
+
+Keep these outputs distinct whenever they apply:
+
+1. **Current artifact:** Exact findings and verdict under the current contract.
+2. **Design requirements:** Required behavior, constraints, consumer
+   propositions, and unresolved intent.
+3. **Candidate design:** Exact proposed contracts, invariant model, proof plan,
+   and remaining premises.
+4. **Compatibility and migration:** Behavior gained or lost, affected callers
+   and implementers, contract channel, and re-audit scope.
+5. **Recommendation:** The preferred candidate and any human decision required.
+6. **Post-change audit:** A separate result for an implemented new snapshot.
+
+In review-only work, provide counterfactual advice without modifying source. In
+authoring work, update implementation, contracts, local proofs, TCB entries,
+and affected downstream proofs together.
diff --git a/skills/unsafe-rust/references/api-boundaries-and-evolution.md b/skills/unsafe-rust/references/api-boundaries-and-evolution.md
new file mode 100644
index 0000000000..7c3fd35dd2
--- /dev/null
+++ b/skills/unsafe-rust/references/api-boundaries-and-evolution.md
@@ -0,0 +1,285 @@
+# API Boundaries, Invariants, and Contract Evolution
+
+## Contents
+
+- [Enumerate every surface](#enumerate-every-surface)
+- [Place the safety boundary](#place-the-safety-boundary)
+- [Use module privacy](#use-module-privacy)
+- [Handle unsafe fields](#handle-unsafe-fields)
+- [Audit traits and sealing](#audit-traits-and-sealing)
+- [Audit macros and hidden APIs](#audit-macros-and-hidden-apis)
+- [Distinguish selected dependencies from caller code](#distinguish-selected-dependencies-from-caller-code)
+- [Prove documented behavior](#prove-documented-behavior)
+- [Evolve contracts deliberately](#evolve-contracts-deliberately)
+
+## Enumerate Every Surface
+
+For soundness, enumerate every language-reachable way untrusted safe code can
+construct, obtain, observe, mutate, replace, borrow, move, copy, drop, implement,
+or invoke the abstraction.
+
+Apply this checklist explicitly:
+
+- public fields;
+- constructors, including literals, constants, defaults, conversions,
+  deserialization, builders, and generated constructors;
+- safe inherent and extension methods;
+- safe trait methods, blanket implementations, default methods, trait objects,
+  and auto traits;
+- public associated types and constants where their choices affect unsafe code;
+- safe free functions and statics;
+- indexing, dereference, iteration, operators, formatting, cloning, comparison,
+  hashing, panic, and destruction behavior when implemented;
+- exported declarative macros, procedural macros, derives, attributes, and APIs
+  produced by them;
+- reexports and feature- or target-dependent public items;
+- callbacks and user-provided implementations invoked internally;
+- FFI entrypoints callable without a Rust-side unsafe obligation;
+- language-reachable `#[doc(hidden)]` items.
+
+This is an advisory discovery list, not an exhaustive statement of Rust's
+semantics. Inspect the exact source, expansions, metadata, and applicable
+authoritative documentation for additional surfaces.
+
+For each safe surface, prove that every behavior available to well-typed safe
+code preserves soundness. For each unsafe surface, prove that its complete
+documented contract is sufficient and that its implementation establishes all
+documented postconditions for every valid use.
+
+Determine the controlling contract from the actual published or otherwise
+applicable normative text. Examples, rationale, tests, names, existing safety
+comments, and inferred design intent may aid discovery but may not narrow or
+replace that contract.
+
+## Place the Safety Boundary
+
+Mark an operation unsafe when callers or implementers must establish a
+soundness-critical proposition that the implementation cannot establish from
+enforced types, checked state, module-owned invariants, and deliberately trusted
+dependencies.
+
+Do not expose a safe API with a prose-only safety precondition. Documentation
+cannot make a well-typed safe use invalid for the purpose of soundness.
+
+Conversely, do not move an obligation to callers merely because doing so is
+convenient. A safe wrapper may discharge an unsafe callee's requirements with
+validation, construction, privacy, typestate, synchronization, or a local proof.
+
+Treat each unsafe declaration or call as a contract boundary. An unsafe helper
+can propagate an obligation through fields and later calls without immediately
+performing an operation that exhibits undefined behavior. Follow the obligation
+through the dataflow until it is discharged.
+
+An `unsafe impl` is an assertion that the implementation satisfies the unsafe
+trait's contract. Prove that assertion and every method-level obligation.
+
+For FFI declarations, distinguish the declaration-time assertion that the
+foreign contract is correct from each call's preconditions and from the foreign
+implementation's behavior. Record external ABI and implementation trust
+explicitly.
+
+## Use Module Privacy
+
+For new invariant-bearing representations:
+
+1. Put the representation and all safely accessible fields in the smallest
+   practical leaf module.
+2. Keep those fields private to that module.
+3. Make all code outside the module—including parents, siblings, cousins, and
+   the rest of the same crate—use checked safe APIs or documented unsafe APIs.
+4. Treat each operation inside the module that can affect the invariant as a
+   proof site.
+
+Do not use `pub(super)`, `pub(crate)`, or another broad safe visibility merely
+because current same-crate code is trusted socially. Such visibility expands
+the region in which safe edits can silently violate the invariant and makes
+human review materially harder.
+
+Existing crates need not be rejected solely for violating this authoring
+discipline. Compute and audit the actual Rust visibility region, including
+fields in ancestors or descendants that the code can access and all code that
+can access the representation. Report broad safe visibility as proof-surface
+debt.
+
+Represent every distant fact by a named invariant or contract that each producer
+preserves and each consumer can use locally.
+
+## Handle Unsafe Fields
+
+When the exact audited Rust version supplies compiler-enforced unsafe fields, a
+properly declared unsafe field is an explicit unsafe API boundary. It may have
+any intentional visibility, analogously to an unsafe function, because untrusted
+safe code cannot perform the gated uses without accepting its documented
+obligations.
+
+Require field documentation to make the obligations for all applicable
+operations derivable, including:
+
+- initialization and replacement;
+- reads, copies, and moves;
+- shared and mutable borrows;
+- pattern matching, destructuring, aggregate update, and whole-value operations;
+- writes through direct access or an escaped capability;
+- transfer or suspension of the enclosing invariant;
+- the state required before control returns to untrusted safe code.
+
+Audit the exact compiler version's enforcement rather than assuming a proposed
+or future design. Separately prove every implicit safe action not gated by field
+projection, especially destruction and compiler- or derive-supplied trait
+behavior. An unsafe modifier does not relax the language validity invariant of
+the field's Rust type and does not make arbitrary drop glue conditional.
+
+When authoritative Reference or standard-library text does not specify the
+feature sufficiently, record the exact semantics relied upon as a documentation
+gap and explicit TCB premise. An RFC or current implementation may explain the
+intent but is not a Rust axiom under this skill's authority policy.
+
+## Audit Traits and Sealing
+
+Treat every safe trait implementation supplied by a caller as adversarial safe
+code. Unsafe code may rely only on facts enforced by Rust's types and semantics,
+module-owned state, or explicit TCB entries—not on a caller faithfully
+implementing behavioral prose.
+
+If unsafe code requires an implementer to uphold a soundness-critical
+obligation, use one of these structures:
+
+- make the trait unsafe and document the complete implementer contract;
+- seal the trait so only deliberately controlled implementations are possible;
+- validate the needed property before unsafe use;
+- redesign the representation or boundary so the property follows locally.
+
+Prove that sealing is effective under Rust privacy and name resolution for every
+supported configuration and macro expansion. A documentation claim,
+`#[doc(hidden)]`, obscure path, or conventional “sealed” name does not by itself
+prevent downstream implementations.
+
+For an unsafe trait:
+
+- state representation and behavioral obligations at the trait and method
+  levels;
+- prove every in-scope `unsafe impl`;
+- ensure safe methods remain sound for every valid implementation;
+- ensure generic unsafe consumers rely on no stronger fact than the contract;
+- audit associated types, constants, default methods, specialization, trait
+  objects, auto traits, negative impls, and generated impls when applicable.
+
+For a sealed safe trait, selected implementations may be audited as controlled
+code, but downstream safe callers remain adversarial. Recheck sealing whenever
+visibility, reexports, macros, or configuration changes.
+
+## Audit Macros and Hidden APIs
+
+Classify a macro invocation by the obligations rustc actually enforces for the
+expanded use, not merely by the absence or presence of `unsafe` in the invocation
+tokens. A macro can be constructed so that expansion succeeds only in an unsafe
+context. If no caller-side unsafe obligation is compiler-enforced, treat the
+macro as a safe API and prove every accepted safe invocation sound.
+
+Auditing only handwritten macro or proc-macro source is insufficient when sound
+output depends on:
+
+- caller tokens, types, paths, hygiene, spans, or name resolution;
+- `cfg`, features, target facts, environment, or build-script data;
+- generated identifiers, item visibility, attributes, or impl selection;
+- compiler expansion order or version;
+- downstream code into which the macro expands.
+
+Inspect expansions to discover API and caller obligations. Then apply
+[Audit generated and expanded code](configurations-and-generated-code.md#audit-generated-and-expanded-code)
+to prove closure over every supported accepted input, output, and
+configuration. Include generated public APIs in the same safe/unsafe surface
+audit as handwritten items.
+
+Treat `#[doc(hidden)]` as a documentation and compatibility signal only to the
+extent promised by the project. It does not create Rust privacy. A
+language-reachable safe hidden item must remain sound for direct safe use and
+may not hide a safety precondition. The project may separately exclude its
+behavior or continued existence from SemVer promises.
+
+## Distinguish Selected Dependencies From Caller Code
+
+A deliberately selected dependency is code whose use and version the project
+author intentionally chose. A function argument, callback, generic parameter,
+trait object, plugin, implementation of a safe trait, or downstream macro input
+is caller-controlled even when its type originates in a selected dependency.
+
+Apply the selected-safe-dependency exception only to the deliberately chosen
+implementation and documented API behavior, never to behavior chosen by the
+caller. Determine whether reexports, dependency-defined traits, feature
+unification, or plugins move a surface across that boundary.
+
+For exact identity, contract channels, safe versus unsafe dependency trust, and
+update triggers, apply
+[Record dependency contracts](tcb-and-evidence.md#record-dependency-contracts).
+
+## Prove Documented Behavior
+
+Soundness is the minimum universal property. The mandatory postcondition scope
+includes every documented postcondition of an unsafe API in scope and every
+guarantee consumed by an in-scope soundness proof. Prove broader safe-API
+behavior only when the user or audit explicitly places it in scope.
+
+At minimum, an unsafe API implementation is responsible for both:
+
+1. avoiding undefined behavior for every valid use; and
+2. establishing every documented postcondition when its safety preconditions
+   and other documented conditions are met.
+
+Do not label a postcondition failure “sound” and stop. Report it separately as
+`CONTRACT-BROKEN`, while also determining whether downstream unsafe code can
+turn the broken guarantee into unsoundness.
+
+Do not invent a universal standard for undocumented robustness. State the exact
+behavioral claim being reviewed: panic freedom, determinism, resource bounds,
+constant time, atomicity, rollback, leak freedom, progress, or another property.
+Record its authority and scope separately from Rust soundness.
+
+## Evolve Contracts Deliberately
+
+Treat safety documentation and documented postconditions as compatibility
+contracts, not comments that can be edited independently of code.
+
+Analyze every change by provider and consumer:
+
+- Strengthening a caller precondition invalidates previously valid calls.
+- Weakening a caller precondition admits more calls and increases the
+  implementation's proof burden.
+- Weakening a provider postcondition invalidates existing caller reasoning.
+- Strengthening a provider postcondition increases what callers may rely upon.
+- Strengthening an unsafe trait implementer's obligation can invalidate existing
+  impls.
+- Strengthening guarantees required from trait implementations can likewise
+  invalidate existing impls even when it benefits trait consumers.
+- Weakening guarantees supplied through a trait can invalidate generic
+  consumers.
+
+Under a conventional SemVer contract, invalidating existing valid callers,
+implementers, or documented reasoning is normally breaking even when Rust type
+signatures do not change. Determine and record the actual project's
+compatibility policy rather than treating SemVer folklore as an axiom.
+
+An exact pin freezes identity but does not authorize an undocumented semantic
+claim. A fork, out-of-band agreement, or consumer-specific promise may supply an
+additional contract for its exact recorded scope; otherwise audit or explicitly
+admit the implementation proposition. Update the TCB and repeat affected proofs
+before changing any identity, contract, or agreement.
+
+When the supported Rust range changes, apply
+[Qualify applicability](proof-obligations.md#qualify-applicability), update any
+compatibility premises in the TCB, and re-audit every proof whose documentation,
+edition, target, feature, configuration, or implementation claim may differ.
+
+For every contract change, search callers, implementers, safety comments, TCB
+entries, generated output, and downstream-facing documentation for proofs that
+consume the changed proposition.
+
+Changing safety prose does not retroactively narrow valid uses of an already
+published version. If that version's implementation failed its published
+contract, it had a soundness or contract defect. Treat the correction as
+remediation requiring compatibility analysis, affected-version disclosure, and
+review of downstream proofs—not as proof that the old implementation was sound.
+
+When redesign is authorized, apply
+[Designing Unsafe Abstractions for Provability](abstraction-design.md) without
+letting the proposed contract alter the verdict for the current artifact.
diff --git a/skills/unsafe-rust/references/audit-reporting.md b/skills/unsafe-rust/references/audit-reporting.md
new file mode 100644
index 0000000000..57ec65d6ed
--- /dev/null
+++ b/skills/unsafe-rust/references/audit-reporting.md
@@ -0,0 +1,196 @@
+# Audit Execution and Reporting
+
+## Contents
+
+- [Freeze the audit claim](#freeze-the-audit-claim)
+- [Maintain an obligation ledger](#maintain-an-obligation-ledger)
+- [Aggregate verdicts](#aggregate-verdicts)
+- [Write actionable findings](#write-actionable-findings)
+- [Deliver a complete report](#deliver-a-complete-report)
+- [Preserve and update the audit](#preserve-and-update-the-audit)
+
+## Freeze the Audit Claim
+
+Before reviewing proofs, record:
+
+- exact repository, source revision/digest, workspace packages, generated
+  artifacts, and relevant uncommitted changes;
+- Rust/compiler/standard-library versions and supported range;
+- dependency resolution and relevant source identities;
+- supported configurations and exclusions;
+- API, module, binary, or whole-project scope;
+- soundness theorem and documented postconditions in scope;
+- TCB log identity/revision;
+- prior audit results being reused;
+- known inaccessible, unsupported, or intentionally excluded regions.
+
+Do not issue a whole-crate verdict for a diff, one feature, one target, or one
+unsafe block. State the narrow result actually established.
+
+If the task is review-only, report findings and proposed remedies without
+silently changing code. If the task includes authoring or fixing, update the
+proof artifacts and contracts together with the implementation.
+
+## Maintain an Obligation Ledger
+
+Track every in-scope obligation sufficiently to detect omissions. The ledger may
+be a table, issue list, annotated source, or another reviewable form. Ensure it
+provides complete location-by-location coverage of producers, transitions,
+consumers, and proof sites.
+
+For each obligation, record:
+
+- stable identifier and source location/API;
+- exact proposition to prove;
+- operation, contract, invariant, or postcondition that requires it;
+- required applicability domain;
+- supporting local facts, invariant clauses, axioms, and TCB entries, with the
+  applicability of each premise;
+- domain actually covered by the derivation and any case partition;
+- proof location;
+- reviewer verification;
+- status and finding link.
+
+Include obligations created by:
+
+- unsafe operations and unsafe API calls;
+- unsafe functions, traits, impls, fields, attributes, declarations, macros, and
+  generated code as applicable;
+- construction, mutation, suspension, consumption, and destruction of
+  invariant-bearing state;
+- safe APIs backed by unsafe code;
+- every documented postcondition of each in-scope unsafe API, and every
+  documented guarantee consumed by later unsafe code;
+- FFI, assembly, allocators, concurrency, target/configuration selection, and
+  external contracts;
+- generated public APIs and code shipped downstream.
+
+This is a discovery aid, not an exhaustive semantic taxonomy. Add whatever the
+actual code and authoritative contracts require.
+
+The ledger complements rather than replaces the proof workflow in
+[proof-obligations.md](proof-obligations.md). Review surrounding safe code and
+follow changed propositions to every consumer; compiler-marked unsafe locations
+and textual diffs are only discovery starting points.
+
+## Aggregate Verdicts
+
+Use the verdict definitions in `SKILL.md` for individual obligations and the
+final in-scope claim.
+
+Report multiple statuses when applicable. For example, soundness can be
+`PROVED` while documented postconditions are `CONTRACT-BROKEN`, or one path can
+be `UNSOUND` while a different configuration remains `UNPROVED`. Issue `PROVED`
+for the combined default claim only when every in-scope soundness and
+documented-postcondition obligation is proved.
+
+Place qualifications in the theorem, not in vague prose. Use:
+
+> PROVED for `<scope>` under `<supported-set predicate>`, relative to TCB
+> `<revision>`.
+
+For a deployment, external, or cryptographic premise, name the exact entry and
+state whether the result is a conditional source, binary, or application claim.
+
+Never use “looks sound,” “no issues found,” “probably safe,” “Miri-clean,”
+“battle-tested,” or “tests pass” as a verdict.
+
+## Write Actionable Findings
+
+Each finding should contain:
+
+- severity/status and affected theorem;
+- exact source/API/configuration;
+- required proposition;
+- existing claimed proof;
+- any material derivation the reviewer had to reconstruct, with citations and
+  applicability, or the smallest portion still missing;
+- proposed replacement proof text when the reviewed artifact omits that
+  derivation;
+- smallest missing, false, circular, or unsupported implication;
+- authoritative contract or TCB entry involved;
+- whether a valid UB counterexample or postcondition counterexample is known;
+- affected callers, producers, consumers, generated output, and configurations;
+- minimal acceptable resolution;
+- compatibility and re-audit consequences.
+
+Distinguish:
+
+- an implementation defect;
+- insufficient or ambiguous safety documentation;
+- a correct implementation with an invalid local comment;
+- an undocumented TCB assumption;
+- an authoritative Reference/std documentation gap;
+- a skill-guidance gap;
+- a compatibility/robustness defect without established UB.
+
+A successfully reconstructed implementation proof does not erase deficient
+safety documentation. Report the implementation obligation and the proof
+artifact separately, and offer corrected proof text. Reconstruction may not add
+a hidden caller or implementer obligation or create a provider guarantee absent
+from the controlling contract.
+
+Keep every verdict for the current artifact independent of design alternatives.
+If redesign was requested, report proposals and their conditional proof plans
+separately; audit an implemented redesign as a new snapshot.
+
+If authoritative documentation is insufficient, quote the exact missing
+proposition and suggest a narrowly scoped upstream report. If this skill failed
+to route the reviewer to a necessary check, identify a proposed skill issue
+without treating the proposed rule as current authority.
+
+## Deliver a Complete Report
+
+A complete audit report contains:
+
+1. **Claim and verdict:** Exact theorem, status, scope, supported configuration
+   predicate, and TCB identity.
+2. **Snapshot:** Source, generated artifacts, Rust/toolchain, dependency
+   resolution, and relevant build inputs.
+3. **Boundary and API coverage:** Safe and unsafe surfaces crossing the owning
+   module or external API boundary, including restricted-visible fields,
+   constructors, safe methods, safe trait methods, macro-generated APIs, and
+   language-reachable hidden items.
+4. **Invariant inventory:** Index of named local contracts, owners, permitted
+   transitions, and consumers—not an informal global proof.
+5. **Obligation coverage:** Proof sites and status summary; link to detailed
+   proofs/findings rather than duplicating them. Include material reconstructed
+   proofs missing from the reviewed proof artifacts.
+6. **Configuration closure:** Supported-set definition, axes, abstract or
+   enumerative coverage proof, generated artifacts, and enforced exclusions.
+7. **TCB audit log:** Every authoritative or admitted proposition and reviewer
+   disposition.
+8. **Tool-derived evidence:** Exact theorem, artifact/model scope, bounds,
+   result, non-vacuity check, and residual TCB.
+9. **Postcondition/robustness scope:** Documented guarantees proved and any
+   separately requested properties.
+10. **Findings:** `UNPROVED`, `UNSOUND`, `CONTRACT-BROKEN`, documentation gaps,
+   compatibility defects, and maintenance risks.
+11. **Residual scope:** Anything not audited, inaccessible, unsupported, or
+    conditional.
+12. **Review triggers:** Changes that invalidate or require revisiting the
+    result.
+
+Use the bundled report and TCB templates for persistent artifacts. For an inline
+review, provide the same information compactly.
+
+## Preserve and Update the Audit
+
+When a canonical audit or TCB log exists:
+
+- reuse its identifiers and format;
+- verify rather than blindly inherit prior `PROVED` entries;
+- update changed source, contracts, configurations, dependencies, and trust;
+- retain historical identity through version control rather than duplicating a
+  stale snapshot;
+- record the skill revision used for the audit;
+- link proofs and findings to exact source revisions.
+
+Trigger review when code or documentation changes any consumed proposition,
+when supported compilation options expand, when generators or generated output
+change, when dependencies or contract channels change, when authoritative Rust
+documentation changes materially, or when a new incident reveals an omitted
+class of obligation.
+
+A prior successful audit is evidence about its exact snapshot and theorem, not a
+permanent certification of later code.
diff --git a/skills/unsafe-rust/references/configurations-and-generated-code.md b/skills/unsafe-rust/references/configurations-and-generated-code.md
new file mode 100644
index 0000000000..aad7a9a89a
--- /dev/null
+++ b/skills/unsafe-rust/references/configurations-and-generated-code.md
@@ -0,0 +1,270 @@
+# Configuration Closure and Generated Unsafe Code
+
+## Contents
+
+- [Define the supported set](#define-the-supported-set)
+- [Discover configuration axes](#discover-configuration-axes)
+- [Prove every supported combination](#prove-every-supported-combination)
+- [Audit generated and expanded code](#audit-generated-and-expanded-code)
+- [Audit targets, SIMD, and concurrency](#audit-targets-simd-and-concurrency)
+- [Audit allocators, panic modes, and assertions](#audit-allocators-panic-modes-and-assertions)
+- [Audit FFI, assembly, linking, and global symbols](#audit-ffi-assembly-linking-and-global-symbols)
+- [Record configuration coverage](#record-configuration-coverage)
+
+## Define the Supported Set
+
+Write a precise predicate `Supported(configuration)` before claiming full
+soundness. Derive it from published package metadata, documentation, target
+policy, feature declarations, build tooling, compiler support, downstream
+integration agreements, and the artifacts that can actually be shipped.
+
+Include every compilation option combination that downstream users are allowed
+to produce, not merely CI jobs or maintainer-preferred builds. If a compilable
+combination is exposed without a clear exclusion, conservatively treat it as
+supported until the project owner establishes otherwise.
+
+Record:
+
+- source revision and workspace/package selection;
+- Rust toolchain range, edition, standard-library identity, and relevant compiler
+  flags;
+- target triples, target specifications, CPUs, features, ABIs, data layouts, and
+  linkers;
+- Cargo features, dependency feature unification, optional dependencies, and
+  resolver behavior;
+- profiles and code-affecting environment or build inputs;
+- generated artifacts and their generators;
+- explicit exclusions and how compilation or distribution enforces them.
+
+An exclusion written only in an audit report does not constrain downstream
+users. If soundness requires rejecting a combination, enforce and document the
+rejection in the build or API.
+
+## Discover Configuration Axes
+
+Search both handwritten and generated source for all code-selection and
+semantic axes. At minimum, investigate when applicable:
+
+- `cfg` and `cfg_attr`, Cargo features, optional dependencies, and feature
+  unification;
+- target architecture, OS, environment, vendor, family, ABI, endianness, pointer
+  width, alignment, atomic widths, and target capabilities;
+- conditional type definitions, representation/layout attributes, constants,
+  const evaluation, static initialization, and build-time execution;
+- compile-time and runtime SIMD or other target features;
+- debug assertions, overflow checks, optimization, LTO, codegen backend, panic
+  strategy, unwinding, sanitizers, and instrumentation;
+- global and per-operation allocator choices, allocation failure behavior, and
+  custom allocator implementations;
+- thread availability, atomics, permitted interleavings, weak memory behavior,
+  signals, cancellation, and runtime/executor choices;
+- build scripts, procedural and declarative macros, derives, code generators,
+  bindgen output, included files, environment variables, and external tools;
+- FFI implementation, ABI, library version, symbol resolution, static/dynamic
+  linking, linker scripts, link arguments, dynamic loading or plugins, and
+  load-time substitution;
+- inline assembly dialect, registers, options, calling convention, instruction
+  availability, and surrounding compiler assumptions;
+- compiler version, edition, unstable features, bootstrap flags, custom target
+  specifications, and standard-library build;
+- tests/examples/binaries versus library code, `no_std`, host versus target
+  builds, and build-dependency versus runtime-dependency configurations.
+
+This list is intentionally advisory and may be incomplete or become outdated.
+Discover the actual axes from the audited project and authoritative toolchain
+contracts. Add newly discovered axes to the audit and report gaps in this
+reference.
+
+## Prove Every Supported Combination
+
+Every supported combination must be sound. A CI matrix, sample of targets, or
+pairwise feature test does not establish this universal claim.
+
+Avoid Cartesian-product enumeration when an abstract proof is clearer. Valid
+coverage arguments include:
+
+- prove one implementation is parametric over an axis;
+- partition configurations into equivalence classes and prove the partition is
+  exhaustive and each class representative shares the relevant semantics;
+- prove mutually exclusive `cfg` predicates form a total partition over the
+  supported set;
+- prove a generator emits only members of a finite audited family;
+- prove independent lemmas for axes, then prove their assumptions remain
+  independent under composition;
+- prove unsupported combinations fail before producing a shippable artifact.
+
+For every abstraction, check interactions between axes. A proof of each feature
+alone does not prove their combination; target facts can change layout, atomic
+availability, calling convention, or macro expansion on which another feature
+depends.
+
+Attach a configuration-domain predicate to every obligation, premise, and
+coverage lemma. A premise proved for one target, toolchain, feature set, or
+generated artifact cannot discharge another case merely because the source
+looks similar. If separate lemmas cover separate regions, prove that their
+union contains the entire supported set and that their assumptions remain true
+where regions interact.
+
+Do not infer semantic coverage from successful compilation. Compilation may
+establish syntax, typing, and selected compiler-enforced conditions; unsafe
+contracts remain separate obligations.
+
+## Audit Generated and Expanded Code
+
+Treat generated code as shipped source. Capture enough information to reproduce
+or identify:
+
+- generator/proc-macro/build-script package and exact version or digest;
+- host toolchain and host configuration;
+- target configuration and all relevant environment inputs;
+- input tokens/files/schema and invocation options;
+- output source, expansion, metadata, or object identity;
+- diagnostics, suppressed checks, and unsupported paths.
+
+Do not stop at the generator's handwritten source. Soundness can depend on the
+mapping from every accepted input and configuration to output, hygiene and name
+resolution in the destination crate, compiler expansion behavior, or external
+tool output.
+
+Use one of these proof strategies:
+
+1. Inspect each member of a proven finite output set.
+2. Prove a property of the generator that entails safety for every supported
+   output.
+3. Record the exact generated artifact in the audited snapshot and enforce that
+   exact output identity or digest. Pinning only the generator does not fix its
+   inputs, environment, compiler interaction, or output.
+
+For macro-generated APIs, audit the expanded visibility and caller obligations.
+A safe-looking invocation is not automatically a safe API if rustc enforces an
+unsafe-context obligation in the expansion; conversely, generated internal
+unsafe code behind an invocation usable from safe context must be sound for
+every accepted safe invocation.
+
+Build scripts may emit `cfg` values, link directives, environment values, or
+generated source. Include both their output and every supported path that can
+produce different output. Include proc-macro and build dependencies in the TCB
+or recursive audit as appropriate.
+
+## Audit Targets, SIMD, and Concurrency
+
+For target-dependent code:
+
+- derive layout, validity, alignment, ABI, instruction, atomic, and pointer-width
+  facts from exact applicable authoritative contracts or TCB entries;
+- distinguish compile-time target features from runtime CPU availability;
+- prove every call edge satisfies target-feature and calling-convention
+  requirements;
+- prove runtime feature detection dominates every specialized instruction path
+  and cannot be invalidated between detection and use;
+- audit fallback paths and combinations of enabled features;
+- include cross-language or dynamic-dispatch edges that may bypass a Rust
+  wrapper.
+
+For concurrency:
+
+- quantify over every permitted interleaving and memory-model behavior within
+  scope;
+- prove synchronization, atomic ordering, initialization publication, lifetime,
+  ownership, and destruction properties from applicable contracts;
+- treat caller-provided safe callbacks and safe trait implementations as
+  adversarial, including reentrancy, blocking, panic, and unexpected timing;
+- distinguish thread-safety properties promised by types and unsafe trait impls
+  from behavior merely observed on one runtime.
+
+Do not use one scheduler run, stress test, or architecture as proof of all
+executions.
+
+## Audit Allocators, Panic Modes, and Assertions
+
+For allocation-sensitive unsafe code, identify the allocator contract actually
+required:
+
+- size and alignment accepted;
+- allocation, reallocation, and deallocation pairing;
+- zero-size behavior;
+- maximum sizes and arithmetic bounds;
+- allocation failure, overcommit, and address reuse;
+- thread safety and reentrancy;
+- allocator identity across FFI, dynamic-library, and configuration boundaries.
+
+A library generic over a valid allocator implementation must be sound for every
+implementation satisfying the applicable unsafe allocator contract. A binary
+that selects a particular allocator may record that exact implementation as a
+TCB dependency when appropriate.
+
+Prove invariant restoration and resource behavior under every supported panic
+strategy. Distinguish:
+
+- normal return;
+- error return;
+- panic with unwind;
+- panic with abort;
+- foreign exceptions or unwinding across boundaries;
+- cancellation or destruction suppression where supported.
+
+Never rely on `debug_assert!` to establish a release-build safety precondition.
+If a check is part of the proof, ensure it executes in every supported
+configuration or prove the proposition independently. Treat differences in
+overflow checks, debug assertions, and optimization as configuration branches
+until shown irrelevant.
+
+## Audit FFI, Assembly, Linking, and Global Symbols
+
+For FFI, prove or explicitly trust:
+
+- exact function and data ABI, types, layout, calling convention, and symbol
+  identity on both sides;
+- validity and ownership of arguments and return values;
+- lifetime, aliasing, allocation, deallocation, callback, thread, and unwinding
+  rules;
+- versioning and configuration of the foreign implementation;
+- behavior of foreign code that Rust unsafe code relies upon.
+
+Declaring an extern item asserts that the declaration matches reality; calling
+it consumes both the declaration contract and call-specific preconditions. Keep
+those obligations distinct.
+
+For inline assembly, derive Rust-side requirements from exact applicable
+Reference or standard-library text. Record ISA manuals, target specifications,
+ABI documents, linker manuals, and other non-Rust sources as versioned
+`EXTERNAL-SPEC` TCB entries unless the exact consumed proposition appears in
+Reference or standard-library text. Audit operands, register classes, clobbers,
+flags, stack, control flow, memory effects, options, instruction availability,
+privilege/environment, and interaction with compiler optimization. This is a
+discovery list, not an authoritative specification.
+
+Audit whole-program/link obligations when relevant, including:
+
+- uniqueness and type/ABI agreement of exported or unmangled symbols;
+- global allocator and panic-runtime selection;
+- link-section placement, alignment, initialization order, and linker-script
+  assumptions;
+- dynamic symbol interposition and library substitution;
+- consistency of declarations across crates and languages;
+- linker flags or custom target settings that alter assumptions used by source
+  proofs.
+
+A compilation or linker option that still emits a binary belongs to the
+supported configuration set if users may ship it. Do not label a flag itself
+“Rust undefined behavior” without authoritative text. Instead, trace any
+resulting execution to the exact violated Rust or external contract, or state
+that the artifact lies outside the proved source-level claim.
+
+## Record Configuration Coverage
+
+For each audit, report:
+
+- the formal or operational definition of the supported set;
+- every discovered axis and its possible supported values/classes;
+- the proof method establishing coverage;
+- the obligation and premise applicability domains used by that proof;
+- generated artifact identities or generator theorem;
+- excluded combinations and their enforcement;
+- untested but abstractly proved combinations;
+- tested combinations and the limited propositions those tests establish;
+- remaining assumptions, unknowns, and unsupported tool features;
+- triggers requiring re-audit.
+
+Mark the audit `UNPROVED` if a shippable supported combination is neither
+individually audited nor covered by a valid universal argument.
diff --git a/skills/unsafe-rust/references/proof-obligations.md b/skills/unsafe-rust/references/proof-obligations.md
new file mode 100644
index 0000000000..017aeb6320
--- /dev/null
+++ b/skills/unsafe-rust/references/proof-obligations.md
@@ -0,0 +1,374 @@
+# Proof Obligations, Safety Contracts, and Local Proofs
+
+## Contents
+
+- [Form the theorem](#form-the-theorem)
+- [Qualify applicability](#qualify-applicability)
+- [Separate kinds of premises](#separate-kinds-of-premises)
+- [Write safety documentation](#write-safety-documentation)
+- [Write local safety proofs](#write-local-safety-proofs)
+- [Carry invariants locally](#carry-invariants-locally)
+- [Prove temporal behavior](#prove-temporal-behavior)
+- [Cite authoritative axioms](#cite-authoritative-axioms)
+- [Search for indirect derivations](#search-for-indirect-derivations)
+- [Review a proof](#review-a-proof)
+
+## Form the Theorem
+
+Turn each soundness claim into explicit propositions before writing prose.
+
+For an unsafe API, use this shape:
+
+> For every state and input satisfying preconditions `P`, every permitted
+> execution of the implementation is free of undefined behavior and establishes
+> documented postconditions `Q`, relative to TCB `T`.
+
+Include ongoing and terminal obligations in `P`; a precondition need not concern
+only the instant of the call. State who must maintain each fact, over what
+interval, and what event discharges it.
+
+For a safe API, prove soundness with no caller-side safety precondition beyond
+well-typed safe use. Also prove any postcondition consumed by the soundness
+argument and any broader behavior explicitly placed in scope. Ordinary input
+validation may reject values, return an error, or panic as documented, but
+soundness may not depend on the safe caller honoring an unenforced rule.
+
+For each local proof site:
+
+1. Obtain the exact preconditions of the operation or contract being used.
+2. Normalize conjunctions, implications, quantifiers, lifetimes, and temporal
+   clauses into separately reviewable obligations.
+3. Derive every obligation from facts available at that point.
+4. Obtain and prove every postcondition used later.
+5. Establish the invariant state after success and every alternative exit.
+
+Treat every operation, declaration, implementation, or state transition that
+supplies or consumes a safety contract as an obligation site. Follow each
+obligation until it reaches checked local facts, named invariants,
+authoritative axioms, or explicit TCB entries.
+
+Undefined behavior is a property of an entire execution. If any event in an
+execution exhibits undefined behavior, make no claim that observations
+elsewhere—or notionally “before” that event—remain guaranteed. An unexecuted bad
+path does not by itself make a different execution undefined, but soundness of a
+safe API still quantifies over every valid use and execution, so one reachable
+valid counterexample refutes it.
+
+## Qualify Applicability
+
+State or inherit the exact domain of every claim and premise. Include whichever
+dimensions can change the proposition, such as:
+
+- source and generated-artifact identity;
+- inputs, states, types, signatures, lifetimes, and execution intervals;
+- Rust, compiler, standard-library, dependency, and external-contract versions;
+- targets, features, profiles, build inputs, and other supported
+  configurations; and
+- deployment or probabilistic restrictions for separately qualified claims.
+
+A derivation proves only the cases in which every consumed premise applies. If
+one proof does not cover the full required domain, partition the claim into
+cases, prove each case, and establish that their union is exhaustive. Do not
+turn an uncovered case into an implicit exclusion.
+
+Avoid repetitive local boilerplate. A proof may inherit applicability from an
+exactly identified project support policy, invariant definition, axiom entry,
+or TCB entry. The local proof must still make the inheritance and relevant case
+clear enough to review.
+
+A documented Rust guarantee from version `R` may support a later stable version
+only when an exact Rust backwards-compatibility commitment preserves that exact
+semantic proposition throughout the later version's relevant edition, target,
+feature, and configuration domain. Under this skill's authority policy, record
+a compatibility commitment outside the Rust Reference or standard-library
+documentation as an explicit TCB premise. An API's stability or `since` badge
+establishes only what its applicable authoritative text says it establishes; it
+does not by itself prove that every behavioral sentence in current
+documentation was guaranteed from that version. Do not extend a guarantee
+beyond its original domain or automatically to unstable features,
+`RUSTC_BOOTSTRAP`, `-Z` behavior, implementation details, custom targets,
+platform availability, or pre-stabilization behavior.
+
+Compatibility does not propagate guarantees backward. Text first documented in
+version `R` does not by itself prove the same proposition for earlier versions.
+A later clarification can support an earlier version only when applicable
+authoritative text expressly gives it historical scope or an accepted TCB
+premise establishes that the guarantee already applied. Unchanged
+implementation, version history, a documentation diff, or advisory prose is
+insufficient by itself. Split the version domain if later text qualifies or
+contradicts the older statement. For an open-ended toolchain range, either
+prove the claim parametrically relative to a named compatibility premise or
+state an audit cutoff and later-release re-audit trigger. A compatibility
+premise about abstract semantics does not prove correctness of future compiler
+binaries.
+
+## Separate Kinds of Premises
+
+Classify every premise:
+
+- **Local fact:** Established by inspected code, control/data flow, a type, or a
+  named invariant. Cite the exact check, branch, assignment, ownership fact, or
+  invariant clause.
+- **Rust axiom:** Entailed by exact applicable text in a versioned Rust Reference
+  or standard-library page. Quote and link it.
+- **Selected safe-dependency fact:** Supplied by a deliberately selected safe
+  dependency contract and recorded in the TCB.
+- **Tool-derived fact:** Established by a verified tool theorem whose exact
+  proposition, model, scope, and premises entail the local fact. Record only its
+  residual unproved tool/model/translation premises in the TCB.
+- **Additional assumption:** External specification, unsafe dependency,
+  compiler implementation, platform behavior, deployment restriction,
+  probabilistic premise, or other admitted proposition recorded in the TCB.
+
+Never blur an assumption into a derived fact. If a premise does not fit one of
+these classes, the proof is incomplete.
+
+Distinguish the validity of a value of type `T` from a stronger library
+invariant attached to its role in an abstraction. Prove both when needed.
+Likewise, distinguish:
+
+- permission to perform an operation;
+- facts established by that operation;
+- facts merely preserved by it;
+- obligations transferred to a returned pointer, reference, guard, token, or
+  caller.
+
+## Write Safety Documentation
+
+Give every unsafe function, trait, impl, field, macro boundary, and other unsafe
+contract a precise safety specification regardless of visibility. Use `# Safety`
+documentation for public contracts. A private contract may cite module-owned
+invariants, but must still state every fact its callers or implementers must
+establish or continue to uphold. Use precise subjects, intervals, and
+quantification.
+
+A complete unsafe API contract should make the following derivable whenever
+applicable:
+
+- which values, memory regions, objects, threads, or executions it covers;
+- validity, initialization, alignment, size, provenance, accessibility,
+  lifetime, aliasing, exclusivity, mutability, and ownership requirements;
+- concurrency, atomic ordering, synchronization, reentrancy, callback, signal,
+  and thread-affinity requirements;
+- target, ABI, feature, allocator, unwinding, linkage, or environmental
+  restrictions;
+- what may be observed, read, written, moved, copied, destroyed, or retained;
+- whether an invariant may be suspended, for how long, and what must not happen
+  before restoration;
+- obligations attached to return values or capabilities;
+- behavior on panic, unwind, cancellation, early return, or partial progress;
+- documented postconditions on success and every other documented outcome.
+
+Use this list as a discovery prompt. Derive the actual requirements from the
+exact operation and applicable authoritative contracts, and add every other
+obligation those contracts create.
+
+Define relative terms. Replace phrases such as “valid pointer,” “properly
+initialized,” “no aliases,” “live,” “same allocation,” “correct layout,” and
+“used normally” with the exact propositions intended. Do not use “the caller
+guarantees” unless the current boundary is unsafe and its documentation actually
+requires the cited fact.
+
+Safety preconditions must be sufficient; they need not be mathematically
+weakest. Nevertheless, avoid irrelevant or unknowable conditions. Every stated
+condition becomes part of the API contract and its evolution constraints.
+
+Document postconditions with the same precision. If callers may rely on a
+result, state:
+
+- the state/value relationship established;
+- the resources, aliases, or ownership transferred;
+- which prior invariants remain true;
+- when the guarantee begins and ends;
+- distinctions among normal return, error, panic, and unwind.
+
+## Write Local Safety Proofs
+
+Place a `SAFETY` comment immediately adjacent to the smallest cohesive unsafe
+operation or block. Prefer one proof unit per independently reviewable
+obligation set.
+
+For new code, require an explicit `unsafe { ... }` block for each unsafe
+operation even inside an `unsafe fn`, and enable `unsafe_op_in_unsafe_fn` at
+`deny` or `forbid` when compatible with project policy. Use documentation and
+undocumented-unsafe-block lints as completeness aids where available; lint
+success is not a proof.
+
+Use this structure:
+
+```rust
+// SAFETY:
+// Obligation: `<operation>` requires P1, P2, and P3.
+// Facts:
+// - F1 follows from <exact check, type fact, or invariant clause>.
+// - F2 follows from TCB-... / AXIOM-... .
+// Derivation:
+// - F1 and F2 imply P1 because ...
+// - ...
+// Result:
+// - The operation establishes Q.
+// - Q re-establishes/preserves/transfers invariant I.
+unsafe { operation() }
+```
+
+Use ordinary prose when clearer, but retain each logical component. Do not write:
+
+- “safe because this is unsafe code”;
+- “the pointer is valid” without defining and proving the required properties;
+- “checked above” without identifying the dominating check and relevant values;
+- “guaranteed by the type/caller/API” without naming the exact contract clause;
+- “this is how the standard library does it”;
+- “Miri/tests pass” as a universal derivation;
+- “obviously,” “trivially,” or “cannot happen” in place of proof;
+- circular arguments in which an invariant is justified only by code that
+  already assumes it.
+
+A proof may cite a canonical checked proof or TCB entry to avoid duplicating
+large quotations. Keep enough local text to show which proposition is used and
+how it entails the local obligation.
+
+When one unsafe block contains multiple operations, prove each operation in
+program order. Include facts established by earlier operations only after
+proving those operations' postconditions.
+
+## Carry Invariants Locally
+
+State each safety invariant near the representation or boundary that owns it.
+Give it a stable name when multiple proofs cite it. Specify:
+
+- the objects and states over which it quantifies;
+- when it is required to hold;
+- who may rely on it;
+- every operation permitted to establish, mutate, suspend, transfer, consume,
+  or destroy it;
+- what must be true while it is suspended;
+- how panic, unwind, cancellation, reentrancy, callbacks, and destruction affect
+  it.
+
+Define the invariant's actual enforcement boundary and prove every producer,
+transition, and consumer within it. Apply
+[Use module privacy](api-boundaries-and-evolution.md#use-module-privacy) to
+choose that boundary for new code or compute the real access region of existing
+code.
+
+An invariant is local when each consumer can cite a named proposition whose
+current truth is established by a local boundary. Its subject may still be
+global state. Do not accept an informal “global invariant” that no boundary
+owns or re-establishes.
+
+## Prove Temporal Behavior
+
+Treat time and interference explicitly:
+
+- Determine the interval during which each pointer, reference, lock, capability,
+  borrow, allocation, and invariant fact remains usable.
+- Check every possible intervening call, callback, destructor, panic, unwind,
+  cancellation point, signal interaction, and reentrant entry.
+- For concurrency, quantify over every permitted thread interleaving and weak
+  memory behavior within scope, not one observed schedule.
+- If an operation returns a capability whose safe methods could violate an
+  invariant, place the ongoing obligation in the unsafe boundary's contract or
+  return a representation that enforces it.
+- If a guard restores an invariant in `Drop`, prove restoration on all paths on
+  which `Drop` runs and separately address paths on which destruction can be
+  skipped, duplicated, reordered, or aborted.
+- If an invariant is suspended across code not controlled by the abstraction,
+  treat that code as adversarial unless it is an explicitly trusted dependency.
+
+Cryptographic infeasibility and low probability do not turn a possible
+execution into an unconditional Rust soundness proof. Move such premises to an
+explicit conditional application claim and TCB entry.
+
+## Cite Authoritative Axioms
+
+For every Rust or standard-library ground-truth proposition:
+
+1. Select documentation applicable to the audited compiler/library version.
+2. Link the narrowest applicable sections, including versions in the URLs.
+3. Quote the smallest sufficient set of excerpts whose propositions participate
+   in the derivation.
+4. State the proposition derived from each excerpt and justify the inference
+   that combines them.
+5. Check that qualifications, definitions, linked clauses, and surrounding
+   scope do not weaken it.
+6. Have the reviewer open the source and independently confirm the derivation.
+
+Apply [Qualify applicability](#qualify-applicability) when a citation and the
+claim concern different Rust versions.
+
+If the Reference or standard-library documentation is missing, ambiguous,
+internally inconsistent, or too weak, record the exact missing proposition.
+Treat explanatory sources or current implementation behavior only as leads or
+explicit additional assumptions. Recommend an upstream documentation report
+when appropriate.
+
+## Search for Indirect Derivations
+
+Do not equate the absence of a single direct documentation sentence with the
+absence of a proof. Before reporting an authoritative documentation gap or
+finalizing an important obligation as unproved:
+
+1. Restate the exact semantic property required and unfold relevant project
+   definitions.
+2. Search for applicable direct guarantees.
+3. Search for stronger, more general, or orthogonal authoritative facts whose
+   conjunction could entail the property.
+4. State every intermediate lemma and justify each inference rather than merely
+   collecting citations.
+5. Check the applicability of every premise and intermediate lemma.
+6. Try to construct a model that satisfies the premises while falsifying the
+   conclusion. If one remains possible, identify the missing implication.
+
+This search does not weaken the fail-closed rule. If no complete admissible
+derivation is established, the obligation remains unproved. Distinguish “this
+audit did not complete a proof” from the stronger claim that authoritative
+documentation cannot support one.
+
+## Review a Proof
+
+For each proof:
+
+1. Reconstruct the required preconditions from the callee or language/library
+   contract rather than trusting the comment's summary.
+2. Open every citation and verify its exact proposition, version, and scope.
+3. Check each claimed local fact against the actual dataflow and all alternative
+   paths.
+4. Expand every named invariant and ensure it is established initially and
+   preserved by every permitted transition.
+5. Check quantifiers, arithmetic boundaries, zero-sized and empty cases,
+   overflow, partial initialization, overlapping ranges, alias duration,
+   provenance, destruction, unwinding, reentrancy, concurrency, and
+   configuration-dependent behavior when relevant.
+6. Verify every postcondition used downstream.
+7. Search for circularity, vacuity, hidden trust, and stronger conclusions than
+   the cited facts entail.
+8. Record every missing implication so it cannot be forgotten, apply
+   [Search for indirect derivations](#search-for-indirect-derivations), and
+   report `UNPROVED` if a required implication remains absent.
+
+If validation requires a material derivation absent from the existing safety
+comment, include that reconstructed derivation—or the smallest missing
+portion—in the review. A derivation is material when it supplies a necessary
+logical bridge that is neither stated nor an immediate syntactic or
+type-enforced fact visible at the proof site. Give its citations,
+applicability, and relationship to the required preconditions and
+postconditions. Report the implementation result separately from the deficient
+proof artifact:
+
+- If the reconstruction succeeds, the implementation obligation may be proved,
+  but report the inadequate comment and provide proposed replacement wording.
+- If the reconstruction fails, leave the obligation unproved.
+- If it yields a valid UB or postcondition counterexample, report `UNSOUND` or
+  `CONTRACT-BROKEN` as applicable.
+
+When changes are authorized, update the adjacent proof rather than leaving the
+reconstructed reasoning only in the review. A canonical checked proof or named
+invariant may hold shared detail; do not demand redundant prose when the local
+comment already identifies the exact proposition and complete derivation path.
+
+Do not use reconstruction to repair a caller-facing contract retroactively. An
+undocumented caller obligation remains hidden under the current API contract,
+even if adding it would make the implementation proof succeed.
+
+These examples identify common omissions; they are not a substitute for reading
+the applicable authoritative contracts.
diff --git a/skills/unsafe-rust/references/tcb-and-evidence.md b/skills/unsafe-rust/references/tcb-and-evidence.md
new file mode 100644
index 0000000000..8e1be81aa4
--- /dev/null
+++ b/skills/unsafe-rust/references/tcb-and-evidence.md
@@ -0,0 +1,294 @@
+# Trusted Computing Base and Evidence
+
+## Contents
+
+- [Maintain an explicit trust boundary](#maintain-an-explicit-trust-boundary)
+- [Classify TCB entries](#classify-tcb-entries)
+- [Record dependency contracts](#record-dependency-contracts)
+- [Record external and deployment assumptions](#record-external-and-deployment-assumptions)
+- [Handle probabilistic claims](#handle-probabilistic-claims)
+- [Judge tools by their theorem](#judge-tools-by-their-theorem)
+- [Audit a tool-derived proof](#audit-a-tool-derived-proof)
+- [Review and evolve the TCB](#review-and-evolve-the-tcb)
+
+## Maintain an Explicit Trust Boundary
+
+A TCB audit log lists every proposition the audit accepts as authoritative or
+correct without proving it from more primitive in-scope premises. Its purpose is
+not to make assumptions respectable; it makes the exact conditional theorem
+visible and reviewable.
+
+For every entry, record:
+
+- stable identifier and category;
+- exact proposition admitted;
+- exact source, artifact, implementation, version, revision, or digest;
+- contract text or other evidence;
+- scope, configurations, and consumers;
+- why admission is permitted;
+- validation or audit already performed;
+- compatibility/update channel;
+- owner and review trigger;
+- status and unresolved limitations.
+
+Do not use entries such as “the platform works,” “dependencies are correct,”
+“normal allocator,” “valid environment,” or “the compiler is sound.” Split them
+into the smallest propositions actually consumed by proofs.
+
+Minimize the TCB where practical, but never hide an assumption to make the list
+look small. Every unproved premise must become either another proof obligation
+or an explicit entry.
+
+Do not make the theorem vacuous by adding an entry that merely assumes the
+in-scope conclusion or trusts the implementation that the declared audit scope
+purports to prove. Either prove that code, or narrow the theorem and expose the
+code as a precisely identified excluded dependency/TCB component.
+
+When a proof applies an older documented Rust guarantee to a later version via
+Rust's backwards-compatibility commitment, record the exact compatibility
+proposition as a TCB entry unless it is itself entailed by applicable Reference
+or standard-library text. Neither an API stability badge nor a general
+expectation of stability silently expands the older guarantee's semantic or
+configuration domain.
+
+The default source-level theorem is relative to the documented Rust abstract
+semantics. It does not require trusting one compiler backend to emit a correct
+binary. A binary-level theorem additionally requires a compiler/toolchain,
+target, linker, loader, platform, and external-runtime story appropriate to the
+claim.
+
+## Classify TCB Entries
+
+Use categories that expose why a proposition is admitted. Suitable categories
+include:
+
+- **AXIOM:** Exact versioned Rust Reference or standard-library proposition.
+- **SAFE-DEP:** Documented behavior of a deliberately selected safe dependency
+  API.
+- **UNSAFE-DEP:** Correctness of a specific unsafe dependency implementation and
+  contract not recursively proved by this audit.
+- **EXTERNAL-SPEC:** ABI, ISA, OS, hardware, foreign-language, allocator, linker,
+  or other non-Rust contract.
+- **IMPLEMENTATION:** Exact compiler, standard-library build, foreign library,
+  runtime, generator, proc macro, build tool, or other implementation assumed
+  correct for a non-source-level claim.
+- **TOOL:** Residual trusted components or model correspondence supporting a
+  tool-derived proof.
+- **ENVIRONMENT/DEPLOYMENT:** Restriction on entry inputs, load environment,
+  symbols, CPU, privileges, resources, or other execution context.
+- **CRYPTO/PROBABILISTIC:** Explicit computational or probabilistic premise for
+  a separately labeled conditional claim.
+- **OUT-OF-BAND:** A bilateral or project-specific promise beyond the published
+  default contract.
+
+Projects may use different names. Preserve the semantic distinctions.
+
+A proof result produced by a tool is not automatically a TCB assumption. It can
+derive a fact when its theorem and premises are verified. Record only the
+remaining unproved tool correctness, translation, model, solver, certificate
+checker, harness, or environmental premises as TCB entries.
+
+Only a consumed entry explicitly accepted by the authorized human reviewer may
+support `PROVED`. A pending entry makes every consuming claim `UNPROVED`. A
+rejected or superseded entry may not be consumed; replace it with a proof or an
+accepted entry, or narrow the claim and expose the exclusion.
+
+## Record Dependency Contracts
+
+For every dependency proposition, identify whether code is deliberately
+selected or caller-controlled.
+
+The project may trust a deliberately selected safe dependency API to behave as
+documented. Record:
+
+- package/source identity and exact resolved version;
+- safe API and exact behavior consumed;
+- documentation version;
+- enabled features and relevant target/configuration scope;
+- contract channel: SemVer range, exact pin, in-tree fork, out-of-band
+  agreement, consumer-specific promise, or another explicit arrangement;
+- compatibility and re-audit trigger.
+
+An exact pin freezes identity; it does not establish an undocumented semantic
+fact. Prove such a fact by auditing the pinned implementation, obtain an
+applicable additional contract, or admit the exact implementation proposition
+explicitly.
+
+Do not apply this exception to behavior supplied by a caller merely because it
+uses a dependency-defined type or trait. Values, callbacks, closures, plugins,
+generic parameters, trait objects, and safe trait implementations selected by
+the caller remain adversarial safe code.
+
+For a third-party unsafe API:
+
+1. Obtain its exact caller safety contract and prove the local call satisfies
+   it.
+2. Separately establish that the dependency implementation upholds its promise
+   for every valid call.
+3. Discharge step 2 by recursively auditing the implementation or recording a
+   precise `UNSAFE-DEP` assumption.
+
+Do not silently include unsafe dependencies in the safe-dependency exception.
+
+When depending on a fork or out-of-band agreement, record the actual authority
+for the additional promise, parties, exact covered uses, duration, notification
+mechanism, and update process. Do not generalize a consumer-specific guarantee
+to other uses.
+
+## Record External and Deployment Assumptions
+
+External specifications are not Rust axioms. Admit only the exact propositions
+needed, with version and scope, for example:
+
+- a foreign function has a stated ABI and obeys stated ownership/lifetime rules;
+- a CPU instruction has stated effects when a named feature and privilege level
+  are present;
+- a linker binds a symbol to a specific definition with a specific layout;
+- a custom allocator satisfies a named contract;
+- a loader, OS, embedded runtime, kernel, or device maintains specified memory
+  or concurrency behavior;
+- a binary entrypoint receives inputs restricted by a deployment boundary.
+
+Distinguish three claims:
+
+1. **Safe library soundness:** every well-typed safe use is sound; deployment
+   restrictions cannot be hidden premises.
+2. **Unsafe API soundness:** every use satisfying documented safety obligations
+   is sound; external conditions may be explicit obligations.
+3. **Binary/application soundness:** executions satisfying stated entry and
+   deployment assumptions are sound.
+
+A cryptographic signature check, authenticated input channel, kernel policy, or
+restricted device state may narrow a binary theorem. It may not make an
+otherwise safe library API conditionally sound without exposing an unsafe
+boundary or enforcing the restriction in safe code.
+
+If a compilation or linker flag still emits an artifact, record it as part of
+the configuration or toolchain scope. Do not call the flag itself undefined
+behavior unless an authoritative contract uses that classification. Identify
+the exact execution contract that the resulting artifact satisfies or violates.
+
+## Handle Probabilistic Claims
+
+Rust soundness is universal over valid uses and permitted executions. A
+non-zero, negligible, computationally infeasible, or empirically unobserved
+chance of undefined behavior is not unconditional soundness.
+
+A user may explicitly admit a cryptographic or probabilistic premise in the TCB,
+such as collision resistance or unforgeability. Then:
+
+- state the exact security experiment or probability bound;
+- identify the primitive, parameters, implementation, threat model, and time
+  horizon;
+- state how the premise restricts executions or inputs;
+- label the result as a conditional computational/application theorem;
+- keep the ordinary unconditional Rust soundness verdict separate.
+
+Do not write `PROVED` without qualification when the result depends on such an
+entry. Use wording such as `PROVED relative to CRYPTO-...` and explain that this
+is not unconditional Rust soundness.
+
+## Judge Tools by Their Theorem
+
+Classify evidence by what the exact result proves:
+
+- A concrete failing execution can refute a universal claim when the execution
+  is in scope and valid.
+- A clean sampled test, fuzzing run, sanitizer run, interpreter execution, or
+  stress run usually establishes only that the explored executions did not
+  trigger the modeled failure.
+- An alarm-free sound over-approximation can prove absence of its modeled bad
+  states over its stated domain.
+- Exhaustive model checking can prove a property over the exhaustively covered
+  state space.
+- Bounded model checking proves only the bounded proposition unless a
+  completeness bound is established.
+- Deductive or interactive verification can prove the encoded theorem relative
+  to its logic, axioms, models, specifications, and trusted components.
+- Successful compilation establishes only the exact properties the applicable
+  compiler contract and checks are relied upon to enforce.
+
+These are examples, not rules attached permanently to tool categories. One tool
+can provide different guarantees in different modes or results. Read its exact
+documentation and output.
+
+Apply this rule:
+
+> A tool result discharges an obligation only if the documented guarantee of
+> that exact result, together with all explicit premises and trusted components,
+> logically implies the obligation for the exact audited artifact and supported
+> configuration set.
+
+Never infer more than the theorem. A tool model is not an additional Rust
+authority; prove its correspondence to exact applicable Reference and
+standard-library contracts or admit the missing correspondence explicitly.
+
+## Audit a Tool-Derived Proof
+
+Before accepting a tool result, verify:
+
+1. **Proposition:** State the exact property proved and why it entails the Rust
+   soundness obligation or documented postcondition.
+2. **Artifact identity:** Record exact source, expansion/generated output, IR,
+   harness, specifications, compiler, target, tool, solver/backend, versions,
+   options, and configuration.
+3. **Quantification:** Check coverage of inputs, states, executions, call
+   contexts, nondeterminism, thread interleavings, and supported configurations.
+4. **Bounds:** Identify loop, recursion, allocation, object-count, integer,
+   search-depth, thread, time, and other bounds. Establish completeness or limit
+   the conclusion.
+5. **Non-vacuity:** Check that the property, assertion, or unsafe operation is
+   reachable under permitted inputs and that assumptions do not make the
+   harness inconsistent or empty.
+6. **Semantic fidelity:** Check validity, layout, provenance, aliasing,
+   initialization, concurrency, panic/unwind, FFI, assembly, allocation, target,
+   and environment modeling whenever relevant.
+7. **Trust and stubs:** List trusted functions, contracts, abstractions,
+   dependency models, unsupported features, suppressions, skipped checks, and
+   manual lemmas.
+8. **Terminal result:** Require the documented successful proof result. Timeout,
+   unknown, incomplete, unsupported, disabled checks, or ignored alarms do not
+   prove the target.
+9. **TCB:** Identify verifier/analyzer correctness, source-to-model translation,
+   semantic models, solver/backend, proof checker, and specification adequacy
+   that remain trusted.
+
+An independently checked certificate may remove the producer or solver from the
+TCB, depending on its guarantee. It does not by itself prove that the encoded
+specification matches the needed Rust theorem or that source-to-model
+translation is faithful.
+
+Suppressing a sound analyzer alarm creates a new proof obligation. A false
+positive does not invalidate the analyzer's soundness guarantee; an unjustified
+suppression invalidates the claimed conclusion.
+
+Tests and dynamic tools remain valuable for finding counterexamples, exercising
+configuration paths, and checking that proof assumptions match reality. Report
+their actual contribution without treating a clean run as a universal proof.
+
+## Review and Evolve the TCB
+
+Reuse the project's canonical TCB log when present. For every audit:
+
+- open and verify every consumed entry;
+- remove unused, expired, superseded, or duplicate entries;
+- add newly discovered assumptions before relying on them;
+- map entries to proof consumers;
+- check versions, feature/configuration scope, and contract channels;
+- distinguish reviewed facts from proposed or unresolved assumptions;
+- identify entries the human reviewer may reject.
+
+Trigger re-audit when:
+
+- a consumed authoritative document changes materially;
+- supported Rust, target, feature, allocator, tool, or environment scope changes;
+- a dependency resolves to a new version or changes contract channel;
+- a fork or out-of-band agreement changes;
+- generated output or its inputs/generator change;
+- a tool, model, harness, bound, suppression, or proof specification changes;
+- a TCB proposition is weakened, invalidated, or replaced;
+- new code consumes an existing entry in a stronger way.
+
+Record the TCB revision or digest in every audit verdict. A `PROVED` result is
+always relative to that stated trust boundary even when it contains only
+authoritative Rust axioms and deliberately permitted safe-dependency trust.