diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index d7c14b68ff..14c1f7d1a4 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -188,7 +188,7 @@ whole-program unsafe-code certification.
 
 ## Scope and proofs
 
-Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs).
+Rust review entry points: [arithmetic assertions](../../zerocopy/src/util/checks.rs), [nested reference](../../zerocopy/src/layout/nested_reference.rs), [primitive assertions](../../zerocopy/src/layout/primitive_checks.rs), [tail assertions](../../zerocopy/src/layout/tail_checks.rs).
 
 Extraction starts from the function and nominal-type owners of every present
 `aeneas` fence in `zerocopy/src`, including their dependencies. Every present
@@ -204,6 +204,7 @@ added without extending the specification set.
 | `DstLayout::{assume_shallow_unpadded,new_zst,for_type,for_unpadded_type,for_slice}` | Exact alignment, size-information fields, and recorded shallow-padding flags under explicit input premises. |
 | `SizeInfo::try_to_nonzero_elem_size`, `max_elems_for_bytes` | Exact zero handling, preserved representation fields, and greatest fitting element count. |
 | `DstLayout::requires_static_padding` | Exact negation of the recorded shallow-unpadded flag. |
+| Trailing size, padding, and capacity | Exact size-offset and capacity formulas, checked-size overflow, and wrapping padding; successful sizes and physical padding refine the independent recursive semantics. |
 
 Every registered function uses total `spec`: accepted raw representations,
 supplied mathematical ghosts, and explicit requirements imply successful
@@ -232,6 +233,9 @@ the unpadded flag; realizability, alignment and fit conditions remain explicit.
 Generic size/alignment reads are external data inputs, not correctness axioms.
 See [SEMANTICS.md](SEMANTICS.md) for the Rust correspondence premise.
 
+The checked trailing-size and padding contracts connect machine arithmetic
+to the independent recursive semantics.
+
 Plain arithmetic clauses use mathematical word values carrying machine bounds
 and NonZero positivity. Their Nat/Int arithmetic does not wrap; explicit raw
 clauses preserve the extracted representation vocabulary while retaining
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index 97afbdadea..a9067814a4 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -650,14 +650,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 23:0-23:62 -/
+    Source: 'src/layout/mod.rs', lines 26:0-26: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 103:4-122:5 -/
+    Source: 'src/layout/mod.rs', lines 106:4-125:5 -/
 def layout.RoundingAlignAndPhase.new
   (align : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize) :
@@ -678,7 +678,7 @@ def layout.RoundingAlignAndPhase.new
   | some encoded1 => ok { _0 := encoded1 }
 
 /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::components]:
-    Source: 'src/layout/mod.rs', lines 136:4-163:5 -/
+    Source: 'src/layout/mod.rs', lines 139:4-166:5 -/
 def layout.RoundingAlignAndPhase.components
   (self : layout.RoundingAlignAndPhase) :
   Result ((core.num.nonzero.NonZero Std.Usize
@@ -706,7 +706,7 @@ def layout.RoundingAlignAndPhase.components
     ok (align1, phase)
 
 /-- [zerocopy::layout::{zerocopy::layout::RoundingAlignAndPhase}::align]:
-    Source: 'src/layout/mod.rs', lines 176:4-185:5 -/
+    Source: 'src/layout/mod.rs', lines 179:4-188:5 -/
 def layout.RoundingAlignAndPhase.align
   (self : layout.RoundingAlignAndPhase) :
   Result (core.num.nonzero.NonZero Std.Usize
@@ -715,8 +715,126 @@ def layout.RoundingAlignAndPhase.align
   let (nz, _) ← layout.RoundingAlignAndPhase.components self
   ok nz
 
+/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
+    Source: 'src/util/mod.rs', lines 264:0-282:1 -/
+def util.round_down_to_next_multiple_of_alignment
+  (n : Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result Std.Usize
+  := do
+  let align1 ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  let b ← core.num.Usize.is_power_of_two align1
+  massert b
+  let i ← align1 - 1#usize
+  let mask ← lift (~~~ i)
+  ok (n &&& mask)
+
+/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout<E>}::size_offset]:
+    Source: 'src/layout/mod.rs', lines 268:4-281:5 -/
+def layout.TrailingSliceLayout.size_offset
+  {E : Type} (self : layout.TrailingSliceLayout E) : Result Std.Usize := do
+  let (size_align, size_phase) ←
+    layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase
+  let aligned_base ←
+    util.round_down_to_next_multiple_of_alignment self.size_base size_align
+  ok (aligned_base ||| size_phase)
+
+/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout<E>}::max_trailing_bytes]:
+    Source: 'src/layout/mod.rs', lines 304:4-393:5 -/
+def layout.TrailingSliceLayout.max_trailing_bytes
+  {E : Type} (self : layout.TrailingSliceLayout E)
+  (available_bytes : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  let (size_align, size_phase) ←
+    layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase
+  let rounded_phase ←
+    if size_phase = 0#usize
+    then ok 0#usize
+    else
+      core.num.nonzero.NonZero.get
+        Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align
+  let o ← lift (Usize.checked_add self.size_base rounded_phase)
+  match o with
+  | none => ok none
+  | some size =>
+    let o1 ← lift (Usize.checked_sub available_bytes size)
+    match o1 with
+    | none => ok none
+    | some bytes =>
+      let aligned_bytes ←
+        util.round_down_to_next_multiple_of_alignment bytes size_align
+      let initial_padding ← rounded_phase - size_phase
+      let trailing_bytes ← lift (aligned_bytes ||| initial_padding)
+      ok (some trailing_bytes)
+
+/-- [zerocopy::util::padding_needed_for]:
+    Source: 'src/util/mod.rs', lines 172:0-232:1 -/
+def util.padding_needed_for
+  (len : Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result Std.Usize
+  := do
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  let mask ← i - 1#usize
+  let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize)
+  let i2 ← lift (~~~ i1)
+  ok (i2 &&& mask)
+
+/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout<usize>}::padding_for_elems]:
+    Source: 'src/layout/mod.rs', lines 418:4-473:5 -/
+def layout.TrailingSliceLayoutUsize.padding_for_elems
+  (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) :
+  Result Std.Usize
+  := do
+  let (size_align, size_phase) ←
+    layout.RoundingAlignAndPhase.components self.size_rounding_align_and_phase
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner size_align
+  let size_mask ← i - 1#usize
+  let elem_remainder ← lift (self.elem_size &&& size_mask)
+  let i1 ← lift (core.num.Usize.wrapping_mul elems elem_remainder)
+  let trailing_remainder ← lift (i1 &&& size_mask)
+  let rounding_input ←
+    lift (core.num.Usize.wrapping_add size_phase trailing_remainder)
+  let rounding_padding ← util.padding_needed_for rounding_input size_align
+  let i2 ← lift (core.num.Usize.wrapping_add self.size_base size_phase)
+  let i3 ← lift (core.num.Usize.wrapping_sub i2 self.offset)
+  ok (core.num.Usize.wrapping_add i3 rounding_padding)
+
+/-- [zerocopy::layout::{zerocopy::layout::TrailingSliceLayout<usize>}::size_for_elems]:
+    Source: 'src/layout/mod.rs', lines 491:4-555:5 -/
+def layout.TrailingSliceLayoutUsize.size_for_elems
+  (self : layout.TrailingSliceLayout Std.Usize) (elems : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  let o ←
+    layout.TrailingSliceLayout.max_trailing_bytes self core.num.Usize.MAX
+  match o with
+  | none => ok none
+  | some bytes =>
+    let o1 ← lift (Usize.checked_mul self.elem_size elems)
+    match o1 with
+    | none => ok none
+    | some bytes1 =>
+      if bytes1 > bytes
+      then ok none
+      else
+        let trailing_end ←
+          lift (core.num.Usize.wrapping_add self.offset bytes1)
+        let i ← layout.TrailingSliceLayoutUsize.padding_for_elems self elems
+        let size ← lift (core.num.Usize.wrapping_add trailing_end i)
+        ok (some size)
+
 /-- [zerocopy::layout::{zerocopy::layout::SizeInfo<usize>}::try_to_nonzero_elem_size]:
-    Source: 'src/layout/mod.rs', lines 791:4-819:5 -/
+    Source: 'src/layout/mod.rs', lines 817:4-845:5 -/
 def layout.SizeInfoUsize.try_to_nonzero_elem_size
   (self : layout.SizeInfo Std.Usize) :
   Result (Option (layout.SizeInfo (core.num.nonzero.NonZero Std.Usize
@@ -741,7 +859,7 @@ def layout.SizeInfoUsize.try_to_nonzero_elem_size
         }))
 
 /-- [zerocopy::layout::max_elems_for_bytes]:
-    Source: 'src/layout/mod.rs', lines 847:0-862:1 -/
+    Source: 'src/layout/mod.rs', lines 873:0-888:1 -/
 def layout.max_elems_for_bytes
   (bytes : Std.Usize)
   (elem_size : core.num.nonzero.NonZero Std.Usize
@@ -758,7 +876,7 @@ def layout.max_elems_for_bytes
   | some used => ok (elems, used)
 
 /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::MIN_ALIGN]
-    Source: 'src/layout/mod.rs', lines 882:4-885:6 -/
+    Source: 'src/layout/mod.rs', lines 908:4-911:6 -/
 @[global_simps, irreducible]
 def layout.DstLayout.MIN_ALIGN
   :
@@ -773,13 +891,13 @@ def layout.DstLayout.MIN_ALIGN
   | some min_align => ok min_align
 
 /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::assume_shallow_unpadded]:
