diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index 46b8f19d5c..1d8ee8b4b8 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -120,7 +120,7 @@ zerocopy's unsafe pointer operations are sound.
 
 ## Scope and proofs
 
-Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs).
+Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs).
 
 Extraction starts from the function and nominal-type owners of every present
 `aeneas` fence in `zerocopy/src`, including their dependencies. Every present
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index f8dad1e701..051c3f642f 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -643,14 +643,14 @@ def byteorder.verification.set_u32_be
   byteorder.U32.get byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder value1
 
 /-- [zerocopy::layout::POINTER_WIDTH_BITS]
-    Source: 'src/layout/mod.rs', lines 17:0-17:62 -/
+    Source: 'src/layout/mod.rs', lines 20:0-20:62 -/
 @[global_simps, irreducible]
 def layout.POINTER_WIDTH_BITS : Result Std.Usize := do
   let i ← core.mem.size_of Std.Usize
   i * 8#usize
 
 /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::new]:
-    Source: 'src/layout/mod.rs', lines 97:4-116:5 -/
+    Source: 'src/layout/mod.rs', lines 100:4-119:5 -/
 def layout.RoundingAlignAndPhase.new
   (align : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) :
@@ -671,7 +671,7 @@ def layout.RoundingAlignAndPhase.new
   | some encoded1 => ok { _0 := encoded1 }
 
 /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]:
