diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index 1ec9bc8ee8..ca0a49648b 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -40,6 +40,15 @@ equal sizes, including zero-sized layouts with different alignments. Rejection
 does not claim that a cast would be impossible. The proof covers the numerical
 decision and sizing comparison, not the resulting pointer's validity.
 
+The checks in [`util/allocation.rs`](../../zerocopy/src/util/allocation.rs) cover
+actual metadata sizing and exact preparation of allocator arguments. Preparation
+preserves every optional size and the supplied alignment, without adding a
+runtime validity filter. Under explicit correspondence to a valid recursive
+layout, separate lemmas establish complete size and tail containment. Numerical
+allocator admission additionally needs the outer alignment and the signed
+metadata-size bound. Allocator behavior, zeroing, and `Box` validity remain
+separate Rust obligations.
+
 These harnesses use the same annotation and proof rules as every other function.
 There is no root marker or separately maintained list of required functions.
 Every present specification must have its corresponding proof in both CI builds.
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index 59244f85cf..d788bed9fe 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -888,7 +888,7 @@ def layout.composition_checks.reference_pad
   else ok none
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 305:0-311:1 -/
+    Source: 'src/util/mod.rs', lines 306:0-312:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -908,7 +908,7 @@ def util.min
   else ok a
 
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 289:0-295:1 -/
+    Source: 'src/util/mod.rs', lines 290:0-296:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -928,7 +928,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 169:0-229:1 -/
+    Source: 'src/util/mod.rs', lines 170:0-230:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -1142,7 +1142,7 @@ def layout.composition_checks.check_extend
   else ok ()
 
 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 261:0-279:1 -/