-    Source: 'src/layout/mod.rs', lines 951:4-960:5 -/
+    Source: 'src/layout/mod.rs', lines 977:4-986:5 -/
 def layout.DstLayout.assume_shallow_unpadded
   (self : layout.DstLayout) : Result layout.DstLayout := do
   ok { self with statically_shallow_unpadded := true }
 
 /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::new_zst]:
-    Source: 'src/layout/mod.rs', lines 989:4-1009:5
+    Source: 'src/layout/mod.rs', lines 1015:4-1035:5
     Visibility: public -/
 def layout.DstLayout.new_zst
   (repr_align : Option (core.num.nonzero.NonZero Std.Usize
@@ -803,7 +921,7 @@ def layout.DstLayout.new_zst
     }
 
 /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_type]:
-    Source: 'src/layout/mod.rs', lines 1033:4-1058:5
+    Source: 'src/layout/mod.rs', lines 1059:4-1084:5
     Visibility: public -/
 def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do
   let i ← core.mem.align_of T
@@ -822,7 +940,7 @@ def layout.DstLayout.for_type (T : Type) : Result layout.DstLayout := do
       }
 
 /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_unpadded_type]:
-    Source: 'src/layout/mod.rs', lines 1088:4-1102:5
+    Source: 'src/layout/mod.rs', lines 1114:4-1128:5
     Visibility: public -/
 def layout.DstLayout.for_unpadded_type
   (T : Type) : Result layout.DstLayout := do
@@ -830,7 +948,7 @@ def layout.DstLayout.for_unpadded_type
   layout.DstLayout.assume_shallow_unpadded dl
 
 /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::for_slice]:
-    Source: 'src/layout/mod.rs', lines 1127:4-1163:5 -/
+    Source: 'src/layout/mod.rs', lines 1153:4-1189:5 -/
 def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do
   let i ← core.mem.align_of T
   let o ←
@@ -856,7 +974,7 @@ def layout.DstLayout.for_slice (T : Type) : Result layout.DstLayout := do
       }
 
 /-- [zerocopy::layout::{zerocopy::layout::DstLayout}::requires_static_padding]:
-    Source: 'src/layout/mod.rs', lines 1554:4-1563:5
+    Source: 'src/layout/mod.rs', lines 1580:4-1589:5
     Visibility: public -/
 def layout.DstLayout.requires_static_padding
   (self : layout.DstLayout) : Result Bool := do
@@ -1069,6 +1187,116 @@ def layout.primitive_checks.check_empty_layout
     massert empty.statically_shallow_unpadded
   else ok ()
 