-    Source: 'src/layout/mod.rs', lines 130:4-157:5 -/
+    Source: 'src/layout/mod.rs', lines 133:4-160:5 -/
 def layout.RoundingAlignAndPhase.components
   (self : layout.RoundingAlignAndPhase) :
   Result ((core.num.nonzero.NonZero Std.Usize
@@ -699,7 +699,7 @@ def layout.RoundingAlignAndPhase.components
     ok (align1, phase)
 
 /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]:
-    Source: 'src/layout/mod.rs', lines 170:4-179:5 -/
+    Source: 'src/layout/mod.rs', lines 173:4-182:5 -/
 def layout.RoundingAlignAndPhase.align
   (self : layout.RoundingAlignAndPhase) :
   Result (core.num.nonzero.NonZero Std.Usize
@@ -708,6 +708,121 @@ def layout.RoundingAlignAndPhase.align
   let (nz, _) ← layout.RoundingAlignAndPhase.components self
   ok nz
 
+/-- [zerocopy::layout::nested_reference::round_up]:
+    Source: 'src/layout/nested_reference.rs', lines 46:0-56:1 -/
+def layout.nested_reference.round_up
+  (size : Std.Usize) (align : Std.Usize) : Result (Option Std.Usize) := do
+  if align = 0#usize
+  then ok none
+  else
+    let remainder ← size % align
+    if remainder = 0#usize
+    then ok (some size)
+    else let i ← align - remainder
+         ok (Usize.checked_add size i)
+
+/-- [zerocopy::layout::nested_reference::apply_layer]:
+    Source: 'src/layout/nested_reference.rs', lines 58:0-80:1 -/
+def layout.nested_reference.apply_layer
+  (layer : layout.nested_reference.NestedLayer) (size : Std.Usize)
+  (alignment : Std.Usize) :
+  Result (Option (Std.Usize × Std.Usize))
+  := do
+  let b ← core.num.Usize.is_power_of_two layer.packed
+  if b
+  then
+    let b1 ← core.num.Usize.is_power_of_two layer.min_align
+    if b1
+    then
+      if layer.min_align > layer.packed
+      then ok none
+      else
+        let field_align ←
+          if alignment < layer.packed
+          then ok alignment
+          else ok layer.packed
+        let o ←
+          layout.nested_reference.round_up layer.prefix_bytes field_align
+        match o with
+        | none => ok none
+        | some offset =>
+          let alignment1 ←
+            if layer.min_align < field_align
+            then ok field_align
+            else ok layer.min_align
+          let o1 ← lift (Usize.checked_add offset size)
+          match o1 with
+          | none => ok none
+          | some size1 =>
+            let o2 ← layout.nested_reference.round_up size1 alignment1
+            match o2 with
+            | none => ok none
+            | some size2 => ok (some (size2, alignment1))
+    else ok none
+  else ok none
+
+/-- [zerocopy::layout::nested_reference::size_for_metadata]: loop body 0:
+    Source: 'src/layout/nested_reference.rs', lines 108:4-115:5 -/
+@[rust_loop_body]
+def layout.nested_reference.size_for_metadata_loop.body
+  (leading : Slice layout.nested_reference.NestedLayer)
+  (state : Option (Std.Usize × Std.Usize)) (i : Std.Usize) :
+  Result (ControlFlow ((Option (Std.Usize × Std.Usize)) × Std.Usize) (Option
+    (Std.Usize × Std.Usize)))
+  := do
+  if i != 0#usize
+  then
+    let i1 ← i - 1#usize
+    let layer ← Slice.index_usize leading i1
+    match state with
+    | none => ok (cont (none, i1))
+    | some p =>
+      let (size, alignment) := p
+      let state1 ← layout.nested_reference.apply_layer layer size alignment
+      ok (cont (state1, i1))
+  else ok (done state)
+
+/-- [zerocopy::layout::nested_reference::size_for_metadata]: loop 0:
+    Source: 'src/layout/nested_reference.rs', lines 108:4-115:5 -/
+@[rust_loop]
+def layout.nested_reference.size_for_metadata_loop
+  (leading : Slice layout.nested_reference.NestedLayer)
+  (state : Option (Std.Usize × Std.Usize)) (i : Std.Usize) :
+  Result (Option (Std.Usize × Std.Usize))
+  := do
+  loop
+    (fun (state1, i1) => layout.nested_reference.size_for_metadata_loop.body
+      leading state1 i1)
+    (state, i)
+
+/-- [zerocopy::layout::nested_reference::size_for_metadata]:
+    Source: 'src/layout/nested_reference.rs', lines 94:0-120:1 -/
+def layout.nested_reference.size_for_metadata
+  (leading : Slice layout.nested_reference.NestedLayer) (elem_size : Std.Usize)
+  (leaf_align : Std.Usize) (elems : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  let b ← core.num.Usize.is_power_of_two leaf_align
+  if b
+  then
+    let i ← elem_size % leaf_align
+    if i != 0#usize
+    then ok none
+    else
+      let o ← lift (Usize.checked_mul elem_size elems)
+      let state ←
+        match o with
+        | none => ok none
+        | some size => ok (some (size, leaf_align))
+      let i1 := Slice.len leading
+      let state1 ←
+        layout.nested_reference.size_for_metadata_loop leading state i1
+      match state1 with
+      | none => ok none
+      | some p => let (size, _) := p
+                  ok (some size)
+  else ok none
+
 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
     Source: 'src/util/mod.rs', lines 261:0-279:1 -/
 def util.round_down_to_next_multiple_of_alignment
diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean
index a53b231469..1d882da79b 100644
--- a/verification/aeneas/golden/Types.lean
+++ b/verification/aeneas/golden/Types.lean
@@ -100,9 +100,16 @@ structure byteorder.U32 (O : Type) where
   _1 : core.marker.PhantomData O
 
 /-- [zerocopy::layout::RoundingAlignAndPhase]
-    Source: 'src/layout/mod.rs', lines 78:0-78:54 -/
+    Source: 'src/layout/mod.rs', lines 81:0-81:54 -/
 structure layout.RoundingAlignAndPhase where
   _0 : core.num.nonzero.NonZero Std.Usize
     core.num.niche_types.NonZeroUsizeInner
 
+/-- [zerocopy::layout::nested_reference::NestedLayer]
+    Source: 'src/layout/nested_reference.rs', lines 27:0-31:1 -/
+structure layout.nested_reference.NestedLayer where
+  packed : Std.Usize
+  min_align : Std.Usize
+  prefix_bytes : Std.Usize
+
 end Zerocopy
diff --git a/verification/aeneas/lean/LayoutModel.lean b/verification/aeneas/lean/LayoutModel.lean
index d2859cdab2..adc6a518f7 100644
--- a/verification/aeneas/lean/LayoutModel.lean
+++ b/verification/aeneas/lean/LayoutModel.lean
@@ -27,3 +27,185 @@ namespace Zerocopy.Proofs
 
 
 end Zerocopy.Proofs
+
+namespace Zerocopy.Proofs.NestedReference
+
+/- The independent recursive rule uses unbounded arithmetic and complete
+inner-field sizes. Layers are ordered from outermost to innermost. These
+definitions do not call an extracted implementation or manipulate its
+normalized base and phase.
+-/
+def layerValid (layer : layout.nested_reference.NestedLayer) : Prop :=
+  layer.packed.val.isPowerOfTwo ∧ layer.min_align.val.isPowerOfTwo ∧
+    layer.min_align.val ≤ layer.packed.val
+
+def valid (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment : Nat) : Prop :=
+  alignment.isPowerOfTwo ∧ elem % alignment = 0 ∧ ∀ layer ∈ layers, layerValid layer
+
+def step (layer : layout.nested_reference.NestedLayer) (inner : Nat × Nat) : Nat × Nat :=
+  let placementAlign := min inner.2 layer.packed.val
+  let alignment := max layer.min_align.val placementAlign
+  (LayoutMath.roundUp (LayoutMath.roundUp layer.prefix_bytes.val placementAlign + inner.1) alignment,
+    alignment)
+
+def state (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata : Nat) : Nat × Nat :=
+  layers.foldr step (metadata * elem, alignment)
+
+theorem state_cons (layer : layout.nested_reference.NestedLayer)
+    (layers : List layout.nested_reference.NestedLayer) (elem alignment metadata : Nat) :
+    state (layer :: layers) elem alignment metadata =
+      step layer (state layers elem alignment metadata) := rfl
+
+theorem step_contains_inner (layer : layout.nested_reference.NestedLayer) (inner : Nat × Nat) :
+    inner.1 ≤ (step layer inner).1 := by
+  simp only [step, LayoutMath.roundUp]
+  omega
+
+theorem step_alignment_power (layer : layout.nested_reference.NestedLayer)
+    (inner : Nat × Nat) (hl : layerValid layer) (ha : inner.2.isPowerOfTwo) :
+    (step layer inner).2.isPowerOfTwo := by
+  simp only [step]
+  have hm : (min inner.2 layer.packed.val).isPowerOfTwo := by
+    by_cases h : inner.2 ≤ layer.packed.val
+    · simpa only [Nat.min_eq_left h] using ha
+    · simpa only [Nat.min_eq_right (by omega : layer.packed.val ≤ inner.2)] using hl.1
+  by_cases h : layer.min_align.val ≤ min inner.2 layer.packed.val
+  · simpa only [Nat.max_eq_right h] using hm
+  · simpa only [Nat.max_eq_left (by omega : min inner.2 layer.packed.val ≤ layer.min_align.val)]
+      using hl.2.1
+
+theorem state_alignment_power (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata : Nat) (h : valid layers elem alignment) :
+    (state layers elem alignment metadata).2.isPowerOfTwo := by
+  induction layers with
+  | nil => exact h.1
+  | cons layer layers ih =>
+    simp only [state, List.foldr_cons]
+    apply step_alignment_power
+    · exact h.2.2 layer (by simp)
+    · apply ih
+      exact ⟨h.1, h.2.1, fun x hx => h.2.2 x (by simp [hx])⟩
+
+theorem state_alignment_bound (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata bound : Nat) (ha : alignment ≤ bound)
+    (hl : ∀ layer ∈ layers, layer.min_align.val ≤ bound) :
+    (state layers elem alignment metadata).2 ≤ bound := by
+  induction layers with
+  | nil => exact ha
+  | cons layer layers ih =>
+    rw [state_cons]
+    simp only [step]
+    apply max_le
+    · exact hl layer (by simp)
+    · apply le_trans (Nat.min_le_left _ _)
+      exact ih (fun x hx => hl x (by simp [hx]))
+
+theorem state_contains_suffix (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata count : Nat) :
+    (state (layers.drop count) elem alignment metadata).1 ≤
+      (state layers elem alignment metadata).1 := by
+  induction layers generalizing count with
+  | nil => simp
+  | cons layer layers ih =>
+    cases count with
+    | zero => simp
+    | succ count =>
+      simp only [List.drop_succ_cons, state_cons]
+      exact le_trans (ih count) (step_contains_inner layer (state layers elem alignment metadata))
+
+theorem suffix_zero_size_fits (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment limit count : Nat) (hfit : (state layers elem alignment 0).1 ≤ limit) :
+    (state (layers.drop count) elem alignment 0).1 ≤ limit :=
+  le_trans (state_contains_suffix layers elem alignment 0 count) hfit
+
+theorem step_contains_placed_field (layer : layout.nested_reference.NestedLayer)
+    (inner : Nat × Nat) :
+    LayoutMath.roundUp layer.prefix_bytes.val (min inner.2 layer.packed.val) + inner.1 ≤
+      (step layer inner).1 := by
+  simp only [step, LayoutMath.roundUp]
+  omega
+
+theorem step_contains_prefix (layer : layout.nested_reference.NestedLayer)
+    (inner : Nat × Nat) : layer.prefix_bytes.val ≤ (step layer inner).1 := by
+  simp only [step, LayoutMath.roundUp]
+  omega
+
+theorem valid_cons (layer : layout.nested_reference.NestedLayer)
+    (layers : List layout.nested_reference.NestedLayer) (elem alignment : Nat) :
+    valid (layer :: layers) elem alignment ↔ layerValid layer ∧ valid layers elem alignment := by
+  simp only [valid, List.mem_cons, forall_eq_or_imp]
+  tauto
+
+noncomputable def checkedState (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata : Nat) : Option (Nat × Nat) := by
+  classical
+  exact if valid layers elem alignment then
+    if (state layers elem alignment metadata).1 ≤ Usize.max
+      then some (state layers elem alignment metadata) else none
+    else none
+
+noncomputable def checkedLayer (layer : layout.nested_reference.NestedLayer)
+    (inner : Option (Nat × Nat)) : Option (Nat × Nat) := by
+  classical
+  exact if layerValid layer then inner.bind (fun inner =>
+    if (step layer inner).1 ≤ Usize.max then some (step layer inner) else none) else none
+
+theorem checkedState_cons (layer : layout.nested_reference.NestedLayer)
+    (layers : List layout.nested_reference.NestedLayer) (elem alignment metadata : Nat) :
+    checkedState (layer :: layers) elem alignment metadata =
+      checkedLayer layer (checkedState layers elem alignment metadata) := by
+  classical
+  by_cases hl : layerValid layer
+  · by_cases hv : valid layers elem alignment
+    · by_cases hf : (state layers elem alignment metadata).1 ≤ Usize.max
+      · simp only [checkedState, checkedLayer, valid_cons, hl, hv, true_and, if_true,
+          hf, state_cons, Option.bind_some]
+      · have ho : ¬(step layer (state layers elem alignment metadata)).1 ≤ Usize.max := by
+          have := step_contains_inner layer (state layers elem alignment metadata)
+          omega
+        simp only [checkedState, checkedLayer, valid_cons, hl, hv, true_and, if_true,
+          hf, if_false, state_cons, ho, Option.bind_none]
+    · simp only [checkedState, checkedLayer, valid_cons, hl, hv, true_and, if_false,
+        if_true, Option.bind_none]
+  · simp only [checkedState, checkedLayer, valid_cons, hl, false_and, if_false]
+
+theorem checkedState_some (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata : Nat) (out : Nat × Nat)
+    (h : checkedState layers elem alignment metadata = some out) :
+    valid layers elem alignment ∧ state layers elem alignment metadata = out ∧ out.1 ≤ Usize.max := by
+  classical
+  unfold checkedState at h
+  split at h
+  · rename_i hv
+    split at h
+    · rename_i hf
+      have heq := Option.some.inj h
+      exact ⟨hv, heq, heq ▸ hf⟩
+    · contradiction
+  · contradiction
+
+theorem checkedState_drop (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata i : Nat) (hi : i < layers.length) :
+    checkedState (layers.drop i) elem alignment metadata =
+      checkedLayer layers[i] (checkedState (layers.drop (i + 1)) elem alignment metadata) := by
+  rw [List.drop_eq_getElem_cons hi, checkedState_cons]
+
+noncomputable def checkedSize (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata : Nat) : Option Nat := by
+  classical
+  exact if valid layers elem alignment then
+    if (state layers elem alignment metadata).1 ≤ Usize.max
+      then some (state layers elem alignment metadata).1 else none
+    else none
+
+theorem checkedSize_eq_map (layers : List layout.nested_reference.NestedLayer)
+    (elem alignment metadata : Nat) :
+    checkedSize layers elem alignment metadata =
+      (checkedState layers elem alignment metadata).map Prod.fst := by
+  classical
+  unfold checkedSize checkedState
+  split <;> (try split) <;> simp
+
+end Zerocopy.Proofs.NestedReference
diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean
index 19453e6e6c..e2b5a5aa10 100644
--- a/verification/aeneas/lean/Obligations.lean
+++ b/verification/aeneas/lean/Obligations.lean
@@ -30,6 +30,29 @@ or a second proof that the compiler implements Rust correctly.
 open Aeneas Aeneas.Std AeneasSpecs
 namespace Zerocopy.Obligations
 open Zerocopy.Proofs
+
+def nested_round_up_spec_contract (size align : Usize)
+    (run : Result (Option Usize)) : Prop :=
+  run ⦃ rounded => rounded.map UScalar.val =
+    if align.val = 0 then none
+    else if LayoutMath.roundUp size.val align.val ≤ Usize.max
+      then some (LayoutMath.roundUp size.val align.val) else none ⦄
+
+def nested_round_up_spec : Prop :=
+  ∀ size align, nested_round_up_spec_contract size align
+    (layout.nested_reference.round_up size align)
+
+def nested_reference_size_spec_contract
+    (leading : Slice layout.nested_reference.NestedLayer) (elem_size leaf_align elems : Usize)
+    (run : Result (Option Usize)) : Prop :=
+  run ⦃ result => result.map UScalar.val =
+    NestedReference.checkedSize leading.val elem_size.val leaf_align.val elems.val ⦄
+
+def nested_reference_size_spec : Prop :=
+  ∀ leading elem_size leaf_align elems,
+    nested_reference_size_spec_contract leading elem_size leaf_align elems
+      (layout.nested_reference.size_for_metadata leading elem_size leaf_align elems)
+
 abbrev NonZeroUsize :=
   core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner
 
diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean
index 89ff7b9e67..bee36adb80 100644
--- a/verification/aeneas/lean/Proofs.lean
+++ b/verification/aeneas/lean/Proofs.lean
@@ -9,6 +9,7 @@ those terms. -/
 module
 public import Specs
 public import Proofs.Util
+public import Proofs.NestedReference
 public import Aeneas
 public import Loops
 public import RepresentationLaws
diff --git a/verification/aeneas/lean/Proofs/NestedReference.lean b/verification/aeneas/lean/Proofs/NestedReference.lean
new file mode 100644
index 0000000000..071f791689
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/NestedReference.lean
@@ -0,0 +1,419 @@
+/- 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 Specs
+public import Loops
+public import Obligations
+public import ModelLemmas
+import all Init.Data.Nat.Power2.Basic
+@[expose] public section
+
+open Aeneas Aeneas.Std
+namespace Zerocopy.Proofs.Raw
+
+def nestedStateView (state : Usize × Usize) : Nat × Nat := (state.1.val, state.2.val)
+
+theorem nested_round_up_spec (size align : Usize) :
+    layout.nested_reference.round_up size align
+      ⦃ rounded => rounded.map UScalar.val =
+        if align.val = 0 then none
+        else if LayoutMath.roundUp size.val align.val ≤ Usize.max
+          then some (LayoutMath.roundUp size.val align.val) else none ⦄ := by
+  unfold layout.nested_reference.round_up
+  by_cases hz : align = 0#usize
+  · subst align
+    simp
+  · simp only [hz, if_false]
+    have ha : 0 < align.val := by
+      have hn : align.val ≠ 0 := by
+        intro h
+        apply hz
+        exact UScalar.eq_of_val_eq (by simpa using h)
+      omega
+    step with Usize.rem_spec size (y := align) (by omega) as ⟨remainder, hr⟩
+    by_cases hrz : remainder = 0#usize
+    · have hr0 : size.val % align.val = 0 := by
+        have h := congrArg UScalar.val hrz
+        simpa only [hr, show (0#usize).val = 0 by simp] using h
+      simp only [hrz, if_true, WP.spec_ok, Option.map_some,
+        show ¬align.val = 0 by omega, if_false, LayoutMath.roundUp_eq _ _ hr0,
+        show size.val ≤ Usize.max by scalar_tac, if_true]
+    · simp only [hrz, if_false]
+      have hrem := Nat.mod_lt size.val ha
+      step with Usize.sub_spec (x := align) (y := remainder) (by rw [hr]; omega)
+        as ⟨padding, hp, _⟩
+      have hrpos : 0 < size.val % align.val := by
+        have hn : remainder.val ≠ 0 := by
+          intro h
+          apply hrz
+          exact UScalar.eq_of_val_eq (by simpa using h)
+        omega
+      have hp' : padding.val = (align.val - size.val % align.val) % align.val := by
+        have hm : (align.val - size.val % align.val) % align.val =
+            align.val - size.val % align.val := Nat.mod_eq_of_lt (by omega)
+        rw [hp, hr, hm]
+      have hchecked := Usize.checked_add_bv_spec size padding
+      cases hc : Usize.checked_add size padding <;>
+        simp only [hc] at hchecked
+      · have hn : ¬LayoutMath.roundUp size.val align.val ≤ Usize.max := by
+          unfold LayoutMath.roundUp
+          omega
+        simp only [Option.map_none, show ¬align.val = 0 by omega, if_false, hn]
+      · rename_i rounded
+        have hs : LayoutMath.roundUp size.val align.val ≤ Usize.max := by
+          unfold LayoutMath.roundUp
+          omega
+        simp only [Option.map_some, show ¬align.val = 0 by omega, if_false, hs, if_true]
+        congr 1
+        unfold LayoutMath.roundUp
+        omega
+
+theorem nested_apply_layer_spec (layer : layout.nested_reference.NestedLayer)
+    (size alignment : Usize) (ha : alignment.val.isPowerOfTwo) :
+    layout.nested_reference.apply_layer layer size alignment
+      ⦃ result => result.map nestedStateView =
+        NestedReference.checkedLayer layer (some (size.val, alignment.val)) ⦄ := by
+  classical
+  unfold layout.nested_reference.apply_layer
+  step as ⟨packedPow, hp⟩
+  cases packedPow with
+  | false =>
+    have hn : ¬layer.packed.val.isPowerOfTwo := by
+      intro h
+      have := (Iff.of_eq hp).mpr h
+      contradiction
+    have hl : ¬NestedReference.layerValid layer := by
+      intro h
+      exact hn h.1
+    simp only [Bool.false_eq_true, if_false, WP.spec_ok, Option.map_none,
+      NestedReference.checkedLayer, hl, if_false]
+  | true =>
+    have hp' : layer.packed.val.isPowerOfTwo := (Iff.of_eq hp).mp rfl
+    simp only [if_true]
+    step as ⟨minimumPow, hm⟩
+    cases minimumPow with
+    | false =>
+      have hn : ¬layer.min_align.val.isPowerOfTwo := by
+        intro h
+        have := (Iff.of_eq hm).mpr h
+        contradiction
+      have hl : ¬NestedReference.layerValid layer := by
+        intro h
+        exact hn h.2.1
+      simp only [Bool.false_eq_true, if_false, WP.spec_ok, Option.map_none,
+        NestedReference.checkedLayer, hl, if_false]
+    | true =>
+      have hm' : layer.min_align.val.isPowerOfTwo := (Iff.of_eq hm).mp rfl
+      simp only [if_true, UScalar.lt_equiv]
+      split
+      · rename_i hlarge
+        have hl : ¬NestedReference.layerValid layer := by
+          intro h
+          exact not_lt_of_ge h.2.2 hlarge
+        simp only [WP.spec_ok, Option.map_none, NestedReference.checkedLayer, hl, if_false]
+      · rename_i hsmall
+        have hl : NestedReference.layerValid layer := ⟨hp', hm', by omega⟩
+        let field := min alignment layer.packed
+        have hfieldRaw : (if alignment < layer.packed then Result.ok alignment else .ok layer.packed) =
+            Result.ok field := by
+          by_cases h : alignment < layer.packed
+          · simp only [h, if_true, field, min_eq_left (le_of_lt h)]
+          · simp only [h, if_false, field, min_eq_right (le_of_not_gt h)]
+        have hfield : (if alignment.val < layer.packed.val then Result.ok alignment else .ok layer.packed) =
+            Result.ok field := by simpa only [UScalar.lt_equiv] using hfieldRaw
+        simp only [hfield, bind_ok]
+        have hf : field.val = min alignment.val layer.packed.val := Arithmetic.coe_min _ _
+        have hfp : field.val.isPowerOfTwo := by
+          rw [hf]
+          by_cases h : alignment.val ≤ layer.packed.val
+          · simpa only [Nat.min_eq_left h] using ha
+          · simpa only [Nat.min_eq_right (by omega : layer.packed.val ≤ alignment.val)] using hp'
+        have hfpos := Nat.pos_of_isPowerOfTwo hfp
+        step with nested_round_up_spec layer.prefix_bytes field as ⟨offset, hoffset⟩
+        change offset.map UScalar.val = if field.val = 0 then none else
+          if LayoutMath.roundUp layer.prefix_bytes.val field.val ≤ Usize.max then
+            some (LayoutMath.roundUp layer.prefix_bytes.val field.val) else none at hoffset
+        simp only [show ¬field.val = 0 by omega, if_false] at hoffset
+        let outer := max layer.min_align field
+        have houtRaw : (if layer.min_align < field then Result.ok field else .ok layer.min_align) =
+            Result.ok outer := by
+          by_cases h : layer.min_align < field
+          · simp only [h, if_true, outer, max_eq_right (le_of_lt h)]
+          · simp only [h, if_false, outer, max_eq_left (le_of_not_gt h)]
+        have hout : (if layer.min_align.val < field.val then Result.ok field else .ok layer.min_align) =
+            Result.ok outer := by simpa only [UScalar.lt_equiv] using houtRaw
+        have ho : outer.val = max layer.min_align.val field.val := Arithmetic.coe_max _ _
+        have hopos : 0 < outer.val := by
+          rw [ho]
+          have := Nat.le_max_right layer.min_align.val field.val
+          omega
+        let target := NestedReference.step layer (size.val, alignment.val)
+        have htarget : target =
+            (LayoutMath.roundUp (LayoutMath.roundUp layer.prefix_bytes.val field.val + size.val)
+              outer.val, outer.val) := by
+          simp only [target, NestedReference.step, hf, ho]
+        have hcontains : LayoutMath.roundUp layer.prefix_bytes.val field.val ≤ target.1 := by
+          rw [htarget]
+          simp only [LayoutMath.roundUp]
+          omega
+        have hmodel : NestedReference.checkedLayer layer (some (size.val, alignment.val)) =
+            if target.1 ≤ Usize.max then some target else none := by
+          simp only [NestedReference.checkedLayer, hl, if_true, Option.bind_some]
+          rfl
+        simp only [hmodel]
+        cases offset with
+        | none =>
+          have hnot : ¬LayoutMath.roundUp layer.prefix_bytes.val field.val ≤ Usize.max := by
+            split at hoffset <;> simp_all
+          have hn : ¬target.1 ≤ Usize.max := by omega
+          simp only [WP.spec_ok, Option.map_none, hn, if_false]
+        | some offset =>
+          have hv : offset.val = LayoutMath.roundUp layer.prefix_bytes.val field.val := by
+            split at hoffset <;> simp_all
+          simp only [hout, bind_ok]
+          step as ⟨unpadded, hu⟩
+          cases unpadded with
+          | none =>
+            have hsum : Usize.max < offset.val + size.val := hu
+            have hn : ¬target.1 ≤ Usize.max := by
+              rw [htarget]
+              simp only [LayoutMath.roundUp] at hv ⊢
+              omega
+            simp only [WP.spec_ok, Option.map_none, hn, if_false]
+          | some unpadded =>
+            have husize : unpadded.val = offset.val + size.val := hu.2.1
+            step with nested_round_up_spec unpadded outer as ⟨rounded, hr⟩
+            change rounded.map UScalar.val = if outer.val = 0 then none else
+              if LayoutMath.roundUp unpadded.val outer.val ≤ Usize.max then
+                some (LayoutMath.roundUp unpadded.val outer.val) else none at hr
+            simp only [show ¬outer.val = 0 by omega, if_false] at hr
+            have hround : LayoutMath.roundUp unpadded.val outer.val = target.1 := by
+              rw [husize, hv, htarget]
+            rw [hround] at hr
+            cases rounded with
+            | none =>
+              have hn : ¬target.1 ≤ Usize.max := by split at hr <;> simp_all
+              simp only [WP.spec_ok, Option.map_none, hn, if_false]
+            | some rounded =>
+              have ht : target.1 ≤ Usize.max := by split at hr <;> simp_all
+              have hsize : rounded.val = target.1 := by split at hr <;> simp_all
+              have halign : outer.val = target.2 := by rw [htarget]
+              simp only [WP.spec_ok, Option.map_some, nestedStateView, ht, if_true, hsize, halign,
+                Prod.mk.eta]
+
+/-- The reverse loop retains complete recursive size at every layer. Its
+termination measure is the remaining layer index; no bound limits nesting. -/
+theorem nested_reference_loop_spec
+    (leading : Slice layout.nested_reference.NestedLayer) (elem alignment metadata : Nat)
+    (state : Option (Usize × Usize)) (i : Usize)
+    (hi : i.val ≤ leading.val.length)
+    (hv : state.map nestedStateView =
+      NestedReference.checkedState (leading.val.drop i.val) elem alignment metadata) :
+    layout.nested_reference.size_for_metadata_loop leading state i
+      ⦃ out => out.map nestedStateView =
+        NestedReference.checkedState leading.val elem alignment metadata ⦄ := by
+  unfold layout.nested_reference.size_for_metadata_loop
+  apply loop.spec_decr_nat
+    (fun s : Option (Usize × Usize) × Usize => s.2.val)
+    (fun s => s.2.val ≤ leading.val.length ∧ s.1.map nestedStateView =
+      NestedReference.checkedState (leading.val.drop s.2.val) elem alignment metadata)
+  · rintro ⟨state, idx⟩ ⟨hi, hv⟩
+    dsimp only at hi hv ⊢
+    unfold layout.nested_reference.size_for_metadata_loop.body
+    simp only [bne_iff_ne]
+    split
+    · rename_i hn
+      have hpos : 0 < idx.val := by
+        have hz : idx.val ≠ 0 := by
+          intro h
+          apply hn
+          exact UScalar.eq_of_val_eq (by simpa using h)
+        omega
+      step with Usize.sub_spec (x := idx) (y := 1#usize) (by simp; omega)
+        as ⟨j, hj, _⟩
+      have hj' : j.val + 1 = idx.val := by
+        change j.val = idx.val - 1 at hj
+        omega
+      have hjlt : j.val < leading.val.length := by omega
+      step with Slice.index_usize_spec leading j hjlt as ⟨layer, hlayer⟩
+      have hmath : NestedReference.checkedState (leading.val.drop j.val) elem alignment metadata =
+          NestedReference.checkedLayer layer
+            (NestedReference.checkedState (leading.val.drop idx.val) elem alignment metadata) := by
+        rw [NestedReference.checkedState_drop leading.val elem alignment metadata j.val hjlt,
+          hj', hlayer]
+      cases state with
+      | none =>
+        have hnext : (none : Option (Usize × Usize)).map nestedStateView =
+            NestedReference.checkedState (leading.val.drop j.val) elem alignment metadata := by
+          rw [hmath, ← hv]
+          simp [NestedReference.checkedLayer]
+        apply WP.spec.ret
+        change j.val ≤ leading.val.length ∧
+          (none : Option (Usize × Usize)).map nestedStateView =
+            NestedReference.checkedState (leading.val.drop j.val) elem alignment metadata ∧
+          j.val < idx.val
+        exact ⟨by omega, hnext, by omega⟩
+      | some pair =>
+        have heq : NestedReference.checkedState (leading.val.drop idx.val) elem alignment metadata =
+            some (nestedStateView pair) := hv.symm
+        obtain ⟨hvalid, heq, hfit⟩ := NestedReference.checkedState_some
+          (leading.val.drop idx.val) elem alignment metadata (nestedStateView pair) heq
+        have hpower : pair.2.val.isPowerOfTwo := by
+          have hp := NestedReference.state_alignment_power (leading.val.drop idx.val)
+            elem alignment metadata hvalid
+          rw [heq] at hp
+          exact hp
+        rcases pair with ⟨size, currentAlignment⟩
+        step with nested_apply_layer_spec layer size currentAlignment hpower as ⟨next, hnext⟩
+        have hview : next.map nestedStateView =
+            NestedReference.checkedState (leading.val.drop j.val) elem alignment metadata := by
+          rw [hmath, ← hv]
+          exact hnext
+        exact ⟨by omega, hview, by omega⟩
+    · rename_i hz
+      have heq : idx.val = 0 := by
+        have h : idx = 0#usize := not_ne_iff.mp hz
+        simpa using congrArg UScalar.val h
+      simpa only [heq, List.drop_zero, WP.spec_ok] using hv
+  · exact ⟨hi, hv⟩
+
+theorem nested_reference_size_spec
+    (leading : Slice layout.nested_reference.NestedLayer) (elem_size leaf_align elems : Usize) :
+    layout.nested_reference.size_for_metadata leading elem_size leaf_align elems
+      ⦃ result => result.map UScalar.val =
+        NestedReference.checkedSize leading.val elem_size.val leaf_align.val elems.val ⦄ := by
+  classical
+  unfold layout.nested_reference.size_for_metadata
+  step as ⟨leafPow, hp⟩
+  cases leafPow with
+  | false =>
+    have hn : ¬leaf_align.val.isPowerOfTwo := by
+      intro h
+      have := (Iff.of_eq hp).mpr h
+      contradiction
+    have hv : ¬NestedReference.valid leading.val elem_size.val leaf_align.val := by
+      intro h
+      exact hn h.1
+    simp only [Bool.false_eq_true, if_false, WP.spec_ok, Option.map_none,
+      NestedReference.checkedSize, hv, if_false]
+  | true =>
+    have hpow : leaf_align.val.isPowerOfTwo := (Iff.of_eq hp).mp rfl
+    have hpos := Nat.pos_of_isPowerOfTwo hpow
+    simp only [if_true]
+    step with Usize.rem_spec elem_size (y := leaf_align) (by omega) as ⟨remainder, hr⟩
+    simp only [bne_iff_ne]
+    split
+    · rename_i hn
+      have hv : ¬NestedReference.valid leading.val elem_size.val leaf_align.val := by
+        intro h
+        apply hn
+        exact UScalar.eq_of_val_eq (by simpa only [hr, show (0#usize).val = 0 by simp] using h.2.1)
+      simp only [WP.spec_ok, Option.map_none, NestedReference.checkedSize, hv, if_false]
+    · rename_i hz
+      have hzero : elem_size.val % leaf_align.val = 0 := by
+        have h : remainder = 0#usize := not_ne_iff.mp hz
+        simpa only [hr, show (0#usize).val = 0 by simp] using congrArg UScalar.val h
+      step as ⟨product, hproduct⟩
+      let start : Option (Usize × Usize) := match product with
+        | none => none
+        | some size => some (size, leaf_align)
+      have hinit : start.map nestedStateView =
+          NestedReference.checkedState (leading.val.drop (Slice.len leading).val)
+            elem_size.val leaf_align.val elems.val := by
+        have hvalid : NestedReference.valid [] elem_size.val leaf_align.val :=
+          ⟨hpow, hzero, by simp⟩
+        simp only [Slice.len_val, Slice.length, List.drop_length, NestedReference.checkedState,
+          hvalid, if_true, NestedReference.state, List.foldr_nil]
+        cases product with
+        | none =>
+          have hn : ¬elems.val * elem_size.val ≤ Usize.max := by
+            simp only [] at hproduct
+            rw [Nat.mul_comm]
+            omega
+          simp only [start, Option.map_none, hn, if_false]
+        | some size =>
+          have hv : size.val = elems.val * elem_size.val := by
+            simp only [] at hproduct
+            rw [Nat.mul_comm]
+            exact hproduct.2.1
+          have hf : elems.val * elem_size.val ≤ Usize.max := by
+            simp only [] at hproduct
+            rw [Nat.mul_comm]
+            exact hproduct.1
+          simp only [start, Option.map_some, nestedStateView, hv, hf, if_true]
+      have hrun := nested_reference_loop_spec leading elem_size.val leaf_align.val elems.val
+        start (Slice.len leading) (by simp only [Slice.len_val, Slice.length, le_refl]) hinit
+      cases product <;> simp only [start] at hrun ⊢
+      all_goals
+        step with hrun as ⟨out, hout⟩
+        have hfinal : (match out with | none => none | some pair => some pair.1).map UScalar.val =
+            NestedReference.checkedSize leading.val elem_size.val leaf_align.val elems.val := by
+          rw [NestedReference.checkedSize_eq_map, ← hout]
+          cases out <;> rfl
+        cases out with
+        | none => simpa only [WP.spec_ok] using hfinal
+        | some pair =>
+          rcases pair with ⟨size, alignment⟩
+          dsimp only
+          exact WP.spec.ret hfinal
+
+end Zerocopy.Proofs.Raw
+
+namespace Zerocopy.Proofs
+open AeneasSpecs
+
+theorem nested_round_up_spec : Zerocopy.Specs.nested_round_up_spec := by
+  intro size align sizeValue hsize alignValue halign
+  apply WP.spec_mono (Raw.nested_round_up_spec size align)
+  intro rounded hr
+  refine ⟨rounded.map unsignedWord, ?_, hr⟩
+  cases rounded <;> rfl
+register_spec_step nested_round_up_spec
+
+theorem nested_reference_size_spec : Zerocopy.Specs.nested_reference_size_spec := by
+  intro leading elem_size leaf_align elems layers hl elemValue he alignmentValue ha metadataValue hn
+  apply WP.spec_mono (Raw.nested_reference_size_spec leading elem_size leaf_align elems)
+  intro result hr
+  refine ⟨result.map unsignedWord, ?_, hr⟩
+  cases result <;> rfl
+register_spec_step nested_reference_size_spec
+
+/-- No descriptor bit pattern is excluded by a hidden decoder guard. -/
+theorem nested_layer_decoder_total (raw : layout.nested_reference.NestedLayer) :
+    isValid raw := by
+  refine ⟨⟨unsignedWord raw.packed, unsignedWord raw.min_align,
+    unsignedWord raw.prefix_bytes⟩, ?_⟩
+  rfl
+
+theorem nested_layers_decoder_total (raw : Slice layout.nested_reference.NestedLayer) :
+    isValid raw :=
+  (slice_valid_iff raw).mpr (fun layer _ => nested_layer_decoder_total layer)
+
+@[contract_simps] theorem nested_reference_size_spec_implies_required
+    (leading : Slice layout.nested_reference.NestedLayer) (elem_size leaf_align elems : Usize)
+    (run : Result (Option Usize))
+    (provided : Zerocopy.Specs.nested_reference_size_spec_contract leading elem_size leaf_align elems run) :
+    Zerocopy.Obligations.nested_reference_size_spec_contract leading elem_size leaf_align elems run := by
+  obtain ⟨layers, hlayers⟩ := nested_layers_decoder_total leading
+  have execution := provided layers hlayers (unsignedWord elem_size) rfl
+    (unsignedWord leaf_align) rfl (unsignedWord elems) rfl
+  apply WP.spec_mono execution
+  rintro result ⟨decoded, hdecoded, hr⟩
+  exact hr
+
+@[contract_simps] theorem nested_round_up_spec_implies_required
+    (size align : Usize) (run : Result (Option Usize))
+    (provided : Zerocopy.Specs.nested_round_up_spec_contract size align run) :
+    Zerocopy.Obligations.nested_round_up_spec_contract size align run := by
+  have execution := provided (unsignedWord size) rfl (unsignedWord align) rfl
+  apply WP.spec_mono execution
+  rintro rounded ⟨decoded, hdecoded, hr⟩
+  exact hr
+
+end Zerocopy.Proofs
diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs
index c99b48969f..9ad84757f8 100644
--- a/zerocopy/src/layout/mod.rs
+++ b/zerocopy/src/layout/mod.rs
@@ -9,6 +9,9 @@
 // This file may not be copied, modified, or distributed except according to
 // those terms.
 
+#[allow(dead_code)]
+mod nested_reference;
+
 use core::{mem, num::NonZeroUsize};
 
 use crate::util;
@@ -2044,7 +2047,7 @@ mod tests {
                 // [2]. Here `prefix` is the end of the preceding fields.
                 //
                 // [6] https://doc.rust-lang.org/1.93.0/reference/type-layout.html#reprc-structs
-                let offset = prefix.checked_add(util::padding_needed_for(prefix, field_align))?;
+                let offset = nested_reference::round_up(prefix, field_align.get())?;
 
                 // `repr(C)` uses the greatest field alignment [6], and an
                 // explicit alignment can only raise it [2]. Here `align`
@@ -2056,7 +2059,7 @@ mod tests {
                 // Advance past the complete field, then round to the struct's
                 // alignment, following `repr(C)`'s final sizing steps [6].
                 size = offset.checked_add(size)?;
-                size = size.checked_add(util::padding_needed_for(size, alignment))?;
+                size = nested_reference::round_up(size, alignment.get())?;
             }
             // Each enclosing size is at least its field's size. Thus any
             // checked multiplication or addition that overflowed above would
diff --git a/zerocopy/src/layout/nested_reference.rs b/zerocopy/src/layout/nested_reference.rs
new file mode 100644
index 0000000000..f13b4e0e10
--- /dev/null
+++ b/zerocopy/src/layout/nested_reference.rs
@@ -0,0 +1,120 @@
+// 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.
+
+//! Independent arithmetic for nested `repr(C)` slice DSTs.
+//!
+//! The layers run from outermost to innermost. Packing caps placement
+//! alignment, while every containing layer retains its field's complete size.
+//! These descriptors also model arithmetic combinations Rust rejects as types,
+//! including simultaneous packing and explicit alignment. No pointer or
+//! allocation operation consumes these synthetic layouts.
+
+// The pinned extraction does not model Option's Try trait. Explicit matches
+// also leave the overflow paths visible in this independent reference.
+#![allow(clippy::question_mark, clippy::manual_map)]
+
+/// One containing record, before placing its final field.
+///
+/// Plain words make the descriptor's mathematical decoding total. The Rust
+/// functions below check the domain explicitly, including zero alignments.
+#[derive(Copy, Clone)]
+#[cfg_attr(test, derive(Debug))]
+pub(super) struct NestedLayer {
+    pub(super) packed: usize,
+    pub(super) min_align: usize,
+    pub(super) prefix_bytes: usize,
+}
+
+/// Returns the least multiple of `align` at least `size`, if representable.
+///
+/// Zero alignment returns `None`. The remainder rule is independent of the
+/// production padding utility and works for every positive alignment.
+///
+/// ```aeneas
+/// spec nested_round_up_spec
+///   ensures(raw) rounded => rounded.map UScalar.val =
+///     if align.val = 0 then none
+///     else if LayoutMath.roundUp size.val align.val ≤ Usize.max
+///       then some (LayoutMath.roundUp size.val align.val) else none
+/// ```
+#[allow(clippy::arithmetic_side_effects)]
+pub(super) fn round_up(size: usize, align: usize) -> Option<usize> {
+    if align == 0 {
+        return None;
+    }
+    let remainder = size % align;
+    if remainder == 0 {
+        Some(size)
+    } else {
+        size.checked_add(align - remainder)
+    }
+}
+
+fn apply_layer(layer: NestedLayer, size: usize, alignment: usize) -> Option<(usize, usize)> {
+    if !layer.packed.is_power_of_two()
+        || !layer.min_align.is_power_of_two()
+        || layer.min_align > layer.packed
+    {
+        return None;
+    }
+    let field_align = if alignment < layer.packed { alignment } else { layer.packed };
+    let offset = match round_up(layer.prefix_bytes, field_align) {
+        Some(offset) => offset,
+        None => return None,
+    };
+    let alignment = if layer.min_align < field_align { field_align } else { layer.min_align };
+    let unpadded_size = match offset.checked_add(size) {
+        Some(size) => size,
+        None => return None,
+    };
+    let size = match round_up(unpadded_size, alignment) {
+        Some(size) => size,
+        None => return None,
+    };
+    Some((size, alignment))
+}
+
+/// Computes complete recursive size at any element count.
+///
+/// `None` means an invalid descriptor or `usize` overflow. An element size of
+/// zero is valid at every power-of-two alignment. Sizes above `isize::MAX`
+/// remain valid arithmetic results; no allocation is performed here.
+///
+/// ```aeneas
+/// spec nested_reference_size_spec
+///   ensures(raw) result => result.map UScalar.val =
+///     NestedReference.checkedSize leading.val elem_size.val leaf_align.val elems.val
+/// ```
+#[allow(clippy::arithmetic_side_effects, clippy::indexing_slicing)]
+pub(super) fn size_for_metadata(
+    leading: &[NestedLayer],
+    elem_size: usize,
+    leaf_align: usize,
+    elems: usize,
+) -> Option<usize> {
+    if !leaf_align.is_power_of_two() || elem_size % leaf_align != 0 {
+        return None;
+    }
+    let mut state = match elem_size.checked_mul(elems) {
+        Some(size) => Some((size, leaf_align)),
+        None => None,
+    };
+    let mut i = leading.len();
+    while i != 0 {
+        i -= 1;
+        let layer = leading[i];
+        state = match state {
+            Some((size, alignment)) => apply_layer(layer, size, alignment),
+            None => None,
+        };
+    }
+    match state {
+        Some((size, _)) => Some(size),
+        None => None,
+    }
+}