diff --git a/verification/aeneas/ADMISSION_DESIGN.md b/verification/aeneas/ADMISSION_DESIGN.md
index 0f9968be5d..16a1ff1a1b 100644
--- a/verification/aeneas/ADMISSION_DESIGN.md
+++ b/verification/aeneas/ADMISSION_DESIGN.md
@@ -35,7 +35,7 @@ storage, and general memory observations remain unsupported. Valid incoming
 references and Aeneas's reviewed borrow translation are explicit premises.
 
 `external.json` supplies exact reviewed leaves, including standard-library
-builtins and two local unsafe helpers. Local opaque body hashes are checked
+builtins and narrow local byte operations. Local opaque body hashes are checked
 against Rust-parser body boundaries. The only admitted generic transmutation
 instantiation is `u8 -> bool`; its interpretation rejects all other bytes and
 instantiations. Byte copying has explicit input and updated-output slices and
@@ -46,6 +46,25 @@ normalization must not lose a guarded call. Pinned builtin mapping and backend
 semantics remain trusted correspondence premises, rather than a translation
 certificate established by the report.
 
+The production `IntoBytes` methods delegate their write selection to
+`util::bytewrite::{exact,prefix,suffix}`. Their contracts prove exact byte
+contents, preservation of untouched destination regions, and unchanged
+rejection. The offset-copy boundary checks `start <= dst.len()` first, matching
+Rust's checked subslicing, then requires `src.len() <= dst.len() - start` for the
+unsafe copy. Its successful result is the original prefix, the source, and the
+original suffix. Incoming slice references provide initialized bytes, access
+permissions, disjointness, and allocation lifetime, just as for `copy_unchecked`.
+The boundary's Rust body subslices and directly calls `copy_nonoverlapping`.
+Keeping that body self-contained makes its source hash cover the actual pointer
+operation; a change to another local helper cannot silently change its meaning.
+
+The pinned backend's `SliceIndexRangeFromUsizeSlice.get_mut` reconstructs a
+modified suffix incorrectly: it prepends the modified suffix to the old suffix
+instead of retaining the original prefix. That builtin remains unregistered.
+The local offset copy avoids admitting its interpretation, without modifying the
+pinned toolchain. A future builtin replacement needs an independent law for the
+reconstructed destination, including unchanged length and prefix preservation.
+
 The report lives in the existing `bindings.json`. It includes both AST digests,
 root coverage, visited executions, call boundaries, registry digest, source
 identity, Cargo configuration hashes, and patched-runtime provenance. Compiler