+/-- [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
+  (left : Option Std.Usize) (right : Option Std.Usize) : Result Bool := do
+  match left with
+  | none => match right with
+            | none => ok true
+            | some _ => ok false
+  | some left1 =>
+    match right with
+    | none => ok false
+    | some right1 => ok (left1 = right1)
+
+/-- [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
+  (bytes : Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result (Option Std.Usize)
+  := do
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  let remainder ← bytes % i
+  let padding ← if remainder = 0#usize
+                  then ok 0#usize
+                  else i - remainder
+  ok (Usize.checked_add bytes padding)
+
+/-- [zerocopy::layout::tail_checks::reference_size]:
+    Source: 'src/layout/tail_checks.rs', lines 44:0-60:1 -/
+def layout.tail_checks.reference_size
+  (tail : layout.TrailingSliceLayout Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (elems : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  let o ← lift (Usize.checked_mul elems tail.elem_size)
+  match o with
+  | none => ok none
+  | some bytes =>
+    let o1 ← lift (Usize.checked_add phase bytes)
+    match o1 with
+    | none => ok none
+    | some input =>
+      let o2 ← layout.tail_checks.reference_round_up input align
+      match o2 with
+      | none => ok none
+      | some rounded => ok (Usize.checked_add tail.size_base rounded)
+
+/-- [zerocopy::layout::tail_checks::reference_capacity]:
+    Source: 'src/layout/tail_checks.rs', lines 63:0-76:1 -/
+def layout.tail_checks.reference_capacity
+  (tail : layout.TrailingSliceLayout Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (budget : Std.Usize) :
+  Result (Option Std.Usize)
+  := do
+  let o ← lift (Usize.checked_sub budget tail.size_base)
+  match o with
+  | none => ok none
+  | some after_base =>
+    let i ←
+      core.num.nonzero.NonZero.get
+        Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+    let i1 ← after_base % i
+    let rounded_budget ← after_base - i1
+    ok (Usize.checked_sub rounded_budget phase)
+
+/-- [zerocopy::layout::tail_checks::trailing_arithmetic_check]:
+    Source: 'src/layout/tail_checks.rs', lines 88:0-111:1 -/
+def layout.tail_checks.trailing_arithmetic_check
+  (tail : layout.TrailingSliceLayout Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (elems : Std.Usize) (budget : Std.Usize) :
+  Result Unit
+  := do
+  let i ←
+    core.num.nonzero.NonZero.get
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+  let b ← core.num.Usize.is_power_of_two i
+  if b
+  then
+    if phase < i
+    then
+      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
+      let b1 ← layout.tail_checks.same_optional_usize o (some i1)
+      if b1
+      then
+        let o1 ← layout.TrailingSliceLayoutUsize.size_for_elems tail elems
+        let o2 ← layout.tail_checks.reference_size tail align phase elems
+        let b2 ← layout.tail_checks.same_optional_usize o1 o2
+        massert b2
+        let o3 ← layout.TrailingSliceLayout.max_trailing_bytes tail budget
+        let o4 ←
+          layout.tail_checks.reference_capacity tail align phase budget
+        let b3 ← layout.tail_checks.same_optional_usize o3 o4
+        massert b3
+      else ok ()
+    else ok ()
+  else ok ()
+
 /-- [zerocopy::util::bytewrite::exact]:
     Source: 'src/util/bytewrite/mod.rs', lines 27:0-37:1 -/
 def util.bytewrite.exact
@@ -1120,39 +1348,6 @@ def util.bytewrite.be_word_prefix
   let s ← lift (Array.to_slice a)
   util.bytewrite.prefix s dst
 
-/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 264:0-282:1 -/
-def util.round_down_to_next_multiple_of_alignment
-  (n : Std.Usize)
-  (align : core.num.nonzero.NonZero Std.Usize
-  core.num.niche_types.NonZeroUsizeInner) :
-  Result Std.Usize
-  := do
-  let align1 ←
-    core.num.nonzero.NonZero.get
-      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
-  let b ← core.num.Usize.is_power_of_two align1
-  massert b
-  let i ← align1 - 1#usize
-  let mask ← lift (~~~ i)
-  ok (n &&& mask)
-
-/-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 172:0-232:1 -/
-def util.padding_needed_for
-  (len : Std.Usize)
-  (align : core.num.nonzero.NonZero Std.Usize
-  core.num.niche_types.NonZeroUsizeInner) :
-  Result Std.Usize
-  := do
-  let i ←
-    core.num.nonzero.NonZero.get
-      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
-  let mask ← i - 1#usize
-  let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize)
-  let i2 ← lift (~~~ i1)
-  ok (i2 &&& mask)
-
 /-- [zerocopy::util::checks::check_arithmetic]:
     Source: 'src/util/checks.rs', lines 38:0-46:1 -/
 def util.checks.check_arithmetic
diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean
index 267aabb722..565f2aaf74 100644
--- a/verification/aeneas/golden/Types.lean
+++ b/verification/aeneas/golden/Types.lean
@@ -100,13 +100,13 @@ structure byteorder.U32 (O : Type) where
   _1 : core.marker.PhantomData O
 
 /-- [zerocopy::layout::RoundingAlignAndPhase]
-    Source: 'src/layout/mod.rs', lines 84:0-84:54 -/
+    Source: 'src/layout/mod.rs', lines 87:0-87:54 -/
 structure layout.RoundingAlignAndPhase where
   _0 : core.num.nonzero.NonZero Std.Usize
     core.num.niche_types.NonZeroUsizeInner
 
 /-- [zerocopy::layout::TrailingSliceLayout]
-    Source: 'src/layout/mod.rs', lines 191:0-245:1 -/
+    Source: 'src/layout/mod.rs', lines 194:0-248:1 -/
 structure layout.TrailingSliceLayout (E : Type) where
   offset : Std.Usize
   elem_size : E
@@ -114,14 +114,14 @@ structure layout.TrailingSliceLayout (E : Type) where
   size_rounding_align_and_phase : layout.RoundingAlignAndPhase
 
 /-- [zerocopy::layout::SizeInfo]
-    Source: 'src/layout/mod.rs', lines 53:0-56:1 -/
+    Source: 'src/layout/mod.rs', lines 56:0-59:1 -/
 @[discriminant isize]
 inductive layout.SizeInfo (E : Type) where
 | Sized : Std.Usize → layout.SizeInfo E
 | SliceDst : layout.TrailingSliceLayout E → layout.SizeInfo E
 
 /-- [zerocopy::layout::DstLayout]
-    Source: 'src/layout/mod.rs', lines 40:0-48:1
+    Source: 'src/layout/mod.rs', lines 43:0-51:1
     Visibility: public -/
 structure layout.DstLayout where
   align : core.num.nonzero.NonZero Std.Usize
diff --git a/verification/aeneas/lean/Corollaries.lean b/verification/aeneas/lean/Corollaries.lean
index edab313551..8adb0db7fd 100644
--- a/verification/aeneas/lean/Corollaries.lean
+++ b/verification/aeneas/lean/Corollaries.lean
@@ -14,14 +14,15 @@ import all Init.Data.Nat.Power2.Basic
 
 /-!
 A function contract is most useful when other proofs can consume it. These
-corollaries compose the checked arithmetic operation lemmas into further
-numeric consequences. They reuse the proved computation and discharge its
-stated requirements, rather than proving a different calculation in its
-place.
+corollaries compose the checked operation lemmas into arithmetic consequences
+and layout equivalence results. In particular, the recursive-size and direct
+record-placement results connect runtime normalization to independent layout
+mathematics for every metadata value in their stated domains.
 
-The results remain conditional functional guarantees. They do not establish
-pointer safety or prove that every Rust caller meets the contract's
-requirements.
+The bridge to an actual Rust type remains the explicit premise documented in
+SEMANTICS.md. A proof about extracted numerical operations does not itself
+prove pointer safety, nor does it prove that every Rust caller meets a
+contract's requirements.
 -/
 open Aeneas Aeneas.Std Aeneas.Std.Result
 namespace Zerocopy.Corollaries
@@ -82,4 +83,50 @@ theorem round_down_monotone (a b : Usize) (align : NonZeroUsize)
   apply (UScalar.le_equiv _ _).mpr
   exact hgreatest m.val ((UScalar.le_equiv _ _).mp (le_trans hbound hab)) haligned
 
+theorem size_matches_recursive (tail : layout.TrailingSliceLayout Usize)
+    (description : LayoutMath.Description) (n : Usize)
+    (hn : 0 < tail.size_rounding_align_and_phase._0.val.val)
+    (hd : description.valid)
+    (hr : trailingFormula tail = description.compile) :
+    layout.TrailingSliceLayoutUsize.size_for_elems tail n
+      ⦃ r => r.map UScalar.val =
+        if description.size n.val ≤ Usize.max then some (description.size n.val) else none ⦄ := by
+  step with Proofs.Raw.size_for_elems_spec tail n hn as ⟨r, hsize⟩
+  rw [hr, LayoutMath.Formula.checkedSize, LayoutMath.compile_size description hd] at hsize
+  exact hsize
+
+theorem padding_matches_recursive (tail : layout.TrailingSliceLayout Usize)
+    (description : LayoutMath.Description) (n : Usize)
+    (hn : 0 < tail.size_rounding_align_and_phase._0.val.val)
+    (hd : description.valid)
+    (hr : trailingFormula tail = description.compile)
+    (hfit : description.size n.val ≤ Usize.max) :
+    layout.TrailingSliceLayoutUsize.padding_for_elems tail n
+      ⦃ p => p.val + description.offset + n.val * description.elem = description.size n.val ⦄ := by
+  step with Proofs.Raw.padding_for_elems_spec tail n hn as ⟨p, hp⟩
+  have ho : tail.offset.val = description.offset := by
+    have h := congrArg LayoutMath.Formula.offset hr
+    simpa only [trailingFormula, byteFormula, LayoutMath.compile_offset] using h
+  have he : tail.elem_size.val = description.elem := by
+    have h := congrArg LayoutMath.Formula.elem hr
+    simpa only [trailingFormula, LayoutMath.compile_elem] using h
+  rw [ho, he, hr, LayoutMath.compile_size description hd] at hp
+  have hcontains := LayoutMath.description_contains_tail description n.val
+  let physical := description.offset + n.val * description.elem
+  let remaining := description.size n.val - physical
+  have hsum : remaining + physical = description.size n.val := by
+    dsimp only [remaining, physical]
+    omega
+  have hmod : Nat.ModEq (UScalar.size .Usize) (p.val + physical) (remaining + physical) := by
+    change (p.val + physical) % UScalar.size .Usize =
+      (remaining + physical) % UScalar.size .Usize
+    rw [hsum]
+    simpa only [physical, Nat.add_assoc, UScalar.size_UScalarTyUsize] using hp
+  have hcancel := Nat.ModEq.add_right_cancel' physical hmod
+  have hremaining : remaining ≤ Usize.max := by dsimp only [remaining]; omega
+  change p.val % UScalar.size .Usize = remaining % UScalar.size .Usize at hcancel
+  rw [Nat.mod_eq_of_lt (UScalar.hSize p), word_mod_of_le remaining hremaining] at hcancel
+  dsimp only [remaining, physical] at hcancel
+  omega
+
 end Zerocopy.Corollaries
diff --git a/verification/aeneas/lean/MathViews.lean b/verification/aeneas/lean/MathViews.lean
index ff28890d68..99f754dc03 100644
--- a/verification/aeneas/lean/MathViews.lean
+++ b/verification/aeneas/lean/MathViews.lean
@@ -167,6 +167,17 @@ def layoutValid (self : layout.DstLayout) : Prop :=
     (∃ value, layout.DstLayout.decode raw = some value) ↔
       layoutValid raw := layout_valid_iff raw
 
+-- Concrete contracts retain the automatic machine-word provider. Making its
+-- carrier explicit avoids recovering a raw dictionary from the type-only Fields
+-- family while preserving the generic admission theorem above.
+@[contract_simps] theorem trailing_usize_admitted_iff
+    (raw : layout.TrailingSliceLayout Usize) :
+    (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize),
+      RustModel.decode raw = some value) ↔
+      0 < raw.size_rounding_align_and_phase._0.val.val := by
+  simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using
+    trailing_admitted_iff raw
+
 @[contract_simps] theorem normalized_nat_pos_iff (n : Nat) :
     Nat.le (Nat.succ 0) n ↔ 0 < n := Nat.succ_le_iff
 
@@ -192,15 +203,6 @@ attribute [contract_simps] encodingValid trailingValid sizeInfoValid layoutValid
 
 -- A named decoder can also occur after a surrounding structural traversal
 -- exposes the retained dictionary. These are the same admission equivalences.
-@[contract_simps] theorem trailing_usize_admitted_iff
-    (raw : layout.TrailingSliceLayout Usize) :
-    (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize),
-      RustModel.decode raw = some value) ↔
-      0 < raw.size_rounding_align_and_phase._0.val.val := by
-  simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using
-    trailing_admitted_iff raw
-
--- Optional traversal exposes the same fixed provider's named decoder directly.
 @[contract_simps] theorem trailing_usize_decoder_admitted_iff
     (raw : layout.TrailingSliceLayout Usize) :
     (∃ value : layout.TrailingSliceLayout.Fields (UnsignedWord .Usize),
diff --git a/verification/aeneas/lean/ModelProjectionLaws.lean b/verification/aeneas/lean/ModelProjectionLaws.lean
index 2e6cfb0b1f..0c97fd6b6d 100644
--- a/verification/aeneas/lean/ModelProjectionLaws.lean
+++ b/verification/aeneas/lean/ModelProjectionLaws.lean
@@ -71,4 +71,13 @@ theorem layoutValue_decode (raw : layout.DstLayout) (value : layout.DstLayout.Fi
     simp only [ModelViews.layoutValue, layoutValue, hs, hva,
       trailingFormula_decode tail tailValue ht]
 
+/-- Optional machine sizes retain both absence and the exact numeric payload. -/
+theorem optionalSize_decode (raw : Option Usize) (value : Option (UnsignedWord .Usize))
+    (h : RustModel.decode raw = some value) :
+    value.map (fun size => (size : Nat)) = raw.map UScalar.val := by
+  cases raw <;>
+    simp only [RustModel.decode, Option.map_some,
+      Option.some.injEq] at h <;>
+    cases h <;> rfl
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean
index c64720befa..a645741c05 100644
--- a/verification/aeneas/lean/Obligations.lean
+++ b/verification/aeneas/lean/Obligations.lean
@@ -126,6 +126,50 @@ def encoding_align_spec : Prop :=
   ∀ (code : layout.RoundingAlignAndPhase),
     encoding_align_spec_contract code (layout.RoundingAlignAndPhase.align code)
 
+def size_offset_spec_contract (E : Type) (t : layout.TrailingSliceLayout E)
+    (run : Result Usize) : Prop :=
+  ∀ [RustModel E], trailingValid t →
+    ∃ offset, run = .ok offset ∧
+      offset.val = t.size_base.val - t.size_base.val % (byteFormula t).align + (byteFormula t).phase
+
+def size_offset_spec : Prop :=
+  ∀ (E : Type) (t : layout.TrailingSliceLayout E),
+    size_offset_spec_contract E t (layout.TrailingSliceLayout.size_offset t)
+
+def max_trailing_bytes_spec_contract
+    (E : Type) (t : layout.TrailingSliceLayout E) (budget : Usize)
+    (run : Result (Option Usize)) : Prop :=
+  ∀ [RustModel E],
+    trailingValid t →
+    ∃ cap, run = .ok cap ∧
+      cap.map UScalar.val = (byteFormula t).capacity budget.val
+
+def max_trailing_bytes_spec : Prop :=
+  ∀ (E : Type) (t : layout.TrailingSliceLayout E) (budget : Usize),
+    max_trailing_bytes_spec_contract E t budget
+      (layout.TrailingSliceLayout.max_trailing_bytes t budget)
+
+def padding_for_elems_spec_contract (t : layout.TrailingSliceLayout Usize) (n : Usize)
+    (run : Result Usize) : Prop :=
+  0 < t.size_rounding_align_and_phase._0.val.val →
+    ∃ p, run = .ok p ∧
+      (p.val + t.offset.val + n.val * t.elem_size.val) % UScalar.size .Usize =
+        (trailingFormula t).size n.val % UScalar.size .Usize
+
+def padding_for_elems_spec : Prop :=
+  ∀ (t : layout.TrailingSliceLayout Usize) (n : Usize),
+    padding_for_elems_spec_contract t n (layout.TrailingSliceLayoutUsize.padding_for_elems t n)
+
+def size_for_elems_spec_contract (t : layout.TrailingSliceLayout Usize) (n : Usize)
+    (run : Result (Option Usize)) : Prop :=
+  0 < t.size_rounding_align_and_phase._0.val.val →
+    ∃ size, run = .ok size ∧
+      size.map UScalar.val = (trailingFormula t).checkedSize Usize.max n.val
+
+def size_for_elems_spec : Prop :=
+  ∀ (t : layout.TrailingSliceLayout Usize) (n : Usize),
+    size_for_elems_spec_contract t n (layout.TrailingSliceLayoutUsize.size_for_elems t n)
+
 def try_nonzero_spec_contract (si : layout.SizeInfo Usize)
     (run : Result (Option (layout.SizeInfo NonZeroUsize))) : Prop :=
   sizeInfoValid si → run ⦃ r => (∀ next ∈ r, sizeInfoValid next) ∧
diff --git a/verification/aeneas/lean/Obligations/TailChecks.lean b/verification/aeneas/lean/Obligations/TailChecks.lean
new file mode 100644
index 0000000000..4fb4d750e6
--- /dev/null
+++ b/verification/aeneas/lean/Obligations/TailChecks.lean
@@ -0,0 +1,33 @@
+/- 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
+@[expose] public section
+
+open Aeneas Aeneas.Std
+namespace Zerocopy.Obligations
+open Zerocopy.Proofs
+set_option linter.unusedVariables false
+
+/- These roots promise that every assertion terminates on the full admitted
+Rust domain. Their observations are the executable assertions in tail_checks;
+the original method obligations retain their separate mathematical promises.
+-/
+def trailing_arithmetic_check_spec_contract
+    (tail : layout.TrailingSliceLayout Usize) (align : NonZeroUsize)
+    (phase elems budget : Usize) (run : Result Unit) : Prop :=
+  0 < tail.size_rounding_align_and_phase._0.val.val → 0 < align.val.val →
+    run ⦃ _ => True ⦄
+
+def trailing_arithmetic_check_spec : Prop :=
+  ∀ tail align phase elems budget,
+    trailing_arithmetic_check_spec_contract tail align phase elems budget
+      (layout.tail_checks.trailing_arithmetic_check tail align phase elems budget)
+
+end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean
index 0119cc2995..79cb66444e 100644
--- a/verification/aeneas/lean/Proofs.lean
+++ b/verification/aeneas/lean/Proofs.lean
@@ -14,6 +14,8 @@ public import Aeneas
 public import Loops
 public import LayoutModel
 public import RepresentationLaws
+public import ModelProjectionLaws
+public import Obligations
 public import LayoutMath
 import all Mathlib.Data.Nat.Log
 import all Init.Data.Nat.Power2.Basic
@@ -36,7 +38,8 @@ implementation each time.
 
 Aeneas Result describes execution success, panic, or divergence. Rust Option
 and Rust Result values may themselves be successful payloads. The proof must
-keep these cases distinct.
+keep these cases distinct. Corollaries connects the operation results to the
+independent recursive layout semantics under the explicit Rust premise.
 -/
 open Aeneas Aeneas.Std
 namespace Zerocopy.Proofs.Raw
@@ -205,6 +208,105 @@ theorem encoding_align_spec :
   step with encoding_components_spec self hn as ⟨a, p, _, _, _, ha, _⟩
   simpa only [WP.spec_ok] using ha
 
+/- Reading physical offset must preserve the raw word even though the element
+carrier can be generic. No size normalization is needed for this observation.
+-/
+theorem size_offset_spec :
+  ∀ {E : Type} (self : layout.TrailingSliceLayout E), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)),
+    @Zerocopy.layout.TrailingSliceLayout.size_offset E self ⦃ offset =>
+    offset.val = self.size_base.val - self.size_base.val % (byteFormula self).align + (byteFormula self).phase ⦄ := by
+  intro E self hn
+  unfold layout.TrailingSliceLayout.size_offset
+  step with encoding_components_spec _ hn as ⟨a, p, ha, hp, hsum, halign, hphase⟩
+  step with round_down_spec self.size_base a ha as ⟨base, _, hb, hmod, _, _⟩
+  simp only [UScalar.val_or]
+  rw [LayoutMath.aligned_or _ _ _ ha hmod hp, hb]
+  simp only [byteFormula]
+  rw [← halign]
+  omega
+
+/- Solve the rounded complete-size inequality for the greatest byte budget. The
+proof must preserve rounding plateaus and the case where even zero bytes do
+not fit; dividing by element stride belongs to a later operation.
+-/
+theorem max_trailing_bytes_spec :
+  ∀ {E : Type} (self : layout.TrailingSliceLayout E) (available_bytes : Usize), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)),
+    @Zerocopy.layout.TrailingSliceLayout.max_trailing_bytes E self available_bytes ⦃ r => r.map UScalar.val = (byteFormula self).capacity available_bytes.val ⦄ := by
+  intro E self available hn
+  unfold layout.TrailingSliceLayout.max_trailing_bytes
+  step with encoding_components_spec _ hn as ⟨a, p, ha, hp, hsum, halign, hphase⟩
+  have apos := Nat.pos_of_isPowerOfTwo ha
+  have hview : byteFormula self = ⟨self.size_base.val, p.val, a.val.val, 0, self.offset.val⟩ := by
+    unfold byteFormula
+    dsimp only
+    rw [← hphase, ← halign]
+  let rp : Usize := if p = 0#usize then 0#usize else a.val
+  have hrp : rp.val = LayoutMath.roundUp p.val a.val.val := by
+    rw [LayoutMath.roundUp_phase _ _ apos hp]
+    by_cases hz : p = 0#usize
+    · simp only [rp, hz, if_true]
+      rfl
+    · have hzero : p.val ≠ 0 := by
+        intro h
+        exact hz (UScalar.eq_of_val_eq (by simpa using h))
+      simp only [rp, hz, hzero, if_false]
+  have hrmod : rp.val % a.val.val = 0 := by rw [hrp]; exact (LayoutMath.roundUp_properties _ _ apos).2.2
+  have hrge : p.val ≤ rp.val := by rw [hrp]; exact (LayoutMath.roundUp_properties _ _ apos).1
+  have hrlt : rp.val - p.val < a.val.val := by
+    have := (LayoutMath.roundUp_properties p.val a.val.val apos).2.1
+    omega
+  have hbranch : (if p = 0#usize then Result.ok 0#usize else
+    core.num.nonzero.NonZero.get Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a) = Result.ok rp := by
+    simp only [core.num.nonzero.NonZero.get]
+    by_cases h : p = 0#usize <;> simp only [h, if_true, if_false, rp]
+  rw [hbranch]
+  simp only [bind_ok]
+  step as ⟨checked, hadd⟩
+  cases checked with
+  | none =>
+    simp only [] at hadd
+    have hav : available.val ≤ Usize.max := by scalar_tac
+    have hmiss : ¬(byteFormula self).bytes 0 ≤ available.val := by
+      rw [hview]
+      simp only [LayoutMath.Formula.bytes, Nat.add_zero, ← hrp]
+      omega
+    simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.capacity, hmiss, if_false]
+  | some minimum =>
+    simp only [] at hadd
+    step as ⟨checked, hsub⟩
+    cases checked with
+    | none =>
+      simp only [] at hsub
+      simp only []
+      have hmiss : ¬(byteFormula self).bytes 0 ≤ available.val := by
+        rw [hview]
+        simp only [LayoutMath.Formula.bytes, Nat.add_zero, ← hrp]
+        omega
+      simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.capacity, hmiss, if_false]
+    | some extra =>
+      simp only [] at hsub
+      simp only []
+      step with round_down_spec extra a ha as ⟨aligned, hle, hal, hmod, _, _⟩
+      step with Usize.sub_spec hrge as ⟨padding, hpadding, _⟩
+      have hfit : (byteFormula self).bytes 0 ≤ available.val := by
+        rw [hview]
+        simp only [LayoutMath.Formula.bytes, Nat.add_zero, ← hrp]
+        omega
+      simp only [lift, bind_ok, WP.spec_ok, Option.map_some,
+        LayoutMath.Formula.capacity, hfit, if_true]
+      have hpl : padding.val < a.val.val := by
+        dsimp only [rp] at hrlt
+        omega
+      rw [UScalar.val_or, LayoutMath.aligned_or _ _ _ ha hmod hpl]
+      rw [hview]
+      dsimp only
+      have hbudget : available.val - self.size_base.val = rp.val + extra.val := by omega
+      rw [hbudget, LayoutMath.floor_shift _ _ _ hrmod]
+      congr 1
+      have hrem := Nat.mod_le extra.val a.val.val
+      dsimp only [rp] at *
+      omega
+
 theorem assume_shallow_unpadded_spec :
   ∀ (self : layout.DstLayout),
     @Zerocopy.layout.DstLayout.assume_shallow_unpadded self ⦃ r => r.align = self.align ∧ r.size_info = self.size_info ∧ r.statically_shallow_unpadded = true ⦄ := by
