diff --git a/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/Cargo.toml b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/Cargo.toml
new file mode 100644
index 0000000000..a900eb4e07
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/Cargo.toml
@@ -0,0 +1,13 @@
+[package]
+name = "conflicting-domain-target"
+version = "0.1.0"
+edition = "2021"
+rust-version = "1.84"
+
+[features]
+default = []
+turbo = []
+hardened = []
+
+[lib]
+path = "src/lib.rs"
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/POLICY-INDIGO.md b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/POLICY-INDIGO.md
new file mode 100644
index 0000000000..fe3f0b22cb
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/POLICY-INDIGO.md
@@ -0,0 +1,25 @@
+# Published support policy: Indigo
+
+For this snapshot, let:
+
+- `V = {1.84.0, 1.85.0, 1.86.0}`;
+- `X = x86_64-unknown-linux-gnu`;
+- `A = aarch64-unknown-linux-gnu`;
+- `W = wasm32-unknown-unknown`;
+- `f` mean that `turbo` is enabled; and
+- `h` mean that `hardened` is enabled.
+
+Both Boolean states of each feature are meaningful. A configuration
+`(v, t, f, h)` is supported by Indigo exactly when `v` is in `V`, `t` is in
+`{X, A, W}`, and this predicate is true:
+
+```text
+!f
+or (f and t = X and (h or v >= 1.86.0))
+or (f and t = A and !h and v >= 1.85.0)
+```
+
+Thus `turbo` on `W` is expressly unsupported. All Cargo profiles and both
+states of debug assertions are supported for every configuration selected by
+the predicate.
+
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/POLICY-SCARLET.md b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/POLICY-SCARLET.md
new file mode 100644
index 0000000000..6f2fa37b53
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/POLICY-SCARLET.md
@@ -0,0 +1,25 @@
+# Published support policy: Scarlet
+
+For this snapshot, let:
+
+- `V = {1.84.0, 1.85.0, 1.86.0}`;
+- `X = x86_64-unknown-linux-gnu`;
+- `A = aarch64-unknown-linux-gnu`;
+- `W = wasm32-unknown-unknown`;
+- `f` mean that `turbo` is enabled; and
+- `h` mean that `hardened` is enabled.
+
+Both Boolean states of each feature are meaningful. A configuration
+`(v, t, f, h)` is supported by Scarlet exactly when `v` is in `V`, `t` is in
+`{X, A, W}`, and this predicate is true:
+
+```text
+!f
+or (f and t = X and (!h or v >= 1.85.0))
+or (f and t = A and h)
+```
+
+Thus `turbo` on `W` is expressly unsupported. All Cargo profiles and both
+states of debug assertions are supported for every configuration selected by
+the predicate.
+
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/REQUEST.md
new file mode 100644
index 0000000000..b55016235f
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/REQUEST.md
@@ -0,0 +1,13 @@
+# Conflicting-policy source review
+
+`POLICY-SCARLET.md` and `POLICY-INDIGO.md` are both current published support
+commitments for this exact source snapshot. No precedence, supersession, or
+conflict-resolution rule has been authorized.
+
+Perform a source-only unsafe-code audit and state the strongest conclusion that
+can be justified without selecting a new support policy. Account for the
+effective configuration rejection in the source. `TCB.md` is an accepted human
+trust decision; apply it only to its exact build-tool mappings and keep it
+conspicuous. Use version-matched Rust Reference and standard-library
+documentation for material Rust propositions. Do not modify, build, run, or
+test the target.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/TCB.md
new file mode 100644
index 0000000000..e3afde8f39
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/TCB.md
@@ -0,0 +1,24 @@
+# Accepted build-tool premise
+
+## BUILD-MAP-C
+
+- **Disposition:** accepted by the authorized human reviewer for this target.
+- **Identity:** the toolchain-bundled Cargo releases corresponding exactly to
+  supported Rust 1.84.0, 1.85.0, and 1.86.0, operating on the supplied
+  `Cargo.toml` and source.
+- **Exact proposition:** for each supported release and ordinary Cargo profile,
+  enabling the named Cargo feature `turbo` or `hardened` sets the corresponding
+  `cfg(feature = "...")` predicate for this library compilation, while leaving
+  it disabled does not set that predicate. Compiling for
+  `x86_64-unknown-linux-gnu`, `aarch64-unknown-linux-gnu`, or
+  `wasm32-unknown-unknown` sets `target_arch` to `x86_64`, `aarch64`, or
+  `wasm32`, respectively.
+- **Consumers:** only configuration reachability and effective-rejection proofs
+  for this target.
+- **Excluded propositions:** no Rust semantic fact, source-branch correctness,
+  compatibility outside the three exact releases, or backend/binary correctness
+  is admitted.
+- **Re-audit trigger:** any change to Cargo/toolchain identity, feature names,
+  target set, manifest, source cfgs, or human disposition.
+
+No other build-tool or implementation premise is accepted.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/src/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/src/lib.rs
new file mode 100644
index 0000000000..25063f8ea4
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/c_conflict/src/lib.rs
@@ -0,0 +1,22 @@
+#![no_std]
+
+#[cfg(all(feature = "turbo", target_arch = "wasm32"))]
+compile_error!("the turbo feature is not supported on wasm32");
+
+/// Returns the contained byte, or zero when `value` is `None`.
+#[cfg(not(feature = "turbo"))]
+pub fn value_or_zero(value: Option<u8>) -> u8 {
+    value.unwrap_or(0)
+}
+
+/// Returns the contained byte, or zero when `value` is `None`.
+#[cfg(feature = "turbo")]
+pub fn value_or_zero(value: Option<u8>) -> u8 {
+    if value.is_none() {
+        return 0;
+    }
+
+    // SAFETY: The `None` case returned above, so this value is `Some`.
+    unsafe { value.unwrap_unchecked() }
+}
+
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/k_regression/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/k_regression/REQUEST.md
new file mode 100644
index 0000000000..df2459dab0
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/k_regression/REQUEST.md
@@ -0,0 +1,18 @@
+# Focused multi-issue review
+
+Audit all three modules in `lib.rs`; do not stop after the first aggregate
+soundness finding.
+
+For `callback_index`, review every safe surface and propose the smallest repair,
+but do not edit the source. For `local_proof`, determine implementation
+correctness separately from the adequacy of its existing `SAFETY` comment and
+provide any materially reconstructed proof. For `published_lane`, treat the
+unsafe trait contract as a published 1.x contract with unknown downstream
+implementations and consumers; repository-visible use is not an exhaustive
+consumer inventory.
+
+Keep every proposed repair uncertified until implemented and freshly audited.
+Do not build, test, or execute the target.
+
+Scope: exactly Rust 1.82.0, all targets and ordinary profiles, no additional
+TCB assumptions.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/k_regression/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/k_regression/lib.rs
new file mode 100644
index 0000000000..165148aaa1
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/k_regression/lib.rs
@@ -0,0 +1,53 @@
+#![allow(dead_code)]
+
+pub mod callback_index {
+    pub trait Position {
+        fn position(&self) -> usize;
+    }
+
+    pub fn read<P: Position>(bytes: &[u8], position: &P) -> u8 {
+        unsafe { *bytes.get_unchecked(position.position()) }
+    }
+
+    pub fn write<P: Position>(bytes: &mut [u8], position: &P, value: u8) {
+        unsafe { *bytes.get_unchecked_mut(position.position()) = value }
+    }
+}
+
+pub mod local_proof {
+    pub fn last(bytes: &[u8]) -> Option<u8> {
+        if bytes.is_empty() {
+            None
+        } else {
+            let index = bytes.len() - 1;
+            // SAFETY: This is the fast path.
+            Some(unsafe { *bytes.get_unchecked(index) })
+        }
+    }
+}
+
+pub mod published_lane {
+    pub struct Word(pub [u32; 2]);
+
+    /// Identifies one of the two lanes in `Word`.
+    ///
+    /// # Safety
+    ///
+    /// `INDEX` must be less than 2. `NAME` must be `"low"` when `INDEX == 0`
+    /// and `"high"` when `INDEX == 1`.
+    pub unsafe trait Lane {
+        const INDEX: usize;
+        const NAME: &'static str;
+    }
+
+    pub struct High;
+
+    unsafe impl Lane for High {
+        const INDEX: usize = 1;
+        const NAME: &'static str = "high";
+    }
+
+    pub fn read<L: Lane>(word: &Word) -> u32 {
+        unsafe { *word.0.get_unchecked(L::INDEX) }
+    }
+}
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/EVIDENCE.md b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/EVIDENCE.md
new file mode 100644
index 0000000000..074f77a4cf
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/EVIDENCE.md
@@ -0,0 +1,62 @@
+# Submitted evidence and applicability
+
+## `acknowledge`
+
+The submitted material for this claim is its exact empty body. It has no
+statements, calls, unsafe blocks, raw-pointer accesses, or state transitions.
+No Rust-version-specific library proposition is submitted for this claim. The
+semantic bridge from that syntactic fact to the multi-release claim is exactly
+accepted entry `SEM-EMPTY-BLOCK-180-182` in `TCB.md`.
+
+## `store_word`
+
+The submitted authorities form two exact applicable cases:
+
+- [`std::ptr::write`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/ptr/fn.write.html):
+  the description says that `write` overwrites without reading or dropping the
+  old value, and its Safety section requires `dst` to be valid for writes and
+  properly aligned.
+- [`std::ptr::write`, Rust 1.81.0](https://doc.rust-lang.org/1.81.0/std/ptr/fn.write.html):
+  the same description and Safety propositions apply to the 1.81.0 case.
+
+No compatibility premise is needed or supplied for this two-member domain.
+
+## `copy_byte`
+
+One exact base authority is supplied:
+
+- [`std::ptr::copy_nonoverlapping`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/ptr/fn.copy_nonoverlapping.html):
+  its description says that it copies `count * size_of::<T>()` bytes and does
+  not permit overlap. Its Safety section requires the source and destination
+  regions to be valid for the corresponding read and write, both pointers to
+  be properly aligned, and the regions not to overlap. For `T = u8` and
+  `count = 1`, these are the exact caller-side clauses in `lib.rs`.
+- [Rust 1.80.0 primitive data layout](https://doc.rust-lang.org/1.80.0/reference/type-layout.html#primitive-data-layout):
+  `u8` has size and alignment 1.
+- [`u8: Copy`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/primitive.u8.html#impl-Copy-for-u8):
+  `u8` implements `Copy`.
+
+The applicability of this authority beyond 1.80.0 is only the exact accepted
+compatibility proposition in `TCB.md`; no stability badge or sampled later
+page is submitted.
+
+## `load_word`
+
+Only the two endpoint authorities are supplied:
+
+- [`std::ptr::read`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/ptr/fn.read.html):
+  the description says that `read` reads without moving and leaves the source
+  unchanged. Its Safety section requires a non-ZST source to be valid for
+  reads, properly aligned, and properly initialized.
+- [`std::ptr::read`, Rust 1.82.0](https://doc.rust-lang.org/1.82.0/std/ptr/fn.read.html):
+  the same description and Safety propositions are supplied for the 1.82.0
+  case.
+- [`u32: Copy`, Rust 1.80.0](https://doc.rust-lang.org/1.80.0/std/primitive.u32.html#impl-Copy-for-u32):
+  `u32` implements `Copy` in the 1.80.0 endpoint case.
+- [`u32: Copy`, Rust 1.82.0](https://doc.rust-lang.org/1.82.0/std/primitive.u32.html#impl-Copy-for-u32):
+  `u32` implements `Copy` in the 1.82.0 endpoint case.
+
+No `ptr::read` authority for 1.80.1 or 1.81.0, compatibility premise, semantic
+continuity theorem, or exhaustive interior partition is supplied. Evidence for
+`ptr::write`, `copy_nonoverlapping`, or the empty `acknowledge` body establishes
+no proposition about `ptr::read` on those two releases.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/REQUEST.md
new file mode 100644
index 0000000000..0626c1be25
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/REQUEST.md
@@ -0,0 +1,20 @@
+# Multi-release source-only review
+
+Audit the four exported unsafe APIs in `lib.rs` as four independent claims over
+their exact release sets in `SUPPORT.md`. For each API, report soundness and
+every documented postcondition separately, recover `Required`, state the exact
+`Covered` release region justified by the submitted evidence, and give the
+strongest combined verdict. A regional result is useful even when the complete
+claim cannot be closed.
+
+The authority entries and their claim-specific applicability are exactly those
+in `EVIDENCE.md`. The only non-authoritative admitted premises are the two
+accepted, narrowly scoped entries in `TCB.md`. Do not transfer an entry between
+different operations merely because their contracts or implementations look
+similar.
+
+This is a source-only evidence-packet review. Do not build, test, execute,
+inspect evaluator material, edit source, search for other Rust releases, or add
+new evidence. You may open only the exact versioned official Rust URLs already
+named in `EVIDENCE.md` to verify the supplied propositions. The audit cutoff
+limits the temporal claim but supplies no release-continuity premise.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/SUPPORT.md b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/SUPPORT.md
new file mode 100644
index 0000000000..7df7ecf55a
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/SUPPORT.md
@@ -0,0 +1,14 @@
+# Exact supported domains
+
+The audit cutoff is 2026-07-31. All listed releases, every target on which the
+item exists, and every ordinary debug or release profile are supported.
+
+The exact release predicates are:
+
+- `acknowledge`: `V_ack = {1.80.0, 1.80.1, 1.81.0, 1.82.0}`.
+- `store_word`: `V_store = {1.80.0, 1.81.0}`.
+- `copy_byte`: `V_copy = {1.80.0, 1.80.1, 1.81.0, 1.82.0}`.
+- `load_word`: `V_load = {1.80.0, 1.80.1, 1.81.0, 1.82.0}`.
+
+These are explicit finite sets, not notation for every release in a numeric
+interval. No other Rust release is in `Required` for this target.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/TCB.md
new file mode 100644
index 0000000000..12594e7342
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/TCB.md
@@ -0,0 +1,50 @@
+# Accepted TCB entries
+
+## SEM-EMPTY-BLOCK-180-182
+
+- **Category:** OUT-OF-BAND general Rust-semantics proposition.
+- **Disposition:** accepted by the authorized human reviewer for this target.
+- **Exact proposition admitted:** for every
+  `v in {1.80.0, 1.80.1, 1.81.0, 1.82.0}`, every target on which this exact
+  source exists, and every ordinary debug or release profile, evaluating an
+  empty block executes no operation or event and yields unit. Marking the
+  function containing that block `unsafe` adds a caller proof obligation but
+  does not itself add an executed operation or event.
+- **Consumers:** only the local proof for `acknowledge`; the consumer must
+  independently verify that its exact function body is empty and connect that
+  fact to this proposition.
+- **Exclusions:** this entry does not assert that `acknowledge` is sound, does
+  not describe any nonempty body, and establishes nothing about any pointer
+  operation or other API.
+- **Re-audit trigger:** any change to `V_ack`, the body of `acknowledge`, its
+  signature, its documented contract, or the human disposition.
+
+## COMPAT-COPY-180-182
+
+- **Category:** OUT-OF-BAND compatibility proposition.
+- **Disposition:** accepted by the authorized human reviewer for this target.
+- **Base identity:** the Rust 1.80.0 `std::ptr::copy_nonoverlapping` page,
+  primitive-data-layout section, and `u8: Copy` implementation page named in
+  `EVIDENCE.md`.
+- **Exact proposition admitted:** for each
+  `v in {1.80.0, 1.80.1, 1.81.0, 1.82.0}`, every target on which the item
+  exists, `T = u8`, and `count = 1`, Rust preserves without weakening,
+  qualification, or added precondition all of these 1.80.0 propositions:
+  (1) if `src` is valid to read one initialized `u8`, `dst` is valid to write
+  one `u8`, both pointers are properly aligned, and the one-byte regions do not
+  overlap, executing `copy_nonoverlapping(src, dst, 1)` satisfies its safety
+  contract; and (2) on return it copies the source byte to the destination
+  while leaving the source byte unchanged; and (3) `u8` has size and alignment
+  1 and implements `Copy`, so this call copies exactly one byte without moving
+  ownership from the source value.
+- **Consumers:** only the soundness and documented-postcondition proofs for
+  `copy_byte`.
+- **Excluded operations:** this entry establishes nothing about `ptr::read`,
+  `ptr::write`, `acknowledge`, or any other API.
+- **Configuration scope:** every ordinary debug or release profile in
+  `V_copy`; no deployment or backend theorem.
+- **Re-audit trigger:** any change to `V_copy`, the base proposition, the exact
+  source call, its type/count, or the human disposition.
+
+There is no entry other than `SEM-EMPTY-BLOCK-180-182` and
+`COMPAT-COPY-180-182`.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/lib.rs
new file mode 100644
index 0000000000..becc85df28
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/m_multirelease/lib.rs
@@ -0,0 +1,37 @@
+#![allow(dead_code)]
+
+/// Has no additional safety requirements.
+pub unsafe fn acknowledge() {}
+
+/// Stores `value` at `dst` without reading or dropping the old `u16`.
+///
+/// # Safety
+///
+/// `dst` must be properly aligned and valid for writes of one `u16`.
+pub unsafe fn store_word(dst: *mut u16, value: u16) {
+    // SAFETY: The caller guarantees exactly the preconditions of `ptr::write`.
+    unsafe { std::ptr::write(dst, value) }
+}
+
+/// Copies the byte at `src` to `dst` and preserves the source byte.
+///
+/// # Safety
+///
+/// `src` must be properly aligned, valid for reads of one `u8`, and point to an
+/// initialized `u8`; `dst` must be properly aligned and valid for writes of one
+/// `u8`; and the two one-byte regions must not overlap.
+pub unsafe fn copy_byte(src: *const u8, dst: *mut u8) {
+    // SAFETY: The caller guarantees every precondition for a one-element copy.
+    unsafe { std::ptr::copy_nonoverlapping(src, dst, 1) }
+}
+
+/// Reads and returns the initialized `u32` at `src` without changing it.
+///
+/// # Safety
+///
+/// `src` must be properly aligned, valid for reads of one `u32`, and point to
+/// a properly initialized `u32`.
+pub unsafe fn load_word(src: *const u32) -> u32 {
+    // SAFETY: The caller guarantees exactly the preconditions of `ptr::read`.
+    unsafe { std::ptr::read(src) }
+}
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/Cargo.toml b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/Cargo.toml
new file mode 100644
index 0000000000..9596e8903f
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/Cargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "quantifier-target"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+peer-unsafe-dep = "=3.4.5"
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/DEPENDENCY-API.md b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/DEPENDENCY-API.md
new file mode 100644
index 0000000000..4baf9d71c1
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/DEPENDENCY-API.md
@@ -0,0 +1,17 @@
+# Submitted dependency surface
+
+The exact resolved package is `peer-unsafe-dep` version 3.4.5. Its public
+documentation supplies this declaration and contract:
+
+```rust
+/// Returns `value`.
+///
+/// # Safety
+///
+/// `value` must not equal zero.
+pub unsafe fn duplicate_nonzero(value: u8) -> u8;
+```
+
+The dependency implementation, generated output, prior audit, and binary are
+not present in the submitted snapshot. No assertion about what its function
+body executes is supplied.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/EVIDENCE.md b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/EVIDENCE.md
new file mode 100644
index 0000000000..daedbff641
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/EVIDENCE.md
@@ -0,0 +1,12 @@
+# Submitted Rust authority
+
+Exactly one Rust proposition is supplied for this review:
+
+- Rust 1.80.0 standard-library documentation for
+  [`std::hint::unreachable_unchecked`](https://doc.rust-lang.org/1.80.0/std/hint/fn.unreachable_unchecked.html#safety)
+  states in its Safety section that reaching the function is undefined
+  behavior. Its applicability is Rust 1.80.0 on every supported target and
+  ordinary profile; the page states no narrower target or profile condition.
+
+The dependency declaration in `DEPENDENCY-API.md` is a caller-facing contract,
+not evidence that the unavailable implementation satisfies that contract.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/REQUEST.md
new file mode 100644
index 0000000000..e766ae875a
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/REQUEST.md
@@ -0,0 +1,17 @@
+# Focused source-only review
+
+Audit the soundness of both exported APIs in `lib.rs` as separate claims. For
+each claim, state the exact valid-use and compilation domain, the strongest
+verdict justified by the supplied source and evidence, and the complete proof
+or the smallest missing proposition.
+
+The supported domain is exactly Rust 1.80.0, every target on which this source
+and its exact dependency resolve, and every ordinary debug or release profile.
+The dependency resolution, submitted dependency API, evidence policy, and trust
+decision are part of the review.
+
+This is a source-only evidence-packet review. Do not build, test, execute,
+download dependency source, inspect any evaluator material, or edit the source.
+You may open only the exact versioned official Rust URL named in `EVIDENCE.md`
+to verify its supplied proposition. Do not assume facts about the unavailable
+dependency implementation beyond an accepted TCB entry.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/TCB.md
new file mode 100644
index 0000000000..c10f2dc6ec
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/TCB.md
@@ -0,0 +1,13 @@
+# Trust decision for this review
+
+- The exact versioned Rust standard-library proposition in `EVIDENCE.md` is an
+  admitted Rust authority after citation verification.
+- No `UNSAFE-DEP` entry for `peer-unsafe-dep` 3.4.5 has been proposed or
+  accepted. The human reviewer expressly declines to trust its unavailable
+  implementation for this audit.
+- Under the supplied dependency-resolution premise, the exact dependency pin
+  identifies the logical package coordinate `peer-unsafe-dep` 3.4.5. It does
+  not authenticate source or artifact bytes and does not establish the
+  selected implementation's correctness.
+- There are no other admitted implementation, compatibility, tool, or
+  deployment propositions.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/lib.rs
new file mode 100644
index 0000000000..50b2e1b373
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/q_quantifiers/lib.rs
@@ -0,0 +1,18 @@
+#![allow(dead_code)]
+
+/// Transfers control to a site declared unreachable.
+pub fn force_unreachable() {
+    // SAFETY: This site is assumed to be unreachable.
+    unsafe { std::hint::unreachable_unchecked() }
+}
+
+/// Delegates a nonzero value to the selected peer implementation.
+///
+/// # Safety
+///
+/// `value` must not equal zero.
+pub unsafe fn delegated_nonzero(value: u8) -> u8 {
+    // SAFETY: The caller guarantees that `value` is nonzero, which is the
+    // dependency API's documented caller-side precondition.
+    unsafe { peer_unsafe_dep::duplicate_nonzero(value) }
+}
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/REQUEST.md
new file mode 100644
index 0000000000..c782b1b3c8
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/REQUEST.md
@@ -0,0 +1,16 @@
+# Focused literal audit and redesign
+
+Audit the current source exactly as written, then separately recommend the most
+parsimonious provable abstraction for its stated requirement.
+
+Only the crate-owned `Tail` behavior is required: increment element 1 of the
+two-element array with wrapping arithmetic. No downstream implementation of
+`Slot` or generic call to `increment` must be preserved. This abstraction has
+not been released, so its public contract and representation may change.
+
+Keep the current-artifact verdict independent of every proposal. Explain the
+contract and migration delta of the preferred design and what must be audited
+after implementation. Do not edit or execute the source.
+
+Scope: exactly Rust 1.82.0, all targets and ordinary profiles, no additional
+TCB assumptions.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/lib.rs
new file mode 100644
index 0000000000..bbcdc1e98d
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/r_redesign/lib.rs
@@ -0,0 +1,18 @@
+#![allow(dead_code)]
+
+pub trait Slot {
+    fn index() -> usize;
+}
+
+pub struct Tail;
+
+impl Slot for Tail {
+    fn index() -> usize {
+        1
+    }
+}
+
+pub fn increment<S: Slot>(pair: &mut [u32; 2]) {
+    let value = unsafe { pair.get_unchecked_mut(S::index()) };
+    *value = value.wrapping_add(1);
+}
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/CI.md b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/CI.md
new file mode 100644
index 0000000000..8034ac7dc9
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/CI.md
@@ -0,0 +1,9 @@
+# Continuous-integration samples
+
+CI currently runs Rust 1.84.0 on `x86_64-unknown-linux-gnu` without
+`telemetry`, and Rust 1.86.0 on all three supported targets with both feature
+states.
+
+This is a sampling plan, not a definition or exhaustive inventory of supported
+configurations.
+
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/Cargo.toml b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/Cargo.toml
new file mode 100644
index 0000000000..ebd1c256ef
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/Cargo.toml
@@ -0,0 +1,12 @@
+[package]
+name = "symbolic-domain-target"
+version = "0.1.0"
+edition = "2021"
+rust-version = "1.84"
+
+[features]
+default = []
+telemetry = []
+
+[lib]
+path = "src/lib.rs"
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/REQUEST.md
new file mode 100644
index 0000000000..940d6b0cae
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/REQUEST.md
@@ -0,0 +1,13 @@
+# Exact-source supported-domain audit
+
+Perform a source-only unsafe-code audit of the complete supplied snapshot.
+Recover the exact supported domain from the policy and configuration files,
+then determine whether the public safe API is sound and satisfies its
+documented behavior throughout that domain.
+
+`TCB.md` is an accepted human trust decision for this review. Apply it only to
+the exact propositions and region it names, and keep it conspicuous in every
+result that consumes it.
+
+Use version-matched Rust Reference and standard-library documentation for
+material Rust propositions. Do not modify, build, run, or test the target.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/SUPPORT.md b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/SUPPORT.md
new file mode 100644
index 0000000000..416fa0dc7d
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/SUPPORT.md
@@ -0,0 +1,25 @@
+# Supported configurations
+
+Let `r` denote a released stable Rust toolchain, ordered by its semantic
+version. This source snapshot supports the symbolic release interval
+
+```text
+1.84.0 <= r <= 1.86.0
+```
+
+The interval means every stable Rust release in that closed interval, not only
+the `.0` releases. In particular, Rust 1.85.1 is expressly supported.
+
+The supported target triples are:
+
+- `x86_64-unknown-linux-gnu`;
+- `aarch64-apple-darwin`; and
+- `wasm32-unknown-unknown`.
+
+Both states of the `telemetry` feature are supported. Every combination of a
+release in the interval, a listed target, and a feature state is supported in
+every Cargo profile, with either state of debug assertions.
+
+`Cargo.toml` states the minimum compiler accepted by Cargo. This document,
+including its upper cutoff, is the project's support commitment.
+
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/TCB.md
new file mode 100644
index 0000000000..6382bef673
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/TCB.md
@@ -0,0 +1,23 @@
+# Accepted compatibility premise
+
+## COMPAT-OPTION-184-186
+
+- **Disposition:** accepted by the authorized human reviewer for this target.
+- **Base authority:** the Rust 1.84.0 `Option::is_none` and
+  `Option::unwrap_unchecked` standard-library pages.
+- **Exact proposition:** for every released stable Rust toolchain `r` satisfying
+  `1.84.0 <= r <= 1.86.0`, on every supported target and ordinary Cargo
+  profile, with either feature or debug-assertion state, Rust preserves these
+  base propositions without weakening, qualification, or added precondition:
+  (1) `is_none` returns true exactly for `None`; and (2)
+  `unwrap_unchecked(Some(v))` returns `v`, while calling it on `None` is
+  undefined behavior.
+- **Consumers:** only the soundness and documented-result proofs for
+  `value_or_zero`.
+- **Excluded propositions:** this entry establishes neither the members of the
+  release interval nor any fact about Cargo, another API, a compiler backend, or
+  an emitted binary.
+- **Re-audit trigger:** any change to the source, support interval, base
+  propositions, feature/target scope, or human disposition.
+
+No other compatibility or implementation premise is accepted.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/src/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/src/lib.rs
new file mode 100644
index 0000000000..d1dbcdabc3
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/s_symbolic/src/lib.rs
@@ -0,0 +1,13 @@
+#![no_std]
+
+/// Returns the contained byte, or zero when `value` is `None`.
+pub fn value_or_zero(value: Option<u8>) -> u8 {
+    if value.is_none() {
+        return 0;
+    }
+
+    // SAFETY: The only `None` case returned above. Therefore `value` is
+    // `Some` here, which is exactly `unwrap_unchecked`'s precondition.
+    unsafe { value.unwrap_unchecked() }
+}
+
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/EVIDENCE.md b/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/EVIDENCE.md
new file mode 100644
index 0000000000..7ac89bbb7c
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/EVIDENCE.md
@@ -0,0 +1,14 @@
+# Submitted Rust authority
+
+- Rust 1.80.0 standard-library documentation for
+  [`std::hint::unreachable_unchecked`](https://doc.rust-lang.org/1.80.0/std/hint/fn.unreachable_unchecked.html#safety)
+  states in its Safety section that reaching the function is undefined
+  behavior.
+- Rust 1.80.0's
+  [undefined-behavior chapter](https://doc.rust-lang.org/1.80.0/reference/behavior-considered-undefined.html)
+  is the controlling Reference section for the source-level undefined-behavior
+  claim.
+
+Both pages apply on every target in this target's declared domain on which the
+exact source and item exist, and every ordinary profile. Open them and verify
+the exact propositions used in the report.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/REQUEST.md
new file mode 100644
index 0000000000..22d2c06c97
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/REQUEST.md
@@ -0,0 +1,16 @@
+# Focused source-only review
+
+Audit the safe API in `lib.rs` on exactly Rust 1.80.0, every target on which
+this exact source and the used Rust 1.80.0 standard-library item exist, and
+every ordinary debug or release profile. Report separate conclusions for:
+
+1. freedom from undefined behavior for every valid safe call;
+2. the documented input-zero panic guarantee; and
+3. the documented normal-return result guarantee.
+
+For any negative conclusion, give the exact witness and justify which claimed
+theorem that witness can establish. Analyze distinct inputs independently.
+
+This is a source-only review. Do not build, test, execute, inspect evaluator
+material, or edit the source. You may open only the exact versioned official
+Rust URLs named in `EVIDENCE.md` to verify the supplied propositions.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/lib.rs
new file mode 100644
index 0000000000..a90853c632
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/w_whole_execution/lib.rs
@@ -0,0 +1,17 @@
+#![allow(dead_code)]
+
+/// Panics when `input == 0`.
+///
+/// On normal return, returns `input` unchanged.
+pub fn classify(input: u8) -> u8 {
+    match input {
+        0 => {
+            let marker = 7u8;
+            let _ = marker;
+            // SAFETY: This branch is assumed to be unreachable.
+            unsafe { std::hint::unreachable_unchecked() }
+        }
+        1 => 2,
+        _ => input,
+    }
+}
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/BUILD.md b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/BUILD.md
new file mode 100644
index 0000000000..eaf4027985
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/BUILD.md
@@ -0,0 +1,15 @@
+# Allocator-selection build interface
+
+Supported builds use Cargo and this crate's `build.rs`.
+
+The `FIXTURE_ALLOCATOR` environment variable selects the allocator model:
+
+- an omitted variable or the value `system` selects `system`;
+- the value `arena` selects `arena`; and
+- every other value is rejected by the build script.
+
+For an accepted value, the build script emits exactly one
+`fixture_allocator="..."` configuration option for the library. This is the
+complete supported interface for selecting the allocator model; manually
+invoking `rustc` with invented configuration options is outside the theorem.
+
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/Cargo.toml b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/Cargo.toml
new file mode 100644
index 0000000000..6066ba618e
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/Cargo.toml
@@ -0,0 +1,13 @@
+[package]
+name = "cross-axis-target"
+version = "0.1.0"
+edition = "2021"
+rust-version = "1.85.1"
+build = "build.rs"
+
+[features]
+default = []
+burst = []
+
+[lib]
+path = "src/lib.rs"
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/REQUEST.md b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/REQUEST.md
new file mode 100644
index 0000000000..47fcf95926
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/REQUEST.md
@@ -0,0 +1,13 @@
+# Cross-configuration source audit
+
+Perform a source-only unsafe-code audit of the complete supplied crate,
+including its build script, support policy, generated configuration options,
+public safe API, and documented behavior. Determine the strongest verdict over
+the complete supported domain and separately account for configurations that
+the project rejects.
+
+`TCB.md` is an accepted human trust decision for the exact Cargo and target-cfg
+mappings it names. Keep it explicit and do not widen it.
+
+Use version-matched Rust Reference and standard-library documentation for
+material Rust propositions. Do not modify, build, run, or test the target.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/SUPPORT.md b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/SUPPORT.md
new file mode 100644
index 0000000000..1a58e64f7f
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/SUPPORT.md
@@ -0,0 +1,17 @@
+# Supported configurations
+
+This snapshot supports Rust 1.85.1 on these target triples:
+
+- `x86_64-unknown-linux-gnu`;
+- `aarch64-unknown-linux-gnu`; and
+- `wasm32-unknown-unknown`.
+
+Both states of the `burst` feature and both allocator models (`system` and
+`arena`, selected as specified in `BUILD.md`) are supported, with exactly one
+exclusion: `arena` is unsupported on `wasm32-unknown-unknown`, regardless of
+the `burst` feature. The source must reject that excluded target/allocator
+pair.
+
+Every other combination of the listed target, feature state, and allocator is
+supported in every Cargo profile, with either state of debug assertions.
+
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/TCB.md b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/TCB.md
new file mode 100644
index 0000000000..19f2f96619
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/TCB.md
@@ -0,0 +1,25 @@
+# Accepted build-tool premise
+
+## BUILD-MAP-X
+
+- **Disposition:** accepted by the authorized human reviewer for this target.
+- **Identity:** Cargo 1.85.1 from the supported Rust 1.85.1 toolchain, operating
+  on the supplied manifest, `build.rs`, environment interface, and library.
+- **Exact proposition:** Cargo executes the build script when required for the
+  selected build; honors its `rerun-if-env-changed=FIXTURE_ALLOCATOR` directive
+  when that environment value changes; and passes each emitted
+  `cargo::rustc-cfg=fixture_allocator="..."` option to this library
+  compilation. Enabling `burst` sets `cfg(feature = "burst")`. Compiling for
+  `x86_64-unknown-linux-gnu`, `aarch64-unknown-linux-gnu`, or
+  `wasm32-unknown-unknown` sets `target_arch` to `x86_64`, `aarch64`, or
+  `wasm32`, respectively.
+- **Consumers:** only allocator/feature/target reachability and effective
+  rejection for this target.
+- **Excluded propositions:** no claim about which string the local build script
+  emits, source correctness, Rust abstract semantics, a backend, or a binary is
+  admitted.
+- **Re-audit trigger:** any change to Cargo/toolchain identity, manifest,
+  `build.rs`, environment interface, target set, source cfgs, or human
+  disposition.
+
+No other build-tool or implementation premise is accepted.
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/build.rs b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/build.rs
new file mode 100644
index 0000000000..8cca97cc43
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/build.rs
@@ -0,0 +1,22 @@
+use std::env;
+
+fn main() {
+    println!("cargo::rerun-if-env-changed=FIXTURE_ALLOCATOR");
+    println!(
+        "cargo::rustc-check-cfg=cfg(fixture_allocator, values(\"system\", \"arena\"))"
+    );
+
+    let allocator = match env::var("FIXTURE_ALLOCATOR") {
+        Ok(value) => value,
+        Err(env::VarError::NotPresent) => "system".to_owned(),
+        Err(env::VarError::NotUnicode(_)) => {
+            panic!("FIXTURE_ALLOCATOR must be valid Unicode")
+        }
+    };
+    match allocator.as_str() {
+        "system" | "arena" => {
+            println!("cargo::rustc-cfg=fixture_allocator=\"{allocator}\"");
+        }
+        _ => panic!("FIXTURE_ALLOCATOR must be `system` or `arena`"),
+    }
+}
diff --git a/evals/unsafe-rust/fixtures/v3-targeted/x_cross/src/lib.rs b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/src/lib.rs
new file mode 100644
index 0000000000..3f31591c5b
--- /dev/null
+++ b/evals/unsafe-rust/fixtures/v3-targeted/x_cross/src/lib.rs
@@ -0,0 +1,43 @@
+use std::num::NonZeroU8;
+
+#[cfg(not(any(
+    fixture_allocator = "system",
+    fixture_allocator = "arena"
+)))]
+compile_error!("build.rs must select exactly one supported allocator");
+
+#[cfg(all(
+    fixture_allocator = "system",
+    fixture_allocator = "arena"
+))]
+compile_error!("only one allocator may be selected");
+
+#[cfg(all(target_arch = "wasm32", fixture_allocator = "arena"))]
+compile_error!("the arena allocator is unsupported on wasm32");
+
+/// Constructs a lane identifier.
+///
+/// # Panics
+///
+/// Panics when `value` is zero.
+pub fn lane_id(value: u8) -> NonZeroU8 {
+    #[cfg(all(
+        feature = "burst",
+        target_arch = "aarch64",
+        fixture_allocator = "arena"
+    ))]
+    {
+        // SAFETY: Burst-mode lane identifiers are never zero.
+        return unsafe { NonZeroU8::new_unchecked(value) };
+    }
+
+    #[cfg(not(all(
+        feature = "burst",
+        target_arch = "aarch64",
+        fixture_allocator = "arena"
+    )))]
+    {
+        NonZeroU8::new(value).expect("lane identifier must be nonzero")
+    }
+}
+
diff --git a/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/SKILL.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/SKILL.md
new file mode 100644
index 0000000000..7c60a97623
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/SKILL.md
@@ -0,0 +1,283 @@
+---
+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.
+
+## Recover the Required Domain
+
+Before consuming premises or issuing a full verdict, derive the exact domain
+quantified by the claim. Let `Required(case)` denote the valid uses, inputs,
+states, executions, Rust/toolchain versions, and configurations that the claim
+requires. Let `Covered(case)` hold exactly where every obligation the claim
+requires for that case has a complete derivation from applicable premises.
+Within one obligation, valid case lemmas may be unioned. Across distinct
+obligations, claim-level coverage is their pointwise conjunction—not a union of
+regions in which different obligations happened to be proved.
+
+- Preserve the controlling domain expressions symbolically, including ranges,
+  unions, exclusions, quantifiers, and conditional or moving policies. Record
+  their exact sources and audit cutoff.
+- If applicable project sources conflict or materially underdetermine support,
+  obtain an authorized resolution, derive an explicit conservative audit
+  domain containing every materially supported candidate predicate, or leave
+  the affected combined claim `UNPROVED`. Do not call a conservative audit
+  domain the resolved project promise.
+- Treat every normalization, enumeration, partition, exclusion, and policy
+  merge as a proof step. Prove equality before replacing one domain expression
+  with another, the required containment before using a conservative superset,
+  and `Required ⊆ Covered` before concluding `PROVED`.
+- A finite inventory requires evidence both that every listed member belongs
+  and that no required member is omitted. Endpoints, one representative per
+  apparent category, CI jobs, lockfiles, and other samples do not prove an
+  interval or set inventory.
+- Prefer a parametric proof over the symbolic predicate when enumeration would
+  be large or its exact membership is unavailable. Otherwise report proved
+  regions and the unresolved remainder; do not turn it into an implicit
+  exclusion.
+- An audit cutoff limits the temporal scope of a claim. It does not establish
+  semantic continuity, enumerate releases before the cutoff, or make sampled
+  documentation applicable between samples.
+
+Apply
+[configuration closure](references/configurations-and-generated-code.md#recover-the-required-supported-set)
+to derive supported compilation cases and prove every transformation of that
+predicate.
+
+## 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.
+- Do not promote a producer's preconditions into a universal invariant of its
+  output type. Any type- or abstraction-wide conclusion needs a complete
+  derivation independent of that invalid reversal—for example, applicable
+  authoritative premises, construction-and-preservation closure under an
+  enforced boundary, or an admissible explicit TCB premise. Local checks and
+  other applicable derivations may instead prove the proposition for the
+  particular consumed values or quantified subset.
+- 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, mandatory postconditions, TCB, exclusions, and whether design
+   alternatives are requested.
+2. **Recover the domain.** Preserve the controlling expressions, derive
+   `Required`, justify every transformation or conservative enlargement, and
+   state how eventual proof cases will establish `Required ⊆ Covered`.
+3. **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 required domain.
+4. **State every obligation.** Obtain each controlling contract, decompose it
+   literally, and state the exact proposition and applicability to prove.
+5. **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.
+6. **Close and challenge.** Give every literal contract clause and safe surface
+   a disposition, establish domain closure, and try to falsify the domain
+   recovery, contract reading, derivations, and coverage with boundary and
+   adversarial cases derived from the actual clauses.
+7. **Certify and report.** Apply the quantifier-sensitive certificates below.
+   Keep every unresolved obligation visible and state the smallest missing
+   implication. Record proofs, TCB, coverage, findings, postcondition failures,
+   documentation gaps, and residual scope without optimism.
+
+## 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 supported-toolchain policy, 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.
+
+| Verdict | Required certificate |
+|---|---|
+| **PROVED** | Every obligation for the exact named claim has a checked derivation over its complete applicability, `Required ⊆ Covered`, and every premise is proved from admissible sources or appears as an accepted entry in the stated TCB. |
+| **UNPROVED** | A required derivation, premise, applicability or domain-closure argument, postcondition proof, or citation remains missing, ambiguous, circular, or unverifiable, and no applicable existential refutation below is complete. |
+| **UNSOUND** | There exists a proved valid in-scope use or execution which reaches an executed operation or semantic event, its exact required safety proposition is false there, and applicable authoritative semantics—possibly together with an explicit TCB premise about the implementation—entails undefined behavior. |
+| **CONTRACT-BROKEN** | There exists a proved valid in-scope execution which, considered as a whole, contains no undefined behavior and falsifies a documented postcondition. |
+
+Failure to prove a universal obligation is enough for `UNPROVED`; do not invent
+a counterexample. Conversely, once all parts of an existential UB certificate
+are proved, report the scoped soundness claim `UNSOUND`; do not continue to
+demand a universal positive lemma and dilute the result to `UNPROVED`. A
+violation of user-authored safety prose is not by itself a runtime UB event:
+trace the certificate through applicable contracts to the exact authoritative
+or explicitly trusted UB consequence.
+
+Classify a witness using the execution as a whole, not observations from a
+prefix of an execution that later reaches undefined behavior. An
+undefined-behavior-containing execution can witness `UNSOUND` but cannot
+establish the existential claim required for `CONTRACT-BROKEN`. If it is the
+only behavioral evidence, report soundness as `UNSOUND` and the postcondition
+as `UNPROVED`. An independent UB-free witness or equivalent existence proof
+may establish `CONTRACT-BROKEN`; separate proofs may therefore establish both
+verdicts.
+
+Apply verdicts separately to soundness, documented postconditions, and
+conditional application claims. State exact scope, applicability, and TCB
+beside every verdict. For every affirmative claim spanning multiple Rust
+releases, identify a parametric proof, an exhaustive applicable partition, or
+an exact proposition-preserving compatibility premise whose covered domain
+contains the claimed release set. Never substitute endpoints, sparse samples,
+an audit cutoff, “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/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/agents/openai.yaml b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/agents/openai.yaml
new file mode 100644
index 0000000000..0f0ca3e7b1
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/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/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/assets/tcb-audit-log-template.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/assets/tcb-audit-log-template.md
new file mode 100644
index 0000000000..0347294827
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/assets/tcb-audit-log-template.md
@@ -0,0 +1,105 @@
+# 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:** `<certified domain ID/link in audit
+  report>`
+- **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, exact release/version
+  regions, 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.
+- [ ] Every version-spanning compatibility entry states the exact proposition
+      preserved and its exact release/configuration region; pins, stability
+      badges, and sampled documentation are not used as interval coverage.
+- [ ] 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/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/assets/unsafe-code-audit-report-template.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/assets/unsafe-code-audit-report-template.md
new file mode 100644
index 0000000000..76d0678280
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/assets/unsafe-code-audit-report-template.md
@@ -0,0 +1,232 @@
+# Unsafe Rust Audit: `<project / scope>`
+
+## Claims and Verdicts
+
+| Claim ID | Exact theorem | Required-domain ID | Verdict | Certificate/proof/finding | TCB and qualification |
+|---|---|---|---|---|---|
+| `<CLAIM-SOUND-...>` | `<source- or binary-level absence-of-UB theorem>` | `<DOMAIN-...>` | `<PROVED / UNPROVED / UNSOUND>` | `<closure proof or finding IDs>` | `<TCB + assumptions>` |
+| `<CLAIM-POST-...>` | `<documented postcondition>` | `<DOMAIN-...>` | `<PROVED / UNPROVED / CONTRACT-BROKEN>` | `<closure proof or finding IDs>` | `<TCB + assumptions>` |
+| `<CLAIM-APP-...>` | `<conditional deployment/security/probabilistic theorem, or omit>` | `<DOMAIN-...>` | `<exact qualified result>` | `<proof/finding IDs>` | `<explicit conditional TCB>` |
+
+- **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>`
+- **Scope:** `<APIs/modules/packages/binaries>`
+- **TCB log:** `<ID/revision/link>`
+- **Skill revision:** `<unsafe-rust revision>`
+
+## 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>` |
+
+## Theorem-Domain and Configuration Closure
+
+### Required Domain Recovery
+
+| Step ID | Controlling source expression or prior predicate | Derived predicate/inventory/partition | Relation to prove (write symbolically) | Equality/containment evidence | Status |
+|---|---|---|---|---|---|
+| `<DOMAIN-...>` | `<exact source + expression>` | `<symbolic result>` | `<derived = source / source ⊆ derived / derived ⊆ source / Required ⊆ union(cases)>` | `<derivation and source>` | `<proved / unresolved>` |
+
+- **Audit cutoff:** `<date/revision and effect on dynamic policies>`
+- **Exact `Required` predicate:** `<symbolic definition or link>`
+- **Policy conflicts/authorized resolution:** `<conflicts, decision, or
+  conservative audit domain without calling it the project promise>`
+- **Unresolved domain:** `<none or exact remainder/finding IDs>`
+
+### Covered Domain
+
+- **Discovered axes:** `<features, cfg, targets, architectures, OSes, SIMD,
+  allocators, debug assertions, panic modes, generated output, and other actual
+  axes>`
+- **Exact `Covered` predicate:** `<union valid case regions within each
+  obligation, then intersect across all claim-required obligations>`
+- **Coverage proof:** `<parametric argument, justified exhaustive partition,
+  justified finite enumeration, generator proof, or combination>`
+- **Closure certificate:** `<proof of Required ⊆ aggregate Covered, or finding
+  ID>`
+- **Version-spanning premise basis:** `<parametric proof, exhaustive applicable
+  cases, exact compatibility entry, or unresolved>`
+- **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>`
+- **UB certificate — valid use:** `<why the use/execution is valid and in scope,
+  or “not established”>`
+- **UB certificate — reachability:** `<executed operation or semantic event,
+  or “not established”>`
+- **UB certificate — false safety proposition:** `<exact required clause and
+  derivation of its falsity, or “not established”>`
+- **UB certificate — consequence:** `<applicable authority/TCB derivation to
+  UB, or “not established”>`
+- **Defined postcondition refutation:** `<valid UB-free witness or equivalent
+  proof that an in-scope UB-free execution falsifies the postcondition, or “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 controlling domain expression is preserved, and every normalization,
+      enumeration, partition, merge, or exclusion has its required equality or
+      containment proof.
+- [ ] Every verdict has the certificate required by `SKILL.md`, including
+      `Required ⊆ Covered` for `PROVED` and every existential link for
+      `UNSOUND` or `CONTRACT-BROKEN`.
+- [ ] Every material derivation reconstructed during review is exposed with its
+      applicability, and deficient proof artifacts are reported separately.
+- [ ] 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/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/abstraction-design.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/abstraction-design.md
new file mode 100644
index 0000000000..b477d8022d
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/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/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/api-boundaries-and-evolution.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/api-boundaries-and-evolution.md
new file mode 100644
index 0000000000..1609e2dc8a
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/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.
+
+Evaluate postconditions independently under the verdict certificates in
+`SKILL.md`, then determine whether a proved broken guarantee can make downstream
+unsafe consumers unsound.
+
+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/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/audit-reporting.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/audit-reporting.md
new file mode 100644
index 0000000000..c895a453de
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/audit-reporting.md
@@ -0,0 +1,214 @@
+# 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;
+- controlling support expressions, conflicts or gaps, audit cutoff, authorized
+  resolution or conservative audit domain, the exact symbolic `Required`
+  predicate, every transformation used to derive it, and enforced exclusions;
+- dependency resolution and relevant source identities;
+- 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;
+- the equality or containment proof for every domain transformation consumed;
+- 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.
+
+Certify each result with the proof shape required by `SKILL.md`. For `PROVED`,
+identify the exact `Required` domain, union valid case lemmas within each
+obligation, intersect coverage across all claim-required obligations, and prove
+`Required ⊆ Covered` for that aggregate predicate. For `UNSOUND`, record every
+link from valid use through reachability and a false safety proposition to the
+applicable UB consequence. For `CONTRACT-BROKEN`, certify that the falsifying
+execution is UB-free as a whole. Otherwise state the smallest gap and use
+`UNPROVED`.
+
+Place qualifications in the theorem, not in vague prose. Use:
+
+> PROVED for `<scope>` over `<Required 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;
+- for a claimed UB witness, the valid use, executed operation or semantic event,
+  false required safety proposition, and authoritative or TCB-backed UB
+  consequence;
+- whether a separate UB-free postcondition refutation or equivalent existence
+  proof 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. **Theorem-domain and configuration closure:** Controlling policy
+   expressions, symbolic `Required`, transformation/equivalence or containment
+   proofs, audit cutoff, axes, `Covered`, `Required ⊆ Covered`, premise-version
+   applicability, generated artifacts, enforced exclusions, and unresolved
+   remainder.
+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/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/configurations-and-generated-code.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/configurations-and-generated-code.md
new file mode 100644
index 0000000000..192a19c973
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/configurations-and-generated-code.md
@@ -0,0 +1,343 @@
+# Configuration Closure and Generated Unsafe Code
+
+## Contents
+
+- [Recover the required supported set](#recover-the-required-supported-set)
+- [Discover configuration axes](#discover-configuration-axes)
+- [Prove coverage of the recovered set](#prove-coverage-of-the-recovered-set)
+- [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)
+
+## Recover the Required Supported Set
+
+Preserve each controlling support expression as a precise symbolic predicate
+before claiming full soundness. Fix the exact source or packaged artifact and
+audit cutoff. Let each predicate range over every relevant toolchain component,
+host/target fact, and build option rather than reducing it to a `rustc` version
+string.
+
+Classify support evidence before using it:
+
+- applicable package metadata, published policy, release documentation,
+  feature/target policy, and authorized downstream agreements may define the
+  project's support contract;
+- manifest checks, build scripts, `compile_error!`, wrappers, packaging rules,
+  and distribution controls may admit or enforce configurations; and
+- CI jobs, lockfiles, successful builds, `rust-toolchain.toml`, and maintainer
+  defaults observe or select particular configurations but do not by themselves
+  define or prove downstream support.
+
+Resolve inherited fields in the exact workspace and inspect the effective
+packaged metadata when it can differ. Interpret every mechanism through its
+applicable contract; do not hard-code a universal precedence among metadata,
+documentation, and agreements. A documented exclusion may delimit a support
+promise, but if soundness depends on preventing that configuration from
+shipping, require effective rejection before claiming closure.
+
+If applicable support declarations conflict or materially underdetermine the
+predicate, do not silently select the narrowest interpretation. Obtain an
+authorized project decision, derive an explicit conservative audit predicate
+containing every materially supported candidate predicate identified from the
+controlling sources, or report regional results and leave the full claim
+`UNPROVED`. Call the resulting predicate `Required(configuration)`. Do not call
+a conservative `Required` predicate a newly inferred project promise. If a
+shippable configuration is exposed and no applicable contract clearly excludes
+it, include it in the unresolved conservative candidate domain until project
+authority resolves its status; successful compilation alone still does not
+define the support promise.
+
+Every transformation from controlling expressions to `Required` is a proof
+obligation. Record the transformation and the relation it must establish:
+
+- an exact normalization requires equality in both directions;
+- a conservative audit domain requires every materially supported candidate
+  predicate to be contained in `Required`;
+- an exclusion requires an applicable support contract and, when soundness
+  depends on preventing shipment, effective enforcement; and
+- a case partition used for proof requires `Required` to be contained in the
+  union of the proved case predicates. Cases need not be disjoint unless the
+  proof relies on uniqueness.
+
+Do not replace a range or conditional predicate with a finite inventory until
+both membership and completeness are established from applicable evidence. A
+list of endpoints, sampled toolchains, one apparent representative per minor
+series, or successfully observed releases is not an inventory proof. When
+exact membership is unavailable or large, retain the symbolic predicate and
+prove it parametrically; if neither parametric proof nor justified exhaustive
+partition closes, leave the remainder `UNPROVED`.
+
+Let `Covered(configuration)` be the union of configuration regions for which
+all applicable semantic obligations and premises are proved. Full configuration
+closure requires a checked containment proof `Required ⊆ Covered`. Coverage of
+an incorrectly contracted restatement does not establish this relation.
+
+Preserve conditional and nonlinear structure across every discovered axis
+rather than collapsing `Required` to a single MSRV. It may be finite,
+nonlinear, or moving and need not have a globally earliest toolchain. Resolve
+dynamic policies at the audit cutoff. A cutoff identifies when a dynamic
+predicate was recovered; it neither enumerates the toolchains before that date
+nor supplies semantic continuity between sampled versions.
+
+Record:
+
+- source revision and workspace/package selection;
+- Rust toolchain range, edition, standard-library identity, and relevant compiler
+  flags;
+- controlling support-policy sources, conflicts, authorized resolutions, and
+  the audit cutoff;
+- 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 Coverage of the Recovered Set
+
+Every case in `Required` must be sound. A CI matrix, sample of targets, or
+pairwise feature test does not establish either the required domain or this
+universal semantic 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
+  `Required`;
+- 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 is `Covered`, that `Required ⊆ Covered`, and that their assumptions remain
+true where regions interact.
+
+Before accepting closure, try to exhibit a required boundary, interior,
+conditional, or cross-axis case absent from `Covered`. This is a falsification
+check, not a substitute for the containment proof.
+
+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 belongs to `Required` only when the controlling
+support predicate includes it; the technical ability to emit or ship a binary
+does not itself define project support. For an included option that emits a
+binary, do not label the flag itself “Rust undefined behavior” without
+authoritative text. 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:
+
+- every controlling support predicate and its exact source;
+- the symbolic `Required` predicate, audit cutoff, and any unresolved policy
+  ambiguity;
+- every normalization, enumeration, partition, merge, or exclusion used to
+  derive `Required`, with its equality or containment proof;
+- every discovered axis and its possible supported values/classes;
+- the proof method and `Covered` predicate;
+- the checked `Required ⊆ Covered` closure argument;
+- 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 `Required` is not justified or if a required
+shippable combination is neither individually audited nor covered by a valid
+universal argument.
diff --git a/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/proof-obligations.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/proof-obligations.md
new file mode 100644
index 0000000000..b66660174c
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/proof-obligations.md
@@ -0,0 +1,431 @@
+# 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.
+
+Apply the quantifier-sensitive verdict certificates in `SKILL.md` when a
+derivation fails or produces a counterexample. Do not confuse failure of a
+universal proof with proof of an existential refutation.
+
+## 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.
+
+Derive the required toolchain/configuration projection and every transformation
+of that projection under
+[Recover the required supported set](configurations-and-generated-code.md#recover-the-required-supported-set),
+then carry it through every premise and case lemma below. The domain covered by
+a derivation is the intersection of the applicability domains of every premise
+it consumes; the union of valid case lemmas must contain the required domain.
+
+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.
+
+Before issuing any affirmative result spanning multiple Rust releases, record
+the exact required release predicate and one coverage basis:
+
+- an applicable parametric derivation over the whole predicate;
+- an exhaustive partition with applicable premises for every class or member;
+  or
+- an exact proposition-preserving backwards-compatibility premise whose domain
+  covers every later release claimed.
+
+Endpoint documentation, sparse version samples, an earliest supported release,
+and an audit cutoff do not prove the releases between them. If the coverage
+basis does not contain the claimed release predicate, narrow the proved region
+and leave the remainder `UNPROVED`.
+
+## 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.
+
+Never promote one producer's admission contract into an invariant of its output
+type. A constructor, conversion, deserializer, FFI ingress, mutation, or other
+producer precondition applies at that invocation. It supports a fact about that
+particular result only through a proved postcondition or dataflow relation; it
+does not prove that every valid value came through that producer or that later
+transitions preserve the property.
+
+To rely on `I` as an invariant of every value in a stated set, provide a
+complete derivation over that set without reversing the producer implication.
+Such a derivation may, for example, use:
+
+1. applicable authoritative premises that entail `I` for every value in the
+   set;
+2. an enforced abstraction boundary plus a complete proof that every in-scope
+   ingress and producer establishes `I` and every transition preserves it;
+3. another applicable derivation, including a verified tool theorem, that
+   entails the exact quantified proposition; or
+4. the exact universal proposition as an admissible accepted TCB premise under
+   the TCB rules.
+
+This enumeration does not replace the entailment requirement or exclude other
+valid proof forms. A consumer may instead establish `I` for its particular
+values or quantified subset from local checks, proved producer and transition
+history, and other applicable premises. If neither derivation closes, leave
+the consuming obligation `UNPROVED`.
+
+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.
+
+When a universal soundness derivation does not close, separately ask whether
+the established facts close an existential refutation. Identify a valid
+in-scope use or execution, prove reachability of the relevant operation or
+semantic event, prove its exact required safety proposition false there, and
+trace that failure to the applicable authoritative or explicitly trusted UB
+consequence. If every link is proved, apply `UNSOUND`; if any link is absent,
+the failed universal obligation remains `UNPROVED`. Do not demand a fact about
+every input to establish one existential witness, and do not infer a witness
+merely from the absence of a universal proof.
+
+## 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—including its quantifier, producer/transition
+   history, and applicability domain—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
+   apply the verdict certificate in `SKILL.md`: report `UNPROVED` if a required
+   implication remains absent and no existential refutation closes, or the
+   applicable refutation verdict if one does.
+
+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 unless it instead
+  closes one of the existential certificates in `SKILL.md`.
+
+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/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/tcb-and-evidence.md b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/tcb-and-evidence.md
new file mode 100644
index 0000000000..ba5efcff73
--- /dev/null
+++ b/evals/unsafe-rust/frozen-packages/668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf/references/tcb-and-evidence.md
@@ -0,0 +1,295 @@
+# 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 execution refutes only a claim whose applicable verdict certificate
+  it satisfies. A valid in-scope execution with a complete UB certificate can
+  refute soundness; a postcondition refutation must be UB-free as a whole.
+- 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.
diff --git a/evals/unsafe-rust/v3-targeted-drafts/controls.md b/evals/unsafe-rust/v3-targeted-drafts/controls.md
new file mode 100644
index 0000000000..c50ce0dba9
--- /dev/null
+++ b/evals/unsafe-rust/v3-targeted-drafts/controls.md
@@ -0,0 +1,136 @@
+# V3 Targeted Oracle Draft — R and K
+
+> Evaluator-only draft. Do not expose to report agents. Freeze only after two
+> independent source and authority reviews.
+
+## R — abstraction redesign
+
+### Exact result
+
+`Required` includes every safe downstream implementation of `Slot` and safe
+instantiation of `increment`, not only the crate-owned `Tail`. A safe
+implementation can return 2. Calling `increment::<Bad>(&mut [0, 0])` then
+executes `get_unchecked_mut(2)` on a length-2 slice. The Rust 1.82.0 contract
+requires an in-bounds index and says an out-of-bounds call is UB even if the
+result is not used. The current safe API is therefore `UNSOUND`.
+
+The requested behavior needs neither generic pointer/index metadata nor an
+unsafe abstraction. A preferred redesign is a nongeneric safe function that
+updates `pair[1]` (or an equivalent checked safe specialization). It eliminates
+the caller implementation capability and the unsafe block. Making `Slot`
+unsafe, adding a prose rule to the safe trait, or preserving the generic
+abstraction by default is less parsimonious because no downstream generic use
+is required. The proposal does not affect the current verdict and needs a fresh
+audit after implementation.
+
+### Atoms
+
+- **R1:** Quantify over arbitrary safe `Slot` implementations; explicitly
+  construct or describe one returning 2 and the safe call using it.
+- **R2:** Prove reachability of `get_unchecked_mut(2)`, falsity of its in-bounds
+  precondition for length 2, and the applicable Rust 1.82 UB consequence.
+- **R3:** Report the current safe API `UNSOUND`, independently of design intent
+  and proposals.
+- **R4:** Extract the exact minimum required behavior: wrapping increment of
+  element 1 for the owned use, with no generic downstream implementation need.
+- **R5:** Prefer a nongeneric safe specialization or an equally parsimonious
+  design that locally enforces the index and transfers no soundness obligation
+  to caller-controlled code.
+- **R6:** Explain that removing the unpublished generic trait/API is an
+  authorized contract delta with no promised downstream migration burden.
+- **R7:** Keep the redesign conditional and require implementation plus fresh
+  audit; do not use it to narrow or alter the current `UNSOUND` result.
+
+Equivalent safe formulations pass R5. Merely making the trait unsafe is a sound
+candidate but does not pass the parsimony atom unless the report explains why
+the unnecessary caller obligation is inferior to the safe specialization.
+
+### Hard errors
+
+Hard error if the report trusts `Tail` as the only safe implementation, treats
+safe trait prose as a caller obligation, calls the current API sound or merely
+`UNPROVED` after closing the witness, certifies an unimplemented redesign, or
+lets design intent narrow the current contract.
+
+### Authority
+
+- Rust 1.82.0 slice `get_unchecked_mut`:
+  `https://doc.rust-lang.org/1.82.0/std/primitive.slice.html#method.get_unchecked_mut`
+  — the index must be in bounds; out-of-bounds calls are UB even if the
+  resulting reference is unused.
+
+## K — multi-issue regression
+
+### Exact results
+
+For `callback_index`, safe implementations of `Position` may return any
+`usize`. For a one-byte slice, an implementation returning 1 gives valid safe
+calls to both `read` and `write`, each of which executes its respective
+out-of-bounds unchecked operation. Both safe surfaces are independently
+`UNSOUND`.
+
+`local_proof::last` is sound. On the nonempty branch, `len > 0`, so
+`index = len - 1` is defined and `index < len`; that discharges
+`get_unchecked(index)`. The existing comment states none of this and does not
+identify the callee obligation. The report must expose the reconstructed proof
+and separately classify the implementation as proved and the proof artifact as
+deficient.
+
+For `published_lane`, the unsafe trait contract makes valid implementations
+responsible for both `INDEX < 2` and the exact `NAME`/`INDEX` relation. The shown
+`High` implementation satisfies both clauses. `read` consumes only the first
+clause and is sound for every valid implementation. Unknown downstream
+consumers mean the unused `NAME` clause cannot be weakened from the published
+1.x contract merely because `read` does not consume it.
+
+### Atoms
+
+- **K1:** For `callback_index::read`, construct the arbitrary-safe-impl witness,
+  prove the length-1/index-1 precondition failure and UB consequence, and report
+  this safe surface `UNSOUND`.
+- **K2:** Independently give the same complete disposition for
+  `callback_index::write`; do not stop after K1.
+- **K3:** For `local_proof::last`, reconstruct the nonempty -> `len > 0` ->
+  `len - 1 < len` derivation, connect it to the exact unchecked-index contract,
+  report the implementation obligation proved, and separately report the
+  existing safety comment materially deficient with replacement proof content.
+- **K4:** Prove both clauses of `High`'s unsafe-trait contract and prove `read`
+  sound relative to the complete valid-implementation contract.
+- **K5:** Retain the `NAME` clause and explain that unknown public
+  implementers/consumers prevent weakening the published 1.x contract merely
+  because the only visible consumer uses `INDEX`.
+- **K6:** Propose a local bounds check or another design that couples and proves
+  the chosen position against the particular slice. Sealing may reduce the
+  implementation set but is not sufficient by itself. Keep every unimplemented
+  repair uncertified and leave both current findings unchanged.
+
+Score each atom independently. Compact shared reasoning may serve K1 and K2
+only if it explicitly names both operations and shows that the witness reaches
+each contract; do not infer the second disposition from the first.
+
+### Hard errors
+
+Hard error if the report trusts arbitrary safe `Position` implementations,
+misses either safe surface while claiming complete coverage, calls either
+surface sound, rejects the correct `last` implementation because its comment is
+bad, explicitly calls the deficient comment adequate, relies on that comment as
+the proof, claims complete requested coverage while omitting the reconstruction,
+weakens the published trait contract from visible use alone, treats sealing
+alone as a sufficient bounds proof, or certifies an unimplemented repair. A
+mere omitted comment-quality disposition fails K3 but is not independently a
+hard error.
+
+### Authority
+
+- Rust 1.82.0 slice `get_unchecked`:
+  `https://doc.rust-lang.org/1.82.0/std/primitive.slice.html#method.get_unchecked`
+- Rust 1.82.0 slice `get_unchecked_mut`:
+  `https://doc.rust-lang.org/1.82.0/std/primitive.slice.html#method.get_unchecked_mut`
+- Rust 1.82.0 slice `len` and `is_empty`:
+  `https://doc.rust-lang.org/1.82.0/std/primitive.slice.html#method.len`
+  and
+  `https://doc.rust-lang.org/1.82.0/std/primitive.slice.html#method.is_empty`
+- Rust 1.82.0 Reference, unsafe traits:
+  `https://doc.rust-lang.org/1.82.0/reference/items/traits.html#unsafe-traits`
+- Rust 1.82.0 Reference, unsafe-trait proof obligations:
+  `https://doc.rust-lang.org/1.82.0/reference/unsafe-keyword.html#unsafe-traits-unsafe-trait`
diff --git a/evals/unsafe-rust/v3-targeted-drafts/domain.md b/evals/unsafe-rust/v3-targeted-drafts/domain.md
new file mode 100644
index 0000000000..957eee289c
--- /dev/null
+++ b/evals/unsafe-rust/v3-targeted-drafts/domain.md
@@ -0,0 +1,439 @@
+# V3 Targeted Domain Evaluator Draft
+
+> **Evaluator-only material.** Never expose this file, its mode labels, atoms,
+> intended predicates, hard-error rules, or authority list to an evaluated
+> agent. The target directories contain no oracle material.
+
+## Scoring Rules
+
+Score propositions rather than keywords, table shapes, or the notation used
+below. An explicit equivalent derivation passes. A report may leave a claim
+`UNPROVED` when it cannot establish an applicable premise; it may not claim
+`PROVED` from samples, endpoints, or an unproved domain transformation.
+
+For each case, `Required` includes configurations, valid safe calls, and
+executions covered by the requested theorem. `Covered` is the set actually
+closed by the report's proof. A universal `PROVED` result requires an explicit
+or readily checkable derivation of `Required subset-of Covered`. An existential
+`UNSOUND` result instead requires one valid in-scope safe use, reachability of
+the unsafe operation, a false exact safety proposition, and the applicable
+authoritative UB consequence.
+
+The evaluator must independently confirm that every cited official page says
+what the report claims and applies to the claimed Rust version. A report does
+not pass merely by supplying a plausible-looking URL.
+
+## S — Symbolic Interval and Parametric Superset
+
+### Intended theorem domain
+
+Let:
+
+```text
+R_S = { r | StableRustRelease(r) and 1.84.0 <= r <= 1.86.0 }
+T_S = { x86_64-unknown-linux-gnu,
+        aarch64-apple-darwin,
+        wasm32-unknown-unknown }
+F_S = { telemetry-off, telemetry-on }
+O_S = { None } union { Some(b) | b is any u8 }
+```
+
+Let `P` range over every Cargo profile accepted by the source and `D` over
+both states of debug assertions. The exact requested case predicate is:
+
+```text
+Required_S(r, t, f, p, d, o)
+  iff r in R_S and t in T_S and f in F_S and p in P and d in D and o in O_S.
+```
+
+This predicate is symbolic. It is not the four minor `.0` releases, the CI
+matrix, or the Cargo minimum. In particular, `Required_S` contains Rust
+1.85.1. Rust 1.84.1 is also an actual stable member, but a report may preserve
+the exact symbolic predicate rather than enumerate released members.
+
+Define `Q_Option(r)` to mean that the Rust 1.84.0 base authorities have been
+verified and accepted entry `COMPAT-OPTION-184-186` applies those exact
+propositions to `r`. The intended proof cases are:
+
+```text
+Covered_S = { (r,t,f,p,d,o) | Q_Option(r), and t/f/p/d/o are otherwise arbitrary }.
+```
+
+The source derivation is parametric in `t`, `f`, `p`, and `d`; it need not and
+should not be expanded into their Cartesian product. Applicability still must
+establish `R_S subset-of {r | Q_Option(r)}`. The accepted fixture-supplied TCB
+entry does so after its base authority is verified. A merely report-authored
+compatibility proposal, generic stability assertion, or endpoints alone does
+not.
+
+### Expected verdicts
+
+- Safe-API soundness over `Required_S`: **PROVED relative to
+  `COMPAT-OPTION-184-186`**.
+- The documented `None -> 0` and `Some(b) -> b` behavior over `Required_S`:
+  **PROVED relative to `COMPAT-OPTION-184-186`**.
+- Configuration closure: **PROVED relative to the same TCB**, because
+  `Required_S subset-of Covered_S`.
+
+The local proof is: `is_none()` returning true takes the `return 0` branch. If
+the unsafe call is reached, `is_none()` returned false; since `Option` has only
+`None` and `Some`, the unchanged, still-owned value is `Some`. This discharges
+`unwrap_unchecked`'s exact precondition, and its return contract supplies the
+contained byte. No target, feature, profile, or debug-assertion fact enters the
+derivation.
+
+### Atoms
+
+- **S1 — Lossless domain recovery:** States `R_S` as the closed symbolic
+  stable-release interval, keeps the three targets and both feature states,
+  and expressly recognizes Rust 1.85.1 as in scope. It does not substitute
+  Cargo's lower bound or CI's endpoint samples for the policy.
+- **S2 — Premise applicability:** Verifies the exact Rust 1.84.0 base
+  propositions, applies only the fixture-supplied accepted
+  `COMPAT-OPTION-184-186` entry over its exact region, and keeps that TCB
+  qualification conspicuous. A report-authored premise does not pass.
+- **S3 — Parametric local proof:** Gives the reachability/variant argument for
+  `unwrap_unchecked`, proves the documented result, and observes that the same
+  derivation covers a superset of all target/feature/profile combinations
+  without Cartesian enumeration.
+- **S4 — Closure and verdict:** Establishes `Required_S subset-of Covered_S`
+  and reports both soundness and behavior `PROVED` over the exact policy domain
+  relative to the accepted entry.
+
+### Hard-error triggers
+
+A report commits a hard error if it:
+
+- contracts the release interval to `.0` releases, CI samples, or the Cargo
+  minimum, including by omitting the expressly supported 1.85.1 case;
+- calls endpoints, a toolchain pin, or sparse documentation a proof of every
+  interior release and then claims `PROVED`;
+- silently invents or accepts a report-authored compatibility premise, or hides
+  the accepted fixture TCB qualification;
+- claims closure while leaving a `Required_S` region outside its proof;
+- finds `None` reachable at `unwrap_unchecked`; or
+- gives an unqualified `UNSOUND` or `CONTRACT-BROKEN` verdict for the shown
+  source.
+
+## C — Nonlinear Conflicting Policies
+
+### Intended predicates
+
+Use the fixture's `V`, `X`, `A`, `W`, `f`, and `h` notation. The two published
+predicates are exactly:
+
+```text
+P_Scarlet(v,t,f,h)
+  iff v in V and t in {X,A,W} and
+      (!f
+       or (f and t = X and (!h or v >= 1.85.0))
+       or (f and t = A and h)).
+
+P_Indigo(v,t,f,h)
+  iff v in V and t in {X,A,W} and
+      (!f
+       or (f and t = X and (h or v >= 1.86.0))
+       or (f and t = A and !h and v >= 1.85.0)).
+```
+
+Neither predicate contains the other. Representative disputed cases include:
+
+- Scarlet-only: `(1.84.0, X, turbo, !hardened)` and
+  `(1.84.0, A, turbo, hardened)`;
+- Indigo-only: `(1.84.0, X, turbo, hardened)` and
+  `(1.85.0, A, turbo, !hardened)`.
+
+There is no authorized exact project predicate. The minimal conservative audit
+domain is the positive-claim union, not a newly selected project promise:
+
+```text
+U_C = P_Scarlet union P_Indigo
+
+U_C(v,t,f,h)
+  iff v in V and t in {X,A,W} and
+      (!f
+       or (f and t = X)
+       or (f and t = A and (h or v >= 1.85.0))).
+```
+
+Thus every non-`turbo` configuration in the base target set is in `U_C`;
+every `turbo` x86 configuration is in it; a `turbo` aarch64 configuration is
+in it exactly when `h` is true or `v >= 1.85.0`; and no `turbo` wasm32
+configuration is in it.
+
+For the conservative source theorem, include every valid `Option<u8>` input,
+every Cargo profile, and both debug-assertion states:
+
+```text
+Required_C = U_C cross O_S cross P cross D.
+```
+
+With applicable versioned `Option` propositions, the source proof is
+parametric over this larger accepted-source region:
+
+```text
+Covered_C = { !f on X/A/W, or f on X/A } cross O_S cross P cross D.
+```
+
+`h` and the exact version do not affect the source derivation. Therefore
+`Required_C subset-of Covered_C` without enumerating `V x T x f x h x P x D`.
+
+### Expected verdicts
+
+- Identity of the controlling exact project support predicate: **UNRESOLVED**
+  (or equivalently `UNPROVED` as a policy-identification claim).
+- Safe-API soundness and documented behavior over conservative union `U_C`:
+  **PROVED relative to `BUILD-MAP-C`**.
+- The conclusion may state that either possible project promise is sound,
+  because both are subsets of the proved union. It must not relabel `U_C` as
+  the recovered exact project promise.
+- `turbo` plus wasm32: outside both policies and effectively rejected by the
+  active `compile_error!` configuration.
+
+The non-`turbo` path uses the documented safe `unwrap_or`. The `turbo` path
+returns on `None`; reaching `unwrap_unchecked` therefore establishes `Some`,
+and the returned byte satisfies the same public behavior. This proof is
+independent of target, `hardened`, profile, and debug assertions.
+
+### Atoms
+
+- **C1 — Both nonlinear predicates:** Reproduces both policies without
+  choosing precedence and identifies at least one Scarlet-only and one
+  Indigo-only region.
+- **C2 — Conservative domain:** Derives the exact minimal `U_C` formula,
+  including the conditional aarch64 clause, and distinguishes it from the
+  unresolved exact project promise. A transparent strict audit superset also
+  passes if the report states `U_C`, proves `U_C` is contained in that superset,
+  does not call it the project promise, and completely covers it.
+- **C3 — Enforced exclusion:** Recognizes that `turbo` wasm32 is excluded by
+  both policies and that the `compile_error!` selected by the matching `cfg`
+  makes the ordinary supported build interface reject it, using only the exact
+  accepted `BUILD-MAP-C` mappings and applicable Rust semantics.
+- **C4 — Parametric superset proof:** Proves both source branches and expresses
+  `Covered_C` as a target/configuration superset of `U_C`, without requiring a
+  Cartesian case inventory.
+- **C5 — Closure and verdict:** Establishes containment of the chosen
+  conservative audit domain in complete source-proof coverage, reports source
+  soundness and behavior `PROVED` over at least `U_C` relative to the accepted
+  build TCB, and leaves only policy identity unresolved.
+
+### Hard-error triggers
+
+A report commits a hard error if it:
+
+- silently selects Scarlet or Indigo, intersects them, or asserts that their
+  union is the recovered exact project promise;
+- contracts `U_C`, misstates it, or uses a larger domain without proving
+  containment and complete coverage; a conspicuously labeled justified strict
+  superset is not an error;
+- treats `turbo` wasm32 as supported, or claims it is effectively rejected
+  without accounting for the selected `compile_error!`;
+- treats Cargo's minimum, a hypothetical build sample, or a policy sentence as
+  a Rust semantic axiom;
+- invents or widens a build-tool mapping beyond accepted `BUILD-MAP-C`;
+- claims `PROVED` while leaving any part of `U_C` uncovered; or
+- calls the shown source `UNSOUND` or `CONTRACT-BROKEN`.
+
+## X — Simultaneous Feature, Target, and Allocator
+
+### Intended theorem domain
+
+Let:
+
+```text
+R_X = { Rust 1.85.1 }
+T_X = { X = x86_64-unknown-linux-gnu,
+        A = aarch64-unknown-linux-gnu,
+        W = wasm32-unknown-unknown }
+B_X = { burst-off, burst-on }
+L_X = { system, arena }
+I_X = { every u8 }
+```
+
+The exact supported configuration predicate is:
+
+```text
+Config_X(t,b,l)
+  iff t in T_X and b in B_X and l in L_X and not (t = W and l = arena).
+
+Required_X = R_X cross Config_X cross P cross D cross I_X.
+```
+
+In particular, this simultaneous cell is supported:
+
+```text
+Q_X = (target = A, burst = on, allocator = arena).
+```
+
+The only target/allocator exclusion is `target = W and allocator = arena`,
+for either feature state. It is distinct from `Q_X`.
+
+The build script maps the accepted `FIXTURE_ALLOCATOR` value to exactly one
+`fixture_allocator` option; the Rust conditional-compilation rules then select
+the corresponding source. For positive proof bookkeeping, the implementation
+closes exactly these relevant call cases:
+
+```text
+Covered_X = { case in Required_X | not Q_X or value != 0 }.
+```
+
+Outside `Q_X`, safe `NonZeroU8::new(value).expect(...)` panics for zero and
+returns a nonzero value otherwise. Inside `Q_X`, `new_unchecked(value)` meets
+its precondition only for nonzero values. Consequently
+`Required_X` is not a subset of `Covered_X`.
+
+### Expected verdicts
+
+- Safe-API soundness over `Required_X`: **UNSOUND relative to accepted
+  `BUILD-MAP-X`**.
+- Whole-domain postcondition “zero panics”: **UNPROVED**, not
+  `CONTRACT-BROKEN`, from the known counterexample, because that execution
+  contains UB.
+- Soundness and documented behavior outside `Q_X`, and for nonzero inputs
+  inside `Q_X`: **PROVED** with the version-matched contracts.
+- The wasm32/arena pair: genuinely excluded and rejected; it is not the UB
+  witness.
+
+The closing witness is the fully safe call `lane_id(0)` on Rust 1.85.1 for
+`aarch64-unknown-linux-gnu`, with `burst` enabled and the accepted `arena`
+allocator selection. The build output and all three true `cfg` conjuncts make
+the unsafe branch reachable. It calls `NonZeroU8::new_unchecked(0)`, whose
+exact safety requirement is false and whose applicable documentation states
+the UB consequence. One supported witness closes `UNSOUND`.
+
+### Atoms
+
+- **X1 — Complete cross-axis domain:** Recovers the target, feature, and
+  allocator axes together; includes `Q_X`; and records only wasm32/arena as the
+  policy exclusion.
+- **X2 — Generated-configuration reachability:** Reads `build.rs` and
+  `BUILD.md`, follows accepted `arena` selection to
+  `fixture_allocator="arena"`, applies only the exact `BUILD-MAP-X` tool
+  mappings, and then applies all three `cfg` conjuncts. It does not audit only
+  handwritten library source in isolation or silently promote Cargo behavior
+  to a Rust axiom.
+- **X3 — Existential UB certificate:** Gives the supported safe
+  `lane_id(0)` call in `Q_X`, reaches `new_unchecked(0)`, states the exact
+  false nonzero proposition and applicable UB consequence, and reports
+  `UNSOUND`.
+- **X4 — Quantifier-sensitive behavior:** Calls the universal zero-input panic
+  guarantee `UNPROVED`, not `CONTRACT-BROKEN`, because the known failing
+  execution has UB; separately proves the checked remainder.
+- **X5 — Genuine exclusion:** Shows both that policy excludes wasm32/arena and
+  that the active `compile_error!` rejects that pair after allocator cfg
+  generation under `BUILD-MAP-X`. It does not use this excluded pair as the
+  witness or generalize the exclusion to aarch64/arena.
+
+### Hard-error triggers
+
+A report commits a hard error if it:
+
+- omits any of feature, target, or allocator from the dangerous conjunction,
+  or treats the supported `Q_X` cell as excluded;
+- ignores build-script output and consequently declares the unsafe branch
+  unreachable;
+- invents, hides, or widens a build-tool/target mapping beyond accepted
+  `BUILD-MAP-X`;
+- uses the excluded wasm32/arena pair as a valid soundness counterexample;
+- calls the current safe API sound or stops at `UNPROVED` despite establishing
+  the complete supported `lane_id(0)` UB witness;
+- calls the zero-panic promise `CONTRACT-BROKEN` based on the UB-containing
+  execution, or claims observations before/after that UB remain guaranteed;
+- claims the policy exclusion alone makes a reachable safe API sound without
+  checking effective rejection; or
+- certifies an unimplemented repair instead of the supplied source snapshot.
+
+## Exact Authority Propositions and URLs
+
+These are the material Rust axioms the scorer must verify. Quotations in a
+report may be short; the logical proposition and exact-version applicability
+must be clear.
+
+### S authorities
+
+The Rust 1.84.0 base `Option` page must support:
+
+1. `is_none` returns true exactly for the `None` variant; and
+2. `unwrap_unchecked` returns the contained `Some` value, while calling it on
+   `None` is undefined behavior.
+
+Exact base pages:
+
+- `https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.is_none`
+- `https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.unwrap_unchecked`
+
+The official release inventory confirms the two patch releases, but is domain
+evidence rather than a substitute for a version-applicable semantic contract:
+
+- `https://doc.rust-lang.org/1.86.0/releases.html#version-1841-2025-01-30`
+- `https://doc.rust-lang.org/1.86.0/releases.html#version-1851-2025-03-18`
+
+The exact accepted compatibility proposition is target entry
+`COMPAT-OPTION-184-186`. It is not Rust authority; verify its identity, human
+disposition, propositions, consumers, and region before using it.
+
+### C authorities
+
+For Rust 1.84.0, 1.85.0, and 1.86.0, verify the same `is_none` and
+`unwrap_unchecked` propositions, plus `unwrap_or` returning the contained value
+or the supplied default:
+
+- `https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.is_none`
+- `https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.unwrap_unchecked`
+- `https://doc.rust-lang.org/1.84.0/std/option/enum.Option.html#method.unwrap_or`
+- `https://doc.rust-lang.org/1.85.0/std/option/enum.Option.html#method.is_none`
+- `https://doc.rust-lang.org/1.85.0/std/option/enum.Option.html#method.unwrap_unchecked`
+- `https://doc.rust-lang.org/1.85.0/std/option/enum.Option.html#method.unwrap_or`
+- `https://doc.rust-lang.org/1.86.0/std/option/enum.Option.html#method.is_none`
+- `https://doc.rust-lang.org/1.86.0/std/option/enum.Option.html#method.unwrap_unchecked`
+- `https://doc.rust-lang.org/1.86.0/std/option/enum.Option.html#method.unwrap_or`
+
+For effective rejection, verify that `cfg(all(...))` is true only when all
+listed predicates are true, that `#[cfg]` includes/removes its attributed form,
+and that `compile_error!` causes compilation to fail:
+
+- `https://doc.rust-lang.org/1.84.0/reference/conditional-compilation.html#configuration-options`
+- `https://doc.rust-lang.org/1.84.0/reference/conditional-compilation.html#the-cfg-attribute`
+- `https://doc.rust-lang.org/1.84.0/std/macro.compile_error.html`
+- `https://doc.rust-lang.org/1.85.0/reference/conditional-compilation.html#configuration-options`
+- `https://doc.rust-lang.org/1.85.0/reference/conditional-compilation.html#the-cfg-attribute`
+- `https://doc.rust-lang.org/1.85.0/std/macro.compile_error.html`
+- `https://doc.rust-lang.org/1.86.0/reference/conditional-compilation.html#configuration-options`
+- `https://doc.rust-lang.org/1.86.0/reference/conditional-compilation.html#the-cfg-attribute`
+- `https://doc.rust-lang.org/1.86.0/std/macro.compile_error.html`
+
+Target entry `BUILD-MAP-C` is the accepted non-authoritative premise for Cargo
+feature and target mapping. It must remain conspicuous and may not be widened.
+
+### X authorities
+
+For Rust 1.85.1:
+
+1. `NonZero::new_unchecked(0)` has undefined behavior and its safety
+   precondition requires a nonzero argument;
+2. `NonZero::new(n)` creates `Some(nonzero)` exactly when `n` is nonzero;
+3. `Option::expect` returns the `Some` value and panics on `None`;
+4. conjunction and key/value configuration predicates select the stated
+   `#[cfg]` forms; and
+5. `compile_error!` causes compilation to fail when selected.
+
+Exact pages:
+
+- `https://doc.rust-lang.org/1.85.1/std/num/struct.NonZero.html#method.new_unchecked`
+- `https://doc.rust-lang.org/1.85.1/std/num/struct.NonZero.html#method.new`
+- `https://doc.rust-lang.org/1.85.1/std/option/enum.Option.html#method.expect`
+- `https://doc.rust-lang.org/1.85.1/reference/conditional-compilation.html#configuration-options`
+- `https://doc.rust-lang.org/1.85.1/reference/conditional-compilation.html#the-cfg-attribute`
+- `https://doc.rust-lang.org/1.85.1/std/macro.compile_error.html`
+
+The build-interface step is an explicit tool/environment premise, not a Rust
+abstract-semantics axiom. Target entry `BUILD-MAP-X` is already accepted for its
+exact identity, mappings, and region. Verify the cited Cargo contracts used to
+review that entry, but do not enlarge it:
+
+- `https://doc.rust-lang.org/1.85.1/cargo/reference/build-scripts.html#rustc-cfg`
+- `https://doc.rust-lang.org/1.85.1/cargo/reference/build-scripts.html#rerun-if-env-changed`
+- `https://doc.rust-lang.org/1.85.1/cargo/reference/features.html`
+
+No release blog, CI outcome, execution result, Miri result, prior report, or
+this evaluator draft is an authoritative Rust semantic premise.
diff --git a/evals/unsafe-rust/v3-targeted-drafts/verdict.md b/evals/unsafe-rust/v3-targeted-drafts/verdict.md
new file mode 100644
index 0000000000..3334189123
--- /dev/null
+++ b/evals/unsafe-rust/v3-targeted-drafts/verdict.md
@@ -0,0 +1,305 @@
+# V3 Targeted Evaluator Draft — Verdict and Release Modes
+
+> **Evaluator-only material.** Never expose this file, its mode labels, atoms,
+> expected verdicts, or coverage relations to an evaluated report agent.
+>
+> This is a draft until both authority reviewers verify every cited page and
+> the final oracle and blind-scoring rubrics are frozen. Score propositions,
+> not keywords or report layout. Equivalent explicit derivations pass. Do not
+> infer a missing material link from vague shorthand.
+
+## Common scoring rules
+
+For each claim, `Required` is the product of its exact release set, supported
+targets/profiles, valid calls, and any conditional postcondition domain.
+`Covered` contains a case only when every obligation for that claim has a
+complete derivation from premises applicable to that case. An existential
+refutation needs no `Required subset Covered` proof; it needs every link of its
+own certificate.
+
+A report may give additional correct regional detail without penalty. A missed
+atom is not automatically a hard error. It is a hard error only where the
+mode-specific rule below or the frozen global rules say so.
+
+## Q — Existential refutation and missing unsafe dependency
+
+Target: `fixtures/v3-targeted/q_quantifiers`.
+
+Let `C_Q` be Rust 1.80.0 times every target on which the exact source and pinned
+dependency resolve times every ordinary profile.
+
+- `Required(Q-force-sound) = C_Q` times the one well-typed safe call
+  `force_unreachable()`.
+- `Required(Q-delegate-sound) = C_Q` times every call
+  `delegated_nonzero(value)` whose caller satisfies `value != 0`.
+
+### Expected results and atoms
+
+- **Q1 — Domain and claim separation:** State both valid-use domains and audit
+  the two APIs independently. In particular, the `unsafe fn`'s documented
+  nonzero precondition restricts its valid uses; it does not restrict the safe
+  `force_unreachable` API.
+- **Q2 — Complete UB certificate:** For `force_unreachable`, give all four
+  links explicitly or by an equivalently exact chain:
+  1. `force_unreachable()` is a well-typed, valid safe call in `Required`;
+  2. the only body path reaches the executed
+     `std::hint::unreachable_unchecked()` call;
+  3. that call requires its site not to be reached, and that exact proposition
+     is false for this call; and
+  4. Rust 1.80.0 std documentation says reaching the function is undefined
+     behavior.
+- **Q3 — Existential closure:** Report `Q-force-sound` as **UNSOUND**. The one
+  complete in-scope witness refutes the universal soundness claim; do not
+  weaken it to `UNPROVED` because no proof covering every safe call was built.
+  The witness exists in every `C_Q` configuration, but that stronger fact is
+  not required for the existential verdict.
+- **Q4 — Exact missing premise:** For `delegated_nonzero`, recognize that a
+  valid caller supplies the dependency API's nonzero caller-side precondition,
+  but the selected unsafe dependency's body is absent and no accepted
+  `UNSAFE-DEP` entry establishes that it honors its contract. The exact pin and
+  caller-facing documentation establish the logical package coordinate and the
+  propagated obligation, not authenticated implementation identity or
+  correctness. The smallest missing proposition is that the selected
+  `peer-unsafe-dep` 3.4.5 implementation satisfies the consumed safety/behavior
+  contract over this domain.
+- **Q5 — No fabricated witness or silent trust:** Report
+  `Q-delegate-sound` as **UNPROVED**, not `PROVED` and not `UNSOUND`. From the
+  submitted packet, claim-level `Covered(Q-delegate-sound)` contains no case:
+  the dependency-correctness obligation is unresolved for all valid inputs.
+  There is also no proved execution of the unavailable body, so no UB witness
+  may be invented. State that recursive source audit or an explicitly accepted
+  exact `UNSAFE-DEP` entry would be required.
+
+### Q hard errors
+
+Any of these is a hard error:
+
+- calling `force_unreachable` sound or only `UNPROVED` after stating all four
+  certificate links;
+- issuing `UNSOUND` for it without a valid call, reachability, the false exact
+  safety proposition, and the authoritative UB consequence;
+- silently trusting the unavailable unsafe dependency, treating the exact pin
+  as implementation proof, or reporting `delegated_nonzero` `PROVED`;
+- fabricating dependency body behavior or a UB execution and reporting
+  `delegated_nonzero` `UNSOUND`; or
+- treating the unsafe dependency's documented caller precondition as though
+  violating its prose were itself an executed UB event.
+
+### Q authority to verify before freezing
+
+- `https://doc.rust-lang.org/1.80.0/std/hint/fn.unreachable_unchecked.html#safety`
+  — exact proposition consumed: reaching
+  `unreachable_unchecked` is undefined behavior; applicability Rust 1.80.0,
+  without a target/profile qualification relevant to this fixture.
+
+No Rust authority is asserted for the absent dependency implementation.
+
+## W — Whole-execution UB and independent behavioral refutation
+
+Target: `fixtures/v3-targeted/w_whole_execution`.
+
+Let `C_W` be Rust 1.80.0 times every target on which this exact source and the
+used Rust 1.80.0 standard-library item exist times every ordinary profile, and
+let `I = {0, ..., 255}`. The claims are:
+
+- `Required(W-sound) = C_W times I`;
+- `Required(W-panic) = C_W times {0}`; and
+- `Required(W-return) = C_W times I`; its theorem is: for every UB-free defined
+  execution in this domain, if that execution returns normally, its result
+  equals its input.
+
+### Expected results and atoms
+
+- **W1 — Soundness witness:** `classify(0)` is a valid safe call, takes the
+  zero arm, evaluates the local statements, and reaches
+  `unreachable_unchecked`. Its unreachable-site proposition is false; the
+  applicable 1.80.0 std contract entails UB. Report `W-sound` **UNSOUND**.
+- **W2 — Whole-execution classification:** The input-zero execution as a whole
+  contains UB. Neither its apparent prefix computation nor the source-level
+  fact that no panic operation appears before the unsafe call remains a
+  guaranteed observation from a defined execution. It therefore cannot prove
+  a UB-free failure of the panic postcondition. With no independent UB-free
+  input-zero execution or equivalent proof, report `W-panic` **UNPROVED**, not
+  `CONTRACT-BROKEN` and not `PROVED`. Its claim-level `Covered` set is empty on
+  the submitted evidence.
+- **W3 — Independent defined witness:** `classify(1)` takes the `1 => 2` arm,
+  executes no unsafe operation, returns normally, and returns `2` rather than
+  the promised input value `1`. That complete execution is UB-free and proves
+  `W-return` **CONTRACT-BROKEN**.
+- **W4 — Cross-execution separation:** Do not transfer a conclusion between
+  the distinct executions. The input-zero UB witness cannot establish failure
+  of the panic promise, while the independent, defined input-one failure
+  remains usable and does not alter the soundness witness.
+
+### W hard errors
+
+Any of these is a hard error:
+
+- calling the safe API sound, reporting only `UNPROVED` after explicitly
+  establishing every input-zero UB-certificate link, or issuing `UNSOUND`
+  without those links;
+- using the UB-containing input-zero execution, an apparent observation before
+  its UB, or the absence of an earlier panic to issue `CONTRACT-BROKEN`;
+- claiming source observations remain guaranteed merely because they occur
+  before the unsafe call;
+- falsely treating the independent input-one refutation as UB-containing, or
+  claiming complete behavioral coverage while omitting it; or
+- replacing the three separate theorem results with one undifferentiated
+  verdict that loses a required conclusion.
+
+### W authorities to verify before freezing
+
+- `https://doc.rust-lang.org/1.80.0/std/hint/fn.unreachable_unchecked.html#safety`
+  — reaching the function is undefined behavior.
+- `https://doc.rust-lang.org/1.80.0/reference/behavior-considered-undefined.html`
+  — controlling Rust 1.80.0 Reference section for what constitutes undefined
+  behavior. Verify that the final evaluator instructions do not attribute to
+  this page prose it does not contain; whole-execution non-observability is the
+  logical consequence of classifying the execution as undefined, not a claimed
+  quotation from a “time travel” subsection.
+
+## M — Multi-release affirmative certificates
+
+Target: `fixtures/v3-targeted/m_multirelease`.
+
+Let `C_M` be every supported target times every ordinary profile. For a
+function `f`, let `Calls_f` be all calls satisfying its documented safety
+preconditions. The exact required domains are:
+
+- `Required(M-ack) = V_ack times C_M times Calls_ack`, where
+  `V_ack = {1.80.0, 1.80.1, 1.81.0, 1.82.0}` and every typed call is valid;
+- `Required(M-store) = V_store times C_M times Calls_store`, where
+  `V_store = {1.80.0, 1.81.0}`;
+- `Required(M-copy) = V_copy times C_M times Calls_copy`, where
+  `V_copy = {1.80.0, 1.80.1, 1.81.0, 1.82.0}`; and
+- `Required(M-load) = V_load times C_M times Calls_load`, where
+  `V_load = {1.80.0, 1.80.1, 1.81.0, 1.82.0}`.
+
+For `store_word`, `copy_byte`, and `load_word`, the same release domain applies
+separately to soundness and the documented normal-return postcondition.
+
+### Expected results and atoms
+
+- **M1 — Exact domains:** Preserve all four finite release sets and the
+  target/profile/call products exactly. Do not treat the cutoff as adding or
+  removing releases. State release regions beside each claim rather than
+  issuing an unscoped crate-wide `PROVED`.
+- **M2 — Parametric `acknowledge` proof:** Verify that accepted general entry
+  `SEM-EMPTY-BLOCK-180-182` has exactly the required release, target, and
+  profile scope. Independently inspect the local syntax and establish that the
+  exact body is an empty block. For arbitrary
+  `(v, target, profile, call) in Required(M-ack)`, combine only those premises:
+  the block executes no operation or event, yields unit, and the `unsafe fn`
+  marker itself adds no executed operation. Thus
+  `Covered(M-ack) = Required(M-ack)` and source-level soundness is **PROVED
+  parametrically relative to `SEM-EMPTY-BLOCK-180-182`**. Keep the admission
+  conspicuous; the TCB entry is general semantics, not a target-specific
+  assertion that the function is sound.
+- **M3 — `store_word` soundness partition:** The 1.80.0 `ptr::write` authority
+  applies exactly to the 1.80.0 case and the 1.81.0 authority to the 1.81.0
+  case. For each case, the documented caller contract entails the applicable
+  page's alignment and write-validity preconditions. The identity
+  `V_store = {1.80.0} union {1.81.0}` proves exhaustiveness. Therefore
+  `Covered(M-store-sound) = Required(M-store-sound)` and soundness is
+  **PROVED** by an exact finite partition.
+- **M4 — `store_word` postcondition partition:** In each exact release case,
+  the applicable page says that `ptr::write(dst, value)` writes the supplied
+  `value` to `dst` without reading or dropping the old value. The same finite
+  partition covers every normal-return postcondition obligation, so
+  `Covered(M-store-post) = Required(M-store-post)` and the documented
+  postcondition is **PROVED**.
+- **M5 — `copy_byte` soundness under the exact TCB:** Verify the Rust 1.80.0
+  `copy_nonoverlapping` safety proposition, primitive `u8` size/alignment, and
+  `u8: Copy` base propositions. Then apply only accepted entry
+  `COMPAT-COPY-180-182`, with its exact release set, `T = u8`, `count = 1`,
+  target/profile domain, and consumer. The caller contract entails its source
+  and destination validity, initialization, alignment, and nonoverlap clauses;
+  the admitted `u8` facts establish the one-byte specialization and avoid the
+  ownership hazard for non-`Copy` values. Thus
+  `Covered(M-copy-sound) = Required(M-copy-sound)` and soundness is **PROVED
+  relative to `COMPAT-COPY-180-182`**.
+- **M6 — `copy_byte` postcondition under the exact TCB:** The accepted entry
+  preserves the base proposition that the call copies the source byte into the
+  destination while leaving the source byte unchanged; `u8` has size one and
+  implements `Copy`. It covers every normal-return postcondition obligation,
+  so `Covered(M-copy-post) = Required(M-copy-post)` and the documented
+  postcondition is **PROVED relative to `COMPAT-COPY-180-182`**.
+- **M7 — `load_word` soundness remainder:** In the 1.80.0 and 1.82.0 endpoint
+  cases, the exact `ptr::read` Safety sections plus exact-version `u32: Copy`
+  facts prove soundness from the caller contract, including safe retention of
+  the source value alongside the returned copy. Thus
+  `Covered(M-load-sound) = {1.80.0, 1.82.0} times C_M times Calls_load`.
+  The 1.80.1 and 1.81.0 regions and therefore the complete `V_load` soundness
+  claim are **UNPROVED**. No UB witness is supplied, so `UNSOUND` does not
+  follow.
+- **M8 — `load_word` postcondition remainder:** In the same two endpoint
+  cases, the applicable `ptr::read` descriptions establish that the returned
+  value is read from `src` while the source is left unchanged; the exact
+  `u32: Copy` facts discharge the ownership qualification. Therefore
+  `Covered(M-load-post) = {1.80.0, 1.82.0} times C_M times Calls_load`.
+  The two interior regions and the complete postcondition claim are
+  **UNPROVED**. No defined wrong-result witness is supplied, so
+  `CONTRACT-BROKEN` does not follow.
+- **M9 — Evidence discipline:** If the report actually relies on endpoint
+  sampling, the cutoff, an unstated stability guarantee, backward projection,
+  evidence for another operation, or a widened TCB entry to fill the
+  `ptr::read` interior, reject that basis explicitly. Identify the smallest
+  missing premise as a verified authority for the interior releases, an exact
+  applicable accepted compatibility entry, or another complete parametric
+  proof. Do not require a report that used none of the listed invalid bases to
+  recite all of them.
+
+### M hard errors
+
+Any of these is a hard error:
+
+- reporting the complete `load_word` claim `PROVED` by endpoint sampling,
+  cutoff reasoning, a stability badge, unprovided interior docs, or another
+  operation's evidence;
+- claiming `Required subset Covered` for `load_word` while omitting either
+  interior release;
+- silently widening `COMPAT-COPY-180-182` by release, operation, type/count,
+  target/profile domain, proposition, or consumer;
+- silently widening `SEM-EMPTY-BLOCK-180-182` by release, source shape,
+  proposition, or consumer;
+- treating either accepted entry as authoritative Rust text rather than a
+  conspicuous TCB premise;
+- projecting a later Rust proposition backward to an earlier release without
+  an exact applicable premise; or
+- issuing `UNSOUND` or `CONTRACT-BROKEN` for an unresolved interior merely from
+  failure to prove it.
+
+Failure to establish a required positive regional result is an atom failure. It
+is not by itself a hard error unless the report also makes one of the false
+affirmative or scope-changing claims above.
+
+### M authorities to verify before freezing
+
+Open each exact page and confirm the named description and Safety propositions,
+including all qualifications relevant to its exact release case:
+
+- `https://doc.rust-lang.org/1.80.0/std/ptr/fn.write.html`
+  — overwrites without reading or dropping the old value; `dst` must be valid
+  for writes and properly aligned.
+- `https://doc.rust-lang.org/1.81.0/std/ptr/fn.write.html`
+  — the same exact propositions for the separate 1.81.0 case.
+- `https://doc.rust-lang.org/1.80.0/std/ptr/fn.copy_nonoverlapping.html`
+  — copies `count * size_of::<T>()` bytes; source/destination validity,
+  alignment, and nonoverlap requirements; base case only.
+- `https://doc.rust-lang.org/1.80.0/reference/type-layout.html#primitive-data-layout`
+  — `u8` has size and alignment 1.
+- `https://doc.rust-lang.org/1.80.0/std/primitive.u8.html#impl-Copy-for-u8`
+  — `u8` implements `Copy` in the compatibility base case.
+- `https://doc.rust-lang.org/1.80.0/std/ptr/fn.read.html`
+  — reads without moving, leaves source unchanged, and requires read validity,
+  alignment, and initialization for this non-ZST.
+- `https://doc.rust-lang.org/1.80.0/std/primitive.u32.html#impl-Copy-for-u32`
+  — `u32` implements `Copy` in the 1.80.0 endpoint case.
+- `https://doc.rust-lang.org/1.82.0/std/ptr/fn.read.html`
+  — the same named propositions for the separate endpoint case.
+- `https://doc.rust-lang.org/1.82.0/std/primitive.u32.html#impl-Copy-for-u32`
+  — `u32` implements `Copy` in the 1.82.0 endpoint case.
+
+The `acknowledge` and compatibility results additionally consume the two exact
+accepted propositions in target file `TCB.md`; that file is not Rust authority
+and both admissions must remain identified as part of the conditional TCB.
diff --git a/evals/unsafe-rust/v3-targeted-plan.md b/evals/unsafe-rust/v3-targeted-plan.md
new file mode 100644
index 0000000000..e50aa8bc5e
--- /dev/null
+++ b/evals/unsafe-rust/v3-targeted-plan.md
@@ -0,0 +1,243 @@
+# Unsafe Rust V3 Targeted Confirmation Plan
+
+> **Evaluator-only material. Do not expose this file to evaluated agents.**
+>
+> **Preregistration status:** DRAFT. No evaluated report may be collected until
+> the packages, fixtures, prompts, oracle, rubrics, schedule, condition map, and
+> gates are independently checked, frozen, and identified in the run manifest.
+
+## Purpose
+
+This confirmatory evaluation tests whether the V3 skill revision reliably
+changes the specific proof behavior that prevented V2 from passing its strict
+release gates, while preserving the abstraction-design and general-audit
+behaviors that V2 already performed well.
+
+It tests mechanisms, not release readiness. Passing this evaluation permits a
+later broad release gate; it does not replace that gate.
+
+## Frozen candidate conditions
+
+The intended conditions are:
+
+| Condition | Package tree digest | `SKILL.md` digest | Role |
+|---|---|---|---|
+| V3 | `668f70202c7bc8f23f7f894fb784a9629fd292c7f6fe69ede815b0e4c10137bf` | `0e23f7747cc63014bade7543efaf745e7e9a7e5d6dee2a48c602ef7a3eba091e` | treatment |
+| V2 | `40b4171cc9daf7e51ba032aef52157a85a49c4c12cea8696deadb948e0867897` | `a0a75ef8a14497aa78b50b459981097ee99605c57fec95c637cf59aaa20fe766` | pre-change comparator |
+
+The comparison uses the coherent V2 package, not a synthetic deletion
+ablation. V3's changes are distributed across the core workflow, specialized
+references, and templates; deleting isolated passages would create a package
+that no maintainer proposes to ship. A no-skill baseline belongs in the later
+broad gate.
+
+## Design
+
+Use eight focused modes, two conditions, and five fresh replicates per cell:
+
+> 8 modes × 2 conditions × 5 replicates = 80 reports.
+
+Each evaluated agent receives one opaque package, one opaque target, and one
+empty output directory. Reports are randomized across conditions and modes.
+Condition identity is revealed only after reports have been preserved, hashed,
+blind-scored twice, and adjudicated.
+
+Five replicates are an engineering reliability minimum, not a population-level
+estimate of model behavior. The primary gates are exact per-replicate capability
+requirements; pooled averages and statistical significance cannot rescue a
+failure.
+
+## Modes
+
+### S — Symbolic interval and patch-release closure
+
+Tests preservation of a symbolic stable-release interval, membership of a
+non-`.0` patch release, rejection of sampled CI/toolchains as an inventory, and
+closure by a version-parametric proof over a justified superset.
+
+### C — Conflicting policies, conservative union, and exclusions
+
+Tests exact recovery of two nonlinear current policies, construction of a
+conservative audit domain without mislabeling it the project promise, a policy
+exclusion backed by effective rejection, and a parametric proof over a simple
+superset without Cartesian enumeration.
+
+### X — Conditional feature/target/allocator cross-product
+
+Tests recovery of an easily missed simultaneous configuration, distinction
+between a supported bad case and a genuinely enforced exclusion, and a complete
+region-scoped UB certificate.
+
+### Q — Existential refutation versus incomplete universal proof
+
+Pairs a complete valid-use UB witness, which must close as `UNSOUND`, with an
+unavailable third-party unsafe implementation, which must remain `UNPROVED`
+without fabricated UB or silent trust.
+
+### W — Whole-execution UB and behavioral contracts
+
+Tests that observations from an execution containing UB cannot establish a
+postcondition counterexample, while an independent UB-free wrong-result path
+can establish `CONTRACT-BROKEN`. Soundness and each behavioral theorem must be
+reported separately.
+
+### M — Multi-release affirmative certificates
+
+Tests the three admitted positive proof forms independently: a parametric proof,
+an exact exhaustive applicable partition, and an exact proposition-preserving
+compatibility premise. A fourth claim has endpoint-only evidence and must retain
+an `UNPROVED` interior. A cutoff, stability badge, or later documentation may
+not supply continuity or backward propagation.
+
+### R — Abstraction-redesign regression
+
+Tests literal current-artifact review of an unsafe abstraction backed by a
+caller-implementable safe trait, recovery of the minimum required capability,
+a parsimonious locally enforced redesign, compatibility analysis, and the
+firewall between an `UNSOUND` current artifact and an uncertified proposal.
+
+### K — Multi-issue regression control
+
+Tests adversarial caller-provided safe behavior, exposure of a materially
+reconstructed local proof, preservation of every clause in a published contract
+despite sparse visible consumers, continued coverage after the first aggregate
+UB witness, and non-certification of proposed repairs.
+
+The exact individually scored propositions are frozen in the oracle and copied
+into per-mode blind-scoring rubrics before collection.
+
+## Hypotheses
+
+- **H-domain:** V3 passes every S, C, and X atom in all five replicates with
+  zero hard errors.
+- **H-verdict:** V3 passes every Q and W atom in all five replicates with zero
+  hard errors.
+- **H-release:** V3 passes every M atom in all five replicates with zero hard
+  errors.
+- **H-regression:** V3 passes every R and K atom in all five replicates, with
+  zero proposal laundering and zero hard errors.
+
+## Primary gates
+
+The targeted confirmation passes only if all of the following hold:
+
+1. Every V3 semantic atom passes 5/5.
+2. V3 has zero hard errors.
+3. V3 has zero proposal laundering.
+4. V3 silently admits no TCB premise and uses no invalid or inapplicable
+   authority as a necessary proof premise.
+5. Every V3 report respects the frozen source-only scope and word budget.
+
+Failure of any primary gate fails the run. Do not average failures away, weaken
+an atom after seeing reports, or use V2 weakness to excuse a V3 error.
+
+## Secondary comparison
+
+After unblinding:
+
+- report V3 and V2 separately for every atom and mode;
+- require that no V3 atom has fewer passes than its matched V2 atom;
+- call V3 5/5 plus lower V2 performance evidence of targeted lift;
+- call matched 5/5 performance ceiling replication, not causal improvement;
+- do not pool heterogeneous modes into a headline score.
+
+## Global hard errors
+
+The frozen oracle may specialize these rules, but may not weaken them:
+
+- asserting full `PROVED` after contracting or failing to justify `Required`;
+- claiming closure without `Required ⊆ Covered`;
+- inventing policy precedence or calling a conservative audit domain the project
+  promise;
+- treating CI, endpoints, sparse documentation, a cutoff, or a stability badge
+  as interval coverage;
+- issuing `UNSOUND` without valid use, reachability, a false exact safety
+  proposition, and an applicable UB consequence;
+- issuing only `UNPROVED` after explicitly proving all four UB links;
+- issuing `CONTRACT-BROKEN` using only an execution containing UB;
+- claiming any observation remains guaranteed because it occurs before UB;
+- silently trusting a third-party unsafe implementation or caller-controlled
+  safe behavior;
+- certifying an unimplemented design or allowing it to narrow a current-artifact
+  obligation;
+- using an unchecked, invalid, or inapplicable authority as a necessary premise;
+- reading oracle, sibling, condition-map, prior-report, or evaluator material.
+
+A missed atom is not automatically a hard error. It becomes one only when it
+also satisfies a frozen hard-error definition, usually by making an affirmative
+false claim.
+
+## Evaluated-agent protocol
+
+Before collection, freeze and hash:
+
+- both package trees;
+- all target trees and opaque runtime copies;
+- the evaluated-agent prompt;
+- the oracle and per-mode scoring rubrics;
+- exact official documentation URLs or a byte-identified mirror;
+- the randomized schedule and condition map;
+- output schema, word budgets, tool policy, and rerun policy.
+
+Each report agent must:
+
+- be fresh and receive no prior conversation (`fork_turns="none"`);
+- audit exactly one cell without helper agents;
+- inspect only its opaque target, package, exact permitted official Rust/std
+  documentation, and empty output directory;
+- avoid building, testing, executing, or macro-expanding the target;
+- write one `report.md` and return the same report;
+- stay within 1,800 words, except that K receives the same preregistered
+  2,200-word cap in both conditions.
+
+Only genuine infrastructure failures may be rerun. Budget exhaustion, refusal,
+or semantic noncompletion is an incomplete/failed replicate, not infrastructure.
+Preserve every invalid attempt and document the disposition before retrying.
+
+## Blind scoring and adjudication
+
+After collection and before unblinding:
+
+1. Preserve and hash every raw report.
+2. Assign random anonymous labels independently within each mode.
+3. Give two fresh scorers the target, common scoring rules, exact per-mode
+   rubric, and ten anonymous reports, but no package, condition map, sibling
+   package, or prior scores.
+4. Score explicit propositions and valid derivations, not preferred terminology.
+5. Use a fresh adjudicator only for scorer disagreements.
+6. Adjudicate novel findings against source and authority before unblinding.
+7. Preserve raw scores, adjudications, ledgers, and all integrity checks.
+
+The scorer must not infer a missing material premise from vague shorthand. The
+rubric must state in advance which compact formulations count, especially where
+one conceptual defect admits multiple independently scored witnesses.
+
+## Oracle review
+
+Before the first report, two independent reviews must confirm:
+
+- each atom expresses one necessary proposition rather than a compound grading
+  preference;
+- the expected verdict follows from the exact source and claim;
+- every required Rust/std proposition is supported by the cited versioned
+  authority;
+- no target leaks its oracle, expected verdict, historical issue identity, or
+  condition;
+- positive fixtures are actually provable, not merely free of an obvious bug;
+- the V2 comparator is not penalized for terminology introduced only in V3;
+- shorthand and alternative correct proofs are accepted consistently.
+
+Any correction before collection changes fixture/oracle digests and is recorded
+as preregistration work. Any semantic correction after collection invalidates
+the affected mode for confirmatory use; it cannot be repaired in place.
+
+## Later broad release gate
+
+Run the broad gate only if this targeted confirmation passes. It must include
+the full abstraction-design and legacy suites, corrected V2 modes, historical
+vulnerable/fixed pairs, generated/configuration cases, authoring and repair,
+current zerocopy owning shards and integration, opaque holdouts, and matched V2
+and no-skill subsets. It retains zero hard errors, zero proposal laundering,
+focused zero-miss recovery, no repaired-side recurrence, and artifact-integrity
+requirements.
+