diff --git a/verification/aeneas/external.json b/verification/aeneas/external.json
index e55775fc28..8f79f04bda 100644
--- a/verification/aeneas/external.json
+++ b/verification/aeneas/external.json
@@ -23,6 +23,7 @@
   {"rust": "core::option::{core::option::Option<T0>}::unwrap", "signature": {"unsafe": false, "inputs": ["core::option::Option<T0>"], "output": "T0", "types": 1, "consts": 0}, "lean": "core.option.Option.unwrap"},
   {"rust": "zerocopy::util::transmute_unchecked", "signature": {"unsafe": true, "inputs": ["T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "util.transmute_unchecked", "opaque": true, "source_body_sha256": "58ee51c915af14bac8c12d66d5ac65feadf59742212c869c7f45f57f847d48b6"},
   {"rust": "zerocopy::util::copy_unchecked", "signature": {"unsafe": true, "inputs": ["&[u8]", "&mut [u8]"], "output": "tuple0", "types": 0, "consts": 0}, "lean": "util.copy_unchecked", "opaque": true, "source_body_sha256": "e3529644308d0a3ce1a407d163f98676faa36a286ba4a85221b894930d54fa20"},
+  {"rust": "zerocopy::util::copy_unchecked_at", "signature": {"unsafe": true, "inputs": ["&[u8]", "&mut [u8]", "usize"], "output": "tuple0", "types": 0, "consts": 0}, "lean": "util.copy_unchecked_at", "opaque": true, "source_body_sha256": "968dea5ce0ba53c6d5922cb87b936d5ed58e7e81dce4bc36459d7a42ae251569"},
   {"rust": "core::num::{u16}::from_be_bytes", "signature": {"unsafe": false, "inputs": ["[u8;2]"], "output": "u16", "types": 0, "consts": 0}, "lean": "core.num.U16.from_be_bytes"},
   {"rust": "core::num::{u16}::from_le_bytes", "signature": {"unsafe": false, "inputs": ["[u8;2]"], "output": "u16", "types": 0, "consts": 0}, "lean": "core.num.U16.from_le_bytes"},
   {"rust": "core::num::{u16}::to_be_bytes", "signature": {"unsafe": false, "inputs": ["u16"], "output": "[u8;2]", "types": 0, "consts": 0}, "lean": "core.num.U16.to_be_bytes"},
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index c55c1bd583..a8d818d0c1 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -425,6 +425,13 @@ def byteorder.U32.from_bytes
   (O : Type) (bytes : Array Std.U8 4#usize) : Result (byteorder.U32 O) := do
   ok { _0 := bytes, _1 := core.marker.PhantomData.mk }
 
+/-- [zerocopy::byteorder::{zerocopy::byteorder::U16<O>}::to_bytes]:
+    Source: 'src/byteorder.rs', lines 578:12-580:13
+    Visibility: public -/
+def byteorder.U16.to_bytes
+  {O : Type} (self : byteorder.U16 O) : Result (Array Std.U8 2#usize) := do
+  ok self._0
+
 /-- [zerocopy::byteorder::{zerocopy::byteorder::U16<O>}::new]:
     Source: 'src/util/macros.rs', lines 568:21-568:88
     Visibility: public -/
@@ -799,6 +806,57 @@ def trait_checks.check_array_into_bytes : Result Unit := do
   trait_checks.require_into_bytes (Array.Insts.ZerocopyIntoBytes 3#usize
     (Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes))
 
+/-- [zerocopy::util::bytewrite::exact]:
+    Source: 'src/util/bytewrite/mod.rs', lines 27:0-37:1 -/
+def util.bytewrite.exact
+  (src : Slice Std.U8) (dst : Slice Std.U8) :
+  Result (Bool × (Slice Std.U8))
+  := do
+  let i := Slice.len dst
+  let i1 := Slice.len src
+  if i = i1
+  then let dst1 ← util.copy_unchecked src dst
+       ok (true, dst1)
+  else ok (false, dst)
+
+/-- [zerocopy::util::bytewrite::prefix]:
+    Source: 'src/util/bytewrite/mod.rs', lines 48:0-57:1 -/
+def util.bytewrite.prefix
+  (src : Slice Std.U8) (dst : Slice Std.U8) :
+  Result (Bool × (Slice Std.U8))
+  := do
+  let i := Slice.len src
+  let i1 := Slice.len dst
+  if i <= i1
+  then let dst1 ← util.copy_unchecked src dst
+       ok (true, dst1)
+  else ok (false, dst)
+
+/-- [zerocopy::util::bytewrite::suffix]:
+    Source: 'src/util/bytewrite/mod.rs', lines 68:0-79:1 -/
+def util.bytewrite.suffix
+  (src : Slice Std.U8) (dst : Slice Std.U8) :
+  Result (Bool × (Slice Std.U8))
+  := do
+  let i := Slice.len dst
+  let i1 := Slice.len src
+  let o ← lift (Usize.checked_sub i i1)
+  match o with
+  | none => ok (false, dst)
+  | some start =>
+    let dst1 ← util.copy_unchecked_at src dst start
+    ok (true, dst1)
+
+/-- [zerocopy::util::bytewrite::be_word_prefix]:
+    Source: 'src/util/bytewrite/mod.rs', lines 93:0-96:1 -/
+def util.bytewrite.be_word_prefix
+  (n : Std.U16) (dst : Slice Std.U8) : Result (Bool × (Slice Std.U8)) := do
+  let value ←
+    byteorder.U16.new byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder n
+  let a ← byteorder.U16.to_bytes value
+  let s ← lift (Array.to_slice a)
+  util.bytewrite.prefix s dst
+
 /-- [zerocopy::impls::_::{impl zerocopy::FromZeros for ()}::only_derive_is_allowed_to_implement_this_trait]:
     Source: 'src/util/macros.rs', lines 165:8-165:62
     Visibility: public -/
@@ -2015,7 +2073,7 @@ def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst :
 }
 
 /-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 166:0-226:1 -/
+    Source: 'src/util/mod.rs', lines 167:0-227:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -2031,7 +2089,7 @@ def util.padding_needed_for
   ok (i2 &&& mask)
 
 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 253:0-271:1 -/
+    Source: 'src/util/mod.rs', lines 254:0-272:1 -/
 def util.round_down_to_next_multiple_of_alignment
   (n : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -2048,7 +2106,7 @@ def util.round_down_to_next_multiple_of_alignment
   ok (n &&& mask)
 
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 280:0-286:1 -/
+    Source: 'src/util/mod.rs', lines 281:0-287:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -2068,7 +2126,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 295:0-301:1 -/
+    Source: 'src/util/mod.rs', lines 296:0-302:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean
index 598b7d38a4..ce24b5be06 100644
--- a/verification/aeneas/golden/FunsExternal_Template.lean
+++ b/verification/aeneas/golden/FunsExternal_Template.lean
@@ -63,6 +63,16 @@ axiom core.num.nonzero.NonZero.get
   core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) :
   core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T
 
+/-- [zerocopy::util::copy_unchecked]:
+    Source: 'src/util/mod.rs', lines 314:0-329:1 -/
+axiom util.copy_unchecked
+  : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8)
+
+/-- [zerocopy::util::copy_unchecked_at]:
+    Source: 'src/util/mod.rs', lines 343:0-354:1 -/
+axiom util.copy_unchecked_at
+  : Slice Std.U8 → Slice Std.U8 → Std.Usize → Result (Slice Std.U8)
+
 /-- [zerocopy::impls::_::{impl zerocopy::TryFromBytes for ()}::is_safe]:
     Source: 'src/util/macros.rs', lines 155:8-160:9
     Visibility: public -/
@@ -119,12 +129,7 @@ axiom Array.Insts.ZerocopyTryFromBytes.is_safe
     pointer.invariant.Shared Alignment pointer.invariant.Initialized → Result
     Bool
 
-/-- [zerocopy::util::copy_unchecked]:
-    Source: 'src/util/mod.rs', lines 313:0-328:1 -/
-axiom util.copy_unchecked
-  : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8)
-
 /-- [zerocopy::util::transmute_unchecked]:
-    Source: 'src/util/mod.rs', lines 340:0-369:1 -/
+    Source: 'src/util/mod.rs', lines 366:0-395:1 -/
 axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst
 
diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean
index 64ea9516f1..752b98e928 100644
--- a/verification/aeneas/golden/Types.lean
+++ b/verification/aeneas/golden/Types.lean
@@ -261,7 +261,7 @@ structure FromBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
 /-- Trait declaration: [zerocopy::IntoBytes]
-    Source: 'src/lib.rs', lines 5953:0-6458:1
+    Source: 'src/lib.rs', lines 5953:0-6426:1
     Visibility: public -/
 structure IntoBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
diff --git a/verification/aeneas/lean/Obligations/ByteWrite.lean b/verification/aeneas/lean/Obligations/ByteWrite.lean
new file mode 100644
index 0000000000..3f73d6b748
--- /dev/null
+++ b/verification/aeneas/lean/Obligations/ByteWrite.lean
@@ -0,0 +1,51 @@
+/- 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 Zerocopy
+public import Rust.Bytes
+@[expose] public section
+open Aeneas Aeneas.Std
+namespace Zerocopy.Obligations
+
+-- Retain all raw inputs, including unsuccessful and empty writes. These
+-- expectations are independent of the specification macro and its decoders.
+def write_exact_spec_contract (src dst : Slice U8)
+    (run : Result (Bool × Slice U8)) : Prop :=
+  run ⦃ out => out.1 = decide (src.val.length = dst.val.length) ∧
+    out.2.val = if src.val.length = dst.val.length then src.val else dst.val ⦄
+
+def write_prefix_spec_contract (src dst : Slice U8)
+    (run : Result (Bool × Slice U8)) : Prop :=
+  run ⦃ out => out.1 = decide (src.val.length ≤ dst.val.length) ∧
+    out.2.val = if src.val.length ≤ dst.val.length
+      then src.val ++ dst.val.drop src.val.length else dst.val ⦄
+
+def write_suffix_spec_contract (src dst : Slice U8)
+    (run : Result (Bool × Slice U8)) : Prop :=
+  run ⦃ out => out.1 = decide (src.val.length ≤ dst.val.length) ∧
+    out.2.val = if src.val.length ≤ dst.val.length
+      then dst.val.take (dst.val.length - src.val.length) ++ src.val else dst.val ⦄
+
+def write_exact_spec : Prop :=
+  ∀ src dst, write_exact_spec_contract src dst (util.bytewrite.exact src dst)
+def write_prefix_spec : Prop :=
+  ∀ src dst, write_prefix_spec_contract src dst (util.bytewrite.prefix src dst)
+def write_suffix_spec : Prop :=
+  ∀ src dst, write_suffix_spec_contract src dst (util.bytewrite.suffix src dst)
+
+def write_be_word_prefix_spec_contract (n : U16) (dst : Slice U8)
+    (run : Result (Bool × Slice U8)) : Prop :=
+  run ⦃ out => out.1 = decide (2 ≤ dst.val.length) ∧
+    out.2.val.map U8.bv = if 2 ≤ dst.val.length
+      then Rust.Bytes.encodeBE 2 n.val ++ (dst.val.drop 2).map U8.bv
+      else dst.val.map U8.bv ⦄
+def write_be_word_prefix_spec : Prop :=
+  ∀ n dst, write_be_word_prefix_spec_contract n dst (util.bytewrite.be_word_prefix n dst)
+
+end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/Proofs/ByteWrite.lean b/verification/aeneas/lean/Proofs/ByteWrite.lean
new file mode 100644
index 0000000000..3543ed3bbb
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/ByteWrite.lean
@@ -0,0 +1,127 @@
+/- 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 Proofs.SafetyChecks
+public import Proofs.Byteorder
+@[expose] public section
+
+/-!
+These functions are the size selection and byte-copy implementation called by
+IntoBytes's three public write methods. The proofs include unsuccessful writes
+and the unaffected destination region, rather than merely checking copied bytes.
+The source-bound copy interpretations retain the reference premises documented
+in ADMISSION_DESIGN.md; their pointer implementations are not extracted.
+-/
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+private theorem decode_write (out : Bool × Slice U8) :
+    (inferInstance : RustModel (Bool × Slice U8)).decode out =
+      some (out.1, byteSlice out.2) := by
+  have decoded := decode_byte_slice out.2
+  simp only [RustModel.decode] at decoded ⊢
+  rw [decoded]
+
+theorem write_exact_raw (src dst : Slice U8) :
+    util.bytewrite.exact src dst ⦃ out =>
+      out.1 = decide (src.val.length = dst.val.length) ∧
+      out.2.val = if src.val.length = dst.val.length then src.val else dst.val ⦄ := by
+  by_cases same : src.val.length = dst.val.length
+  · simp [util.bytewrite.exact, Slice.len,
+      util.copy_unchecked, same, bind_ok]
+  · simp [util.bytewrite.exact, Slice.len, same, Ne.symm same]
+
+theorem write_prefix_raw (src dst : Slice U8) :
+    util.bytewrite.prefix src dst ⦃ out =>
+      out.1 = decide (src.val.length ≤ dst.val.length) ∧
+      out.2.val = if src.val.length ≤ dst.val.length
+        then src.val ++ dst.val.drop src.val.length else dst.val ⦄ := by
+  by_cases fits : src.val.length ≤ dst.val.length
+  · simp [util.bytewrite.prefix, Slice.len, UScalar.le_equiv,
+      util.copy_unchecked, fits, bind_ok]
+  · simp [util.bytewrite.prefix, Slice.len, UScalar.le_equiv, fits]
+
+theorem write_suffix_raw (src dst : Slice U8) :
+    util.bytewrite.suffix src dst ⦃ out =>
+      out.1 = decide (src.val.length ≤ dst.val.length) ∧
+      out.2.val = if src.val.length ≤ dst.val.length
+        then dst.val.take (dst.val.length - src.val.length) ++ src.val else dst.val ⦄ := by
+  unfold util.bytewrite.suffix
+  step as ⟨start, facts⟩
+  cases start with
+  | none =>
+    have unfit : ¬ src.val.length ≤ dst.val.length := by simpa [Slice.len] using facts
+    simp [unfit]
+  | some start =>
+    have bounds : start.val = dst.val.length - src.val.length ∧
+        src.val.length ≤ dst.val.length := by
+      simp only [Slice.len] at facts
+      exact ⟨facts.2.1, facts.1⟩
+    have offset : start.val ≤ dst.val.length := by omega
+    have fits : src.val.length ≤ dst.val.length - start.val := by omega
+    have finish : start.val + src.val.length = dst.val.length := by omega
+    simp only [util.copy_unchecked_at, if_pos offset, dif_pos fits, bind_ok, WP.spec_ok]
+    simp [bounds.1, bounds.2]
+
+-- The concrete consumer uses the public byteorder operations, then the same
+-- prefix writer as IntoBytes. Reuse the proved encoder rather than recalculate
+-- its bitvector arithmetic inside this caller proof.
+theorem write_be_word_prefix_raw (n : U16) (dst : Slice U8) :
+    util.bytewrite.be_word_prefix n dst ⦃ out =>
+      out.1 = decide (2 ≤ dst.val.length) ∧
+      out.2.val.map U8.bv = if 2 ≤ dst.val.length
+        then Rust.Bytes.encodeBE 2 n.val ++ (dst.val.drop 2).map U8.bv
+        else dst.val.map U8.bv ⦄ := by
+  have encoding_eq : (do
+      let value ← byteorder.U16.new byteorder.BigEndian.Insts.ZerocopyByteorderByteOrder n
+      byteorder.U16.to_bytes value) = byteorder.verification.write_u16_be n := by
+    simp only [byteorder.verification.write_u16_be, core.convert.IntoFrom.into,
+      ArrayU82.Insts.CoreConvertFromU16.from,
+      byteorder.U16.to_bytes]
+  unfold util.bytewrite.be_word_prefix
+  rw [← Aeneas.Std.bind_assoc, encoding_eq]
+  step with Raw.write_u16_be n as ⟨bytes, encoded⟩
+  simp only [lift, bind_ok]
+  apply WP.spec_mono (write_prefix_raw (Array.to_slice bytes) dst)
+  intro out facts
+  have length : bytes.val.length = 2 := by simp
+  simp only [Array.to_slice, Slice.from_val, length] at facts
+  refine ⟨facts.1, ?_⟩
+  by_cases fits : 2 ≤ dst.val.length
+  · simp only [if_pos fits] at facts ⊢
+    rw [facts.2, List.map_append, encoded]
+  · simp only [if_neg fits] at facts ⊢
+    rw [facts.2]
+
+theorem write_exact_spec : Specs.write_exact_spec := by
+  intro src dst _ _ _ _
+  apply WP.spec_mono (write_exact_raw src dst)
+  intro out facts
+  exact ⟨(out.1, byteSlice out.2), decode_write out, facts⟩
+
+theorem write_prefix_spec : Specs.write_prefix_spec := by
+  intro src dst _ _ _ _
+  apply WP.spec_mono (write_prefix_raw src dst)
+  intro out facts
+  exact ⟨(out.1, byteSlice out.2), decode_write out, facts⟩
+
+theorem write_suffix_spec : Specs.write_suffix_spec := by
+  intro src dst _ _ _ _
+  apply WP.spec_mono (write_suffix_raw src dst)
+  intro out facts
+  exact ⟨(out.1, byteSlice out.2), decode_write out, facts⟩
+
+theorem write_be_word_prefix_spec : Specs.write_be_word_prefix_spec := by
+  intro n dst _ _ _ _
+  apply WP.spec_mono (write_be_word_prefix_raw n dst)
+  intro out facts
+  exact ⟨(out.1, byteSlice out.2), decode_write out, facts⟩
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/RequiredModelContracts/ByteWrite.lean b/verification/aeneas/lean/RequiredModelContracts/ByteWrite.lean
new file mode 100644
index 0000000000..79cf69d5b7
--- /dev/null
+++ b/verification/aeneas/lean/RequiredModelContracts/ByteWrite.lean
@@ -0,0 +1,55 @@
+/- 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 RequiredContracts
+public import Proofs.ByteWrite
+public import Obligations.ByteWrite
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+-- Challenge each contract with an arbitrary execution outcome. Using only the
+-- actual function's good behavior here could hide an accidentally weaker spec.
+@[contract_simps] theorem required_write_exact (src dst : Slice U8)
+    (run : Result (Bool × Slice U8))
+    (provided : Specs.write_exact_spec_contract src dst run) :
+    Obligations.write_exact_spec_contract src dst run := by
+  apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src)
+    (byteSlice dst) (decode_byte_slice dst))
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_write_prefix (src dst : Slice U8)
+    (run : Result (Bool × Slice U8))
+    (provided : Specs.write_prefix_spec_contract src dst run) :
+    Obligations.write_prefix_spec_contract src dst run := by
+  apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src)
+    (byteSlice dst) (decode_byte_slice dst))
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_write_suffix (src dst : Slice U8)
+    (run : Result (Bool × Slice U8))
+    (provided : Specs.write_suffix_spec_contract src dst run) :
+    Obligations.write_suffix_spec_contract src dst run := by
+  apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src)
+    (byteSlice dst) (decode_byte_slice dst))
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_write_be_word_prefix (n : U16) (dst : Slice U8)
+    (run : Result (Bool × Slice U8))
+    (provided : Specs.write_be_word_prefix_spec_contract n dst run) :
+    Obligations.write_be_word_prefix_spec_contract n dst run := by
+  apply WP.spec_mono (provided (unsignedWord n) rfl
+    (byteSlice dst) (decode_byte_slice dst))
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/SafetyTests.lean b/verification/aeneas/lean/SafetyTests.lean
index ec86c7c89e..e374074266 100644
--- a/verification/aeneas/lean/SafetyTests.lean
+++ b/verification/aeneas/lean/SafetyTests.lean
@@ -31,6 +31,13 @@ theorem copy_rejects_oversize (src dst : Slice U8)
     util.copy_unchecked src dst = .fail .undef := by
   simp [util.copy_unchecked, Zerocopy.forbiddenExecution, Nat.not_le.mpr oversize]
 