@@ -302,6 +404,138 @@ theorem requires_static_padding_spec :
   simp only [layout.DstLayout.requires_static_padding, WP.spec_ok]
   cases self.statically_shallow_unpadded <;> rfl
 
+theorem wrapping_sub_cancel (x y : Usize) :
+    ((core.num.Usize.wrapping_sub x y).val + y.val) % UScalar.size .Usize = x.val := by
+  rw [core.num.Usize.wrapping_sub_val_eq, Nat.mod_add_mod]
+  have hy := UScalar.hSize y
+  rw [show x.val + (UScalar.size .Usize - y.val) + y.val =
+    x.val + UScalar.size .Usize by omega, Nat.add_mod_right]
+  exact Nat.mod_eq_of_lt (UScalar.hSize x)
+
+/- Compute padding with wrapping machine arithmetic. The raw theorem records the
+modular result; physical padding follows only when the complete size fits.
+-/
+theorem padding_for_elems_spec :
+  ∀ (self : layout.TrailingSliceLayout Usize) (elems : Usize), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)),
+    @Zerocopy.layout.TrailingSliceLayoutUsize.padding_for_elems self elems ⦃ p => (p.val + self.offset.val + elems.val * self.elem_size.val) % UScalar.size .Usize =
+    (trailingFormula self).size elems.val % UScalar.size .Usize ⦄ := by
+  intro self elems hn
+  unfold layout.TrailingSliceLayoutUsize.padding_for_elems
+  step with encoding_components_spec _ hn as ⟨a, r, ha, hr, hsum, halign, hphase⟩
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  have apos := Nat.pos_of_isPowerOfTwo ha
+  step with Usize.sub_spec (show (1#usize).val ≤ a.val.val by simpa using (show 1 ≤ a.val.val by omega)) as ⟨mask, hm, _⟩
+  simp only [lift, bind_ok]
+  have low (x : Usize) : (x &&& mask).val = x.val % a.val.val := by
+    obtain ⟨k, hk⟩ := ha
+    rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod]
+  let t := core.num.Usize.wrapping_mul elems (self.elem_size &&& mask) &&& mask
+  have ht : t.val = (elems.val * self.elem_size.val) % a.val.val := by
+    rw [low, core.num.Usize.wrapping_mul_val_eq, low,
+      Nat.mod_mod_of_dvd _ (Arithmetic.alignment_dvd_size a.val ha)]
+    rw [Nat.mul_mod, Nat.mod_mod, ← Nat.mul_mod]
+  let input := core.num.Usize.wrapping_add r t
+  have hi : input.val % a.val.val =
+      (r.val + elems.val * self.elem_size.val) % a.val.val := by
+    rw [core.num.Usize.wrapping_add_val_eq,
+      Nat.mod_mod_of_dvd _ (Arithmetic.alignment_dvd_size a.val ha), ht, Nat.add_mod_mod]
+  step with Zerocopy.Proofs.Raw.padding_lt_alignment input a ha as ⟨rp, _, hp, _, _, _⟩
+  have hp' : rp.val = (a.val.val - (r.val + elems.val * self.elem_size.val) % a.val.val) % a.val.val := by
+    rw [hi] at hp
+    exact hp
+  simp only [core.num.Usize.wrapping_add_val_eq, Nat.add_assoc, Nat.mod_add_mod]
+  rw [show
+    (core.num.Usize.wrapping_sub (core.num.Usize.wrapping_add self.size_base r) self.offset).val +
+      (rp.val + (self.offset.val + elems.val * self.elem_size.val)) =
+    ((core.num.Usize.wrapping_sub (core.num.Usize.wrapping_add self.size_base r) self.offset).val +
+      self.offset.val) + (elems.val * self.elem_size.val + rp.val) by omega,
+    ← Nat.mod_add_mod, wrapping_sub_cancel, core.num.Usize.wrapping_add_val_eq, Nat.mod_add_mod]
+  simp only [trailingFormula, byteFormula, LayoutMath.Formula.size, LayoutMath.Formula.bytes,
+    LayoutMath.roundUp]
+  rw [← hphase, ← halign, hp']
+  congr 1
+  omega
+
+theorem trailing_align_pos (self : layout.TrailingSliceLayout Usize) :
+    0 < (trailingFormula self).align := Nat.two_pow_pos _
+
+theorem trailing_product_le_size (self : layout.TrailingSliceLayout Usize) (n : Nat) :
+    n * self.elem_size.val ≤ (trailingFormula self).size n := by
+  have h := (LayoutMath.roundUp_properties
+    ((trailingFormula self).phase + n * self.elem_size.val)
+    (trailingFormula self).align (trailing_align_pos self)).1
+  unfold trailingFormula byteFormula LayoutMath.Formula.size LayoutMath.Formula.bytes at *
+  dsimp only at *
+  omega
+
+theorem word_mod_of_le (n : Nat) (h : n ≤ Usize.max) : n % UScalar.size .Usize = n := by
+  apply Nat.mod_eq_of_lt
+  have hp := Nat.two_pow_pos System.Platform.numBits
+  simp only [Usize.max, Usize.numBits, UScalarTy.Usize_numBits_eq, UScalar.size] at h ⊢
+  omega
+
+/- Distinguish a successful checked size from overflow using the unbounded
+complete-size formula. Rust None is a successful payload, not a panic.
+-/
+theorem size_for_elems_spec :
+  ∀ (self : layout.TrailingSliceLayout Usize) (elems : Usize), ∀ (hn : (0 < self.size_rounding_align_and_phase._0.val.val : Prop)),
+    @Zerocopy.layout.TrailingSliceLayoutUsize.size_for_elems self elems ⦃ r => r.map UScalar.val = (trailingFormula self).checkedSize Usize.max elems.val ⦄ := by
+  intro self elems hn
+  unfold layout.TrailingSliceLayoutUsize.size_for_elems
+  step with max_trailing_bytes_spec self core.num.Usize.MAX hn as ⟨cap, hc⟩
+  have hc' := LayoutMath.capacity_spec (byteFormula self) core.num.Usize.MAX.val
+    (show 0 < (byteFormula self).align from Nat.two_pow_pos _)
+  simp only [core.num.Usize.MAX, UScalar.ofNatCore_val_eq] at hc'
+  have hprod := trailing_product_le_size self elems.val
+  cases cap with
+  | none =>
+    simp only [Option.map_none] at hc
+    rw [← hc] at hc'
+    have hmiss := hc' (elems.val * self.elem_size.val)
+    change Usize.max < (trailingFormula self).size elems.val at hmiss
+    simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.checkedSize,
+      show ¬(trailingFormula self).size elems.val ≤ Usize.max by omega, if_false]
+  | some cap =>
+    simp only [Option.map_some] at hc
+    rw [← hc] at hc'
+    have hiff := hc' (elems.val * self.elem_size.val)
+    change (trailingFormula self).size elems.val ≤ Usize.max ↔
+      elems.val * self.elem_size.val ≤ cap.val at hiff
+    step as ⟨product, hm⟩
+    cases product with
+    | none =>
+      simp only [] at hm
+      have hmiss : ¬(trailingFormula self).size elems.val ≤ Usize.max := by
+        rw [Nat.mul_comm] at hm
+        omega
+      simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.checkedSize, hmiss, if_false]
+    | some bytes =>
+      simp only [] at hm
+      simp only [UScalar.lt_equiv]
+      split
+      · rename_i hbig
+        have hmiss : ¬(trailingFormula self).size elems.val ≤ Usize.max := by
+          rw [Nat.mul_comm] at hm
+          omega
+        simp only [WP.spec_ok, Option.map_none, LayoutMath.Formula.checkedSize, hmiss, if_false]
+      · rename_i hsmall
+        have hfit : (trailingFormula self).size elems.val ≤ Usize.max := by
+          apply hiff.mpr
+          rw [hm.2.1, Nat.mul_comm] at hsmall
+          omega
+        simp only [lift, bind_ok]
+        step with padding_for_elems_spec self elems hn as ⟨p, hp⟩
+        have hsz : Usize.size = UScalar.size .Usize := by
+          simp only [Usize.size, Usize.numBits, UScalarTy.Usize_numBits_eq, UScalar.size]
+        rw [hsz] at hp
+        simp only [Option.map_some,
+          LayoutMath.Formula.checkedSize, hfit, if_true,
+          core.num.Usize.wrapping_add_val_eq, Nat.mod_add_mod]
+        rw [hm.2.1, Nat.mul_comm]
+        rw [show self.offset.val + elems.val * self.elem_size.val + p.val =
+          p.val + self.offset.val + elems.val * self.elem_size.val by omega,
+          hp, word_mod_of_le _ hfit]
+
 /- Explain both zero-stride rejection and successful conversion. The raw lemma
 retains broad representation coverage; the canonical spec adds recursive
 admission rather than silently changing that useful raw theorem.
