diff --git a/verification/aeneas/DESIGN.md b/verification/aeneas/DESIGN.md
index b9aa5b58cf..b1b28560ae 100644
--- a/verification/aeneas/DESIGN.md
+++ b/verification/aeneas/DESIGN.md
@@ -304,6 +304,92 @@ the library already models every part of Rust's abstract machine.
 
 ## Deferred decisions and reopening evidence
 
+### Resource-free layout and storage work
+
+The shared library supplies two independent foundations for layout and owned
+byte-cast proofs:
+
+- `Rust.Pointer.Value` retains an address, opaque optional provenance, and
+  metadata. Its casts and metadata operations preserve the exact provenance
+  value. Pointer equality observes address and metadata; it does not compare
+  provenance. Non-nullness supplies no alignment, liveness, or access permission.
+- `Rust.Storage.StorageDecoder` takes metadata explicitly, checks the requested
+  byte width, and checks that a successful raw result carries that metadata.
+  Fixed-width decoders adapt through unit metadata. Slice counts are inputs,
+  including for zero-sized elements; byte length cannot recover those counts.
+
+These are mathematical definitions and checked laws, not newly admitted Rust
+operations. The storage carrier still contains only initialized numeric bytes
+and uninitialized bytes. It does not encode pointers or decide where provenance
+lives in a pointer's representation. Pointer-bearing byte operations remain
+unsupported. Typed copies still require the treatment described in
+[the lowering audit](LOWERING_AUDIT.md), including
+[Aeneas issue #1405](https://github.com/AeneasVerif/aeneas/issues/1405).
+
+Byte-cast reasoning uses the existing distinction between language validity and
+optional mathematical admission. The source's `IntoBytes` law ranges over all
+accepted language representations, regardless of mathematical admission. The
+destination's intended `FromBytes` law must accept every initialized storage of
+the correct width at both stages. The shared cast lemma composes these laws for
+arbitrary represented bytes. It supplies no encoder and does not claim that a
+particular Rust transmutation follows this interpretation.
+
+The concrete `check_u32_slice_known_layout` Rust harness checks the actual
+`<[u32] as KnownLayout>::LAYOUT` initializer, its descriptor fields, and sizing
+for every element count, including checked-multiplication overflow. Admission
+visits the local constant's initializer body; no axiom supplies the descriptor.
+The visible guards expose the power-of-two and size-divisibility premises of
+the ABI reads. This checks that concrete numerical behavior, not the complete
+generic trait invariant. The proof also rejects an initializer changed from
+`for_slice` to `for_type`.
+
+The native capability fixtures under `tests/capabilities/` preserve the next
+translation boundaries. With the current pins, the generic `KnownLayout`
+fixture retains an associated-type equality that Aeneas rejects. A second
+fixture without an explicit caller-side equality fails on the trait's own
+`MaybeUninit` metadata equality. The production
+`transmute!` fixture retains its compile-time trait-check helper and a loop that
+Aeneas rejects. The required `FromBytes` declaration dependencies additionally
+reach the unsupported recursive `Invariants`/`Alignment` group. These failures
+are not successful extraction or completed Rust proofs. Do not delete bounds,
+equalities, or required declarations to make those targets extract. Required
+recursive declaration support is deferred; dependent work must wait for tools
+that support it.
+
+Native raw-pointer emission has a separate limitation. The pinned backend's
+carrier stores only `v : T`, and its scalar pointer cast returns `undef`.
+Emitted slice construction and `NonNull` operations remain external templates.
+The mathematical pointer model does not repair that carrier or grant admission
+to those operations. The existing checker continues to reject them. A faithful
+carrier and checked primitive interpretations are prerequisites for proving
+their address, metadata, or provenance behavior.
+
+When those boundaries are supported, bind `KnownLayout::LAYOUT` to the original
+Rust type and its metadata-indexed geometry. Reuse the complete recursive
+layout semantics, which preserves an inner field's padding before outer
+rounding. Preserve physical tail offset, stride, alignment, and conservative
+padding flags. Keep mathematical extent, `usize` representability, and the
+`isize` object-size restriction separate. The `MaybeUninit` obligation also
+requires identical metadata and layout and acceptance of uninitialized storage
+in every position; a layout-only theorem must not be presented as the full
+trait invariant.
+
+Concrete owned conversions use the actual standard transmute primitive for
+`u32` and four-byte arrays, plus a guarded `u8`-to-`bool` conversion. These types
+have no pointers, resources, destruction, or external-state invariants. Original
+Rust endpoint checks and a compiled canonical-provider audit restrict that
+interpretation to those cases; it does not admit the production macro or an
+arbitrary generic transmute. Invalid Boolean encodings take the forbidden path,
+even with postcondition `True`. Reference creation remains a later target because
+numerical geometry and provenance presence alone do not supply permissions or
+lifetimes. Derive
+proof requests are also deferred. Existing annotation discovery, native binding
+records, independent golden/live proofs, and dependency audits remain the sole
+route to reporting a Rust specification as checked; these foundations add no
+parallel coverage registry or automatic Rust ABI assumptions.
+
+### Other deferred decisions
+
 - **Canonical layout abstraction.** Retain structural `DstLayout` and existing
   `ModelViews` initially. Padding and trailing-size pilots already use those
   views. Use `extend`, sequence queries, and capacity contracts to compare total
@@ -325,8 +411,8 @@ the library already models every part of Rust's abstract machine.
   tactics, and the existing loop adapter. Introduce a larger lifting DSL,
   per-model tactics, or new loop abstraction only after concrete repeated
   failures show a net benefit over ordinary lemmas and a thin tactic.
-- **Broader carriers and effects.** Recursive nominal groups, indexed carriers,
-  const generics, associated-type trait laws, higher-ranked bounds, bounded
+- **Broader carriers and effects.** Recursive nominal groups, general indexed
+  carriers, const generics, associated-type trait laws, higher-ranked bounds, bounded
   nominal models, and escaping borrow reconstruction remain unsupported with
   explicit errors. The first trait-law bridge supports `Self`-only traits and
   simple generic bounds, with `Unaligned` and a total byte codec as checked
@@ -338,11 +424,12 @@ the library already models every part of Rust's abstract machine.
   execution, independently of ordinary library-model admission. A storage model
   must account for the translation's omissions as well as its primitives. The
   [pinned lowering audit](LOWERING_AUDIT.md) records known omissions and the
-  additional admission checks needed before making memory-safety claims.
-  [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) specifies the proposed closed
+  admission checks needed before making memory-safety claims.
+  [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) specifies the closed
   dependency traversal, controlled build origins using Charon's existing MIR
-  preservation setup, primitive rules, and mandatory CI path. These additional
-  checks are not implemented yet.
+  preservation setup, primitive rules, and mandatory CI path. CI enforces
+  these checks for the admitted fragment; extending that fragment requires
+  corresponding operation semantics and coverage checks.
   <!-- FIXME: Typed transfers lose storage events; track support at
   https://github.com/AeneasVerif/aeneas/issues/1405. Until then, a typed storage
   abstraction must forget all padding contents and initialization facts. It
diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index 174d79af6e..f54c86163f 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -390,6 +390,10 @@ padding inside packed fields.
 A positive size-sequence comparison establishes equal sizes for every natural
 metadata value; a negative result does not assert that the sequences differ.
 
+Cast validation and exact metadata inference establish error priority, exact
+splits and rejection of unattainable sizes. Intentional zero-stride panic is
+checked separately.
+
 Plain arithmetic clauses use mathematical word values carrying machine bounds
 and, for NonZero, positivity. They coerce to `Nat` or `Int` without unwrapping
 raw fields. Binding `let N : Nat := n` makes addition and remainder ordinary
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index 0c426e3c83..5d756948c4 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -1682,6 +1682,100 @@ def layout.DstLayout.requires_dynamic_padding
       then ok true
       else ok (¬ (i1 = 0#usize))
 
+/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::validate_cast_and_convert_metadata]:
+    Source: 'src/layout/mod.rs', lines 1839:4-1986:5 -/
+def layout.DstLayout.validate_cast_and_convert_metadata
+  (self : layout.DstLayout) (addr : Std.Usize) (bytes_len : Std.Usize)
+  (cast_type : layout.CastType) :
+  Result (core.result.Result (Std.Usize × Std.Usize) layout.MetadataCastError)
+  := do
+  let o ← layout.SizeInfoUsize.try_to_nonzero_elem_size self.size_info
+  match o with
+  | none => fail panic
+  | some size_info =>
+    let o1 ← lift (Usize.checked_add addr bytes_len)
+    let e := core.option.Option.is_some o1
+    massert e
+    let offset ←
+      match cast_type with
+      | layout.CastType.Prefix => ok 0#usize
+      | layout.CastType.Suffix => ok bytes_len
+    let i ← addr + offset
+    let i1 ←
+      core.num.nonzero.NonZero.get
+        Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner 
+        self.align
+    let i2 ← i % i1
+    if i2 != 0#usize
+    then ok (core.result.Result.Err layout.MetadataCastError.Alignment)
+    else
+      match size_info with
+      | layout.SizeInfo.Sized size =>
+        massert ((size > bytes_len) || (size <= bytes_len))
+        if size > bytes_len
+        then ok (core.result.Result.Err layout.MetadataCastError.Size)
+        else
+          match cast_type with
+          | layout.CastType.Prefix =>
+            ok (core.result.Result.Ok (0#usize, size))
+          | layout.CastType.Suffix =>
+            let split_at ← bytes_len - size
+            ok (core.result.Result.Ok (0#usize, split_at))
+      | layout.SizeInfo.SliceDst trailing =>
+        let o2 ←
+          layout.TrailingSliceLayout.max_trailing_bytes trailing bytes_len
+        match o2 with
+        | none => ok (core.result.Result.Err layout.MetadataCastError.Size)
+        | some bytes =>
+          let (elems, _) ←
+            layout.max_elems_for_bytes bytes trailing.elem_size
+          let size_align ←
+            layout.RoundingAlignAndPhase.align
+              trailing.size_rounding_align_and_phase
+          let i3 ←
+            core.num.nonzero.NonZero.get
+              Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+              trailing.elem_size
+          let unused_bytes ← bytes % i3
+          let unused_aligned_bytes ←
+            util.round_down_to_next_multiple_of_alignment unused_bytes
+              size_align
+          let i4 ← bytes_len - trailing.size_base
+          let max_rounded_bytes ←
+            util.round_down_to_next_multiple_of_alignment i4 size_align
+          let i5 ← max_rounded_bytes - unused_aligned_bytes
+          let self_bytes ← trailing.size_base + i5
+          massert (self_bytes <= bytes_len)
+          match cast_type with
+          | layout.CastType.Prefix =>
+            ok (core.result.Result.Ok (elems, self_bytes))
+          | layout.CastType.Suffix =>
+            let split_at ← bytes_len - self_bytes
+            ok (core.result.Result.Ok (elems, split_at))
+
+/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::metadata_for_exact_size]:
+    Source: 'src/layout/mod.rs', lines 1701:4-1724:5 -/
+def layout.DstLayout.metadata_for_exact_size
+  (self : layout.DstLayout) (size : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  match self.size_info with
+  | layout.SizeInfo.Sized _ => ok none
+  | layout.SizeInfo.SliceDst tsl =>
+    match tsl.elem_size.val with
+    | 0 => ok none
+    | _ =>
+      let r ←
+        layout.DstLayout.validate_cast_and_convert_metadata self 0#usize size
+          layout.CastType.Prefix
+      match r with
+      | core.result.Result.Ok p =>
+        let (elems, object_size) := p
+        if object_size = size
+        then ok (some elems)
+        else ok none
+      | core.result.Result.Err _ => ok none
+
 /-- [zerocopy::layout::nested_reference::round_up]:
     Source: 'src/layout/nested_reference.rs', lines 48:0-58:1 -/
 def layout.nested_reference.round_up
@@ -1889,6 +1983,14 @@ def layout.primitive_checks.check_empty_layout
     massert empty.statically_shallow_unpadded
   else ok ()
 
+/-- [zerocopy::{impl zerocopy::KnownLayout for [T]}::LAYOUT]
+    Source: 'src/lib.rs', lines 1123:4-1123:58
+    Visibility: public -/
+@[global_simps, irreducible]
+def Slice.Insts.ZerocopyKnownLayout.LAYOUT (T : Type)
+  : Result layout.DstLayout :=
+  layout.DstLayout.for_slice T
+
 /-- [zerocopy::layout::tail_checks::same_optional_usize]:
     Source: 'src/layout/tail_checks.rs', lines 29:0-35:1 -/
 def layout.tail_checks.same_optional_usize
@@ -1902,6 +2004,44 @@ def layout.tail_checks.same_optional_usize
     | none => ok false
     | some right1 => ok (left1 = right1)
 
+/-- [zerocopy::layout::primitive_checks::check_u32_slice_known_layout]:
+    Source: 'src/layout/primitive_checks.rs', lines 95:0-120:1 -/
+def layout.primitive_checks.check_u32_slice_known_layout
+  (elems : Std.Usize) : Result Unit := do
+  let size ← core.mem.size_of Std.U32
+  let align ← core.mem.align_of Std.U32
+  let b ← core.num.Usize.is_power_of_two align
+  if b
+  then
+    let i ← size % align
+    if i != 0#usize
+    then ok ()
+    else
+      let slice ← Slice.Insts.ZerocopyKnownLayout.LAYOUT Std.U32
+      let i1 ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+          slice.align
+      massert (i1 = align)
+      massert slice.statically_shallow_unpadded
+      match slice.size_info with
+      | layout.SizeInfo.Sized _ => fail panic
+      | layout.SizeInfo.SliceDst tail =>
+        massert (tail.offset = 0#usize)
+        massert (tail.elem_size = size)
+        massert (tail.size_base = 0#usize)
+        let i2 ←
+          core.num.nonzero.NonZero.get
+            Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+            tail.size_rounding_align_and_phase._0
+        massert (i2 = align)
+        let actual ←
+          layout.TrailingSliceLayoutUsize.size_for_elems tail elems
+        let expected ← lift (Usize.checked_mul elems size)
+        let b1 ← layout.tail_checks.same_optional_usize actual expected
+        massert b1
+  else ok ()
+
 /-- [zerocopy::layout::tail_checks::reference_round_up]:
     Source: 'src/layout/tail_checks.rs', lines 38:0-42:1 -/
 def layout.tail_checks.reference_round_up
@@ -1961,8 +2101,82 @@ def layout.tail_checks.reference_capacity
     let rounded_budget ← after_base - i1
     ok (Usize.checked_sub rounded_budget phase)
 
+/-- [zerocopy::layout::tail_checks::reference_metadata]:
+    Source: 'src/layout/tail_checks.rs', lines 78:0-104:1 -/
+def layout.tail_checks.reference_metadata
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (size : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  match runtime_layout.size_info with
+  | layout.SizeInfo.Sized _ => ok none
+  | layout.SizeInfo.SliceDst tail =>
+    if tail.elem_size = 0#usize
+    then ok none
+    else
+      let o ← layout.tail_checks.reference_capacity tail align phase size
+      match o with
+      | none => ok none
+      | some bytes =>
+        let elems ← bytes / tail.elem_size
+        let o1 ← layout.tail_checks.reference_size tail align phase elems
+        let b ← layout.tail_checks.same_optional_usize o1 (some size)
+        if b
+        then ok (some elems)
+        else ok none
+
+/-- [zerocopy::layout::tail_checks::reference_cast]:
+    Source: 'src/layout/tail_checks.rs', lines 107:0-154:1 -/
+def layout.tail_checks.reference_cast
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (addr : Std.Usize) (length : Std.Usize) (side : layout.CastType) :
+  Result (core.result.Result (Std.Usize × Std.Usize) layout.MetadataCastError)
+  := do
+  let anchor ←
+    match side with
+    | layout.CastType.Prefix => ok addr
+    | layout.CastType.Suffix => addr + length
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+      runtime_layout.align
+  let i1 ← anchor % i
+  if i1 != 0#usize
+  then ok (core.result.Result.Err layout.MetadataCastError.Alignment)
+  else
+    let candidate ←
+      match runtime_layout.size_info with
+      | layout.SizeInfo.Sized size =>
+        if size <= length
+        then ok (some (0#usize, size))
+        else ok none
+      | layout.SizeInfo.SliceDst tail =>
+        do
+        let o ← layout.tail_checks.reference_capacity tail align phase length
+        match o with
+        | none => ok none
+        | some bytes =>
+          let elems ← bytes / tail.elem_size
+          let o1 ← layout.tail_checks.reference_size tail align phase elems
+          match o1 with
+          | none => ok none
+          | some size => ok (some (elems, size))
+    match candidate with
+    | none => ok (core.result.Result.Err layout.MetadataCastError.Size)
+    | some p =>
+      let (elems, size) := p
+      match side with
+      | layout.CastType.Prefix => ok (core.result.Result.Ok p)
+      | layout.CastType.Suffix =>
+        let split ← length - size
+        ok (core.result.Result.Ok (elems, split))
+
 /-- [zerocopy::layout::tail_checks::trailing_arithmetic_check]:
-    Source: 'src/layout/tail_checks.rs', lines 88:0-111:1 -/
+    Source: 'src/layout/tail_checks.rs', lines 166:0-189:1 -/
 def layout.tail_checks.trailing_arithmetic_check
   (tail : layout.TrailingSliceLayout Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -1999,6 +2213,96 @@ def layout.tail_checks.trailing_arithmetic_check
     else ok ()
   else ok ()
 
+/-- [zerocopy::layout::tail_checks::layout_observations_check]:
+    Source: 'src/layout/tail_checks.rs', lines 204:0-247:1 -/
+def layout.tail_checks.layout_observations_check
+  (runtime_layout : layout.DstLayout)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (size : Std.Usize) (addr : Std.Usize) (length : Std.Usize)
+  (side : layout.CastType) :
+  Result Unit
+  := do
+  let (si, encoding_matches) ←
+    match runtime_layout.size_info with
+    | layout.SizeInfo.Sized _ => ok (runtime_layout.size_info, true)
+    | layout.SizeInfo.SliceDst tail =>
+      do
+      let i ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+      let b ← core.num.Usize.is_power_of_two i
+      let b1 ←
+        if b
+        then
+          if phase < i
+          then
+            do
+            let o ← lift (Usize.checked_add i phase)
+            let i1 ←
+              core.num.nonzero.NonZero.get
+                Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+                tail.size_rounding_align_and_phase._0
+            layout.tail_checks.same_optional_usize o (some i1)
+          else ok false
+        else ok false
+      ok (runtime_layout.size_info, b1)
+  if encoding_matches
+  then
+    let o ←
+      layout.DstLayout.metadata_for_exact_size
+        { runtime_layout with size_info := si } size
+    let o1 ←
+      layout.tail_checks.reference_metadata
+        { runtime_layout with size_info := si } align phase size
+    let b ← layout.tail_checks.same_optional_usize o o1
+    massert b
+    let nonzero_stride ←
+      match si with
+      | layout.SizeInfo.Sized _ => ok true
+      | layout.SizeInfo.SliceDst tail => ok (tail.elem_size != 0#usize)
+    let o2 ← lift (Usize.checked_add addr length)
+    let b1 := core.option.Option.is_some o2
+    if b1
+    then
+      if nonzero_stride
+      then
+        let actual ←
+          layout.DstLayout.validate_cast_and_convert_metadata
+            { runtime_layout with size_info := si } addr length side
+        let expected ←
+          layout.tail_checks.reference_cast
+            { runtime_layout with size_info := si } align phase addr length
+            side
+        let same ←
+          match actual with
+          | core.result.Result.Ok p =>
+            match expected with
+            | core.result.Result.Ok p1 =>
+              let (elems, split) := p
+              let (expected_elems, expected_split) := p1
+              if elems = expected_elems
+              then ok (split = expected_split)
+              else ok false
+            | core.result.Result.Err _ => ok false
+          | core.result.Result.Err mce =>
+            match expected with
+            | core.result.Result.Ok _ => ok false
+            | core.result.Result.Err mce1 =>
+              match mce with
+              | layout.MetadataCastError.Alignment =>
+                match mce1 with
+                | layout.MetadataCastError.Alignment => ok true
+                | layout.MetadataCastError.Size => ok false
+              | layout.MetadataCastError.Size =>
+                match mce1 with
+                | layout.MetadataCastError.Alignment => ok false
+                | layout.MetadataCastError.Size => ok true
+        massert same
+      else ok ()
+    else ok ()
+  else ok ()
+
 /-- [zerocopy::layout::tail_transform_checks::witness_matches]:
     Source: 'src/layout/tail_transform_checks.rs', lines 30:0-41:1 -/
 def layout.tail_transform_checks.witness_matches
diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean
index 0e63ebd96e..714facef25 100644
--- a/verification/aeneas/golden/Types.lean
+++ b/verification/aeneas/golden/Types.lean
@@ -232,6 +232,21 @@ structure layout.DstLayout where
   size_info : layout.SizeInfo Std.Usize
   statically_shallow_unpadded : Bool
 
+/-- [zerocopy::layout::CastType]
+    Source: 'src/layout/mod.rs', lines 913:0-916:1
+    Visibility: public -/
+@[discriminant isize]
+inductive layout.CastType where
+| Prefix : layout.CastType
+| Suffix : layout.CastType
+
+/-- [zerocopy::layout::MetadataCastError]
+    Source: 'src/layout/mod.rs', lines 920:0-923:1 -/
+@[discriminant isize]
+inductive layout.MetadataCastError where
+| Alignment : layout.MetadataCastError
+| Size : layout.MetadataCastError
+
 /-- [zerocopy::layout::nested_reference::NestedLayer]
     Source: 'src/layout/nested_reference.rs', lines 29:0-33:1 -/
 structure layout.nested_reference.NestedLayer where
diff --git a/verification/aeneas/lean/Corollaries.lean b/verification/aeneas/lean/Corollaries.lean
index f5ccc84d61..3c74904bff 100644
--- a/verification/aeneas/lean/Corollaries.lean
+++ b/verification/aeneas/lean/Corollaries.lean
@@ -166,4 +166,15 @@ theorem padding_matches_recursive (tail : layout.TrailingSliceLayout Usize)
   dsimp only [remaining, physical] at hcancel
   omega
 
+theorem validate_zero_stride (self : layout.DstLayout) (tail : layout.TrailingSliceLayout Usize)
+    (hs : self.size_info = .SliceDst tail) (he : tail.elem_size = 0#usize)
+    (addr length : Usize) (side : layout.CastType) :
+    layout.DstLayout.validate_cast_and_convert_metadata self addr length side = .fail .panic := by
+  have hp := Proofs.Raw.try_nonzero_spec self.size_info
+  obtain ⟨converted, hconverted, hv⟩ := WP.spec_imp_exists hp
+  simp only [hs, he, if_true] at hv
+  unfold layout.DstLayout.validate_cast_and_convert_metadata
+  rw [hconverted, hv]
+  simp only [bind_ok]
+
 end Zerocopy.Corollaries
diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean
index bbcb36f971..87586631af 100644
--- a/verification/aeneas/lean/LayoutModel.lean
+++ b/verification/aeneas/lean/LayoutModel.lean
@@ -16,8 +16,9 @@ public import LayoutMath
 /-!
 Extracted records contain machine words and compressed rounding encodings.
 This module gives those records ordinary mathematical observations: a size
-formula, a physical slice offset, and field placement. The definitions do not
-call an extracted operation or assume that it is correct.
+formula, a physical slice offset, field placement, and cast or metadata
+outcomes. The definitions do not call an extracted operation or assume that
+it is correct.
 
 Proofs uses the raw observations to state implementation lemmas and
 independent expectations. ModelViews exposes corresponding observations of
@@ -65,6 +66,48 @@ def fieldAlignment (field : layout.DstLayout) (packed : Option NonZeroUsize) : N
 def placement (size : Usize) (field : layout.DstLayout) (packed : Option NonZeroUsize) :=
   LayoutMath.roundUp size.val (fieldAlignment field packed)
 
+def castSide (cast : layout.CastType) (length : Nat) : Nat :=
+  match cast with | .Prefix => 0 | .Suffix => length
+
+def castSplit (cast : layout.CastType) (length size : Nat) : Nat :=
+  match cast with | .Prefix => size | .Suffix => length - size
+
+/- Describe exact cast outcomes independently of the implementation. Alignment
+errors have priority; a suffix checks the end address; successful trailing
+casts return the greatest fitting metadata and the corresponding physical
+split.
+-/
+def castSpec (self : layout.DstLayout) (addr length : Nat) (cast : layout.CastType)
+    (result : core.result.Result (Usize × Usize) layout.MetadataCastError) : Prop :=
+  let anchor := addr + castSide cast length
+  match result with
+  | .Err .Alignment => anchor % self.align.val.val ≠ 0
+  | .Err .Size => anchor % self.align.val.val = 0 ∧
+    match self.size_info with
+    | .Sized size => length < size.val
+    | .SliceDst tail => ∀ n : Nat, length < (trailingFormula tail).size n
+  | .Ok (elems, split) => anchor % self.align.val.val = 0 ∧
+    match self.size_info with
+    | .Sized size => elems.val = 0 ∧ size.val ≤ length ∧
+      split.val = castSplit cast length size.val
+    | .SliceDst tail => (trailingFormula tail).size elems.val ≤ length ∧
+      (∀ n : Nat, (trailingFormula tail).size n ≤ length ↔ n ≤ elems.val) ∧
+      split.val = castSplit cast length ((trailingFormula tail).size elems.val)
+
+/- Describe exact-size metadata, including failure when no count has that
+complete size. On a rounding plateau, success must select the greatest count;
+fixed layouts and zero element strides have no inferred trailing metadata.
+-/
+def metadataSpec (self : layout.DstLayout) (size : Nat) (r : Option Usize) : Prop :=
+  match self.size_info with
+  | .Sized _ => r = none
+  | .SliceDst tail =>
+    if tail.elem_size.val = 0 then r = none else
+    match r with
+    | none => ∀ n : Nat, (trailingFormula tail).size n ≠ size
+    | some elems => (trailingFormula tail).size elems.val = size ∧
+      (∀ n : Nat, (trailingFormula tail).size n ≤ size ↔ n ≤ elems.val)
+
 /- Project the raw record to the fragment vocabulary used by layout operations.
 This preserves alignment, payload, physical offset, stride, and unpadded
 flag.
@@ -89,6 +132,8 @@ is an explicit operation domain, not a consequence of NonZeroUsize alone.
 -/
 def alignmentDomain (a : Nat) : Prop := a.isPowerOfTwo ∧ a ≤ 2 ^ 29
 
+attribute [contract_simps] castSide castSplit castSpec metadataSpec
+
 end Zerocopy.Proofs
 
 -- Mathematical projections consume the one recursively decoded record. The
diff --git a/verification/aeneas/lean/MathViews.lean b/verification/aeneas/lean/MathViews.lean
index bfb06410d0..5700db3e06 100644
--- a/verification/aeneas/lean/MathViews.lean
+++ b/verification/aeneas/lean/MathViews.lean
@@ -120,6 +120,24 @@ def layoutValid (self : layout.DstLayout) : Prop :=
   change (isValid self.align ∧ isValid self.size_info ∧ isValid self.statically_shallow_unpadded) ↔ _
   simp only [nonzero_valid_iff, size_info_valid_iff, bool_valid_iff, and_true]
 
+@[simp, contract_simps] theorem cast_type_valid_iff (side : layout.CastType) : isValid side ↔ True := by
+  cases side <;>
+    simp [isValid, RustModel.decode, layout.CastType.aeneasModel,
+      layout.CastType.decode, layout.CastType.decodeFields]
+
+@[simp, contract_simps] theorem metadata_error_valid_iff (error : layout.MetadataCastError) :
+    isValid error ↔ True := by
+  cases error <;>
+    simp [isValid, RustModel.decode, layout.MetadataCastError.aeneasModel,
+      layout.MetadataCastError.decode, layout.MetadataCastError.decodeFields]
+
+@[simp, contract_simps] theorem cast_result_valid_iff
+    (r : core.result.Result (Usize × Usize) layout.MetadataCastError) : isValid r ↔ True := by
+  cases r <;> simp [result_valid_iff]
+
+attribute [contract_simps] option_valid_iff prod_valid_iff result_valid_iff
+  list_valid_iff slice_valid_iff
+
 @[contract_simps] theorem scalar_admitted_iff (x : UScalar ty) :
     (∃ value, RustModel.decode x = some value) ↔ True := scalar_valid_iff x
 
@@ -141,6 +159,12 @@ def layoutValid (self : layout.DstLayout) : Prop :=
 @[contract_simps] theorem bool_admitted_iff (x : Bool) :
     (∃ value, RustModel.decode x = some value) ↔ True := bool_valid_iff x
 
+@[contract_simps] theorem cast_type_admitted_iff (x : layout.CastType) :
+    (∃ value, RustModel.decode x = some value) ↔ True := cast_type_valid_iff x
+
+@[contract_simps] theorem cast_result_admitted_iff (x : core.result.Result (Usize × Usize) layout.MetadataCastError) :
+    (∃ value, RustModel.decode x = some value) ↔ True := cast_result_valid_iff x
+
 @[contract_simps] theorem option_admitted_iff {α : Type} [RustModel α] (x : Option α) :
     (∃ value : Option (ModelOf α), RustModel.decode x = some value) ↔
       ∀ v ∈ x, isValid v := option_valid_iff x
@@ -189,8 +213,6 @@ def layoutValid (self : layout.DstLayout) : Prop :=
 @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) :
     Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff
 
-attribute [contract_simps] option_valid_iff prod_valid_iff result_valid_iff
-
 attribute [contract_simps] and_true true_and and_self true_implies forall_true_iff
 attribute [contract_simps] encodingValid trailingValid sizeInfoValid layoutValid
 
diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean
index 3002b1cad9..01ffe7113a 100644
--- a/verification/aeneas/lean/Obligations.lean
+++ b/verification/aeneas/lean/Obligations.lean
@@ -348,6 +348,61 @@ def requires_dynamic_padding_spec : Prop :=
     requires_dynamic_padding_spec_contract self
       (layout.DstLayout.requires_dynamic_padding self)
 
+def validate_cast_spec_contract
+    (self : layout.DstLayout) (addr length : Usize) (side : layout.CastType)
+    (run : Result (core.result.Result (Usize × Usize) layout.MetadataCastError)) : Prop :=
+  layoutValid self →
+    0 < self.align.val.val → addr.val + length.val ≤ Usize.max →
+    (match self.size_info with
+      | .Sized _ => True
+      | .SliceDst t => 0 < t.size_rounding_align_and_phase._0.val.val ∧ 0 < t.elem_size.val) →
+    ∃ r, run = .ok r ∧
+      -- State the expected cases independently of the inline outcome helper.
+      let anchor := addr.val + (match side with | .Prefix => 0 | .Suffix => length.val)
+      match r with
+      | .Err .Alignment => anchor % self.align.val.val ≠ 0
+      | .Err .Size => anchor % self.align.val.val = 0 ∧
+        match self.size_info with
+        | .Sized bytes => length.val < bytes.val
+        | .SliceDst tail => ∀ n : Nat, length.val < (trailingFormula tail).size n
+      | .Ok (elems, split) => anchor % self.align.val.val = 0 ∧
+        match self.size_info with
+        | .Sized bytes => elems.val = 0 ∧ bytes.val ≤ length.val ∧
+          split.val = (match side with
+            | .Prefix => bytes.val
+            | .Suffix => length.val - bytes.val)
+        | .SliceDst tail => (trailingFormula tail).size elems.val ≤ length.val ∧
+          (∀ n : Nat, (trailingFormula tail).size n ≤ length.val ↔ n ≤ elems.val) ∧
+          split.val = (match side with
+            | .Prefix => (trailingFormula tail).size elems.val
+            | .Suffix => length.val - (trailingFormula tail).size elems.val)
+
+def validate_cast_spec : Prop :=
+  ∀ (self : layout.DstLayout) (addr length : Usize) (side : layout.CastType),
+    validate_cast_spec_contract self addr length side
+      (layout.DstLayout.validate_cast_and_convert_metadata self addr length side)
+
+def metadata_exact_spec_contract (self : layout.DstLayout) (size : Usize)
+    (run : Result (Option Usize)) : Prop :=
+  layoutValid self → 0 < self.align.val.val →
+    (match self.size_info with
+      | .Sized _ => True
+      | .SliceDst t => t.elem_size.val ≠ 0 → 0 < t.size_rounding_align_and_phase._0.val.val) →
+    ∃ r, run = .ok r ∧
+      -- Pin exact size and maximal metadata without sharing the inline predicate.
+      match self.size_info with
+      | .Sized _ => r = none
+      | .SliceDst tail =>
+        if tail.elem_size.val = 0 then r = none else
+        match r with
+        | none => ∀ n : Nat, (trailingFormula tail).size n ≠ size.val
+        | some elems => (trailingFormula tail).size elems.val = size.val ∧
+          (∀ n : Nat, (trailingFormula tail).size n ≤ size.val ↔ n ≤ elems.val)
+
+def metadata_exact_spec : Prop :=
+  ∀ (self : layout.DstLayout) (size : Usize),
+    metadata_exact_spec_contract self size (layout.DstLayout.metadata_for_exact_size self size)
+
 
 end Zerocopy.Obligations
 
@@ -383,4 +438,12 @@ def empty_layout_checks_spec : Prop :=
   ∀ repr_align, empty_layout_checks_spec_contract repr_align
     (layout.primitive_checks.check_empty_layout repr_align)
 
+def u32_slice_known_layout_checks_spec_contract (_elems : Usize)
+    (run : Result Unit) : Prop :=
+  run ⦃ _ => True ⦄
+
+def u32_slice_known_layout_checks_spec : Prop :=
+  ∀ elems, u32_slice_known_layout_checks_spec_contract elems
+    (layout.primitive_checks.check_u32_slice_known_layout elems)
+
 end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/Obligations/TailChecks.lean b/verification/aeneas/lean/Obligations/TailChecks.lean
index 4fb4d750e6..8e271fb901 100644
--- a/verification/aeneas/lean/Obligations/TailChecks.lean
+++ b/verification/aeneas/lean/Obligations/TailChecks.lean
@@ -30,4 +30,15 @@ def trailing_arithmetic_check_spec : Prop :=
     trailing_arithmetic_check_spec_contract tail align phase elems budget
       (layout.tail_checks.trailing_arithmetic_check tail align phase elems budget)
 
+def layout_observations_check_spec_contract
+    (runtime_layout : layout.DstLayout) (align : NonZeroUsize)
+    (phase size addr length : Usize) (side : layout.CastType)
+    (run : Result Unit) : Prop :=
+  layoutValid runtime_layout → 0 < align.val.val → run ⦃ _ => True ⦄
+
+def layout_observations_check_spec : Prop :=
+  ∀ runtime_layout align phase size addr length side,
+    layout_observations_check_spec_contract runtime_layout align phase size addr length side
+      (layout.tail_checks.layout_observations_check runtime_layout align phase size addr length side)
+
 end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/OutcomeTests.lean b/verification/aeneas/lean/OutcomeTests.lean
new file mode 100644
index 0000000000..b3cf7db109
--- /dev/null
+++ b/verification/aeneas/lean/OutcomeTests.lean
@@ -0,0 +1,124 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import LayoutModel
+public import Mathlib.Tactic.NormNum
+@[expose] public section
+
+/-!
+Proof verification is only useful if the supplied outcome predicate rejects
+wrong answers. These numerical examples challenge the independent cast and
+metadata predicates directly: error priority, prefix versus suffix anchors,
+maximum metadata on padded-size plateaus, and zero-stride behavior. They do
+not run the extracted functions; they check what the predicates mean.
+-/
+open Aeneas Aeneas.Std Zerocopy Zerocopy.Proofs
+
+namespace Zerocopy.OutcomeTests
+
+-- Numerical boundary cases independently pin the inline outcome predicates.
+def fixedEight : layout.DstLayout :=
+  { align := ⟨4#usize⟩, size_info := .Sized 8#usize,
+    statically_shallow_unpadded := false }
+
+def plateauTail : layout.TrailingSliceLayout Usize :=
+  { offset := 0#usize, elem_size := 1#usize, size_base := 0#usize,
+    size_rounding_align_and_phase := ⟨⟨4#usize⟩⟩ }
+
+def plateauFour : layout.DstLayout :=
+  { align := ⟨4#usize⟩, size_info := .SliceDst plateauTail,
+    statically_shallow_unpadded := true }
+
+def zeroStride : layout.DstLayout :=
+  { plateauFour with size_info := .SliceDst { plateauTail with elem_size := 0#usize } }
+
+-- Incorrect Sized metadata is excluded even when the size and split fit.
+theorem rejects_wrong_sized_elems :
+    ¬ castSpec fixedEight 0 20 .Prefix (.Ok (1#usize, 8#usize)) := by
+  norm_num [castSpec, fixedEight, castSide, castSplit]
+
+-- Prefix and suffix splits differ when length is larger than twice the size.
+theorem rejects_wrong_prefix_split :
+    ¬ castSpec fixedEight 0 20 .Prefix (.Ok (0#usize, 12#usize)) := by
+  norm_num [castSpec, fixedEight, castSide, castSplit]
+
+theorem rejects_wrong_suffix_split :
+    ¬ castSpec fixedEight 0 20 .Suffix (.Ok (0#usize, 8#usize)) := by
+  norm_num [castSpec, fixedEight, castSide, castSplit]
+
+theorem admits_correct_suffix_split :
+    castSpec fixedEight 0 20 .Suffix (.Ok (0#usize, 12#usize)) := by
+  norm_num [castSpec, fixedEight, castSide, castSplit]
+
+-- Misalignment has priority over insufficient size.
+theorem rejects_wrong_error_priority :
+    ¬ castSpec fixedEight 1 0 .Prefix (.Err .Size) := by
+  norm_num [castSpec, fixedEight, castSide]
+
+theorem admits_alignment_before_size :
+    castSpec fixedEight 1 0 .Prefix (.Err .Alignment) := by
+  norm_num [castSpec, fixedEight, castSide]
+
+-- A suffix uses the end address: 1+3 is aligned even though 1 is not.
+theorem rejects_wrong_suffix_anchor :
+    ¬ castSpec fixedEight 1 3 .Suffix (.Err .Alignment) := by
+  norm_num [castSpec, fixedEight, castSide]
+
+theorem admits_suffix_size_error :
+    castSpec fixedEight 1 3 .Suffix (.Err .Size) := by
+  norm_num [castSpec, fixedEight, castSide]
+
+-- One element fits at length 4, but metadata must be the greatest fitting 4.
+theorem rejects_nonmaximal_cast_metadata :
+    ¬ castSpec plateauFour 0 4 .Prefix (.Ok (1#usize, 4#usize)) := by
+  intro h
+  have hmaximum := h.2.2.1 4
+  norm_num [trailingFormula, byteFormula, plateauFour, plateauTail,
+    LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp,
+    show Nat.log2 4 = 2 by decide] at hmaximum
+
+
+theorem rejects_fixed_metadata :
+    ¬ metadataSpec fixedEight 8 (some 1#usize) := by
+  simp [metadataSpec, fixedEight]
+
+theorem admits_no_fixed_metadata : metadataSpec fixedEight 8 none := by
+  simp [metadataSpec, fixedEight]
+
+theorem rejects_zero_stride_metadata :
+    ¬ metadataSpec zeroStride 4 (some 1#usize) := by
+  simp [metadataSpec, zeroStride, plateauFour, plateauTail]
+
+-- Returning none is incorrect when n=4 has exact complete size 4.
+theorem rejects_absent_exact_metadata :
+    ¬ metadataSpec plateauFour 4 none := by
+  intro h
+  have hmissing := h 4
+  norm_num [trailingFormula, byteFormula, plateauFour, plateauTail,
+    LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp,
+    show Nat.log2 4 = 2 by decide] at hmissing
+
+-- Exact complete size alone does not suffice on a padded-size plateau.
+theorem rejects_nonmaximal_exact_metadata :
+    ¬ metadataSpec plateauFour 4 (some 1#usize) := by
+  intro h
+  have hmaximum := h.2 4
+  norm_num [trailingFormula, byteFormula, plateauFour, plateauTail,
+    LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp,
+    show Nat.log2 4 = 2 by decide] at hmaximum
+
+theorem rejects_inexact_metadata :
+    ¬ metadataSpec plateauFour 3 (some 3#usize) := by
+  intro h
+  have hexact := h.1
+  norm_num [trailingFormula, byteFormula, plateauFour, plateauTail,
+    LayoutMath.Formula.size, LayoutMath.Formula.bytes, LayoutMath.roundUp,
+    show Nat.log2 4 = 2 by decide] at hexact
+
+end Zerocopy.OutcomeTests
diff --git a/verification/aeneas/lean/Proofs/Contracts.lean b/verification/aeneas/lean/Proofs/Contracts.lean
index 49a14110e0..fead244b30 100644
--- a/verification/aeneas/lean/Proofs/Contracts.lean
+++ b/verification/aeneas/lean/Proofs/Contracts.lean
@@ -8,6 +8,7 @@ those terms. -/
 
 module
 public import Proofs.Raw.Trailing
+public import Proofs.Raw.Cast
 public import Proofs.Raw.Construction
 @[expose] public section
 
@@ -223,6 +224,50 @@ theorem requires_dynamic_padding_spec : Zerocopy.Specs.requires_dynamic_padding_
   | SliceDst _ => simpa only [hs] using hv.2
 register_spec_step requires_dynamic_padding_spec
 
+/- Prove exact metadata inference, including rejection of unattainable sizes and
+greatest-count selection when several counts share the same padded size.
+-/
+theorem metadata_exact_spec : Zerocopy.Specs.metadata_exact_spec := by
+  unfold Zerocopy.Specs.metadata_exact_spec
+  representation_simps
+  intro self size hv
+  have ht : match self.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => tail.elem_size.val ≠ 0 →
+        0 < tail.size_rounding_align_and_phase._0.val.val := by
+    cases hs : self.size_info with
+    | Sized _ => trivial
+    | SliceDst tail =>
+      simp only [hs] at hv
+      intro _
+      exact hv.2
+  apply WP.spec_mono (Raw.metadata_exact_spec self size hv.1 ht)
+  intro result facts
+  refine ⟨?_, facts⟩
+  change isValid result
+  simp
+register_spec_step metadata_exact_spec
+
+/- Track alignment-error priority, complete-size capacity, and prefix/suffix
+splitting through the actual branches. A zero trailing stride intentionally
+panics and therefore lies outside this total contract's required domain.
+-/
+theorem validate_cast_spec : Zerocopy.Specs.validate_cast_spec := by
+  unfold Zerocopy.Specs.validate_cast_spec
+  representation_simps
+  intro self addr length side hv hroom helem
+  have ht : match self.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val ∧
+        0 < tail.elem_size.val := by
+    cases hs : self.size_info with
+    | Sized _ => trivial
+    | SliceDst tail =>
+      simp only [hs] at hv helem
+      exact ⟨hv.2, helem⟩
+  exact Raw.validate_cast_spec self addr length side hv.1 hroom ht
+register_spec_step validate_cast_spec
+
 end Zerocopy.Proofs
 
 namespace Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/PrimitiveChecks.lean b/verification/aeneas/lean/Proofs/PrimitiveChecks.lean
index 9413da9e7f..8196553cec 100644
--- a/verification/aeneas/lean/Proofs/PrimitiveChecks.lean
+++ b/verification/aeneas/lean/Proofs/PrimitiveChecks.lean
@@ -8,6 +8,7 @@ those terms. -/
 
 module
 public import Proofs
+public import Proofs.TailReference
 @[expose] public section
 
 /-!
@@ -66,6 +67,71 @@ theorem empty_layout_checks (repr_align : Option NonZeroUsize) :
       simp [ha, hs, hp, massert, UScalar.val]
     · simp only [WP.spec_ok]
 
+/- Follow the actual built-in associated-constant initializer. This proves
+the concrete numerical assertions without assuming a KnownLayout trait law.
+-/
+theorem u32_slice_known_layout_checks (elems : Usize) :
+    layout.primitive_checks.check_u32_slice_known_layout elems ⦃ _ => True ⦄ := by
+  classical
+  let size : Usize := if U32 = Usize then
+    { bv := BitVec.ofNat _ (System.Platform.numBits / 8) } else RustLayout.size U32
+  let align := RustLayout.align U32
+  have hs : core.mem.size_of U32 = .ok size := rfl
+  have ha : core.mem.align_of U32 = .ok align := rfl
+  unfold layout.primitive_checks.check_u32_slice_known_layout
+  rw [hs, ha]
+  simp only [bind_ok]
+  step as ⟨enabled, he⟩
+  split
+  · rename_i yes
+    have power : align.val.isPowerOfTwo := Eq.mp he yes
+    have positive := Nat.pos_of_isPowerOfTwo power
+    step with Usize.rem_spec size (y := align) (by omega) as ⟨remainder, hr⟩
+    simp only [UScalar.eq_equiv, UScalar.ofNatCore_val_eq]
+    split
+    · simp only [WP.spec_ok]
+    · rename_i divisible
+      have remainder_zero : remainder = 0#usize := by
+        simpa only [bne_iff_ne, not_not] using divisible
+      have multiple : size.val % align.val = 0 := by
+        change remainder.val = size.val % align.val at hr
+        rw [remainder_zero] at hr
+        simpa only [UScalar.ofNatCore_val_eq] using hr.symm
+      unfold Slice.Insts.ZerocopyKnownLayout.LAYOUT
+      step with for_slice_spec U32 size align hs ha power as
+        ⟨slice, hsa, hsp, tail, hsi, ho, hel, hb, hc⟩
+      simp [core.num.nonzero.NonZero.get, hsa, hsp, hsi, ho, hel, hb,
+        align, size, massert]
+      have same : tail.size_rounding_align_and_phase._0.val = align :=
+        UScalar.eq_of_val_eq hc
+      simp [same, align]
+      have encoded_positive : 0 < tail.size_rounding_align_and_phase._0.val.val := by
+        rw [same]
+        exact positive
+      have formula := TailChecks.witness_view tail ⟨align⟩ 0#usize power
+        (by simpa using positive) (by simpa using hc)
+      step with size_for_elems_spec tail elems encoded_positive as ⟨actual, actual_value⟩
+      have product_aligned : (elems.val * size.val) % align.val = 0 := by
+        simp [Nat.mul_mod, multiple]
+      have size_formula : (trailingFormula tail).size elems.val = elems.val * size.val := by
+        rw [formula]
+        simp only [TailChecks.witnessFormula, LayoutMath.Formula.size,
+          LayoutMath.Formula.bytes, hb, hel, UScalar.ofNatCore_val_eq,
+          Nat.zero_add]
+        change LayoutMath.roundUp (elems.val * size.val) align.val = elems.val * size.val
+        exact LayoutMath.roundUp_eq _ _ product_aligned
+      have actual_expected : actual = Usize.checked_mul elems size :=
+        TailChecks.optional_value_injective (by
+          simp only [LayoutMath.Formula.checkedSize, size_formula] at actual_value
+          simpa only [TailChecks.checkedNat] using
+            actual_value.trans (TailChecks.checked_mul_value elems size).symm)
+      simp only [lift, bind_ok]
+      step with TailChecks.same_optional_usize actual (Usize.checked_mul elems size) as
+        ⟨same_result, result_iff⟩
+      have same_true := result_iff.mpr actual_expected
+      simp only [same_true, if_true, WP.spec_ok]
+  · simp only [WP.spec_ok]
+
 end Zerocopy.Proofs.Raw
 
 namespace Zerocopy.Proofs
@@ -82,4 +148,10 @@ theorem empty_layout_checks_spec : Specs.empty_layout_checks_spec := by
   intro _ _
   exact ⟨(), rfl, trivial⟩
 
+theorem u32_slice_known_layout_checks_spec : Specs.u32_slice_known_layout_checks_spec := by
+  intro elems _ _
+  apply WP.spec_mono (Raw.u32_slice_known_layout_checks elems)
+  intro _ _
+  exact ⟨(), rfl, trivial⟩
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/Raw/Cast.lean b/verification/aeneas/lean/Proofs/Raw/Cast.lean
new file mode 100644
index 0000000000..9dcb4b0427
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/Raw/Cast.lean
@@ -0,0 +1,283 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+This file may not be copied, modified, or distributed except according to
+those terms. -/
+
+module
+public import Proofs.Raw.Trailing
+public import Proofs.Raw.Layout
+import all Mathlib.Data.Nat.Log
+import all Init.Data.Nat.Power2.Basic
+@[expose] public section
+
+open Aeneas Aeneas.Std
+namespace Zerocopy.Proofs.Raw
+
+set_option linter.unusedVariables false
+theorem cast_offset_spec (cast : layout.CastType) (length : Usize) :
+    (match cast with | .Prefix => Result.ok 0#usize | .Suffix => Result.ok length)
+      ⦃ offset => offset.val = castSide cast length.val ∧ offset ≤ length ⦄ := by
+  cases cast <;> simp [castSide, WP.spec_ok]
+
+theorem cast_split_spec (cast : layout.CastType) (length size elems : Usize)
+    (h : size.val ≤ length.val) :
+    (match cast with
+      | .Prefix => Result.ok (core.result.Result.Ok (elems, size))
+      | .Suffix => do
+        let split ← length - size
+        Result.ok (core.result.Result.Ok (elems, split)) :
+      Result (core.result.Result (Usize × Usize) layout.MetadataCastError))
+      ⦃ r => ∃ split, r = .Ok (elems, split) ∧
+        split.val = castSplit cast length.val size.val ⦄ := by
+  cases cast with
+  | Prefix => exact WP.spec.ret ⟨size, rfl, rfl⟩
+  | Suffix =>
+    step with Usize.sub_spec h as ⟨split, hs, _⟩
+    exact ⟨split, rfl, hs⟩
+
+/- Track alignment-error priority, complete-size capacity, and prefix/suffix
+splitting through the actual branches. A zero trailing stride intentionally
+panics and therefore lies outside this total contract's required domain.
+-/
+theorem validate_cast_spec :
+  ∀ (self : layout.DstLayout) (addr bytes_len : Usize) (cast_type : layout.CastType), ∀ (ha : (0 < self.align.val.val : Prop)), ∀ (hroom : (addr.val + bytes_len.val ≤ Usize.max : Prop)), ∀ (ht : (match self.size_info with
+    | .Sized _ => True
+    | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val ∧ 0 < tail.elem_size.val : Prop)),
+    @Zerocopy.layout.DstLayout.validate_cast_and_convert_metadata self addr bytes_len cast_type ⦃ r => castSpec self addr.val bytes_len.val cast_type r ⦄ := by
+  intro self addr length cast ha hroom ht
+  unfold layout.DstLayout.validate_cast_and_convert_metadata
+  cases hs : self.size_info with
+  | Sized size =>
+    step with try_nonzero_spec (.Sized size) as ⟨converted, hconverted⟩
+    rw [hconverted]
+    step as ⟨checked, haddr⟩
+    cases checked with
+    | none => simp only [] at haddr; omega
+    | some ending =>
+      simp only [] at haddr
+      simp only [Option.isSome_some, massert, if_true, bind_ok]
+      step with cast_offset_spec cast length as ⟨offset, ho, hle⟩
+      have hlen := (UScalar.le_equiv _ _).mp hle
+      step with Usize.add_spec (x := addr) (y := offset) (by omega) as ⟨aligned, haligned⟩
+      simp only [core.num.nonzero.NonZero.get, bind_ok]
+      step with Usize.rem_spec aligned (y := self.align.val) (by omega) as ⟨rem, hr⟩
+      simp only [bne_iff_ne]
+      split
+      · rename_i hne
+        apply WP.spec.ret
+        unfold castSpec
+        have hv : rem.val ≠ 0 := by
+          intro h
+          apply hne
+          exact (UScalar.eq_equiv _ _).mpr h
+        rw [hr, haligned, ho] at hv
+        exact hv
+      · rename_i heq
+        have hzero : (addr.val + castSide cast length.val) % self.align.val.val = 0 := by
+          have h : rem = 0#usize := not_ne_iff.mp heq
+          have hv := congrArg UScalar.val h
+          rw [hr, haligned, ho] at hv
+          exact hv
+        have htotal : (decide (size > length) || decide (size ≤ length)) = true := by
+          simp only [Bool.or_eq_true, decide_eq_true_eq]
+          exact lt_or_ge length size
+        simp only [UScalar.lt_equiv, UScalar.le_equiv] at htotal ⊢
+        simp only [htotal, if_true, bind_ok]
+        split
+        · rename_i hbig
+          apply WP.spec.ret
+          simp only [castSpec, hs]
+          exact ⟨hzero, hbig⟩
+        · rename_i hsmall
+          step with cast_split_spec cast length size 0#usize (by omega) as ⟨r, split, hr, hv⟩
+          rw [hr]
+          simp only [castSpec, hs, show (0#usize).val = 0 by simp]
+          exact ⟨hzero, trivial, by omega, hv⟩
+  | SliceDst tail =>
+    simp only [hs] at ht
+    step with try_nonzero_spec (.SliceDst tail) as ⟨converted, hconverted⟩
+    have hne : tail.elem_size ≠ 0#usize := by
+      intro h
+      have hv := congrArg UScalar.val h
+      change tail.elem_size.val = 0 at hv
+      omega
+    simp only [hne, if_false] at hconverted
+    obtain ⟨t, hconverted, hoffset, hbase, hcode, helem⟩ := hconverted
+    rw [hconverted]
+    step as ⟨checked, haddr⟩
+    cases checked with
+    | none => simp only [] at haddr; omega
+    | some ending =>
+      simp only [] at haddr
+      simp only [Option.isSome_some, massert, if_true, bind_ok]
+      step with cast_offset_spec cast length as ⟨offset, ho, hle⟩
+      have hlen := (UScalar.le_equiv _ _).mp hle
+      step with Usize.add_spec (x := addr) (y := offset) (by omega) as ⟨aligned, haligned⟩
+      simp only [core.num.nonzero.NonZero.get, bind_ok]
+      step with Usize.rem_spec aligned (y := self.align.val) (by omega) as ⟨rem, hr⟩
+      simp only [bne_iff_ne]
+      split
+      · rename_i hne
+        apply WP.spec.ret
+        unfold castSpec
+        have hv : rem.val ≠ 0 := by
+          intro h
+          apply hne
+          exact (UScalar.eq_equiv _ _).mpr h
+        rw [hr, haligned, ho] at hv
+        exact hv
+      · rename_i heq
+        have hzero : (addr.val + castSide cast length.val) % self.align.val.val = 0 := by
+          have h : rem = 0#usize := not_ne_iff.mp heq
+          have hv := congrArg UScalar.val h
+          rw [hr, haligned, ho] at hv
+          exact hv
+        have htn : 0 < t.size_rounding_align_and_phase._0.val.val := by rw [hcode]; exact ht.1
+        have hte : 0 < t.elem_size.val.val := by rw [helem]; exact ht.2
+        have hview : byteFormula t = byteFormula tail := by simp only [byteFormula, hbase, hcode, hoffset]
+        step with max_trailing_bytes_spec t length htn as ⟨capacity, hc⟩
+        rw [hview] at hc
+        cases capacity with
+        | none =>
+          have hmiss := LayoutMath.capacity_spec (byteFormula tail) length.val (Nat.two_pow_pos _)
+          rw [← hc] at hmiss
+          apply WP.spec.ret
+          refine ⟨hzero, ?_⟩
+          simp only [hs]
+          intro n
+          exact hmiss (n * tail.elem_size.val)
+        | some capacity =>
+          dsimp only
+          step with max_elems_for_bytes_spec capacity t.elem_size hte as ⟨elems, used, hen, _, _, _, _⟩
+          step with encoding_align_spec t.size_rounding_align_and_phase htn as ⟨a, ha⟩
+          have hav : a.val.val = (trailingFormula tail).align := by
+            simpa only [trailingFormula, byteFormula, hcode] using ha
+          step with Usize.rem_spec capacity (y := t.elem_size.val) (by omega) as ⟨unused, hu⟩
+          have hap : a.val.val.isPowerOfTwo := ⟨_, by simpa only [hcode] using ha⟩
+          step with round_down_spec unused a hap as ⟨unused_aligned, _, huf, _, _, _⟩
+          have hcap : (trailingFormula tail).capacity length.val = some capacity.val := hc.symm
+          have hmax := LayoutMath.maximal_metadata _ _ _ ht.2 hcap (trailing_align_pos tail)
+          have hfit : (trailingFormula tail).size elems.val ≤ length.val := by
+            apply (hmax elems.val).mpr
+            rw [hen, helem]
+            exact le_rfl
+          have hmin := (LayoutMath.capacity_spec (trailingFormula tail) length.val (trailing_align_pos tail))
+          rw [hcap] at hmin
+          have hminfit := (hmin 0).mpr (by omega)
+          have hbfit : t.size_base.val ≤ length.val := by
+            rw [hbase]
+            simp only [trailingFormula, byteFormula, LayoutMath.Formula.bytes] at hminfit
+            omega
+          step with Usize.sub_spec hbfit as ⟨available, hb, _⟩
+          step with round_down_spec available a hap as ⟨budget, _, hbudget, _, _, _⟩
+          have hused := LayoutMath.capacity_object_size (trailingFormula tail) length.val capacity.val
+            (trailing_align_pos tail) hcap
+          change (trailingFormula tail).size (capacity.val / tail.elem_size.val) =
+            tail.size_base.val + (length.val - tail.size_base.val -
+              (length.val - tail.size_base.val) % (trailingFormula tail).align) -
+              (capacity.val % tail.elem_size.val -
+                capacity.val % tail.elem_size.val % (trailingFormula tail).align) at hused
+          rw [← hav, ← hbase] at hused
+          have hunused : unused.val = capacity.val % tail.elem_size.val := by rw [hu, helem]
+          have hbval : budget.val = length.val - t.size_base.val -
+              (length.val - t.size_base.val) % a.val.val := by rw [hbudget, hb]
+          have hus : unused_aligned.val ≤ budget.val := by
+            have hmod := Nat.mod_le capacity.val tail.elem_size.val
+            have hcapval : capacity.val = length.val - t.size_base.val -
+                (length.val - t.size_base.val) % a.val.val - (trailingFormula tail).phase := by
+              unfold LayoutMath.Formula.capacity at hcap
+              simp only [hminfit, if_true, Option.some.injEq] at hcap
+              have hav' : a.val.val = 2 ^ tail.size_rounding_align_and_phase._0.val.val.log2 := hav
+              simpa only [trailingFormula, byteFormula, ← hav', ← hbase] using hcap.symm
+            rw [huf, hbval, hunused]
+            omega
+          step with Usize.sub_spec hus as ⟨remaining, hremaining, _⟩
+          have hsum : t.size_base.val + remaining.val ≤ Usize.max := by
+            have hlenfit : length.val ≤ Usize.max := by scalar_tac
+            rw [hremaining]
+            have hbudget_bound : budget.val ≤ length.val - t.size_base.val := by rw [hbval]; omega
+            omega
+          step with Usize.add_spec (x := t.size_base) (y := remaining) hsum as ⟨size, hsize⟩
+          have hexact : size.val = (trailingFormula tail).size elems.val := by
+            rw [hen, helem]
+            rw [hused]
+            rw [hsize, hremaining, huf, hunused, hbval]
+            rw [huf, hunused, hbval] at hus
+            omega
+          have hsizefit : size ≤ length := (UScalar.le_equiv _ _).mpr (by rw [hexact]; exact hfit)
+          simp only [hsizefit, if_true, bind_ok]
+          step with cast_split_spec cast length size elems (by rw [hexact]; exact hfit) as ⟨r, split, hr, hv⟩
+          rw [hr]
+          simp only [castSpec, hs]
+          refine ⟨hzero, hfit, ?_, ?_⟩
+          · intro n
+            rw [hmax n, hen, helem]
+            rfl
+          · simpa only [hexact] using hv
+
+/- Prove exact metadata inference, including rejection of unattainable sizes and
+greatest-count selection when several counts share the same padded size.
+-/
+theorem metadata_exact_spec :
+  ∀ (self : layout.DstLayout) (size : Usize), ∀ (ha : (0 < self.align.val.val : Prop)), ∀ (ht : (match self.size_info with
+    | .Sized _ => True
+    | .SliceDst tail => tail.elem_size.val ≠ 0 →
+      0 < tail.size_rounding_align_and_phase._0.val.val : Prop)),
+    @Zerocopy.layout.DstLayout.metadata_for_exact_size self size ⦃ r => metadataSpec self size.val r ⦄ := by
+  intro self size ha ht
+  unfold layout.DstLayout.metadata_for_exact_size
+  cases hs : self.size_info with
+  | Sized s => simp only [WP.spec_ok, metadataSpec, hs]
+  | SliceDst tail =>
+    simp only [hs] at ht ⊢
+    cases hz : tail.elem_size.val with
+    | zero =>
+      simp only [WP.spec_ok, metadataSpec, hs, hz, if_true]
+    | succ k =>
+      simp only []
+      have he : 0 < tail.elem_size.val := by omega
+      have hn : tail.elem_size.val ≠ 0 := by omega
+      step with validate_cast_spec self 0#usize size .Prefix ha (by scalar_tac)
+        (by simp only [hs]; exact ⟨ht hn, he⟩) as ⟨cast, hc⟩
+      cases cast with
+      | Err err =>
+        cases err with
+        | Alignment =>
+          simp only [castSpec, castSide, Nat.zero_add, Nat.zero_mod,
+            ] at hc
+          exact False.elim (hc rfl)
+        | Size =>
+          simp only [castSpec, castSide, hs,
+            Nat.zero_add, Nat.zero_mod, true_and] at hc
+          apply WP.spec.ret
+          simp only [metadataSpec, hs, hn, if_false]
+          intro n h
+          have := hc n
+          omega
+      | Ok pair =>
+        rcases pair with ⟨elems, bytes⟩
+        change (if bytes = size then Result.ok (some elems) else Result.ok none)
+          ⦃ r => metadataSpec self size.val r ⦄
+        simp only [castSpec, castSide, castSplit, hs,
+          Nat.zero_add, Nat.zero_mod, true_and] at hc
+        split
+        · rename_i hsame
+          apply WP.spec.ret
+          simp only [metadataSpec, hs, hn, if_false]
+          have hbytes := congrArg UScalar.val hsame
+          exact ⟨by omega, hc.2.1⟩
+        · rename_i hdiff
+          apply WP.spec.ret
+          simp only [metadataSpec, hs, hn, if_false]
+          intro n h
+          have hle : n ≤ elems.val := (hc.2.1 n).mp (by omega)
+          have hmono := LayoutMath.Formula.size_mono (trailingFormula tail)
+            (trailing_align_pos tail) hle
+          apply hdiff
+          apply (UScalar.eq_equiv _ _).mpr
+          omega
+
+end Zerocopy.Proofs.Raw
diff --git a/verification/aeneas/lean/Proofs/TailChecks.lean b/verification/aeneas/lean/Proofs/TailChecks.lean
index 2323571ddc..c4d9d6657a 100644
--- a/verification/aeneas/lean/Proofs/TailChecks.lean
+++ b/verification/aeneas/lean/Proofs/TailChecks.lean
@@ -68,6 +68,150 @@ theorem trailing_arithmetic_check (tail : layout.TrailingSliceLayout Usize)
     · simp only [WP.spec_ok]
   · simp only [WP.spec_ok]
 
+theorem encoding_guard_spec (runtime_layout : layout.DstLayout)
+    (align : NonZeroUsize) (phase : Usize) :
+    (match (generalizing := false) runtime_layout.size_info with
+      | .Sized _ => Result.ok (runtime_layout.size_info, true)
+      | .SliceDst tail => do
+        let power ← core.num.Usize.is_power_of_two align.val
+        let code_matches ←
+          if power then
+            if phase < align.val then
+              do
+              let encoded ← lift (Usize.checked_add align.val phase)
+              layout.tail_checks.same_optional_usize encoded (some tail.size_rounding_align_and_phase._0.val)
+            else Result.ok false
+          else Result.ok false
+        Result.ok (runtime_layout.size_info, code_matches)) ⦃ pair =>
+      pair.1 = runtime_layout.size_info ∧
+        (pair.2 = true → witnessMatches runtime_layout align phase) ⦄ := by
+  cases info_eq : runtime_layout.size_info with
+  | Sized bytes => simp [WP.spec_ok, witnessMatches, info_eq]
+  | SliceDst tail =>
+    step as ⟨power, power_iff⟩
+    split
+    · rename_i power_true
+      have power_fact : align.val.val.isPowerOfTwo := Eq.mp power_iff power_true
+      simp only [UScalar.lt_equiv]
+      split
+      · rename_i phase_lt
+        step as ⟨encoded, encoded_facts⟩
+        step with same_optional_usize encoded
+          (some tail.size_rounding_align_and_phase._0.val) as ⟨code_matches, matches_iff⟩
+        simp only [WP.spec_ok, Prod.fst, Prod.snd, witnessMatches, info_eq]
+        intro matches_true
+        have same_code := matches_iff.mp matches_true
+        rw [same_code] at encoded_facts
+        exact ⟨power_fact, phase_lt, encoded_facts.2.1⟩
+      · simp [bind_ok, WP.spec_ok]
+    · simp [bind_ok, WP.spec_ok]
+
+theorem witness_positive (runtime_layout : layout.DstLayout)
+    (align : NonZeroUsize) (phase : Usize)
+    (witness : witnessMatches runtime_layout align phase) :
+    match runtime_layout.size_info with
+    | .Sized _ => True
+    | .SliceDst tail => 0 < tail.size_rounding_align_and_phase._0.val.val := by
+  cases info_eq : runtime_layout.size_info with
+  | Sized bytes => trivial
+  | SliceDst tail =>
+    simp only [witnessMatches, info_eq] at witness
+    have positive := Nat.pos_of_isPowerOfTwo witness.1
+    omega
+
+theorem layout_observations_check (runtime_layout : layout.DstLayout)
+    (align : NonZeroUsize) (phase size addr length : Usize) (side : layout.CastType)
+    (layout_positive : 0 < runtime_layout.align.val.val) (align_positive : 0 < align.val.val) :
+    layout.tail_checks.layout_observations_check runtime_layout align phase size addr length side ⦃ _ => True ⦄ := by
+  unfold layout.tail_checks.layout_observations_check
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  change (Aeneas.Std.bind (match (generalizing := false) runtime_layout.size_info with
+      | .Sized _ => Result.ok (runtime_layout.size_info, true)
+      | .SliceDst tail => do
+        let power ← core.num.Usize.is_power_of_two align.val
+        let code_matches ←
+          if power then
+            if phase < align.val then
+              do
+              let encoded ← lift (Usize.checked_add align.val phase)
+              layout.tail_checks.same_optional_usize encoded (some tail.size_rounding_align_and_phase._0.val)
+            else Result.ok false
+          else Result.ok false
+        Result.ok (runtime_layout.size_info, code_matches)) _) ⦃ _ ⦄
+  step with encoding_guard_spec runtime_layout align phase as ⟨info, code_matches, same_info, when_matches⟩
+  subst info
+  split
+  · rename_i matches_true
+    have witness := when_matches matches_true
+    have positive := witness_positive runtime_layout align phase witness
+    have meta_domain : match runtime_layout.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => tail.elem_size.val ≠ 0 → 0 < tail.size_rounding_align_and_phase._0.val.val := by
+      cases info_eq : runtime_layout.size_info with
+      | Sized bytes => trivial
+      | SliceDst tail =>
+        simp only [info_eq] at positive ⊢
+        intro nonzero
+        exact positive
+    step with Zerocopy.Proofs.Raw.metadata_exact_spec runtime_layout size layout_positive meta_domain
+      as ⟨actual_metadata, actual_metadata_spec⟩
+    step with reference_metadata runtime_layout align phase size align_positive witness
+      as ⟨expected_metadata, expected_metadata_spec⟩
+    have metadata_same := metadata_unique runtime_layout size.val actual_metadata expected_metadata
+      actual_metadata_spec expected_metadata_spec
+    step with same_optional_usize actual_metadata expected_metadata as ⟨same_metadata, same_metadata_iff⟩
+    have metadata_true := same_metadata_iff.mpr metadata_same
+    simp only [massert, metadata_true, if_true, bind_ok]
+    cases info_eq : runtime_layout.size_info with
+    | Sized bytes =>
+      simp only [info_eq, bind_ok]
+      have updated_eq : { runtime_layout with size_info := .Sized bytes } = runtime_layout := by
+        rw [← info_eq]
+      rw [updated_eq]
+      step as ⟨ending, ending_facts⟩
+      cases ending with
+      | none => simp [Option.isSome, WP.spec_ok]
+      | some ending =>
+        simp only [] at ending_facts
+        simp only [Option.isSome, if_true]
+        have room : addr.val + length.val ≤ Usize.max := ending_facts.1
+        step with Zerocopy.Proofs.Raw.validate_cast_spec runtime_layout addr length side layout_positive room
+          (by simp only [info_eq]) as ⟨actual, actual_spec⟩
+        step with reference_cast runtime_layout align phase addr length side layout_positive align_positive room witness
+          (by simp only [info_eq]) as ⟨expected, expected_spec⟩
+        have same := cast_unique runtime_layout addr.val length.val side actual expected actual_spec expected_spec
+        subst expected
+        cases actual with
+        | Ok pair => rcases pair with ⟨elems, split⟩; simp [massert, WP.spec_ok]
+        | Err error => cases error <;> simp [massert, WP.spec_ok]
+    | SliceDst tail =>
+      simp only [info_eq, bind_ok]
+      simp only [info_eq] at positive
+      have updated_eq : { runtime_layout with size_info := .SliceDst tail } = runtime_layout := by
+        rw [← info_eq]
+      rw [updated_eq]
+      step as ⟨ending, ending_facts⟩
+      cases ending with
+      | none => simp [Option.isSome, WP.spec_ok]
+      | some ending =>
+        simp only [] at ending_facts
+        simp only [Option.isSome, if_true, bne_iff_ne]
+        split
+        · rename_i stride_nonzero
+          have stride : 0 < tail.elem_size.val := by scalar_tac
+          have room : addr.val + length.val ≤ Usize.max := ending_facts.1
+          step with Zerocopy.Proofs.Raw.validate_cast_spec runtime_layout addr length side layout_positive room
+            (by simpa only [info_eq] using And.intro positive stride) as ⟨actual, actual_spec⟩
+          step with reference_cast runtime_layout align phase addr length side layout_positive align_positive room witness
+            (by simpa only [info_eq] using stride) as ⟨expected, expected_spec⟩
+          have same := cast_unique runtime_layout addr.val length.val side actual expected actual_spec expected_spec
+          subst expected
+          cases actual with
+          | Ok pair => rcases pair with ⟨elems, split⟩; simp [massert, WP.spec_ok]
+          | Err error => cases error <;> simp [massert, WP.spec_ok]
+        · simp only [WP.spec_ok]
+  · simp only [WP.spec_ok]
+
 end Zerocopy.Proofs.Raw.TailChecks
 
 namespace Zerocopy.Proofs
@@ -80,4 +224,16 @@ theorem trailing_arithmetic_check_spec : Specs.trailing_arithmetic_check_spec :=
   intro result facts
   exact ⟨(), rfl, trivial⟩
 
+theorem layout_observations_check_spec : Specs.layout_observations_check_spec := by
+  unfold Specs.layout_observations_check_spec
+  intro runtime_layout align phase size addr length side runtime_value runtime_decoded
+    align_value align_decoded phase_value phase_decoded size_value size_decoded
+    addr_value addr_decoded length_value length_decoded side_value side_decoded
+  have runtime_valid := (layout_valid_iff runtime_layout).mp ⟨runtime_value, runtime_decoded⟩
+  have align_valid := (nonzero_valid_iff align).mp ⟨align_value, align_decoded⟩
+  apply WP.spec_mono (Raw.TailChecks.layout_observations_check runtime_layout align phase size addr length side
+    runtime_valid.1 align_valid)
+  intro result facts
+  exact ⟨(), rfl, trivial⟩
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/TailReference.lean b/verification/aeneas/lean/Proofs/TailReference.lean
index 6357054a1c..0bd38440a5 100644
--- a/verification/aeneas/lean/Proofs/TailReference.lean
+++ b/verification/aeneas/lean/Proofs/TailReference.lean
@@ -234,4 +234,252 @@ theorem reference_capacity (tail : layout.TrailingSliceLayout Usize)
       congr 1
       omega
 
+theorem metadata_unique (runtime_layout : layout.DstLayout) (size : Nat)
+    (left right : Option Usize)
+    (left_spec : metadataSpec runtime_layout size left)
+    (right_spec : metadataSpec runtime_layout size right) : left = right := by
+  cases info_eq : runtime_layout.size_info with
+  | Sized bytes =>
+    simp only [metadataSpec, info_eq] at left_spec right_spec
+    rw [left_spec, right_spec]
+  | SliceDst tail =>
+    by_cases zero : tail.elem_size.val = 0
+    · simp only [metadataSpec, info_eq, zero, if_true] at left_spec right_spec
+      rw [left_spec, right_spec]
+    · simp only [metadataSpec, info_eq, zero, if_false] at left_spec right_spec
+      cases left with
+      | none =>
+        cases right with
+        | none => rfl
+        | some right => exact False.elim (left_spec right.val right_spec.1)
+      | some left =>
+        cases right with
+        | none => exact False.elim (right_spec left.val left_spec.1)
+        | some right =>
+          have le_right := (right_spec.2 left.val).mp (by omega)
+          have le_left := (left_spec.2 right.val).mp (by omega)
+          congr 1
+          exact UScalar.eq_of_val_eq (by omega)
+
+theorem cast_unique (runtime_layout : layout.DstLayout) (addr length : Nat)
+    (side : layout.CastType)
+    (left right : core.result.Result (Usize × Usize) layout.MetadataCastError)
+    (left_spec : castSpec runtime_layout addr length side left)
+    (right_spec : castSpec runtime_layout addr length side right) : left = right := by
+  cases left with
+  | Ok left =>
+    rcases left with ⟨left_elems, left_split⟩
+    cases right with
+    | Err error =>
+      cases error with
+      | Alignment => exact False.elim (right_spec left_spec.1)
+      | Size =>
+        cases info_eq : runtime_layout.size_info with
+        | Sized bytes => simp only [castSpec, info_eq] at left_spec right_spec; omega
+        | SliceDst tail =>
+          simp only [castSpec, info_eq] at left_spec right_spec
+          have miss := right_spec.2 left_elems.val
+          omega
+    | Ok right =>
+      rcases right with ⟨right_elems, right_split⟩
+      cases info_eq : runtime_layout.size_info with
+      | Sized bytes =>
+        simp only [castSpec, info_eq] at left_spec right_spec
+        have elems_eq : left_elems = right_elems := UScalar.eq_of_val_eq (by omega)
+        have split_eq : left_split = right_split := UScalar.eq_of_val_eq (by omega)
+        rw [elems_eq, split_eq]
+      | SliceDst tail =>
+        simp only [castSpec, info_eq] at left_spec right_spec
+        have le_right := (right_spec.2.2.1 left_elems.val).mp left_spec.2.1
+        have le_left := (left_spec.2.2.1 right_elems.val).mp right_spec.2.1
+        have elems_eq : left_elems = right_elems := UScalar.eq_of_val_eq (by omega)
+        have split_eq : left_split = right_split := UScalar.eq_of_val_eq (by
+          rw [elems_eq] at left_spec
+          omega)
+        rw [elems_eq, split_eq]
+  | Err left_error =>
+    cases right with
+    | Ok right =>
+      rcases right with ⟨right_elems, right_split⟩
+      cases left_error with
+      | Alignment => exact False.elim (left_spec right_spec.1)
+      | Size =>
+        cases info_eq : runtime_layout.size_info with
+        | Sized bytes => simp only [castSpec, info_eq] at left_spec right_spec; omega
+        | SliceDst tail =>
+          simp only [castSpec, info_eq] at left_spec right_spec
+          have miss := left_spec.2 right_elems.val
+          omega
+    | Err right_error =>
+      cases left_error <;> cases right_error <;> simp_all [castSpec]
+
+theorem reference_cast (runtime_layout : layout.DstLayout) (align : NonZeroUsize)
+    (phase addr length : Usize) (side : layout.CastType)
+    (layout_positive : 0 < runtime_layout.align.val.val)
+    (align_positive : 0 < align.val.val)
+    (room : addr.val + length.val ≤ Usize.max)
+    (witness : witnessMatches runtime_layout align phase)
+    (stride : match runtime_layout.size_info with | .Sized _ => True | .SliceDst t => 0 < t.elem_size.val) :
+    layout.tail_checks.reference_cast runtime_layout align phase addr length side ⦃ result =>
+      castSpec runtime_layout addr.val length.val side result ⦄ := by
+  have anchor_spec : (match side with
+      | .Prefix => Result.ok addr
+      | .Suffix => addr + length) ⦃ anchor => anchor.val = addr.val + castSide side length.val ⦄ := by
+    cases side with
+    | Prefix => simp [WP.spec_ok, castSide]
+    | Suffix =>
+      apply WP.spec_mono (Usize.add_spec (x := addr) (y := length) room)
+      intro result facts
+      simpa only [castSide] using facts
+  unfold layout.tail_checks.reference_cast
+  change ((match side with
+    | .Prefix => Result.ok addr
+    | .Suffix => addr + length) >>= _) ⦃ result => castSpec runtime_layout addr.val length.val side result ⦄
+  step with anchor_spec as ⟨anchor, anchor_value⟩
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  step with Usize.rem_spec anchor (y := runtime_layout.align.val) (by omega) as ⟨remainder, remainder_value⟩
+  rw [anchor_value] at remainder_value
+  simp only [bne_iff_ne, UScalar.eq_equiv, UScalar.ofNatCore_val_eq]
+  split
+  · rename_i not_aligned
+    simp only [ne_eq, UScalar.eq_equiv, UScalar.ofNatCore_val_eq] at not_aligned
+    apply WP.spec.ret
+    change (addr.val + castSide side length.val) % runtime_layout.align.val.val ≠ 0
+    rwa [← remainder_value]
+  · rename_i aligned
+    simp only [ne_eq, not_not, UScalar.eq_equiv, UScalar.ofNatCore_val_eq] at aligned
+    have anchor_aligned : (addr.val + castSide side length.val) % runtime_layout.align.val.val = 0 := by omega
+    cases info_eq : runtime_layout.size_info with
+    | Sized size =>
+      simp only [info_eq, bind_ok]
+      split
+      · rename_i size_fits
+        have fits : size.val ≤ length.val := (UScalar.le_equiv _ _).mp size_fits
+        cases side with
+        | Prefix =>
+          simp only [bind_ok, WP.spec_ok, castSpec, info_eq, castSplit, UScalar.ofNatCore_val_eq]
+          exact ⟨anchor_aligned, rfl, fits, rfl⟩
+        | Suffix =>
+          step with Usize.sub_spec (x := length) (y := size) fits as ⟨split, split_value⟩
+          simp only [castSpec, info_eq, castSplit, UScalar.ofNatCore_val_eq]
+          exact ⟨anchor_aligned, trivial, fits, split_value⟩
+      · rename_i size_misses
+        simp only [bind_ok, WP.spec_ok, castSpec, info_eq]
+        exact ⟨anchor_aligned, by scalar_tac⟩
+    | SliceDst tail =>
+      simp only [witnessMatches, info_eq] at witness
+      simp only [info_eq] at stride ⊢
+      have formula_eq := witness_view tail align phase witness.1 witness.2.1 witness.2.2
+      let f := witnessFormula tail align phase
+      step with reference_capacity tail align phase length align_positive as ⟨capacity, capacity_value⟩
+      have capacity_spec := LayoutMath.capacity_spec f length.val align_positive
+      cases capacity with
+      | none =>
+        simp only [Option.map_none] at capacity_value
+        rw [← capacity_value] at capacity_spec
+        simp only [bind_ok, WP.spec_ok, castSpec, info_eq]
+        refine ⟨anchor_aligned, ?_⟩
+        intro n
+        rw [formula_eq]
+        exact capacity_spec (n * tail.elem_size.val)
+      | some capacity =>
+        simp only [Option.map_some] at capacity_value
+        step with Usize.div_spec capacity (y := tail.elem_size) (by omega) as ⟨elems, elems_value⟩
+        have greatest : ∀ n, f.size n ≤ length.val ↔ n ≤ elems.val := by
+          have maximal := LayoutMath.maximal_metadata f length.val capacity.val stride
+            capacity_value.symm align_positive
+          simpa only [f, witnessFormula, elems_value] using maximal
+        have selected_fits := (greatest elems.val).mpr (by rfl)
+        have checked_fits : f.size elems.val ≤ Usize.max := by scalar_tac
+        step with reference_size tail align phase elems align_positive as ⟨selected_size, selected_value⟩
+        have selected_exact : selected_size.map UScalar.val = some (f.size elems.val) := by
+          change selected_size.map UScalar.val = f.checkedSize Usize.max elems.val at selected_value
+          simpa only [LayoutMath.Formula.checkedSize, checked_fits, if_true] using selected_value
+        cases selected_size with
+        | none => cases selected_exact
+        | some selected_size =>
+          have size_value : selected_size.val = f.size elems.val := Option.some.inj selected_exact
+          have fits : selected_size.val ≤ length.val := by rw [size_value]; exact selected_fits
+          change selected_size.val = (witnessFormula tail align phase).size elems.val at size_value
+          cases side with
+          | Prefix =>
+            simp only [bind_ok, WP.spec_ok, castSpec, info_eq, castSplit]
+            rw [formula_eq]
+            exact ⟨anchor_aligned, selected_fits, greatest, size_value⟩
+          | Suffix =>
+            simp only [bind_ok]
+            step with Usize.sub_spec (x := length) (y := selected_size) fits as ⟨split, split_value⟩
+            simp only [castSpec, info_eq, castSplit]
+            rw [formula_eq]
+            exact ⟨anchor_aligned, selected_fits, greatest, by omega⟩
+
+theorem reference_metadata (runtime_layout : layout.DstLayout) (align : NonZeroUsize)
+    (phase size : Usize) (align_positive : 0 < align.val.val)
+    (witness : witnessMatches runtime_layout align phase) :
+    layout.tail_checks.reference_metadata runtime_layout align phase size ⦃ result =>
+      metadataSpec runtime_layout size.val result ⦄ := by
+  unfold layout.tail_checks.reference_metadata
+  cases info_eq : runtime_layout.size_info with
+  | Sized bytes => simp only [WP.spec_ok, metadataSpec, info_eq]
+  | SliceDst tail =>
+    simp only [witnessMatches, info_eq] at witness
+    have formula_eq := witness_view tail align phase witness.1 witness.2.1 witness.2.2
+    let f := witnessFormula tail align phase
+    simp only [info_eq, UScalar.eq_equiv, UScalar.ofNatCore_val_eq]
+    split
+    · rename_i zero
+      simp only [WP.spec_ok, metadataSpec, info_eq, zero, if_true]
+    · rename_i nonzero
+      have stride : 0 < tail.elem_size.val := by omega
+      step with reference_capacity tail align phase size align_positive as ⟨capacity, capacity_value⟩
+      have capacity_spec := LayoutMath.capacity_spec f size.val align_positive
+      cases capacity with
+      | none =>
+        simp only [Option.map_none] at capacity_value
+        rw [← capacity_value] at capacity_spec
+        simp only [WP.spec_ok, metadataSpec, info_eq, nonzero, if_false]
+        intro n exact_size
+        have misses := capacity_spec (n * tail.elem_size.val)
+        rw [formula_eq] at exact_size
+        change size.val < f.size n at misses
+        change f.size n = size.val at exact_size
+        omega
+      | some capacity =>
+        simp only [Option.map_some] at capacity_value
+        step with Usize.div_spec capacity (y := tail.elem_size) (by omega) as ⟨elems, elems_value⟩
+        have greatest : ∀ n, f.size n ≤ size.val ↔ n ≤ elems.val := by
+          have maximal := LayoutMath.maximal_metadata f size.val capacity.val stride
+            capacity_value.symm align_positive
+          simpa only [f, witnessFormula, elems_value] using maximal
+        have selected_fits := (greatest elems.val).mpr (by rfl)
+        have checked_fits : f.size elems.val ≤ Usize.max := by scalar_tac
+        step with reference_size tail align phase elems align_positive as ⟨selected_size, selected_value⟩
+        have selected_exact : selected_size.map UScalar.val = some (f.size elems.val) := by
+          change selected_size.map UScalar.val = f.checkedSize Usize.max elems.val at selected_value
+          simpa only [LayoutMath.Formula.checkedSize, checked_fits, if_true] using selected_value
+        cases selected_size with
+        | none => cases selected_exact
+        | some selected_size =>
+          have size_value : selected_size.val = f.size elems.val := Option.some.inj selected_exact
+          step with same_optional_usize (some selected_size) (some size) as ⟨same, same_iff⟩
+          split
+          · rename_i same_true
+            have same_size := Option.some.inj (same_iff.mp same_true)
+            simp only [WP.spec_ok, metadataSpec, info_eq, nonzero, if_false]
+            rw [formula_eq]
+            exact ⟨by rw [← size_value, same_size], greatest⟩
+          · rename_i different
+            have different_size : selected_size ≠ size := by
+              intro same_size
+              exact different (same_iff.mpr (by rw [same_size]))
+            simp only [WP.spec_ok, metadataSpec, info_eq, nonzero, if_false]
+            intro n exact_size
+            rw [formula_eq] at exact_size
+            change f.size n = size.val at exact_size
+            have count_le := (greatest n).mp (by omega)
+            have monotone := LayoutMath.Formula.size_mono f align_positive count_le
+            apply different_size
+            apply UScalar.eq_of_val_eq
+            omega
+
 end Zerocopy.Proofs.Raw.TailChecks
diff --git a/verification/aeneas/lean/RequiredModelContracts.lean b/verification/aeneas/lean/RequiredModelContracts.lean
index efb0a1c6e8..96ff2be744 100644
--- a/verification/aeneas/lean/RequiredModelContracts.lean
+++ b/verification/aeneas/lean/RequiredModelContracts.lean
@@ -143,4 +143,48 @@ attribute [contract_simps] encoding_decoder_admitted_iff trailing_decoder_admitt
     simpa only [option_valid_iff, size_info_valid_iff] using valid
   · cases self <;> simpa only using facts
 
+@[contract_simps] theorem required_metadata_exact (self : layout.DstLayout) (size : Usize)
+    (run : Result (Option Usize)) (provided : Specs.metadata_exact_spec_contract self size run) :
+    Obligations.metadata_exact_spec_contract self size run := by
+  intro valid _align _rounding
+  obtain ⟨value, decoded⟩ := (layout_decoder_admitted_iff self).mpr valid
+  have result := provided value decoded (unsignedWord size) rfl
+  simp only [WP.spec_equiv_exists] at result
+  obtain ⟨output, call, math, admitted, facts⟩ := result
+  refine ⟨output, call, ?_⟩
+  cases info : self.size_info <;> cases output <;>
+    simp only [metadataSpec, info] at facts ⊢
+  all_goals exact facts
+
+@[contract_simps] theorem required_validate_cast (self : layout.DstLayout)
+    (addr length : Usize) (side : layout.CastType)
+    (run : Result (core.result.Result (Usize × Usize) layout.MetadataCastError))
+    (provided : Specs.validate_cast_spec_contract self addr length side run) :
+    Obligations.validate_cast_spec_contract self addr length side run := by
+  intro valid _align room trailing
+  obtain ⟨value, decoded⟩ := (layout_decoder_admitted_iff self).mpr valid
+  obtain ⟨sideValue, sideDecoded⟩ := (cast_type_valid_iff side).mpr trivial
+  have elems : match self.size_info with
+      | .Sized _ => True
+      | .SliceDst tail => 0 < tail.elem_size.val := by
+    cases info : self.size_info with
+    | Sized _ => trivial
+    | SliceDst _ =>
+      simp only [info] at trailing
+      exact trailing.2
+  have result := provided value decoded (unsignedWord addr) rfl
+    (unsignedWord length) rfl sideValue sideDecoded room elems
+  simp only [WP.spec_equiv_exists] at result
+  obtain ⟨output, call, math, admitted, facts⟩ := result
+  refine ⟨output, call, ?_⟩
+  cases output with
+  | Err error =>
+    cases error <;> cases side <;> cases info : self.size_info <;>
+      simpa only [castSpec, castSide, castSplit, info] using facts
+  | Ok pair =>
+    rcases pair with ⟨count, split⟩
+    cases side <;> cases info : self.size_info <;>
+      simpa only [castSpec, castSide, castSplit, info] using facts
+
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean b/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean
index bbe3d294a6..418b8197c6 100644
--- a/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean
+++ b/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean
@@ -33,4 +33,22 @@ supplied arbitrary-outcome contract. These adapters do not run either check.
   rintro result ⟨value, decoded, facts⟩
   trivial
 
+@[contract_simps] theorem required_layout_observations_check
+    (runtime_layout : layout.DstLayout) (align : NonZeroUsize)
+    (phase size addr length : Usize) (side : layout.CastType) (run : Result Unit)
+    (provided : Specs.layout_observations_check_spec_contract
+      runtime_layout align phase size addr length side run) :
+    Obligations.layout_observations_check_spec_contract
+      runtime_layout align phase size addr length side run := by
+  intro valid_runtime align_positive
+  obtain ⟨layout_value, decoded_layout⟩ := (layout_valid_iff runtime_layout).mpr valid_runtime
+  let av : NonZeroUsizeValue := ⟨unsignedWord align.val, align_positive⟩
+  have decoded_align := (decodeNonZeroUScalar_iff align av).mpr rfl
+  obtain ⟨side_value, decoded_side⟩ := (cast_type_valid_iff side).mpr trivial
+  apply WP.spec_mono (provided layout_value decoded_layout av decoded_align
+    (unsignedWord phase) rfl (unsignedWord size) rfl (unsignedWord addr) rfl
+    (unsignedWord length) rfl side_value decoded_side)
+  rintro result ⟨value, decoded, facts⟩
+  trivial
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/projections/ModelShapes.lean b/verification/aeneas/projections/ModelShapes.lean
index a350e0329e..551bc8819a 100644
--- a/verification/aeneas/projections/ModelShapes.lean
+++ b/verification/aeneas/projections/ModelShapes.lean
@@ -65,6 +65,10 @@ derive_model_shape Zerocopy.layout.SizeInfo with 1 type parameters
 
 derive_model_shape Zerocopy.layout.DstLayout with 0 type parameters
 
+derive_model_shape Zerocopy.layout.CastType with 0 type parameters
+
+derive_model_shape Zerocopy.layout.MetadataCastError with 0 type parameters
+
 derive_model_shape Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters
 
 derive_model_shape Zerocopy.wrappers.read_only_def.ReadOnly with 1 type parameters
diff --git a/verification/aeneas/projections/Models.lean b/verification/aeneas/projections/Models.lean
index e1982fca2c..66fe244db2 100644
--- a/verification/aeneas/projections/Models.lean
+++ b/verification/aeneas/projections/Models.lean
@@ -83,6 +83,12 @@ check_model_binding Zerocopy.layout.SizeInfo with 1 type parameters
 derive_rust_model Zerocopy.layout.DstLayout with 0 type parameters
 check_model_binding Zerocopy.layout.DstLayout with 0 type parameters
 
+derive_rust_model Zerocopy.layout.CastType with 0 type parameters
+check_model_binding Zerocopy.layout.CastType with 0 type parameters
+
+derive_rust_model Zerocopy.layout.MetadataCastError with 0 type parameters
+check_model_binding Zerocopy.layout.MetadataCastError with 0 type parameters
+
 derive_rust_model Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters
 check_model_binding Zerocopy.layout.nested_reference.NestedLayer with 0 type parameters
 
diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean
index 6c6a9f1d20..6634cd6c3f 100644
--- a/verification/aeneas/projections/Specs.lean
+++ b/verification/aeneas/projections/Specs.lean
@@ -345,6 +345,26 @@ spec requires_dynamic_padding_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.requires_dynamic_padding_spec for Zerocopy.layout.DstLayout.requires_dynamic_padding with 1
 
+check_model_inputs Zerocopy.layout.DstLayout.metadata_for_exact_size with 0 type parameters
+aeneas_spec_begin
+spec metadata_exact_spec
+  for @Zerocopy.layout.DstLayout.metadata_for_exact_size with 0 type parameters
+  ensures(raw) r => metadataSpec self size.val r
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.metadata_exact_spec for Zerocopy.layout.DstLayout.metadata_for_exact_size with 2
+
+check_model_inputs Zerocopy.layout.DstLayout.validate_cast_and_convert_metadata with 0 type parameters
+aeneas_spec_begin
+spec validate_cast_spec
+  for @Zerocopy.layout.DstLayout.validate_cast_and_convert_metadata with 0 type parameters
+  requires(raw) hroom : addr.val + bytes_len.val ≤ Usize.max
+  requires(raw) ht : match self.size_info with
+    | .Sized _ => True
+    | .SliceDst tail => 0 < tail.elem_size.val
+  ensures(raw) r => castSpec self addr.val bytes_len.val cast_type r
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.validate_cast_spec for Zerocopy.layout.DstLayout.validate_cast_and_convert_metadata with 4
+
 check_model_inputs Zerocopy.layout.nested_reference.round_up with 0 type parameters
 aeneas_spec_begin
 spec nested_round_up_spec
@@ -381,6 +401,14 @@ spec empty_layout_checks_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.empty_layout_checks_spec for Zerocopy.layout.primitive_checks.check_empty_layout with 1
 
+check_model_inputs Zerocopy.layout.primitive_checks.check_u32_slice_known_layout with 0 type parameters
+aeneas_spec_begin
+spec u32_slice_known_layout_checks_spec
+  for @Zerocopy.layout.primitive_checks.check_u32_slice_known_layout with 0 type parameters
+  ensures _ => True
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.u32_slice_known_layout_checks_spec for Zerocopy.layout.primitive_checks.check_u32_slice_known_layout with 1
+
 check_model_inputs Zerocopy.layout.tail_checks.trailing_arithmetic_check with 0 type parameters
 aeneas_spec_begin
 spec trailing_arithmetic_check_spec
@@ -389,6 +417,14 @@ spec trailing_arithmetic_check_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.trailing_arithmetic_check_spec for Zerocopy.layout.tail_checks.trailing_arithmetic_check with 5
 
+check_model_inputs Zerocopy.layout.tail_checks.layout_observations_check with 0 type parameters
+aeneas_spec_begin
+spec layout_observations_check_spec
+  for @Zerocopy.layout.tail_checks.layout_observations_check with 0 type parameters
+  ensures(raw) _ => True
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.layout_observations_check_spec for Zerocopy.layout.tail_checks.layout_observations_check with 7
+
 check_model_inputs Zerocopy.layout.tail_transform_checks.tail_transformations_check with 0 type parameters
 aeneas_spec_begin
 spec tail_transformations_check_spec
diff --git a/verification/aeneas/tests/capabilities/README.md b/verification/aeneas/tests/capabilities/README.md
new file mode 100644
index 0000000000..446f60e5cb
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/README.md
@@ -0,0 +1,107 @@
+<!-- Copyright 2026 The Fuchsia Authors
+SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT -->
+
+# Native capability fixtures
+
+These small, independent crates challenge the pinned native extraction without
+editing compiler output, deleting associated equalities, or replacing local
+helpers with axioms. They are capability probes, not admitted Rust soundness
+proofs. Each new observation records the repository's actual HEAD, dirty status,
+source digests, and validated runtime metadata.
+
+Run from the repository root with the existing `AENEAS_TOOLCHAIN_DIR` and
+`CARGO_HOME` from the verification setup, using a fresh evidence directory:
+
+```bash
+python3 -B verification/aeneas/tests/capabilities/probe.py known-layout \
+  --runtime "$AENEAS_TOOLCHAIN_DIR" \
+  --cargo-home "$CARGO_HOME" \
+  --work target/capabilities/known-layout-new \
+  --cargo-target target/owned-transmute-capability/cargo-target
+```
+
+Replace the case and work directory with `owned-transmute`, `invalid-transmute`,
+`raw-pointers`, `std-transmute`, `known-layout-unconstrained`, or
+`known-layout-concrete`.
+The last two select only their own root from the `known-layout` fixture.
+Each run records commands, exit codes, source digest, and
+logs in `evidence.json`. Charon also records the pre-transformation ULLBC and
+final LLBC. The driver refuses an existing evidence directory and returns the
+first failing stage's status. Inspect the recorded stage results to distinguish
+the expected negative fixture from an unexpected failure.
+The tracked Cargo lockfiles are used with `--locked`; the probe does not
+regenerate them. Compilation occurs through the native Charon driver, as in the
+verification pipeline.
+
+Observed with the preserved patched runtime on October 14, 2026:
+
+| Case | Charon | Aeneas | Result |
+| --- | --- | --- | --- |
+| `known-layout` | 0 | 2 | The original `KnownLayout<PointerMetadata = usize>` constraint survives lifting. `SymbolicToPureTypes.ml:1000` requires an empty associated-type constraint list and rejects the generic root signature. |
+| `known-layout-unconstrained` | 0 | 2 | The generic root has no associated-type constraints. The original trait's `MaybeUninit` metadata equality survives lifting and triggers the same check while Aeneas translates the trait's method signatures. |
+| `known-layout-concrete` | 0 | 0 | The concrete slice root emits, but calls an external associated-constant axiom template; its descriptor value or initializer is not translated or proved. |
+| `owned-transmute` | 0 | 2 | The actual production `transmute!` expansion retains its compile-time trait-check helper. `InterpLoops.ml:411` rejects that helper's infinite loop. No conversion theorem is established. |
+| `invalid-transmute` | 101 | Not run | Rust rejects `u8 -> bool` because `bool` does not implement `FromBytes` (E0277). This confirms a compilation gate, not a runtime byte-decoder proof. |
+| `raw-pointers` | 0 | 0 | Native emission succeeds, but does not establish useful raw-pointer semantics or an admitted proof. |
+
+The raw-pointer result needs particular care. The pinned backend's
+`Aeneas/Std/RawPtr.lean` represents a raw pointer by `v : T`; it carries no
+address or provenance. Its `RawPtr.cast_scalar` always returns `.fail .undef`.
+The emitted slice-pointer constructor and `NonNull::new` are external function
+axiom templates, and `NonNull` is an external type axiom template. None of those
+templates is an accepted interpretation in this experiment. The existing
+admission checker also rejects raw-pointer types. Successful emission therefore
+does not provide a pointer-preservation or memory-safety theorem.
+
+The exact `KnownLayout` experiment fails before recursive trait extraction.
+Its error must not be relabeled as a recursive-declaration diagnostic. The
+trait's recursive `MaybeUninit: KnownLayout` bound and metadata equality remain
+in the preserved original compiler evidence; no translation patch or weakened
+trait was introduced.
+
+The unconstrained follow-up isolates that retained trait equality from the
+explicit equality in the first root. Its final trait constraint identifies
+`<Self::MaybeUninit as KnownLayout>::PointerMetadata = Self::PointerMetadata`.
+The concrete follow-up emits a call to
+`Slice.Insts.ZerocopyKnownLayout.LAYOUT Std.U32`, with the implementation's
+associated constant left in `FunsExternal_Template.lean` as an axiom because
+zerocopy is a dependency of the independent fixture. This emission cannot stand
+in for a proof of the constant's body or of a generic `KnownLayout` dictionary.
+
+## Checked local initializer
+
+The production harness `check_u32_slice_known_layout` in
+`zerocopy/src/layout/primitive_checks.rs` compiles inside zerocopy's own crate.
+Unlike the independent dependency fixture, it reaches the local slice
+implementation's actual associated-constant initializer. The preserved and
+final compiler evidence retains that body; admission traverses its execution.
+Native output defines `Slice.Insts.ZerocopyKnownLayout.LAYOUT T` by calling
+`layout.DstLayout.for_slice T`. No external axiom supplies the descriptor.
+
+The harness checks the actual `[u32]` descriptor fields and its size for every
+count against independent checked multiplication. Its Lean proof uses that
+retained initializer under the visible ABI-read guards. A development negative
+control changes the initializer from `for_slice` to `for_type`: the native module
+still elaborates, but the proof fails. The associated constant is thus part of
+the checked behavior, rather than an assumed trait promise.
+
+This remains a concrete numerical assertion proof under the existing primitive
+interpretations and Rust correspondence premise. It does not supply a generic
+`KnownLayout` law, its `MaybeUninit` obligations, or pointer/reference safety.
+
+## Direct standard transmute
+
+`std-transmute` calls the standard primitive directly for `u32 -> [u8; 4]`,
+the reverse conversion, and `u8 -> bool` after checking Boolean validity. It
+rejects non-little-endian targets at compilation. Native emission succeeds and
+retains all local wrapper bodies, with one external `core::intrinsics::transmute`
+template. This observation isolates the standard primitive from the production
+macro's unsupported compile-time helper loop; it does not prove the macro.
+
+The separate owned-operation proof adds an explicit interpretation-only provider
+to that standard boundary. Admission checks each original Rust endpoint pair;
+compiled auditing binds every reached call to its canonical provider and checks
+the whole provider definitions. Numerical cases use the verified 64-bit
+little-endian profile. The Boolean provider checks validity before construction
+and returns forbidden execution outside its domain. Neither this boundary nor
+its providers cover padding, pointers, resources, or arbitrary Rust types.
diff --git a/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.lock b/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.lock
new file mode 100644
index 0000000000..6b3392da3b
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.lock
@@ -0,0 +1,61 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "owned-transmute-negative"
+version = "0.0.0"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.63"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.63"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.toml b/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.toml
new file mode 100644
index 0000000000..99178873ae
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/invalid-transmute/Cargo.toml
@@ -0,0 +1,12 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "owned-transmute-negative"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+zerocopy = { path = "../../../../../zerocopy", default-features = false }
diff --git a/verification/aeneas/tests/capabilities/invalid-transmute/src/lib.rs b/verification/aeneas/tests/capabilities/invalid-transmute/src/lib.rs
new file mode 100644
index 0000000000..2d6c73cb4d
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/invalid-transmute/src/lib.rs
@@ -0,0 +1,11 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+pub fn to_bool(value: u8) -> bool {
+    zerocopy::transmute!(value)
+}
diff --git a/verification/aeneas/tests/capabilities/known-layout/Cargo.lock b/verification/aeneas/tests/capabilities/known-layout/Cargo.lock
new file mode 100644
index 0000000000..9499ba46fc
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/known-layout/Cargo.lock
@@ -0,0 +1,61 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "known-layout-probe"
+version = "0.0.0"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.63"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.63"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/verification/aeneas/tests/capabilities/known-layout/Cargo.toml b/verification/aeneas/tests/capabilities/known-layout/Cargo.toml
new file mode 100644
index 0000000000..05ad38ca5b
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/known-layout/Cargo.toml
@@ -0,0 +1,12 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "known-layout-probe"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+zerocopy = { path = "../../../../../zerocopy", default-features = false }
diff --git a/verification/aeneas/tests/capabilities/known-layout/src/lib.rs b/verification/aeneas/tests/capabilities/known-layout/src/lib.rs
new file mode 100644
index 0000000000..1661dab3bf
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/known-layout/src/lib.rs
@@ -0,0 +1,25 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+use zerocopy::{DstLayout, KnownLayout};
+
+pub fn layout<T: ?Sized + KnownLayout<PointerMetadata = usize>>() -> DstLayout {
+    T::LAYOUT
+}
+
+pub fn slice_u32_layout() -> DstLayout {
+    layout::<[u32]>()
+}
+
+pub fn layout_unconstrained<T: KnownLayout>() -> DstLayout {
+    T::LAYOUT
+}
+
+pub fn slice_u32_layout_direct() -> DstLayout {
+    <[u32] as KnownLayout>::LAYOUT
+}
diff --git a/verification/aeneas/tests/capabilities/owned-transmute/Cargo.lock b/verification/aeneas/tests/capabilities/owned-transmute/Cargo.lock
new file mode 100644
index 0000000000..00b1b8beec
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/owned-transmute/Cargo.lock
@@ -0,0 +1,61 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "owned-transmute-probe"
+version = "0.0.0"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.63"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.63"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/verification/aeneas/tests/capabilities/owned-transmute/Cargo.toml b/verification/aeneas/tests/capabilities/owned-transmute/Cargo.toml
new file mode 100644
index 0000000000..1a3d13ac7d
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/owned-transmute/Cargo.toml
@@ -0,0 +1,12 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "owned-transmute-probe"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+zerocopy = { path = "../../../../../zerocopy", default-features = false }
diff --git a/verification/aeneas/tests/capabilities/owned-transmute/src/lib.rs b/verification/aeneas/tests/capabilities/owned-transmute/src/lib.rs
new file mode 100644
index 0000000000..6962e4eeda
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/owned-transmute/src/lib.rs
@@ -0,0 +1,15 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+pub fn to_bytes(value: u32) -> [u8; 4] {
+    zerocopy::transmute!(value)
+}
+
+pub fn from_bytes(value: [u8; 4]) -> u32 {
+    zerocopy::transmute!(value)
+}
diff --git a/verification/aeneas/tests/capabilities/probe.py b/verification/aeneas/tests/capabilities/probe.py
new file mode 100644
index 0000000000..6a997a5419
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/probe.py
@@ -0,0 +1,97 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+"""Record exact native capability failures without modifying extracted ASTs."""
+
+import argparse
+import hashlib
+import json
+from pathlib import Path
+import subprocess
+import sys
+import time
+
+
+CASES = {
+    'known-layout': 'known_layout_probe::layout,known_layout_probe::slice_u32_layout',
+    'known-layout-unconstrained': 'known_layout_probe::layout_unconstrained',
+    'known-layout-concrete': 'known_layout_probe::slice_u32_layout_direct',
+    'owned-transmute': 'owned_transmute_probe::to_bytes,owned_transmute_probe::from_bytes',
+    'invalid-transmute': 'owned_transmute_negative::to_bool',
+    'std-transmute': 'std_transmute_probe::to_bytes,std_transmute_probe::from_bytes,std_transmute_probe::guarded_bool',
+    'raw-pointers': 'raw_pointer_probe::cast,raw_pointer_probe::with_len,raw_pointer_probe::nonnull',
+}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('case', choices=CASES)
+    parser.add_argument('--runtime', type=Path, required=True)
+    parser.add_argument('--cargo-home', type=Path, required=True)
+    parser.add_argument('--work', type=Path, required=True)
+    parser.add_argument('--cargo-target', type=Path, required=True)
+    args = parser.parse_args()
+    runtime, work = args.runtime.resolve(), args.work.resolve()
+    root = Path(__file__).resolve().parents[4]
+    sys.path.insert(0, str(root / 'verification/aeneas'))
+    import toolchain
+    metadata, charon_version = toolchain.validate(root, runtime)
+    fixture_case = ('known-layout' if args.case.startswith('known-layout')
+                    else args.case)
+    fixture = Path(__file__).resolve().parent / fixture_case
+    work.mkdir(parents=True, exist_ok=False)
+    (work / 'native').mkdir(exist_ok=True)
+    environment = toolchain.runtime_env(runtime)
+    environment.update({
+        'RUSTUP_TOOLCHAIN': metadata['rust-toolchain-version'],
+        'CARGO_HOME': str(args.cargo_home.resolve()),
+        'CARGO_TARGET_DIR': str(args.cargo_target.resolve()),
+        'CARGO_BUILD_JOBS': '2', 'CARGO_NET_OFFLINE': 'true',
+        'CHARON_ADMISSION_SNAPSHOT': str(work / 'probe.before.ullbc'),
+    })
+    commands = [
+        ('charon', [str(runtime / 'charon'), 'cargo', '--preset=aeneas',
+                    '--sysroot', 'default', '--start-from', CASES[args.case],
+                    '--mir', 'promoted', '--no-dedup-serialized-ast',
+                    '--dest-file', str(work / 'probe.llbc'), '--abort-on-error',
+                    '--error-on-warnings', '--', '--lib', '--locked', '--offline']),
+        ('aeneas', [str(runtime / 'aeneas'), '-backend', 'lean', '-namespace',
+                    'Probe', '-dest', str(work / 'native'), '-split-files',
+                    '-emit-json', '-abort-on-error', '-warnings-as-errors',
+                    '-no-progress-bar', '-use-tuple-structs', 'false',
+                    str(work / 'probe.llbc')]),
+    ]
+    sources = sorted((root / 'zerocopy/src').rglob('*.rs')) + [
+        root / 'zerocopy/build.rs', root / 'zerocopy/Cargo.toml',
+        root / 'zerocopy/Cargo.lock', fixture / 'src/lib.rs',
+        fixture / 'Cargo.toml', fixture / 'Cargo.lock', Path(__file__).resolve(),
+    ]
+    evidence = {'case': args.case, 'fixture': str(fixture),
+                'runtime': str(runtime), 'runtime_metadata': metadata,
+                'charon_version': charon_version,
+                'repository_head': subprocess.check_output(
+                    ['git', 'rev-parse', 'HEAD'], cwd=root, text=True).strip(),
+                'repository_status': subprocess.check_output(
+                    ['git', 'status', '--porcelain'], cwd=root, text=True),
+                'source_sha256': {str(path.relative_to(root)):
+                    hashlib.sha256(path.read_bytes()).hexdigest()
+                    for path in sources}, 'steps': []}
+    for name, command in commands:
+        log_path = work / (name + '.log')
+        started = time.monotonic()
+        with log_path.open('w') as log:
+            result = subprocess.run(command, cwd=fixture, env=environment,
+                                    stdout=log, stderr=subprocess.STDOUT)
+        evidence['steps'].append({'name': name, 'command': command,
+                                  'exit_code': result.returncode,
+                                  'seconds': round(time.monotonic() - started, 2),
+                                  'log': str(log_path)})
+        (work / 'evidence.json').write_text(json.dumps(evidence, indent=2) + '\n')
+        print(name, result.returncode, log_path, flush=True)
+        if result.returncode:
+            return result.returncode
+    return 0
+
+
+if __name__ == '__main__':
+    raise SystemExit(main())
diff --git a/verification/aeneas/tests/capabilities/raw-pointers/Cargo.lock b/verification/aeneas/tests/capabilities/raw-pointers/Cargo.lock
new file mode 100644
index 0000000000..a4c65c14e6
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/raw-pointers/Cargo.lock
@@ -0,0 +1,61 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "proc-macro2"
+version = "1.0.106"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934"
+dependencies = [
+ "unicode-ident",
+]
+
+[[package]]
+name = "quote"
+version = "1.0.45"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
+dependencies = [
+ "proc-macro2",
+]
+
+[[package]]
+name = "raw-pointer-probe"
+version = "0.0.0"
+dependencies = [
+ "zerocopy",
+]
+
+[[package]]
+name = "syn"
+version = "2.0.117"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e665b8803e7b1d2a727f4023456bbbbe74da67099c585258af0ad9c5013b9b99"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
+[[package]]
+name = "unicode-ident"
+version = "1.0.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
+
+[[package]]
+name = "zerocopy"
+version = "0.8.63"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.63"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
diff --git a/verification/aeneas/tests/capabilities/raw-pointers/Cargo.toml b/verification/aeneas/tests/capabilities/raw-pointers/Cargo.toml
new file mode 100644
index 0000000000..630530baec
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/raw-pointers/Cargo.toml
@@ -0,0 +1,12 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "raw-pointer-probe"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
+
+[dependencies]
+zerocopy = { path = "../../../../../zerocopy", default-features = false }
diff --git a/verification/aeneas/tests/capabilities/raw-pointers/src/lib.rs b/verification/aeneas/tests/capabilities/raw-pointers/src/lib.rs
new file mode 100644
index 0000000000..8244c2fff0
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/raw-pointers/src/lib.rs
@@ -0,0 +1,21 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+use core::ptr::NonNull;
+
+pub fn cast(pointer: *const u32) -> *const u8 {
+    pointer as *const u8
+}
+
+pub fn with_len(pointer: *const u8, count: usize) -> *const [u8] {
+    core::ptr::slice_from_raw_parts(pointer, count)
+}
+
+pub fn nonnull(pointer: *mut u8) -> Option<NonNull<u8>> {
+    NonNull::new(pointer)
+}
diff --git a/verification/aeneas/tests/capabilities/std-transmute/Cargo.lock b/verification/aeneas/tests/capabilities/std-transmute/Cargo.lock
new file mode 100644
index 0000000000..81c95e1f23
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/std-transmute/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "std-transmute-probe"
+version = "0.0.0"
diff --git a/verification/aeneas/tests/capabilities/std-transmute/Cargo.toml b/verification/aeneas/tests/capabilities/std-transmute/Cargo.toml
new file mode 100644
index 0000000000..5dfbe5f385
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/std-transmute/Cargo.toml
@@ -0,0 +1,9 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+[package]
+name = "std-transmute-probe"
+version = "0.0.0"
+edition = "2021"
+
+[workspace]
diff --git a/verification/aeneas/tests/capabilities/std-transmute/src/lib.rs b/verification/aeneas/tests/capabilities/std-transmute/src/lib.rs
new file mode 100644
index 0000000000..73ca76f63e
--- /dev/null
+++ b/verification/aeneas/tests/capabilities/std-transmute/src/lib.rs
@@ -0,0 +1,20 @@
+// Copyright 2026 The Fuchsia Authors
+// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+#[cfg(not(target_endian = "little"))]
+compile_error!("this concrete byte-conversion probe supports little-endian targets only");
+
+#[allow(unnecessary_transmutes)]
+pub fn to_bytes(value: u32) -> [u8; 4] {
+    unsafe { core::mem::transmute::<u32, [u8; 4]>(value) }
+}
+
+#[allow(unnecessary_transmutes)]
+pub fn from_bytes(value: [u8; 4]) -> u32 {
+    unsafe { core::mem::transmute::<[u8; 4], u32>(value) }
+}
+
+pub fn guarded_bool(value: u8) -> bool {
+    assert!(value < 2);
+    unsafe { core::mem::transmute::<u8, bool>(value) }
+}
diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs
index 1a5c8cb965..f2ded8d82e 100644
--- a/zerocopy/src/layout/mod.rs
+++ b/zerocopy/src/layout/mod.rs
@@ -1693,6 +1693,11 @@ impl DstLayout {
             _ => None,
         }
     }))]
+    ///
+    /// ```aeneas
+    /// spec metadata_exact_spec
+    ///   ensures(raw) r => metadataSpec self size.val r
+    /// ```
     const fn metadata_for_exact_size(&self, size: usize) -> Option<usize> {
         #[cfg(all(kani, kani_slow))]
         #[kani::proof_for_contract(DstLayout::metadata_for_exact_size)]
@@ -1822,6 +1827,15 @@ impl DstLayout {
             _ => false,
         }
     }))]
+    ///
+    /// ```aeneas
+    /// spec validate_cast_spec
+    ///   requires(raw) hroom : addr.val + bytes_len.val ≤ Usize.max
+    ///   requires(raw) ht : match self.size_info with
+    ///     | .Sized _ => True
+    ///     | .SliceDst tail => 0 < tail.elem_size.val
+    ///   ensures(raw) r => castSpec self addr.val bytes_len.val cast_type r
+    /// ```
     pub(crate) const fn validate_cast_and_convert_metadata(
         &self,
         addr: usize,
diff --git a/zerocopy/src/layout/primitive_checks.rs b/zerocopy/src/layout/primitive_checks.rs
index b1b0b2041f..bd34705c33 100644
--- a/zerocopy/src/layout/primitive_checks.rs
+++ b/zerocopy/src/layout/primitive_checks.rs
@@ -80,6 +80,45 @@ fn check_empty_layout(repr_align: Option<NonZeroUsize>) {
     assert!(empty.statically_shallow_unpadded);
 }
 
+/// Checks the actual built-in `[u32]` descriptor and every element count.
+///
+/// The ABI guard makes the primitive-read premises visible in the extracted
+/// model. The comparison retains overflow: both computations must return
+/// `None` when the mathematical byte length does not fit in `usize`.
+/// This checks one associated constant, not the complete `KnownLayout` trait.
+///
+/// ```aeneas
+/// spec u32_slice_known_layout_checks_spec
+///   ensures _ => True
+/// ```
+#[allow(clippy::arithmetic_side_effects)]
+fn check_u32_slice_known_layout(elems: usize) {
+    let size = mem::size_of::<u32>();
+    let align = mem::align_of::<u32>();
+    if !align.is_power_of_two() {
+        return;
+    }
+    if size % align != 0 {
+        return;
+    }
+
+    let slice = <[u32] as crate::KnownLayout>::LAYOUT;
+    assert!(slice.align.get() == align);
+    assert!(slice.statically_shallow_unpadded);
+    match slice.size_info {
+        SizeInfo::SliceDst(tail) => {
+            assert!(tail.offset == 0);
+            assert!(tail.elem_size == size);
+            assert!(tail.size_base == 0);
+            assert!(tail.size_rounding_align_and_phase.0.get() == align);
+            let actual = tail.size_for_elems(elems);
+            let expected = elems.checked_mul(size);
+            assert!(super::tail_checks::same_optional_usize(actual, expected));
+        }
+        SizeInfo::Sized { .. } => panic!("slice descriptor returned a sized layout"),
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -92,6 +131,9 @@ mod tests {
         check_primitive_layouts::<(u8, u64)>();
         check_primitive_layouts::<[u64; 3]>();
         check_empty_layout(None);
+        for elems in [0, 1, usize::MAX / 4, usize::MAX / 4 + 1, usize::MAX] {
+            check_u32_slice_known_layout(elems);
+        }
         for align in [1, 2, 8, 3] {
             check_empty_layout(NonZeroUsize::new(align));
         }
diff --git a/zerocopy/src/layout/tail_checks.rs b/zerocopy/src/layout/tail_checks.rs
index 2a0e616841..bd31bbfcf8 100644
--- a/zerocopy/src/layout/tail_checks.rs
+++ b/zerocopy/src/layout/tail_checks.rs
@@ -24,7 +24,7 @@
 
 use core::num::NonZeroUsize;
 
-use super::TrailingSliceLayout;
+use super::{CastType, DstLayout, MetadataCastError, SizeInfo, TrailingSliceLayout};
 
 pub(crate) fn same_optional_usize(left: Option<usize>, right: Option<usize>) -> bool {
     match (left, right) {
@@ -75,6 +75,84 @@ fn reference_capacity(
     }
 }
 
+fn reference_metadata(
+    runtime_layout: DstLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    size: usize,
+) -> Option<usize> {
+    match runtime_layout.size_info {
+        SizeInfo::Sized { .. } => None,
+        SizeInfo::SliceDst(tail) => {
+            if tail.elem_size == 0 {
+                return None;
+            }
+            match reference_capacity(tail, align, phase, size) {
+                None => None,
+                Some(bytes) => {
+                    #[allow(clippy::arithmetic_side_effects)]
+                    let elems = bytes / tail.elem_size;
+                    if same_optional_usize(reference_size(tail, align, phase, elems), Some(size)) {
+                        Some(elems)
+                    } else {
+                        None
+                    }
+                }
+            }
+        }
+    }
+}
+
+#[allow(clippy::arithmetic_side_effects)]
+fn reference_cast(
+    runtime_layout: DstLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    addr: usize,
+    length: usize,
+    side: CastType,
+) -> Result<(usize, usize), MetadataCastError> {
+    // The caller checks address addition and excludes the zero-stride panic
+    // before either the production or reference cast is evaluated.
+    let anchor = match side {
+        CastType::Prefix => addr,
+        CastType::Suffix => addr + length,
+    };
+    // Alignment failure has priority over insufficient size.
+    if anchor % runtime_layout.align.get() != 0 {
+        return Err(MetadataCastError::Alignment);
+    }
+    let candidate = match runtime_layout.size_info {
+        SizeInfo::Sized { size } => {
+            if size <= length {
+                Some((0, size))
+            } else {
+                None
+            }
+        }
+        SizeInfo::SliceDst(tail) => match reference_capacity(tail, align, phase, length) {
+            None => None,
+            Some(bytes) => {
+                let elems = bytes / tail.elem_size;
+                match reference_size(tail, align, phase, elems) {
+                    Some(size) => Some((elems, size)),
+                    None => None,
+                }
+            }
+        },
+    };
+    match candidate {
+        None => Err(MetadataCastError::Size),
+        Some((elems, size)) => {
+            let split = match side {
+                CastType::Prefix => size,
+                CastType::Suffix => length - size,
+            };
+            Ok((elems, split))
+        }
+    }
+}
+
 /// Check the entire optional size and capacity results, including overflow.
 ///
 /// Physical slice offset does not constrain this claim: a raw layout can have
@@ -109,3 +187,210 @@ fn trailing_arithmetic_check(
         ));
     }
 }
+
+/// Check exact-size metadata and complete cast results against independent
+/// calculations. A successful cast must select the greatest fitting element
+/// count and its padded prefix/suffix split; errors must have the same kind.
+///
+/// The address guard is the production method's no-overflow premise. The
+/// explicit zero-stride guard excludes its documented panic, even when an
+/// alignment error would otherwise be returned. Exact-size inference itself
+/// is also checked for zero-stride tails, for which it must return `None`.
+///
+/// ```aeneas
+/// spec layout_observations_check_spec
+///   ensures(raw) _ => True
+/// ```
+fn layout_observations_check(
+    runtime_layout: DstLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    size: usize,
+    addr: usize,
+    length: usize,
+    side: CastType,
+) {
+    let encoding_matches = match runtime_layout.size_info {
+        SizeInfo::Sized { .. } => true,
+        SizeInfo::SliceDst(tail) => {
+            align.get().is_power_of_two()
+                && phase < align.get()
+                && same_optional_usize(
+                    align.get().checked_add(phase),
+                    Some(tail.size_rounding_align_and_phase.0.get()),
+                )
+        }
+    };
+    if encoding_matches {
+        assert!(same_optional_usize(
+            runtime_layout.metadata_for_exact_size(size),
+            reference_metadata(runtime_layout, align, phase, size),
+        ));
+        let nonzero_stride = match runtime_layout.size_info {
+            SizeInfo::Sized { .. } => true,
+            SizeInfo::SliceDst(tail) => tail.elem_size != 0,
+        };
+        if addr.checked_add(length).is_some() && nonzero_stride {
+            let actual = runtime_layout.validate_cast_and_convert_metadata(addr, length, side);
+            let expected = reference_cast(runtime_layout, align, phase, addr, length, side);
+            let same = match (actual, expected) {
+                (Ok((elems, split)), Ok((expected_elems, expected_split))) => {
+                    elems == expected_elems && split == expected_split
+                }
+                (Err(MetadataCastError::Alignment), Err(MetadataCastError::Alignment))
+                | (Err(MetadataCastError::Size), Err(MetadataCastError::Size)) => true,
+                _ => false,
+            };
+            assert!(same);
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::layout::RoundingAlignAndPhase;
+
+    fn tail_layout(
+        outer_align: usize,
+        size_align: usize,
+        elem_size: usize,
+        size_base: usize,
+        phase: usize,
+        offset: usize,
+    ) -> DstLayout {
+        DstLayout {
+            align: NonZeroUsize::new(outer_align).unwrap(),
+            size_info: SizeInfo::SliceDst(TrailingSliceLayout {
+                offset,
+                elem_size,
+                size_base,
+                size_rounding_align_and_phase: RoundingAlignAndPhase::new(
+                    NonZeroUsize::new(size_align).unwrap(),
+                    phase,
+                ),
+            }),
+            statically_shallow_unpadded: false,
+        }
+    }
+
+    fn check_cast(
+        layout: DstLayout,
+        size_align: usize,
+        phase: usize,
+        addr: usize,
+        length: usize,
+        side: CastType,
+        expected: Result<(usize, usize), MetadataCastError>,
+    ) {
+        let size_align = NonZeroUsize::new(size_align).unwrap();
+        // The proved root compares complete results, including both error
+        // kinds. Pin the reference result too, so each case documents its path.
+        layout_observations_check(layout, size_align, phase, length, addr, length, side);
+        assert!(match (reference_cast(layout, size_align, phase, addr, length, side), expected) {
+            (Ok(actual), Ok(expected)) => actual == expected,
+            (Err(MetadataCastError::Alignment), Err(MetadataCastError::Alignment))
+            | (Err(MetadataCastError::Size), Err(MetadataCastError::Size)) => true,
+            _ => false,
+        });
+    }
+
+    fn check_both(
+        layout: DstLayout,
+        size_align: usize,
+        phase: usize,
+        length: usize,
+        elems: usize,
+        size: usize,
+    ) {
+        check_cast(layout, size_align, phase, 0, length, CastType::Prefix, Ok((elems, size)));
+        check_cast(
+            layout,
+            size_align,
+            phase,
+            0,
+            length,
+            CastType::Suffix,
+            Ok((elems, length.checked_sub(size).unwrap())),
+        );
+    }
+
+    #[test]
+    fn cast_rounded_size_branches() {
+        // An input below the rounding alignment can select an empty object.
+        check_both(tail_layout(1, 8, 1, 0, 0, 4), 8, 0, 7, 0, 0);
+
+        // Strides below, equal to, and above the size alignment all use the
+        // complete size. Nonzero base and phase differ from physical offset.
+        // For stride 10, the unused remainders are 2, 4, and 6: below, equal
+        // to, and above alignment 4. Only the last two discard a rounded unit.
+        for &(align, stride, length, elems, size) in &[
+            (8, 3, 29, 7, 29),
+            (4, 4, 29, 5, 29),
+            (4, 10, 29, 2, 29),
+            (4, 10, 21, 1, 17),
+            (4, 10, 33, 2, 29),
+        ] {
+            check_both(tail_layout(1, align, stride, 5, 2, 63), align, 2, length, elems, size);
+        }
+
+        // This raw layout need not describe a completed Rust type. Comparing
+        // stride 6 to outer alignment 8 would incorrectly retain all 16 bytes;
+        // size alignment 4 requires discarding the aligned remainder of 4.
+        check_both(tail_layout(8, 4, 6, 0, 0, 3), 4, 0, 16, 2, 12);
+    }
+
+    #[test]
+    fn cast_errors_keep_alignment_priority() {
+        let sized = DstLayout {
+            align: NonZeroUsize::new(8).unwrap(),
+            size_info: SizeInfo::Sized { size: 24 },
+            statically_shallow_unpadded: false,
+        };
+        check_both(sized, 4, 2, 32, 0, 24);
+        for &layout in &[sized, tail_layout(8, 4, 6, 16, 2, 3)] {
+            for &side in &[CastType::Prefix, CastType::Suffix] {
+                check_cast(layout, 4, 2, 1, 4, side, Err(MetadataCastError::Alignment));
+                let addr = match side {
+                    CastType::Prefix => 0,
+                    CastType::Suffix => 4,
+                };
+                check_cast(layout, 4, 2, addr, 4, side, Err(MetadataCastError::Size));
+            }
+        }
+    }
+
+    #[test]
+    fn cast_sizes_near_word_limit() {
+        let max = usize::MAX;
+        let rounded = max.checked_sub(7).unwrap();
+        check_both(tail_layout(1, 8, 1, 0, 0, max), 8, 0, max, rounded, rounded);
+        check_both(tail_layout(1, 4, 8, 0, 0, max), 4, 0, max, rounded / 8, rounded);
+        check_both(tail_layout(1, 4, 1, rounded, 3, 0), 4, 3, max, 1, max.checked_sub(3).unwrap());
+        let sized = DstLayout {
+            align: NonZeroUsize::new(1).unwrap(),
+            size_info: SizeInfo::Sized { size: max },
+            statically_shallow_unpadded: false,
+        };
+        check_both(sized, 4, 2, max, 0, max);
+        let overflowing = tail_layout(1, 4, 1, max.checked_sub(3).unwrap(), 1, 0);
+        for &side in &[CastType::Prefix, CastType::Suffix] {
+            check_cast(overflowing, 4, 1, 0, max, side, Err(MetadataCastError::Size));
+            check_cast(
+                tail_layout(1, 4, 6, 0, 0, 3),
+                4,
+                0,
+                max.checked_sub(16).unwrap(),
+                16,
+                side,
+                Ok((
+                    2,
+                    match side {
+                        CastType::Prefix => 12,
+                        CastType::Suffix => 4,
+                    },
+                )),
+            );
+        }
+    }
+}