+theorem offset_copy_rejects_oversize (src dst : Slice U8) (start : Usize)
+    (inside : start.val ≤ dst.val.length)
+    (oversize : dst.val.length - start.val < src.val.length) :
+    util.copy_unchecked_at src dst start = .fail .undef := by
+  simp [util.copy_unchecked_at, Zerocopy.forbiddenExecution, inside,
+    Nat.not_le.mpr oversize]
+
 -- This is the model of an unsafe producer with an invalid bit pattern. These
 -- examples execute no Rust UB: they examine its forbidden abstract outcome.
 noncomputable def badBool : Result Bool := util.transmute_unchecked Bool (2#u8)
diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean
index f2eb383889..6b58a42033 100644
--- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean
+++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean
@@ -90,6 +90,23 @@ def util.copy_unchecked (src dst : Slice U8) : Result (Slice U8) :=
       omega))
   else forbiddenExecution
 
+-- The offset copy has the same reference premises. Check bounds before
+-- constructing a subslice, and preserve BOTH untouched regions. A start past
+-- the end panics at Rust's checked subslicing; an oversized copy is forbidden.
+-- FIXME: Pinned SliceIndexRangeFromUsizeSlice.get_mut reconstructs its output
+-- incorrectly (ca282ec, Aeneas/Std/Slice.lean). Do not admit that builtin until
+-- its prefix-preservation law has been repaired and checked independently.
+def util.copy_unchecked_at (src dst : Slice U8) (start : Usize) : Result (Slice U8) :=
+  if start.val ≤ dst.val.length then
+    if h : src.val.length ≤ dst.val.length - start.val then
+      .ok (Slice.from
+        (dst.val.take start.val ++ src.val ++ dst.val.drop (start.val + src.val.length)) (by
+          have := dst.property
+          simp only [List.length_append, List.length_take, List.length_drop]
+          omega))
+    else forbiddenExecution
+  else .fail .panic
+
 -- Only the u8-to-bool instantiation is supported. The admission checker also
 -- checks the original Rust type arguments, before Aeneas can erase them. This
 -- guard checks bit validity BEFORE creating a Bool, whose Lean carrier cannot
diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean
index e789f38735..febac5a7e4 100644
--- a/verification/aeneas/projections/Specs.lean
+++ b/verification/aeneas/projections/Specs.lean
@@ -160,6 +160,46 @@ spec array_into_bytes_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.array_into_bytes_spec for Zerocopy.trait_checks.check_array_into_bytes with 0
 
+check_model_inputs Zerocopy.util.bytewrite.exact with 0 type parameters
+aeneas_spec_begin
+spec write_exact_spec
+  for @Zerocopy.util.bytewrite.exact with 0 type parameters
+  ensures(raw) out => out.1 = decide (src.val.length = dst.val.length) ∧
+    out.2.val = if src.val.length = dst.val.length then src.val else dst.val
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.write_exact_spec for Zerocopy.util.bytewrite.exact with 2
+
+check_model_inputs Zerocopy.util.bytewrite.prefix with 0 type parameters
+aeneas_spec_begin
+spec write_prefix_spec
+  for @Zerocopy.util.bytewrite.prefix with 0 type parameters
+  ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧
+    out.2.val = if src.val.length ≤ dst.val.length
+      then src.val ++ dst.val.drop src.val.length else dst.val
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.write_prefix_spec for Zerocopy.util.bytewrite.prefix with 2
+
+check_model_inputs Zerocopy.util.bytewrite.suffix with 0 type parameters
+aeneas_spec_begin
+spec write_suffix_spec
+  for @Zerocopy.util.bytewrite.suffix with 0 type parameters
+  ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧
+    out.2.val = if src.val.length ≤ dst.val.length
+      then dst.val.take (dst.val.length - src.val.length) ++ src.val else dst.val
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.write_suffix_spec for Zerocopy.util.bytewrite.suffix with 2
+
+check_model_inputs Zerocopy.util.bytewrite.be_word_prefix with 0 type parameters
+aeneas_spec_begin
+spec write_be_word_prefix_spec
+  for @Zerocopy.util.bytewrite.be_word_prefix with 0 type parameters
+  ensures(raw) out => out.1 = decide (2 ≤ dst.val.length) ∧
+    out.2.val.map (fun byte => byte.bv) = if 2 ≤ dst.val.length
+      then Rust.Bytes.encodeBE 2 n.val ++ (dst.val.drop 2).map (fun byte => byte.bv)
+      else dst.val.map (fun byte => byte.bv)
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.write_be_word_prefix_spec for Zerocopy.util.bytewrite.be_word_prefix with 2
+
 check_model_inputs Zerocopy.util.padding_needed_for with 0 type parameters
 aeneas_spec_begin
 spec padding_lt_alignment
diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs
index 595b0c449d..6fb83f7a1a 100644
--- a/zerocopy/src/lib.rs
+++ b/zerocopy/src/lib.rs
@@ -6190,13 +6190,7 @@ pub unsafe trait IntoBytes {
     where
         Self: Immutable,
     {
-        let src = self.as_bytes();
-        if dst.len() == src.len() {
-            // SAFETY: Within this branch of the conditional, we have ensured
-            // that `dst.len()` is equal to `src.len()`. Neither the size of the
-            // source nor the size of the destination change between the above
-            // size check and the invocation of `copy_unchecked`.
-            unsafe { util::copy_unchecked(src, dst) }
+        if util::bytewrite::exact(self.as_bytes(), dst) {
             Ok(())
         } else {
             Err(SizeError::new(self))
@@ -6276,18 +6270,10 @@ pub unsafe trait IntoBytes {
     where
         Self: Immutable,
     {
-        let src = self.as_bytes();
-        match dst.get_mut(..src.len()) {
-            Some(dst) => {
-                // SAFETY: Within this branch of the `match`, we have ensured
-                // through fallible subslicing that `dst.len()` is equal to
-                // `src.len()`. Neither the size of the source nor the size of
-                // the destination change between the above subslicing operation
-                // and the invocation of `copy_unchecked`.
-                unsafe { util::copy_unchecked(src, dst) }
-                Ok(())
-            }
-            None => Err(SizeError::new(self)),
+        if util::bytewrite::prefix(self.as_bytes(), dst) {
+            Ok(())
+        } else {
+            Err(SizeError::new(self))
         }
     }
 
@@ -6371,29 +6357,11 @@ pub unsafe trait IntoBytes {
     where
         Self: Immutable,
     {
-        let src = self.as_bytes();
-        let start = if let Some(start) = dst.len().checked_sub(src.len()) {
-            start
-        } else {
-            return Err(SizeError::new(self));
-        };
-        let dst = if let Some(dst) = dst.get_mut(start..) {
-            dst
+        if util::bytewrite::suffix(self.as_bytes(), dst) {
+            Ok(())
         } else {
-            // get_mut() should never return None here. We return a `SizeError`
-            // rather than .unwrap() because in the event the branch is not
-            // optimized away, returning a value is generally lighter-weight
-            // than panicking.
-            return Err(SizeError::new(self));
-        };
-        // SAFETY: Through fallible subslicing of `dst`, we have ensured that
-        // `dst.len()` is equal to `src.len()`. Neither the size of the source
-        // nor the size of the destination change between the above subslicing
-        // operation and the invocation of `copy_unchecked`.
-        unsafe {
-            util::copy_unchecked(src, dst);
+            Err(SizeError::new(self))
         }
-        Ok(())
     }
 
     /// Writes a copy of `self` to an `io::Write`.
diff --git a/zerocopy/src/util/bytewrite/mod.rs b/zerocopy/src/util/bytewrite/mod.rs
new file mode 100644
index 0000000000..edbdfbaeb4
--- /dev/null
+++ b/zerocopy/src/util/bytewrite/mod.rs
@@ -0,0 +1,153 @@
+// 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.
+
+//! The byte-writing part of `IntoBytes`.
+//!
+//! Keeping size selection here lets Lean check the code used by all three
+//! public methods. Obtaining `src` from a typed value remains the separate
+//! `IntoBytes::as_bytes` safety argument. These functions receive valid slice
+//! references, so they need not reconstruct allocation lifetime or provenance.
+
+/// Writes the whole destination, rejecting unequal lengths without mutation.
+///
+/// ```aeneas
+/// spec write_exact_spec
+///   ensures(raw) out => out.1 = decide (src.val.length = dst.val.length) ∧
+///     out.2.val = if src.val.length = dst.val.length then src.val else dst.val
+/// ```
+#[inline]
+pub(crate) fn exact(src: &[u8], dst: &mut [u8]) -> bool {
+    if dst.len() == src.len() {
+        // SAFETY: Equal lengths imply the helper's length requirement. The
+        // input references supply an initialized source and exclusive
+        // destination, and neither length changes before the copy.
+        unsafe { super::copy_unchecked(src, dst) };
+        true
+    } else {
+        false
+    }
+}
+
+/// Writes a fitting prefix, preserving the suffix and rejecting without mutation.
+///
+/// ```aeneas
+/// spec write_prefix_spec
+///   ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧
+///     out.2.val = if src.val.length ≤ dst.val.length
+///       then src.val ++ dst.val.drop src.val.length else dst.val
+/// ```
+#[inline]
+pub(crate) fn prefix(src: &[u8], dst: &mut [u8]) -> bool {
+    if src.len() <= dst.len() {
+        // SAFETY: This branch establishes the helper's sole extra requirement.
+        // It copies only src.len() bytes, leaving the destination suffix alone.
+        unsafe { super::copy_unchecked(src, dst) };
+        true
+    } else {
+        false
+    }
+}
+
+/// Writes a fitting suffix, preserving the prefix and rejecting without mutation.
+///
+/// ```aeneas
+/// spec write_suffix_spec
+///   ensures(raw) out => out.1 = decide (src.val.length ≤ dst.val.length) ∧
+///     out.2.val = if src.val.length ≤ dst.val.length
+///       then dst.val.take (dst.val.length - src.val.length) ++ src.val else dst.val
+/// ```
+#[inline]
+pub(crate) fn suffix(src: &[u8], dst: &mut [u8]) -> bool {
+    let start = if let Some(start) = dst.len().checked_sub(src.len()) {
+        start
+    } else {
+        return false;
+    };
+    // SAFETY: Successful subtraction gives start <= dst.len() and
+    // src.len() == dst.len() - start. The input references provide the source
+    // and destination access conditions required by copy_unchecked_at.
+    unsafe { super::copy_unchecked_at(src, dst, start) };
+    true
+}
+
+/// A concrete padding-free consumer: encode a big-endian word using the public
+/// byteorder constructor/accessor, then run the production prefix writer.
+/// The tests below compare this composition with `IntoBytes::write_to_prefix`.
+///
+/// ```aeneas
+/// spec write_be_word_prefix_spec
+///   ensures(raw) out => out.1 = decide (2 ≤ dst.val.length) ∧
+///     out.2.val.map (fun byte => byte.bv) = if 2 ≤ dst.val.length
+///       then Rust.Bytes.encodeBE 2 n.val ++ (dst.val.drop 2).map (fun byte => byte.bv)
+///       else dst.val.map (fun byte => byte.bv)
+/// ```
+#[allow(dead_code)]
+fn be_word_prefix(n: u16, dst: &mut [u8]) -> bool {
+    let value = crate::byteorder::big_endian::U16::new(n);
+    prefix(&value.to_bytes(), dst)
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::{byteorder::big_endian::U16, IntoBytes};
+
+    // These exercise the public methods, including their typed-to-byte bridge.
+    // Lean checks the shared selection/copying code; these regression tests
+    // additionally catch a public method wired to the wrong selection helper.
+    #[test]
+    fn public_writes() {
+        let value = U16::from_bytes([1, 2]);
+        for length in 0..=4 {
+            for mode in 0..3 {
+                let mut storage = [9, 8, 7, 6];
+                let dst = &mut storage[..length];
+                let accepted = match mode {
+                    0 => value.write_to(dst).is_ok(),
+                    1 => value.write_to_prefix(dst).is_ok(),
+                    _ => value.write_to_suffix(dst).is_ok(),
+                };
+                let fits = if mode == 0 { length == 2 } else { length >= 2 };
+                assert_eq!(accepted, fits);
+                let mut expected = [9, 8, 7, 6];
+                if fits {
+                    let start = if mode == 2 { length - 2 } else { 0 };
+                    expected[start..start + 2].copy_from_slice(&[1, 2]);
+                }
+                assert_eq!(storage, expected);
+            }
+        }
+    }
+
+    #[test]
+    fn empty_writes() {
+        let value: [u8; 0] = [];
+        let mut dst = [9; 3];
+        value.write_to(&mut []).unwrap();
+        value.write_to(&mut dst).unwrap_err();
+        value.write_to_prefix(&mut dst).unwrap();
+        value.write_to_suffix(&mut dst).unwrap();
+        assert_eq!(dst, [9; 3]);
+    }
+
+    #[test]
+    fn concrete_word_consumer() {
+        for n in [0, 1, 255, 256, u16::MAX] {
+            for length in 0..=4 {
+                let mut via_array = [9, 8, 7, 6];
+                let mut via_into_bytes = via_array;
+                let accepted = super::be_word_prefix(n, &mut via_array[..length]);
+                let value = U16::new(n);
+                assert_eq!(accepted, value.write_to_prefix(&mut via_into_bytes[..length]).is_ok());
+                assert_eq!(via_array, via_into_bytes);
+            }
+        }
+    }
+}
diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs
index e9167686c1..f4c53b4428 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;
 
+pub(crate) mod bytewrite;
 #[cfg(target_endian = "little")]
 #[allow(dead_code)]
 mod owned_transmute;
@@ -327,6 +328,31 @@ pub(crate) unsafe fn copy_unchecked(src: &[u8], dst: &mut [u8]) {
     };
 }
 
+/// Copies `src` into `dst` beginning at byte `start`.
+///
+/// This is a separate reviewed Aeneas boundary, using the same byte-copy
+/// contract as `copy_unchecked`. The model checks the subslice bounds and
+/// retains both untouched regions of the destination.
+///
+/// # Safety
+///
+/// The caller guarantees `start <= dst.len()` and
+/// `src.len() <= dst.len() - start`.
+#[inline(always)]
+#[allow(clippy::indexing_slicing)] // The caller promises an in-bounds start.
+pub(crate) unsafe fn copy_unchecked_at(src: &[u8], dst: &mut [u8], start: usize) {
+    let dst = &mut dst[start..];
+    // Keep this trusted boundary self-contained: its body hash also covers the
+    // actual pointer operation, rather than hiding a mutable local dependency.
+    // SAFETY: The caller guarantees enough bytes in this subslice. The source
+    // reference supplies initialized readable bytes; the mutable destination
+    // supplies writable, disjoint bytes. Byte alignment is one, and subslicing
+    // retains the destination's allocation and exclusive access.
+    unsafe {
+        core::ptr::copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), src.len());
+    };
+}
+
 /// Unsafely transmutes the given `src` into a type `Dst`.
 ///
 /// Aeneas admits only the `u8` to `bool` instantiation as a trusted boundary