@@ -415,6 +649,60 @@ theorem encoding_align_spec : Zerocopy.Specs.encoding_align_spec := by
   exact ⟨av, (decodeNonZeroUScalar_iff align av).mpr rfl, he.trans hvalue.1.symm⟩
 register_spec_step encoding_align_spec
 
+/- Reading physical offset must preserve the raw word even though the element
+carrier can be generic. No size normalization is needed for this observation.
+-/
+theorem size_offset_spec : Zerocopy.Specs.size_offset_spec := by
+  unfold Zerocopy.Specs.size_offset_spec
+  representation_simps
+  intro E self validity hv
+  exact Raw.size_offset_spec self hv.2
+register_spec_step size_offset_spec
+
+/- Solve the rounded complete-size inequality for the greatest byte budget. The
+proof must preserve rounding plateaus and the case where even zero bytes do
+not fit; dividing by element stride belongs to a later operation.
+-/
+theorem max_trailing_bytes_spec : Zerocopy.Specs.max_trailing_bytes_spec := by
+  unfold Zerocopy.Specs.max_trailing_bytes_spec
+  representation_simps
+  intro E self available validity hv
+  apply WP.spec_mono (Raw.max_trailing_bytes_spec self available hv.2)
+  intro result facts
+  refine ⟨?_, facts⟩
+  change isValid result
+  simp
+register_spec_step max_trailing_bytes_spec
+
+/- Compute padding with wrapping machine arithmetic. The raw theorem records the
+modular result; physical padding follows only when the complete size fits.
+-/
+theorem padding_for_elems_spec : Zerocopy.Specs.padding_for_elems_spec := by
+  unfold Zerocopy.Specs.padding_for_elems_spec
+  representation_simps
+  intro self elems hv
+  exact Raw.padding_for_elems_spec self elems hv
+register_spec_step padding_for_elems_spec
+
+/- Distinguish a successful checked size from overflow using the unbounded
+complete-size formula. Rust None is a successful payload, not a panic.
+-/
+theorem size_for_elems_spec : Zerocopy.Specs.size_for_elems_spec := by
+  intro self elems value hvalue count hcount
+  have hv : 0 < self.size_rounding_align_and_phase._0.val.val :=
+    by simpa only [trailingValid, encodingValid, scalar_valid_iff, true_and] using
+      (trailing_decoder_admitted_iff self).mp ⟨value, hvalue⟩
+  have hformula := trailingFormula_decode self value hvalue
+  have hn := (decodeUScalar_iff elems count).mp hcount
+  apply WP.spec_mono (Raw.size_for_elems_spec self elems hv)
+  intro result facts
+  obtain ⟨decoded, hd⟩ := (option_valid_iff result).mpr (by simp)
+  refine ⟨decoded, hd, ?_⟩
+  change decoded.map (fun size => (size : Nat)) = _
+  rw [optionalSize_decode result decoded hd, hformula, ← hn]
+  exact facts
+register_spec_step size_for_elems_spec
+
 theorem max_elems_for_bytes_spec : Zerocopy.Specs.max_elems_for_bytes_spec := by
   unfold Zerocopy.Specs.max_elems_for_bytes_spec
   representation_simps