+    Source: 'src/util/mod.rs', lines 262:0-280:1 -/
 def util.round_down_to_next_multiple_of_alignment
   (n : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -2487,6 +2487,105 @@ def split_at.numerical_checks.check_split_geometry
               else ok ()
   else ok ()
 
+/-- [zerocopy::util::allocation::prepare]:
+    Source: 'src/util/allocation.rs', lines 33:0-38:1 -/
+def util.allocation.prepare
+  (size : Option Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result (Option (Std.Usize × (core.num.nonzero.NonZero Std.Usize
+    core.num.niche_types.NonZeroUsizeInner)))
+  := do
+  match size with
+  | none => ok none
+  | some size1 => ok (some (size1, align))
+
+/-- [zerocopy::util::allocation::assert_preparation]:
+    Source: 'src/util/allocation.rs', lines 52:0-64:1 -/
+def util.allocation.assert_preparation
+  (size : Option Std.Usize)
+  (align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) :
+  Result Unit
+  := do
+  let prepared ← util.allocation.prepare size align
+  match size with
+  | none => let b := core.option.Option.is_none prepared
+            massert b
+  | some size1 =>
+    match prepared with
+    | none => fail panic
+    | some p =>
+      let (actual_size, actual_align) := p
+      massert (actual_size = size1)
+      let i ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner
+          actual_align
+      let i1 ←
+        core.num.nonzero.NonZero.get
+          Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align
+      massert (i = i1)
+
+/-- [zerocopy::util::allocation::assert_allocation_size]:
+    Source: 'src/util/allocation.rs', lines 80:0-126:1 -/
+def util.allocation.assert_allocation_size
+  (runtime_layout : layout.DstLayout)
+  (rounding_align : core.num.nonzero.NonZero Std.Usize
+  core.num.niche_types.NonZeroUsizeInner) (phase : Std.Usize)
+  (metadata : Std.Usize) :
+  Result Unit
+  := do
+  match runtime_layout.size_info with
+  | layout.SizeInfo.Sized size =>
+    let actual ← pointer_metadata_unit_size_for_metadata runtime_layout
+    let b ← layout.tail_checks.same_optional_usize actual (some size)
+    massert b
+    util.allocation.assert_preparation actual runtime_layout.align
+    let o ← util.allocation.prepare actual runtime_layout.align
+    match o with
+    | none => ok ()
+    | some p =>
+      let (size1, _) := p
+      let b1 ←
+        layout.tail_checks.same_optional_usize (some size) (some size1)
+      massert b1
+  | layout.SizeInfo.SliceDst tail =>
+    let b ←
+      layout.tail_transform_checks.witness_matches tail rounding_align phase
+    if b
+    then
+      let actual ←
+        pointer_metadata_usize_size_for_metadata metadata runtime_layout
+      let expected ←
+        layout.tail_checks.reference_size tail rounding_align phase metadata
+      let b1 ← layout.tail_checks.same_optional_usize actual expected
+      massert b1
+      util.allocation.assert_preparation actual runtime_layout.align
+      let o ← util.allocation.prepare actual runtime_layout.align
+      match o with
+      | none => ok ()
+      | some p =>
+        let (size, _) := p
+        let b2 ← layout.tail_checks.same_optional_usize expected (some size)
+        massert b2
+        let o1 ← lift (Usize.checked_add tail.size_base phase)
+        match o1 with
+        | none => fail panic
+        | some start =>
+          if tail.offset > start
+          then ok ()
+          else
+            let o2 ← lift (Usize.checked_mul metadata tail.elem_size)
+            match o2 with
+            | none => fail panic
+            | some bytes =>
+              let o3 ← lift (Usize.checked_add tail.offset bytes)
+              match o3 with
+              | none => fail panic
+              | some «end» => massert («end» <= size)
+    else ok ()
+
 /-- [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/lean/Obligations/Allocation.lean b/verification/aeneas/lean/Obligations/Allocation.lean
new file mode 100644
index 0000000000..5d7198a923
--- /dev/null
+++ b/verification/aeneas/lean/Obligations/Allocation.lean
@@ -0,0 +1,47 @@
+/- 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
+
+/- This expectation independently classifies all optional machine sizes. The
+numerical preparation does not allocate or change the supplied metadata size.
+-/
+def allocation_prepare_spec_contract (size : Option Usize) (align : NonZeroUsize)
+    (run : Result (Option (Usize × NonZeroUsize))) : Prop :=
+  0 < align.val.val → run ⦃ result =>
+    result.map (fun pair => (pair.1.val, pair.2.val.val)) =
+      size.map (fun size => (size.val, align.val.val)) ⦄
+
+def allocation_prepare_spec : Prop :=
+  ∀ size align, allocation_prepare_spec_contract size align
+    (util.allocation.prepare size align)
+
+def allocation_preparation_check_spec_contract (_size : Option Usize) (align : NonZeroUsize)
+    (run : Result Unit) : Prop := 0 < align.val.val → run ⦃ _ => True ⦄
+
+def allocation_preparation_check_spec : Prop :=
+  ∀ size align, allocation_preparation_check_spec_contract size align
+    (util.allocation.assert_preparation size align)
+
+def allocation_size_check_spec_contract (runtime_layout : layout.DstLayout)
+    (rounding_align : NonZeroUsize) (_phase _metadata : Usize) (run : Result Unit) : Prop :=
+  0 < runtime_layout.align.val.val → canonicalLayout runtime_layout →
+  0 < rounding_align.val.val → run ⦃ _ => True ⦄
+
+def allocation_size_check_spec : Prop :=
+  ∀ runtime_layout rounding_align phase metadata,
+    allocation_size_check_spec_contract runtime_layout rounding_align phase metadata
+      (util.allocation.assert_allocation_size runtime_layout rounding_align phase metadata)
+
+end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/Proofs/Allocation.lean b/verification/aeneas/lean/Proofs/Allocation.lean
new file mode 100644
index 0000000000..4c1a415edc
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/Allocation.lean
@@ -0,0 +1,311 @@
+/- 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.Util
+public import Obligations.Allocation
+public import RepresentationLaws
+public import Proofs.TailReference
+public import Proofs.PointerMetadata
+public import Proofs.TailTransformChecks
+import all Init.Data.Nat.Power2.Basic
+@[expose] public section
+
+open Aeneas Aeneas.Std
+set_option linter.unusedVariables false
+set_option linter.unusedSimpArgs false
+namespace Zerocopy.Proofs.Raw.Allocation
+
+/- Allocator validity is a separate domain supplied by the completed Rust
+layout contract and valid metadata. Decoding or Some alone does not imply it.
+-/
+def limit : Nat := 2 ^ (System.Platform.numBits - 1) - 1
+
+def admittedAllocation (size alignment : Nat) : Prop :=
+  alignment.isPowerOfTwo ∧ size % alignment = 0 ∧ size ≤ limit
+
+theorem admitted_allocator_bound (size alignment : Nat)
+    (admitted : admittedAllocation size alignment) :
+    alignment.isPowerOfTwo ∧ LayoutMath.roundUp size alignment ≤ limit := by
+  refine ⟨admitted.1, ?_⟩
+  rw [LayoutMath.roundUp_eq _ _ admitted.2.1]
+  exact admitted.2.2
+
+/- Complete recursive descriptions derive the alignment part of this domain.
+The signed-size premise is explicit: it corresponds to valid Rust metadata.
+-/
+theorem description_aligned (description : LayoutMath.Description)
+    (valid : description.valid) (metadata : Nat) :
+    description.size metadata % 2 ^ description.alignExponent = 0 := by
+  cases description with
+  | slice elem exponent =>
+    simp only [LayoutMath.Description.valid] at valid
+    simp only [LayoutMath.Description.size, LayoutMath.Description.alignExponent,
+      Nat.mul_mod, valid, Nat.mul_zero, Nat.zero_mod]
+  | record leading minimum packed tail =>
+    exact (LayoutMath.roundUp_properties _ _ (Nat.two_pow_pos _)).2.2
+
+theorem recursive_admitted_allocation (description : LayoutMath.Description)
+    (valid : description.valid) (metadata : Nat)
+    (fits : description.size metadata ≤ limit) :
+    admittedAllocation (description.size metadata) (2 ^ description.alignExponent) := by
+  exact ⟨⟨description.alignExponent, rfl⟩, description_aligned description valid metadata, fits⟩
+
+/- Independently intended optional-value preservation, without a layout filter. -/
+def preparedValue (size : Option Nat) (alignment : Nat) : Option (Nat × Nat) :=
+  size.map (fun size => (size, alignment))
+
+theorem preparedValue_input (size : Option Usize) (alignment : Nat) :
+    preparedValue (size.map UScalar.val) alignment =
+      size.map (fun size => (size.val, alignment)) := by
+  cases size <;> rfl
+
+theorem preparedValue_some (size : Option Nat) (alignment allocated result_align : Nat)
+    (accepted : preparedValue size alignment = some (allocated, result_align)) :
+    size = some allocated ∧ result_align = alignment := by
+  cases size with
+  | none => cases accepted
+  | some size =>
+    have same : (size, alignment) = (allocated, result_align) := Option.some.inj accepted
+    cases same
+    exact ⟨rfl, rfl⟩
+
+/- Accepted metadata size is connected to an independent recursive description.
+Exact complete size and tail containment follow before allocator validity is
+introduced. The latter additionally needs the outer layout alignment and the
+explicit signed-size condition of valid metadata.
+-/
+theorem recursive_allocation_contains_tail (description : LayoutMath.Description)
+    (valid : description.valid) (metadata alignment allocated result_align : Nat)
+    (metadata_size : Option Nat)
+    (sized : metadata_size = description.compile.checkedSize Usize.max metadata)
+    (accepted : preparedValue metadata_size alignment = some (allocated, result_align)) :
+    allocated = description.size metadata ∧
+    description.offset + metadata * description.elem ≤ allocated := by
+  have facts := preparedValue_some metadata_size alignment allocated result_align accepted
+  rw [sized] at facts
+  unfold LayoutMath.Formula.checkedSize at facts
+  split at facts
+  · have exact_size : description.compile.size metadata = allocated := Option.some.inj facts.1
+    have recursive_size := LayoutMath.compile_size description valid metadata
+    refine ⟨exact_size.symm.trans recursive_size, ?_⟩
+    rw [← exact_size, recursive_size]
+    exact LayoutMath.description_contains_tail description metadata
+  · cases facts.1
+
+theorem recursive_allocation_valid (description : LayoutMath.Description)
+    (valid : description.valid) (metadata alignment allocated result_align : Nat)
+    (metadata_size : Option Nat)
+    (sized : metadata_size = description.compile.checkedSize Usize.max metadata)
+    (accepted : preparedValue metadata_size alignment = some (allocated, result_align))
+    (alignment_matches : alignment = 2 ^ description.alignExponent)
+    (metadata_valid : description.size metadata ≤ limit) :
+    admittedAllocation allocated result_align ∧
+    LayoutMath.roundUp allocated result_align ≤ limit := by
+  have complete := (recursive_allocation_contains_tail description valid metadata alignment
+    allocated result_align metadata_size sized accepted).1
+  have unchanged := (preparedValue_some metadata_size alignment allocated result_align accepted).2
+  have admitted := recursive_admitted_allocation description valid metadata metadata_valid
+  rw [complete, unchanged, alignment_matches]
+  exact ⟨admitted, (admitted_allocator_bound _ _ admitted).2⟩
+
+theorem prepare (size : Option Usize) (align : NonZeroUsize) :
+    util.allocation.prepare size align ⦃ result =>
+      result.map (fun pair => (pair.1.val, pair.2.val.val)) =
+        preparedValue (size.map UScalar.val) align.val.val ⦄ := by
+  cases size <;> simp [util.allocation.prepare, preparedValue, WP.spec_ok]
+
+/- The extracted assertions force exact preservation on every optional size,
+including oversized and unaligned values. They do not certify allocator use.
+-/
+theorem assert_preparation (size : Option Usize) (align : NonZeroUsize) :
+    util.allocation.assert_preparation size align ⦃ _ => True ⦄ := by
+  unfold util.allocation.assert_preparation
+  step with prepare size align as ⟨prepared, prepared_facts⟩
+  cases size with
+  | none =>
+    have absent : prepared = none := by
+      simpa only [preparedValue, Option.map_none, Option.map_eq_none_iff] using prepared_facts
+    simp [absent, core.option.Option.is_none, WP.spec_ok]
+  | some size =>
+    cases prepared with
+    | none => simp [preparedValue] at prepared_facts
+    | some pair =>
+      rcases pair with ⟨actual_size, actual_align⟩
+      have pair_eq := Option.some.inj prepared_facts
+      have size_value := congrArg Prod.fst pair_eq
+      have align_value := congrArg Prod.snd pair_eq
+      have size_same : actual_size = size := UScalar.eq_of_val_eq size_value
+      have align_same : actual_align.val = align.val := UScalar.eq_of_val_eq align_value
+      simp [size_same, align_same, core.num.nonzero.NonZero.get, WP.spec_ok]
+
+end Zerocopy.Proofs.Raw.Allocation
+
+namespace Zerocopy.Proofs
+open AeneasSpecs
+
+theorem allocation_prepare_spec : Specs.allocation_prepare_spec := by
+  unfold Specs.allocation_prepare_spec
+  representation_simps
+  intro size align positive
+  apply WP.spec_mono (Raw.Allocation.prepare size align)
+  intro result facts
+  refine ⟨?_, ?_⟩
+  · change ∀ pair ∈ result, isValid pair
+    cases result with
+    | none => simp
+    | some pair =>
+      rcases pair with ⟨allocated, result_align⟩
+      have accepted := Raw.Allocation.preparedValue_some (size.map UScalar.val)
+        align.val.val allocated.val result_align.val.val facts.symm
+      have output_positive : 0 < result_align.val.val := by
+        simpa only [accepted.2] using positive
+      have pair_valid : isValid (allocated, result_align) := (prod_valid_iff _).mpr
+        ⟨by simp, (nonzero_valid_iff _).mpr output_positive⟩
+      simpa using pair_valid
+  · rw [Raw.Allocation.preparedValue_input] at facts
+    exact facts
+register_spec_step allocation_prepare_spec
+
+theorem allocation_preparation_check_spec : Specs.allocation_preparation_check_spec := by
+  unfold Specs.allocation_preparation_check_spec
+  representation_simps
+  intro size align positive
+  apply WP.spec_mono (Raw.Allocation.assert_preparation size align)
+  intro result facts
+  exact ⟨(), rfl⟩
+register_spec_step allocation_preparation_check_spec
+
+end Zerocopy.Proofs
+
+namespace Zerocopy.Proofs.Raw.Allocation
+open Zerocopy.Proofs.Raw.TailChecks
+
+/- Recover the unchanged optional metadata size from an accepted preparation. -/
+theorem accepted_size (size : Option Usize) (align : NonZeroUsize)
+    (allocated : Usize) (output_align : NonZeroUsize)
+    (facts : (some (allocated, output_align)).map (fun pair => (pair.1.val, pair.2.val.val)) =
+      preparedValue (size.map UScalar.val) align.val.val) : size = some allocated := by
+  have accepted := preparedValue_some (size.map UScalar.val) align.val.val allocated.val
+    output_align.val.val facts.symm
+  apply optional_value_injective
+  simpa only [Option.map_some] using accepted.1
+
+/- Both the concrete trait path and the independent reference are executed.
+A present concrete sizing result establishes representability; preparation
+only preserves it and does not impose an allocator-validity filter.
+-/
+theorem assert_allocation_size (runtime_layout : layout.DstLayout)
+    (rounding_align : NonZeroUsize) (phase metadata : Usize)
+    (layout_positive : 0 < runtime_layout.align.val.val)
+    (layout_canonical : canonicalLayout runtime_layout)
+    (rounding_positive : 0 < rounding_align.val.val) :
+    util.allocation.assert_allocation_size runtime_layout rounding_align phase metadata ⦃ _ => True ⦄ := by
+  unfold util.allocation.assert_allocation_size
+  cases info : runtime_layout.size_info with
+  | Sized size =>
+    step with PointerMetadata.pointer_metadata_unit_size_for_metadata_spec runtime_layout
+      as ⟨actual, actual_value⟩
+    simp only [info] at actual_value
+    subst actual
+    step with same_optional_usize (some size) (some size) as ⟨same, same_iff⟩
+    simp only [same_iff.mpr (by simp), massert, if_true, bind_ok]
+    step with assert_preparation (some size) runtime_layout.align
+    step with prepare (some size) runtime_layout.align as ⟨prepared, prepared_facts⟩
+    cases prepared with
+    | none => simp only [WP.spec_ok]
+    | some pair =>
+      rcases pair with ⟨allocated, output_align⟩
+      have same := accepted_size (some size) runtime_layout.align allocated output_align prepared_facts
+      have size_same := Option.some.inj same
+      subst allocated
+      step with same_optional_usize (some size) (some size) as ⟨same, same_iff⟩
+      simp [same_iff.mpr (by simp), WP.spec_ok]
+  | SliceDst tail =>
+    step with TailTransforms.witness_matches tail rounding_align phase as ⟨matching_result, matching⟩
+    split
+    · rename_i matches_true
+      have witness := matching matches_true
+      have canonical : 0 < tail.size_rounding_align_and_phase._0.val.val := by
+        simpa only [canonicalLayout, info] using layout_canonical
+      have view := witness_view tail rounding_align phase witness.1 witness.2.1 witness.2.2
+      step with PointerMetadata.pointer_metadata_usize_size_for_metadata_spec metadata runtime_layout
+        (by simpa only [info] using canonical) as ⟨actual, actual_value⟩
+      simp only [info, view] at actual_value
+      step with reference_size tail rounding_align phase metadata rounding_positive
+        as ⟨expected, expected_value⟩
+      have size_same : actual = expected := optional_value_injective
+        (actual_value.trans expected_value.symm)
+      step with same_optional_usize actual expected as ⟨same, same_iff⟩
+      simp only [same_iff.mpr size_same, massert, if_true, bind_ok]
+      step with assert_preparation actual runtime_layout.align
+      step with prepare actual runtime_layout.align as ⟨prepared, prepared_facts⟩
+      cases prepared with
+      | none => simp only [WP.spec_ok]
+      | some pair =>
+        rcases pair with ⟨allocated, output_align⟩
+        have actual_same := accepted_size actual runtime_layout.align allocated output_align prepared_facts
+        have expected_same : expected = some allocated := size_same.symm.trans actual_same
+        step with same_optional_usize expected (some allocated) as ⟨same, same_iff⟩
+        simp only [same_iff.mpr expected_same, massert, if_true, bind_ok]
+        rw [expected_same] at expected_value
+        simp only [Option.map_some] at expected_value
+        have size_facts := (checkedNat_some _ _).mp expected_value.symm
+        have lower := LayoutMath.Formula.size_lower_bound
+          (witnessFormula tail rounding_align phase) metadata.val
+        have unrounded_bound : tail.size_base.val + phase.val + metadata.val * tail.elem_size.val ≤
+            allocated.val := by
+          simpa only [witnessFormula, ← size_facts.2] using lower
+        have fits : allocated.val ≤ Usize.max := by scalar_tac
+        step as ⟨start, start_facts⟩
+        cases start with
+        | none =>
+          simp only [] at start_facts
+          omega
+        | some start =>
+          simp only [] at start_facts
+          have start_value : start.val = tail.size_base.val + phase.val := by omega
+          simp only [UScalar.lt_equiv]
+          split
+          · simp only [WP.spec_ok]
+          · rename_i offset_bound
+            have contained : tail.offset.val + metadata.val * tail.elem_size.val ≤ allocated.val := by omega
+            step as ⟨bytes, bytes_facts⟩
+            cases bytes with
+            | none => simp only [] at bytes_facts; omega
+            | some bytes =>
+              simp only [] at bytes_facts
+              have bytes_value : bytes.val = metadata.val * tail.elem_size.val := by omega
+              step as ⟨ending, ending_facts⟩
+              cases ending with
+              | none => simp only [] at ending_facts; omega
+              | some ending =>
+                simp only [] at ending_facts
+                have ending_le : ending ≤ allocated := by scalar_tac
+                simp [ending_le, WP.spec_ok]
+    · simp only [WP.spec_ok]
+
+end Zerocopy.Proofs.Raw.Allocation
+
+namespace Zerocopy.Proofs
+
+theorem allocation_size_check_spec : Specs.allocation_size_check_spec := by
+  unfold Specs.allocation_size_check_spec
+  representation_simps
+  intro runtime_layout rounding_align phase metadata layout_valid rounding_positive
+  have canonical : canonicalLayout runtime_layout := by
+    cases info : runtime_layout.size_info with
+    | Sized size => simp only [canonicalLayout, info]
+    | SliceDst tail => simpa only [canonicalLayout, info] using layout_valid.2
+  apply WP.spec_mono (Raw.Allocation.assert_allocation_size runtime_layout rounding_align phase metadata
+    layout_valid.1 canonical rounding_positive)
+  intro result facts
+  exact ⟨(), rfl⟩
+register_spec_step allocation_size_check_spec
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/RequiredModelContracts/Allocation.lean b/verification/aeneas/lean/RequiredModelContracts/Allocation.lean
new file mode 100644
index 0000000000..aefcd6c183
--- /dev/null
+++ b/verification/aeneas/lean/RequiredModelContracts/Allocation.lean
@@ -0,0 +1,66 @@
+/- 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 Obligations.Allocation
+public import Specs
+public import MathViews
+public import RequiredModelContracts.PrimitiveChecks
+@[expose] public section
+
+open Aeneas Aeneas.Std AeneasSpecs
+set_option linter.unusedVariables false
+set_option linter.unusedSimpArgs false
+namespace Zerocopy.Proofs
+
+/- Consume the authored promise for this arbitrary outcome. Neither adapter
+executes the implementation or uses its correctness theorem.
+-/
+@[contract_simps] theorem required_allocation_prepare (size : Option Usize)
+    (align : NonZeroUsize) (run : Result (Option (Usize × NonZeroUsize)))
+    (provided : Specs.allocation_prepare_spec_contract size align run) :
+    Obligations.allocation_prepare_spec_contract size align run := by
+  intro positive
+  have size_valid : isValid size := by simp
+  obtain ⟨size_value, size_decoded⟩ := size_valid
+  let align_value : NonZeroUsizeValue := ⟨unsignedWord align.val, positive⟩
+  have align_decoded := (decodeNonZeroUScalar_iff align align_value).mpr rfl
+  apply WP.spec_mono (provided size_value size_decoded align_value align_decoded)
+  rintro result ⟨_value, _decoded, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_allocation_preparation_check (size : Option Usize)
+    (align : NonZeroUsize) (run : Result Unit)
+    (provided : Specs.allocation_preparation_check_spec_contract size align run) :
+    Obligations.allocation_preparation_check_spec_contract size align run := by
+  intro positive
+  have size_valid : isValid size := by simp
+  obtain ⟨size_value, size_decoded⟩ := size_valid
+  let align_value : NonZeroUsizeValue := ⟨unsignedWord align.val, positive⟩
+  have align_decoded := (decodeNonZeroUScalar_iff align align_value).mpr rfl
+  apply WP.spec_mono (provided size_value size_decoded align_value align_decoded)
+  rintro result ⟨_value, _decoded, facts⟩
+  trivial
+
+@[contract_simps] theorem required_allocation_size_check (runtime_layout : layout.DstLayout)
+    (rounding_align : NonZeroUsize) (phase metadata : Usize) (run : Result Unit)
+    (provided : Specs.allocation_size_check_spec_contract
+      runtime_layout rounding_align phase metadata run) :
+    Obligations.allocation_size_check_spec_contract
+      runtime_layout rounding_align phase metadata run := by
+  intro layout_positive layout_canonical rounding_positive
+  obtain ⟨layout_value, layout_decoded⟩ :=
+    layout_admitted_of_canonical runtime_layout layout_positive layout_canonical
+  let rounding_value : NonZeroUsizeValue := ⟨unsignedWord rounding_align.val, rounding_positive⟩
+  have rounding_decoded := (decodeNonZeroUScalar_iff rounding_align rounding_value).mpr rfl
+  apply WP.spec_mono (provided layout_value layout_decoded rounding_value rounding_decoded
+    (unsignedWord phase) rfl (unsignedWord metadata) rfl)
+  intro result facts
+  trivial
+
+end Zerocopy.Proofs
diff --git a/zerocopy/src/util/allocation.rs b/zerocopy/src/util/allocation.rs
new file mode 100644
index 0000000000..5cf609b17a
--- /dev/null
+++ b/zerocopy/src/util/allocation.rs
@@ -0,0 +1,172 @@
+// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+//
+// 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.
+
+#![allow(dead_code, clippy::needless_nonzero_get)]
+
+use core::num::NonZeroUsize;
+
+use crate::DstLayout;
+
+/// Prepares the actual metadata size without changing allocator arguments.
+///
+/// `None` propagates metadata sizing overflow. A present size and alignment are
+/// preserved exactly, including zero size. Allocator validity additionally
+/// requires the completed KnownLayout contract and valid metadata; this helper
+/// does not infer those facts from an arbitrary size or decoded layout.
+///
+/// ```aeneas
+/// spec allocation_prepare_spec
+///   ensures(raw) result =>
+///     result.map (fun pair => (pair.1.val, pair.2.val.val)) =
+///       size.map (fun s => (s.val, align.val.val))
+/// ```
+#[inline]
+// The explicit match keeps this extraction independent of closure translation.
+#[allow(clippy::manual_map)]
+pub(super) fn prepare(size: Option<usize>, align: NonZeroUsize) -> Option<(usize, NonZeroUsize)> {
+    match size {
+        Some(size) => Some((size, align)),
+        None => None,
+    }
+}
+
+/// Checks exact preparation against the supplied optional metadata size.
+///
+/// Every input is covered, including `None`, zero, unaligned sizes, sizes above
+/// `isize::MAX`, and non-power-of-two alignments. Acceptance here asserts only
+/// unchanged numerical arguments. The separate mathematical admitted-layout
+/// domain requires power-of-two alignment, aligned complete size, and the
+/// signed-size bound before concluding allocator validity.
+///
+/// ```aeneas
+/// spec allocation_preparation_check_spec
+///   ensures(raw) _ => True
+/// ```
+fn assert_preparation(size: Option<usize>, align: NonZeroUsize) {
+    let prepared = prepare(size, align);
+    match size {
+        None => assert!(prepared.is_none()),
+        Some(size) => match prepared {
+            Some((actual_size, actual_align)) => {
+                assert!(actual_size == size);
+                assert!(actual_align.get() == align.get());
+            }
+            None => panic!("metadata size disappeared during preparation"),
+        },
+    }
+}
+
+/// Checks the concrete metadata-to-allocation numerical dataflow.
+///
+/// The independent reference keeps complete object rounding, including inner
+/// padding. Encoding witnesses are checked before use. Numerical overflow
+/// is a covered sizing outcome; allocator validity has a separate domain. The
+/// final containment assertion also needs a physical-offset premise: it is
+/// checked only when
+/// the tail starts within the unrounded fixed region. Recursive completed
+/// layouts have a separate containment theorem; decoding alone is insufficient.
+///
+/// ```aeneas
+/// spec allocation_size_check_spec
+///   ensures(raw) _ => True
+/// ```
+fn assert_allocation_size(
+    runtime_layout: DstLayout,
+    rounding_align: NonZeroUsize,
+    phase: usize,
+    metadata: usize,
+) {
+    use crate::layout::SizeInfo;
+    let (actual, expected) = match runtime_layout.size_info {
+        SizeInfo::Sized { size } => {
+            (crate::pointer_metadata_unit_size_for_metadata(runtime_layout), Some(size))
+        }
+        SizeInfo::SliceDst(tail) => {
+            if !crate::layout::tail_transform_checks::witness_matches(tail, rounding_align, phase) {
+                return;
+            }
+            (
+                crate::pointer_metadata_usize_size_for_metadata(metadata, runtime_layout),
+                crate::layout::tail_checks::reference_size(tail, rounding_align, phase, metadata),
+            )
+        }
+    };
+    assert!(crate::layout::tail_checks::same_optional_usize(actual, expected));
+    assert_preparation(actual, runtime_layout.align);
+    let size = match prepare(actual, runtime_layout.align) {
+        Some((size, _align)) => size,
+        None => return,
+    };
+    assert!(crate::layout::tail_checks::same_optional_usize(expected, Some(size)));
+    if let SizeInfo::SliceDst(tail) = runtime_layout.size_info {
+        let unrounded_start = match tail.size_base.checked_add(phase) {
+            Some(start) => start,
+            None => panic!("accepted complete size has an overflowing fixed region"),
+        };
+        if tail.offset > unrounded_start {
+            return;
+        }
+        let bytes = match metadata.checked_mul(tail.elem_size) {
+            Some(bytes) => bytes,
+            None => panic!("accepted complete size has an overflowing tail"),
+        };
+        let tail_end = match tail.offset.checked_add(bytes) {
+            Some(end) => end,
+            None => panic!("accepted complete size has an overflowing tail end"),
+        };
+        assert!(tail_end <= size);
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use crate::layout::{RoundingAlignAndPhase, SizeInfo, TrailingSliceLayout};
+
+    #[test]
+    fn preparation_boundaries() {
+        for alignment in [1, 2, 4, 8, 3, 1 << (usize::BITS - 1)] {
+            let alignment = NonZeroUsize::new(alignment).unwrap();
+            assert_preparation(None, alignment);
+            for size in [0, 1, 7, 8, 9, DstLayout::MAX_SIZE, DstLayout::MAX_SIZE + 1, usize::MAX] {
+                assert_preparation(Some(size), alignment);
+            }
+        }
+    }
+
+    #[test]
+    fn metadata_preparation_boundaries() {
+        let one = NonZeroUsize::new(1).unwrap();
+        let eight = NonZeroUsize::new(8).unwrap();
+        for size in [0, 1, 8, DstLayout::MAX_SIZE, DstLayout::MAX_SIZE + 1, usize::MAX] {
+            let layout = DstLayout {
+                align: one,
+                size_info: SizeInfo::Sized { size },
+                statically_shallow_unpadded: false,
+            };
+            assert_allocation_size(layout, one, 0, 0);
+        }
+        for (base, phase, stride, offset) in [(0, 0, 0, 0), (0, 0, 1, 0), (8, 1, 1, 9)] {
+            let layout = DstLayout {
+                align: one,
+                size_info: SizeInfo::SliceDst(TrailingSliceLayout {
+                    offset,
+                    elem_size: stride,
+                    size_base: base,
+                    size_rounding_align_and_phase: RoundingAlignAndPhase::new(eight, phase),
+                }),
+                statically_shallow_unpadded: false,
+            };
+            for metadata in [0, 1, 7, DstLayout::MAX_SIZE, usize::MAX] {
+                assert_allocation_size(layout, eight, phase, metadata);
+            }
+        }
+    }
+}
diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs
index ddd876429a..6b76d63b91 100644
--- a/zerocopy/src/util/mod.rs
+++ b/zerocopy/src/util/mod.rs
@@ -14,6 +14,7 @@ pub(crate) mod macros;
 #[doc(hidden)]
 pub mod macro_util;
 
+mod allocation;
 mod checks;
 
 use core::{
@@ -427,28 +428,23 @@ pub(crate) unsafe fn new_box<T>(
 where
     T: ?Sized + crate::KnownLayout,
 {
-    let align = T::LAYOUT.align.get();
     if !T::is_valid_metadata(meta) {
         return Err(AllocError);
     }
-    let size = match T::size_for_metadata(meta) {
-        Some(size) => size,
-        // Thanks to the `!T::is_valid_metadata(meta)` check
-        // above, this branch is unreachable. Fortunately, the
-        // optimizer recognizes this, so replacing this branch
-        // with `unreachable_unchecked` produces no codegen
-        // improvements.
+    let (size, align) = match allocation::prepare(T::size_for_metadata(meta), T::LAYOUT.align) {
+        Some(prepared) => prepared,
+        // Valid metadata guarantees a representable complete size by the
+        // KnownLayout contract. Preparation preserves a failed sizing result.
         None => return Err(AllocError),
     };
+    let align = align.get();
     let ptr = if size != 0 {
         // SAFETY:
         // - `align` is derived from a `NonZeroUsize` and is thus non-zero.
-        // - `align` is a power of two because, by invariant on
-        //   `KnownLayout::LAYOUT` `<T as KnownLayout>::LAYOUT` accurately
-        //   reflects the layout of `T`.
-        // - `size`, by invariant on `size_for_metadata` is well-aligned for
-        //   `align` and, by the check on `T::is_valid_metadata(meta)`, is less
-        //   than `isize::MAX`.
+        // - `align` is a power of two by the KnownLayout::LAYOUT contract.
+        // - The complete metadata size is aligned to `align` and bounded by
+        //   `isize::MAX` by KnownLayout and the valid-metadata check above.
+        // - `prepare` preserves the actual metadata size and alignment.
         let layout: Layout = unsafe { Layout::from_size_align_unchecked(size, align) };
         // SAFETY: By contract on the caller, `allocate` is either
         // `alloc::alloc::alloc` or `alloc::alloc::alloc_zeroed`. The above