@@ -547,4 +835,22 @@ theorem new_zst_spec : Zerocopy.Specs.new_zst_spec := by
   | some a => simpa only [Option.getD_some, and_true] using Nat.pos_of_isPowerOfTwo (hp a rfl)
 register_spec_step new_zst_spec
 
+/-- An arbitrary proof of the compact mathematical clause implies the separately
+maintained exact optional-size and overflow obligation. -/
+@[contract_simps] theorem size_for_elems_spec_implies_required
+    (self : layout.TrailingSliceLayout Usize) (elems : Usize) (run : Result (Option Usize))
+    (provided : Zerocopy.Specs.size_for_elems_spec_contract self elems run) :
+    Zerocopy.Obligations.size_for_elems_spec_contract self elems run := by
+  intro positive
+  have valid : trailingValid self := ⟨by simp, positive⟩
+  obtain ⟨value, hvalue⟩ := (trailing_decoder_admitted_iff self).mpr valid
+  have hformula := trailingFormula_decode self value hvalue
+  have execution := provided value hvalue (unsignedWord elems) rfl
+  simp only [WP.spec_equiv_exists] at execution
+  obtain ⟨result, hexec, decoded, hd, hsize⟩ := execution
+  refine ⟨result, hexec, ?_⟩
+  change decoded.map (fun size => (size : Nat)) = _ at hsize
+  rw [optionalSize_decode result decoded hd, hformula, unsignedWord_value] at hsize
+  exact hsize
+
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/TailChecks.lean b/verification/aeneas/lean/Proofs/TailChecks.lean
new file mode 100644
index 0000000000..2323571ddc
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/TailChecks.lean
@@ -0,0 +1,83 @@
+/- 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
+public import Proofs.TailReference
+public import RequiredModelContracts.TailChecks
+@[expose] public section
+
+open Aeneas Aeneas.Std
+namespace Zerocopy.Proofs.Raw.TailChecks
+set_option linter.unusedVariables false
+set_option linter.unusedSimpArgs false
+
+/- The roots execute the production operation and the separate reference,
+then prove the actual Rust assertion. The reference lemmas retain their own
+arithmetic derivations; neither side is substituted for an extracted body.
+-/
+theorem trailing_arithmetic_check (tail : layout.TrailingSliceLayout Usize)
+    (align : NonZeroUsize) (phase elems budget : Usize) :
+    layout.tail_checks.trailing_arithmetic_check tail align phase elems budget ⦃ _ => True ⦄ := by
+  unfold layout.tail_checks.trailing_arithmetic_check
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  step as ⟨power, power_iff⟩
+  split
+  · rename_i power_true
+    have power_fact : align.val.val.isPowerOfTwo := Eq.mp power_iff power_true
+    have align_positive := Nat.pos_of_isPowerOfTwo power_fact
+    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⟩
+      split
+      · rename_i matches_true
+        have encoded_eq := matches_iff.mp matches_true
+        rw [encoded_eq] at encoded_facts
+        simp only [] at encoded_facts
+        have encoding : tail.size_rounding_align_and_phase._0.val.val = align.val.val + phase.val :=
+          encoded_facts.2.1
+        have positive : 0 < tail.size_rounding_align_and_phase._0.val.val := by omega
+        have formula_eq := witness_view tail align phase power_fact phase_lt encoding
+        step with Zerocopy.Proofs.Raw.size_for_elems_spec tail elems positive as ⟨actual_size, actual_size_value⟩
+        step with reference_size tail align phase elems align_positive as ⟨expected_size, expected_size_value⟩
+        rw [formula_eq] at actual_size_value
+        have size_same : actual_size = expected_size := optional_value_injective
+          (actual_size_value.trans expected_size_value.symm)
+        step with same_optional_usize actual_size expected_size as ⟨same_size, same_size_iff⟩
+        have size_true := same_size_iff.mpr size_same
+        simp only [massert, size_true, if_true, bind_ok]
+        step with Zerocopy.Proofs.Raw.max_trailing_bytes_spec tail budget positive as ⟨actual_capacity, actual_capacity_value⟩
+        step with reference_capacity tail align phase budget align_positive as ⟨expected_capacity, expected_capacity_value⟩
+        have byte_capacity : (byteFormula tail).capacity budget.val =
+            (trailingFormula tail).capacity budget.val := rfl
+        rw [byte_capacity, formula_eq] at actual_capacity_value
+        have capacity_same : actual_capacity = expected_capacity := optional_value_injective
+          (actual_capacity_value.trans expected_capacity_value.symm)
+        step with same_optional_usize actual_capacity expected_capacity as ⟨same_capacity, same_capacity_iff⟩
+        have capacity_true := same_capacity_iff.mpr capacity_same
+        simp [massert, capacity_true, WP.spec_ok]
+      · simp only [WP.spec_ok]
+    · simp only [WP.spec_ok]
+  · simp only [WP.spec_ok]
+
+end Zerocopy.Proofs.Raw.TailChecks
+
+namespace Zerocopy.Proofs
+open AeneasSpecs
+
+theorem trailing_arithmetic_check_spec : Specs.trailing_arithmetic_check_spec := by
+  unfold Specs.trailing_arithmetic_check_spec
+  intros
+  apply WP.spec_mono (Raw.TailChecks.trailing_arithmetic_check _ _ _ _ _)
+  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
new file mode 100644
index 0000000000..6357054a1c
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/TailReference.lean
@@ -0,0 +1,237 @@
+/- 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 RepresentationLaws
+@[expose] public section
+
+open Aeneas Aeneas.Std
+namespace Zerocopy.Proofs.Raw.TailChecks
+set_option linter.unusedVariables false
+set_option linter.unusedSimpArgs false
+
+def witnessFormula (tail : layout.TrailingSliceLayout Usize)
+    (align : NonZeroUsize) (phase : Usize) : LayoutMath.Formula :=
+  ⟨tail.size_base.val, phase.val, align.val.val, tail.elem_size.val, tail.offset.val⟩
+
+def checkedNat (n : Nat) : Option Nat := if n ≤ Usize.max then some n else none
+
+@[simp] theorem checkedNat_none (n : Nat) : checkedNat n = none ↔ Usize.max < n := by
+  simp [checkedNat]
+
+@[simp] theorem checkedNat_some (n value : Nat) :
+    checkedNat n = some value ↔ n ≤ Usize.max ∧ n = value := by
+  unfold checkedNat
+  split <;> simp_all
+
+theorem checked_add_value (x y : Usize) :
+    (Usize.checked_add x y).map UScalar.val = checkedNat (x.val + y.val) := by
+  have h := Usize.checked_add_bv_spec x y
+  cases output_eq : Usize.checked_add x y with
+  | none =>
+    simp only [output_eq] at h ⊢
+    simp [checkedNat, show ¬x.val + y.val ≤ Usize.max by omega]
+  | some result =>
+    simp only [output_eq] at h ⊢
+    simp [checkedNat, h.1, h.2.1]
+
+theorem checked_mul_value (x y : Usize) :
+    (Usize.checked_mul x y).map UScalar.val = checkedNat (x.val * y.val) := by
+  have h := Usize.checked_mul_bv_spec x y
+  cases output_eq : Usize.checked_mul x y with
+  | none =>
+    simp only [output_eq] at h ⊢
+    simp [checkedNat, show ¬x.val * y.val ≤ Usize.max by omega]
+  | some result =>
+    simp only [output_eq] at h ⊢
+    simp [checkedNat, h.1, h.2.1]
+
+theorem same_optional_usize (left right : Option Usize) :
+    layout.tail_checks.same_optional_usize left right ⦃ b => (b = true ↔ left = right) ⦄ := by
+  cases left <;> cases right <;>
+    simp [layout.tail_checks.same_optional_usize, WP.spec_ok]
+
+theorem optional_value_injective {left right : Option Usize}
+    (same : left.map UScalar.val = right.map UScalar.val) : left = right := by
+  cases left with
+  | none =>
+    cases right with
+    | none => rfl
+    | some right => cases same
+  | some left =>
+    cases right with
+    | none => cases same
+    | some right =>
+      congr 1
+      exact UScalar.eq_of_val_eq (Option.some.inj same)
+
+/- This is coverage of the Rust witness guard, rather than an additional
+restriction on the compressed representation. Every positive stored word
+decodes to a power of two and a phase below it.
+-/
+theorem encoding_witness_coverage (tail : layout.TrailingSliceLayout Usize)
+    (positive : 0 < tail.size_rounding_align_and_phase._0.val.val) :
+    ∃ a p : Nat, a.isPowerOfTwo ∧ p < a ∧
+      a + p = tail.size_rounding_align_and_phase._0.val.val := by
+  obtain ⟨value, decoded⟩ := rounding_decode_positive tail.size_rounding_align_and_phase positive
+  have h := (rounding_decode_iff tail.size_rounding_align_and_phase value).mp decoded
+  exact ⟨value.align, value.phase, value.align_pow2, value.phase_lt, h.symm⟩
+
+theorem witness_view (tail : layout.TrailingSliceLayout Usize)
+    (align : NonZeroUsize) (phase : Usize) (power : align.val.val.isPowerOfTwo)
+    (phase_lt : phase.val < align.val.val)
+    (encoding : tail.size_rounding_align_and_phase._0.val.val = align.val.val + phase.val) :
+    trailingFormula tail = witnessFormula tail align phase := by
+  let value : layout.RoundingAlignAndPhase.RoundingValue :=
+    { align := align.val.val, phase := phase.val, align_pow2 := power,
+      phase_lt := phase_lt, fits := by rw [← encoding]; scalar_tac }
+  have decoded := (rounding_decode_iff tail.size_rounding_align_and_phase value).mpr encoding
+  have components := rounding_decode_components tail.size_rounding_align_and_phase value decoded
+  simp only [value] at components
+  rw [encoding] at components
+  simp only [trailingFormula, byteFormula, witnessFormula, ← components.1,
+    encoding, Nat.add_sub_cancel_left]
+
+def witnessMatches (runtime_layout : layout.DstLayout)
+    (align : NonZeroUsize) (phase : Usize) : Prop :=
+  match runtime_layout.size_info with
+  | .Sized _ => True
+  | .SliceDst tail => align.val.val.isPowerOfTwo ∧ phase.val < align.val.val ∧
+      tail.size_rounding_align_and_phase._0.val.val = align.val.val + phase.val
+
+theorem reference_round_up (bytes : Usize) (align : NonZeroUsize)
+    (positive : 0 < align.val.val) :
+    layout.tail_checks.reference_round_up bytes align ⦃ result =>
+      result.map UScalar.val = checkedNat (LayoutMath.roundUp bytes.val align.val.val) ⦄ := by
+  unfold layout.tail_checks.reference_round_up
+  simp only [core.num.nonzero.NonZero.get, bind_ok]
+  step with Usize.rem_spec bytes (y := align.val) (by omega) as ⟨remainder, remainder_value⟩
+  have remainder_lt := Nat.mod_lt bytes.val positive
+  simp only [UScalar.eq_equiv, UScalar.ofNatCore_val_eq]
+  split
+  · rename_i zero
+    have rounded : LayoutMath.roundUp bytes.val align.val.val = bytes.val := by
+      apply LayoutMath.roundUp_eq
+      omega
+    simp only [bind_ok, WP.spec_ok]
+    rw [checked_add_value, rounded, UScalar.ofNatCore_val_eq, Nat.add_zero]
+  · rename_i nonzero
+    step with Usize.sub_spec (x := align.val) (y := remainder) (by omega) as ⟨padding, padding_value⟩
+    rw [checked_add_value]
+    congr 1
+    unfold LayoutMath.roundUp
+    have padding_lt : align.val.val - bytes.val % align.val.val < align.val.val := by omega
+    rw [Nat.mod_eq_of_lt padding_lt]
+    omega
+
+theorem reference_size (tail : layout.TrailingSliceLayout Usize)
+    (align : NonZeroUsize) (phase elems : Usize) (positive : 0 < align.val.val) :
+    layout.tail_checks.reference_size tail align phase elems ⦃ result =>
+      result.map UScalar.val = (witnessFormula tail align phase).checkedSize Usize.max elems.val ⦄ := by
+  let f := witnessFormula tail align phase
+  have lower := (LayoutMath.roundUp_properties
+    (phase.val + elems.val * tail.elem_size.val) align.val.val positive).1
+  have size_eq : f.size elems.val = tail.size_base.val +
+      LayoutMath.roundUp (phase.val + elems.val * tail.elem_size.val) align.val.val := rfl
+  unfold layout.tail_checks.reference_size
+  step as ⟨product, product_facts⟩
+  cases product with
+  | none =>
+    simp only [] at product_facts
+    have overflow : Usize.max < f.size elems.val := by omega
+    simp [LayoutMath.Formula.checkedSize, ← size_eq, f, overflow, Nat.not_le.mpr overflow]
+  | some bytes =>
+    simp only [] at product_facts
+    step as ⟨input, input_facts⟩
+    cases input with
+    | none =>
+      simp only [] at input_facts
+      have overflow : Usize.max < f.size elems.val := by omega
+      simp [LayoutMath.Formula.checkedSize, ← size_eq, f, overflow, Nat.not_le.mpr overflow]
+    | some input =>
+      simp only [] at input_facts
+      step with reference_round_up input align positive as ⟨rounded, rounded_facts⟩
+      have input_value : input.val = phase.val + elems.val * tail.elem_size.val := by omega
+      rw [input_value] at rounded_facts
+      cases rounded with
+      | none =>
+        simp only [Option.map_none] at rounded_facts
+        have overflow_round := (checkedNat_none _).mp rounded_facts.symm
+        have overflow : Usize.max < f.size elems.val := by omega
+        simp [LayoutMath.Formula.checkedSize, ← size_eq, f, Nat.not_le.mpr overflow]
+      | some rounded =>
+        simp only [Option.map_some] at rounded_facts
+        have rounded_value := (checkedNat_some _ _).mp rounded_facts.symm
+        simp only [WP.spec_ok]
+        rw [checked_add_value]
+        change checkedNat _ = _
+        rw [← rounded_value.2]
+        rfl
+
+theorem capacity_condition (tail : layout.TrailingSliceLayout Usize)
+    (align : NonZeroUsize) (phase budget : Usize) (positive : 0 < align.val.val) :
+    (witnessFormula tail align phase).bytes 0 ≤ budget.val ↔
+      tail.size_base.val ≤ budget.val ∧
+      phase.val ≤ (budget.val - tail.size_base.val) -
+        (budget.val - tail.size_base.val) % align.val.val := by
+  have nonnegative := (LayoutMath.roundUp_properties phase.val align.val.val positive).1
+  have round_condition := LayoutMath.roundUp_le_budget phase.val align.val.val
+    (budget.val - tail.size_base.val) positive
+  change tail.size_base.val + LayoutMath.roundUp (phase.val + 0) align.val.val ≤ _ ↔ _
+  rw [Nat.add_zero]
+  constructor
+  · intro fit
+    exact ⟨by omega, round_condition.mp (by omega)⟩
+  · rintro ⟨base_fits, phase_fits⟩
+    have := round_condition.mpr phase_fits
+    omega
+
+theorem reference_capacity (tail : layout.TrailingSliceLayout Usize)
+    (align : NonZeroUsize) (phase budget : Usize) (positive : 0 < align.val.val) :
+    layout.tail_checks.reference_capacity tail align phase budget ⦃ result =>
+      result.map UScalar.val = (witnessFormula tail align phase).capacity budget.val ⦄ := by
+  have condition := capacity_condition tail align phase budget positive
+  unfold layout.tail_checks.reference_capacity
+  step as ⟨after_base, base_facts⟩
+  cases after_base with
+  | none =>
+    simp only [] at base_facts
+    have miss : ¬(witnessFormula tail align phase).bytes 0 ≤ budget.val := by
+      intro fit
+      have := condition.mp fit
+      omega
+    simp [LayoutMath.Formula.capacity, miss]
+  | some after_base =>
+    simp only [] at base_facts
+    simp only [core.num.nonzero.NonZero.get, bind_ok]
+    step with Usize.rem_spec after_base (y := align.val) (by omega) as ⟨remainder, remainder_value⟩
+    have remainder_bound := Nat.mod_le after_base.val align.val.val
+    step with Usize.sub_spec (x := after_base) (y := remainder) (by omega) as ⟨rounded, rounded_value⟩
+    have rounded_budget : rounded.val = (budget.val - tail.size_base.val) -
+        (budget.val - tail.size_base.val) % align.val.val := by
+      rw [rounded_value, remainder_value, base_facts.2.1]
+    have phase_facts := Usize.checked_sub_bv_spec rounded phase
+    cases result_eq : Usize.checked_sub rounded phase with
+    | none =>
+      simp only [result_eq] at phase_facts
+      have miss : ¬(witnessFormula tail align phase).bytes 0 ≤ budget.val := by
+        intro fit
+        have := condition.mp fit
+        omega
+      simp [result_eq, LayoutMath.Formula.capacity, miss]
+    | some result =>
+      simp only [result_eq] at phase_facts
+      have fit : (witnessFormula tail align phase).bytes 0 ≤ budget.val :=
+        condition.mpr ⟨base_facts.1, by omega⟩
+      simp only [result_eq, WP.spec_ok, Option.map_some, LayoutMath.Formula.capacity, fit, if_true]
+      dsimp only [witnessFormula]
+      congr 1
+      omega
+
+end Zerocopy.Proofs.Raw.TailChecks
diff --git a/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean b/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean
new file mode 100644
index 0000000000..bbe3d294a6
--- /dev/null
+++ b/verification/aeneas/lean/RequiredModelContracts/TailChecks.lean
@@ -0,0 +1,36 @@
+/- 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 Obligations.TailChecks
+@[expose] public section
+
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+set_option linter.unusedVariables false
+
+/- Recover the full raw domain from the actual decoders before consuming the
+supplied arbitrary-outcome contract. These adapters do not run either check.
+-/
+@[contract_simps] theorem required_trailing_arithmetic_check
+    (tail : layout.TrailingSliceLayout Usize) (align : NonZeroUsize)
+    (phase elems budget : Usize) (run : Result Unit)
+    (provided : Specs.trailing_arithmetic_check_spec_contract tail align phase elems budget run) :
+    Obligations.trailing_arithmetic_check_spec_contract tail align phase elems budget run := by
+  intro positive align_positive
+  have valid_tail : isValid tail := (trailing_valid_iff tail).mpr ⟨by simp, positive⟩
+  obtain ⟨tail_value, decoded_tail⟩ := valid_tail
+  let av : NonZeroUsizeValue := ⟨unsignedWord align.val, align_positive⟩
+  have decoded_align := (decodeNonZeroUScalar_iff align av).mpr rfl
+  apply WP.spec_mono (provided tail_value decoded_tail av decoded_align
+    (unsignedWord phase) rfl (unsignedWord elems) rfl (unsignedWord budget) rfl)
+  rintro result ⟨value, decoded, facts⟩
+  trivial
+
+end Zerocopy.Proofs
diff --git a/zerocopy/src/layout/mod.rs b/zerocopy/src/layout/mod.rs
index e96564bee3..71928c6d8b 100644
--- a/zerocopy/src/layout/mod.rs
+++ b/zerocopy/src/layout/mod.rs
@@ -15,6 +15,9 @@ mod nested_reference;
 #[allow(dead_code)]
 mod primitive_checks;
 
+#[allow(dead_code)]
+mod tail_checks;
+
 use core::{mem, num::NonZeroUsize};
 
 use crate::util;
@@ -256,6 +259,12 @@ impl<E> TrailingSliceLayout<E> {
         let (align, phase) = self.size_rounding_align_and_phase.components();
         offset == util::round_down_to_next_multiple_of_alignment(self.size_base, align) + phase
     }))]
+    ///
+    /// ```aeneas
+    /// spec size_offset_spec
+    ///   ensures(raw) offset =>
+    ///     offset.val = self.size_base.val - self.size_base.val % (byteFormula self).align + (byteFormula self).phase
+    /// ```
     const fn size_offset(&self) -> usize {
         #[cfg(all(kani, kani_slow))]
         #[kani::proof_for_contract(TrailingSliceLayout::<usize>::size_offset)]
@@ -287,6 +296,11 @@ impl<E> TrailingSliceLayout<E> {
             .map(|bytes| util::round_down_to_next_multiple_of_alignment(bytes, align))
             .and_then(|rounded| rounded.checked_sub(phase))
     }))]
+    ///
+    /// ```aeneas
+    /// spec max_trailing_bytes_spec
+    ///   ensures(raw) r => r.map UScalar.val = (byteFormula self).capacity available_bytes.val
+    /// ```
     const fn max_trailing_bytes(&self, available_bytes: usize) -> Option<usize> {
         #[cfg(all(kani, kani_slow))]
         #[kani::proof_for_contract(TrailingSliceLayout::<usize>::max_trailing_bytes)]
@@ -395,6 +409,12 @@ impl TrailingSliceLayout {
         let object_size = self.size_base.wrapping_add(rounded);
         padding == object_size.wrapping_sub(self.offset.wrapping_add(trailing_bytes))
     }))]
+    ///
+    /// ```aeneas
+    /// spec padding_for_elems_spec
+    ///   ensures(raw) p => (p.val + self.offset.val + elems.val * self.elem_size.val) % UScalar.size .Usize =
+    ///     (trailingFormula self).size elems.val % UScalar.size .Usize
+    /// ```
     pub(crate) const fn padding_for_elems(self, elems: usize) -> usize {
         #[cfg(all(kani, kani_slow))]
         #[kani::proof_for_contract(TrailingSliceLayout::padding_for_elems)]
@@ -462,6 +482,12 @@ impl TrailingSliceLayout {
         size == elems.checked_mul(self.elem_size)
             .and_then(|bytes| proofs::slice_dst_size_for_trailing_bytes(self, bytes))
     }))]
+    ///
+    /// ```aeneas
+    /// spec size_for_elems_spec
+    ///   ensures result => result.map (fun size => (size : Nat)) =
+    ///     (ModelViews.trailingFormula self).checkedSize Usize.max (elems : Nat)
+    /// ```
     pub(crate) const fn size_for_elems(self, elems: usize) -> Option<usize> {
         #[cfg(all(kani, kani_slow))]
         #[kani::proof_for_contract(TrailingSliceLayout::size_for_elems)]
diff --git a/zerocopy/src/layout/tail_checks.rs b/zerocopy/src/layout/tail_checks.rs
new file mode 100644
index 0000000000..9706950641
--- /dev/null
+++ b/zerocopy/src/layout/tail_checks.rs
@@ -0,0 +1,111 @@
+// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+//
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, 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.
+
+//! Executable assertions for trailing sizes, capacities, and cast metadata.
+//!
+//! The reference calculations receive an explicit alignment and phase. They
+//! use division remainders and checked arithmetic, and never decode the
+//! production rounding representation or call production size helpers. The
+//! checks bind these independent witnesses to the stored word before comparing
+//! results. Every nonzero stored word has such witnesses: its highest set bit
+//! is the alignment, and the lower bits are the phase.
+
+// Explicit scalar reads and matches keep the reference independent of extra
+// trait dictionaries and higher-order library models in the pinned extraction.
+#![allow(clippy::needless_nonzero_get, clippy::manual_map)]
+
+use core::num::NonZeroUsize;
+
+use super::TrailingSliceLayout;
+
+pub(super) fn same_optional_usize(left: Option<usize>, right: Option<usize>) -> bool {
+    match (left, right) {
+        (Some(left), Some(right)) => left == right,
+        (None, None) => true,
+        _ => false,
+    }
+}
+
+#[allow(clippy::arithmetic_side_effects)]
+fn reference_round_up(bytes: usize, align: NonZeroUsize) -> Option<usize> {
+    let remainder = bytes % align.get();
+    let padding = if remainder == 0 { 0 } else { align.get() - remainder };
+    bytes.checked_add(padding)
+}
+
+pub(super) fn reference_size(
+    tail: TrailingSliceLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    elems: usize,
+) -> Option<usize> {
+    match elems.checked_mul(tail.elem_size) {
+        None => None,
+        Some(bytes) => match phase.checked_add(bytes) {
+            None => None,
+            Some(input) => match reference_round_up(input, align) {
+                None => None,
+                Some(rounded) => tail.size_base.checked_add(rounded),
+            },
+        },
+    }
+}
+
+#[allow(clippy::arithmetic_side_effects)]
+fn reference_capacity(
+    tail: TrailingSliceLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    budget: usize,
+) -> Option<usize> {
+    match budget.checked_sub(tail.size_base) {
+        None => None,
+        Some(after_base) => {
+            let rounded_budget = after_base - after_base % align.get();
+            rounded_budget.checked_sub(phase)
+        }
+    }
+}
+
+/// Check the entire optional size and capacity results, including overflow.
+///
+/// Physical slice offset does not constrain this claim: a raw layout can have
+/// its slice outside the complete object. Nor is rounding alignment restricted
+/// to Rust's maximum type alignment; every nonzero encoding is covered.
+///
+/// ```aeneas
+/// spec trailing_arithmetic_check_spec
+///   ensures(raw) _ => True
+/// ```
+fn trailing_arithmetic_check(
+    tail: TrailingSliceLayout,
+    align: NonZeroUsize,
+    phase: usize,
+    elems: usize,
+    budget: usize,
+) {
+    if 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()),
+        )
+    {
+        assert!(same_optional_usize(
+            tail.size_for_elems(elems),
+            reference_size(tail, align, phase, elems),
+        ));
+        assert!(same_optional_usize(
+            tail.max_trailing_bytes(budget),
+            reference_capacity(tail, align, phase, budget),
+        ));
+    }
+}