diff --git a/tools/aeneas-inline/src/main.rs b/tools/aeneas-inline/src/main.rs
index f54fa089d4..8a64b35a82 100644
--- a/tools/aeneas-inline/src/main.rs
+++ b/tools/aeneas-inline/src/main.rs
@@ -129,7 +129,8 @@ impl Functions<'_> {
                     supported &= receiver.reference.is_none() || receiver.mutability.is_none();
                 }
                 syn::FnArg::Typed(input) => {
-                    supported &= !unsupported_borrow(&input.ty, true);
+                    supported &=
+                        !unsupported_borrow(&input.ty, true) || mutable_byte_slice(&input.ty);
                     match input.pat.as_ref() {
                         syn::Pat::Ident(pattern)
                             if pattern.by_ref.is_none() && pattern.subpat.is_none() =>
@@ -298,6 +299,17 @@ fn unsupported_borrow(ty: &syn::Type, allow_shared: bool) -> bool {
     visitor.found
 }
 
+// Aeneas returns this mutable input as ordinary updated byte-slice state.
+// This narrow shape has no nested loans, stored references, or escaping borrow
+// transformer. Other mutable inputs remain unsupported until their returned
+// state and reconstruction semantics have an explicit audit.
+fn mutable_byte_slice(ty: &syn::Type) -> bool {
+    let syn::Type::Reference(reference) = ty else { return false };
+    let syn::Type::Slice(slice) = reference.elem.as_ref() else { return false };
+    let syn::Type::Path(element) = slice.elem.as_ref() else { return false };
+    reference.mutability.is_some() && element.qself.is_none() && element.path.is_ident("u8")
+}
+
 fn has_borrowed_fields(fields: &Value) -> bool {
     // Struct fields and enum variants share the report's recursive container
     // shape. A borrowed field in any variant makes the nominal owner unsupported.
diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index 20ca4da81b..5319434f5a 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -168,6 +168,31 @@ builtin correspondence also remains part of the pinned translator's trust
 boundary. See [ADMISSION_DESIGN.md](ADMISSION_DESIGN.md) for the implemented
 fragment and [LOWERING_AUDIT.md](LOWERING_AUDIT.md) for the erasure inventory.
 
+The first storage examples are in
+[`util/safety_checks/mod.rs`](../../zerocopy/src/util/safety_checks/mod.rs):
+
+- `checked_bool` accepts exactly byte encodings 0 and 1 and rejects all others.
+- `checked_copy` copies a fitting prefix, preserves the suffix, and leaves the
+  entire destination unchanged when the source is too long. Its model returns
+  the updated mutable slice explicitly.
+
+The existing production `add_scaled_metadata` exercises guarded unchecked
+addition and multiplication. Each of these four primitive definitions has an
+independent complete-definition check, including its forbidden branch. Kernel
+controls prove rejection even if an invalid result is discarded or followed by
+divergence. Extraction controls check actual generated callers that discard an
+invalid Boolean or reach it before a loop. Mutation controls also challenge the
+failure tag and helper guards.
+
+Incoming references must already denote valid Rust allocations with the
+necessary exclusivity and initializedness. Logical byte lists do not establish
+provenance, allocation lifetime, or reference validity. Both storage examples
+use padding-free `u8`/`bool`; general padding and typed-copy effects remain
+unsupported. No panic-catching, thread, callback, or failure-recovery model is
+admitted. Both today's total and partial contracts reject *every* execution
+failure, including source UB aborts whose tag the pinned importer merges with
+panic. Supporting a recovery handler would require preserving that distinction.
+
 The binding manifest records both inspected snapshots, their dependency
 closures, exact registry identity, sources, compiler configuration, and patched
 runtime. Inputs are captured before compilation and checked again during binding
diff --git a/verification/aeneas/control_runner.py b/verification/aeneas/control_runner.py
index d42318c462..e5f67ee322 100644
--- a/verification/aeneas/control_runner.py
+++ b/verification/aeneas/control_runner.py
@@ -26,7 +26,7 @@
 import tempfile
 import time
 
-FAMILIES = ('authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi',
+FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi',
             'contracts', 'dependencies', 'admission', 'semantics')
 MODELS = ('golden-verification', 'verification')
 FIXTURES = ('NegativeControl.lean', 'WeakOutcome.lean',
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index f63b0dc3e7..a5dfa5edf3 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -65,7 +65,7 @@ def Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner :
 }
 
 /-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 161:0-221:1 -/
+    Source: 'src/util/mod.rs', lines 163:0-223:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -81,7 +81,7 @@ def util.padding_needed_for
   ok (i2 &&& mask)
 
 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 248:0-266:1 -/
+    Source: 'src/util/mod.rs', lines 250:0-268:1 -/
 def util.round_down_to_next_multiple_of_alignment
   (n : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -98,7 +98,7 @@ def util.round_down_to_next_multiple_of_alignment
   ok (n &&& mask)
 
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 275:0-281:1 -/
+    Source: 'src/util/mod.rs', lines 277:0-283:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -118,7 +118,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 290:0-296:1 -/
+    Source: 'src/util/mod.rs', lines 292:0-298:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -137,4 +137,26 @@ def util.min
   then ok b
   else ok a
 
+/-- [zerocopy::util::safety_checks::checked_bool]:
+    Source: 'src/util/safety_checks/mod.rs', lines 28:0-38:1 -/
+def util.safety_checks.checked_bool
+  (byte : Std.U8) : Result (Option Bool) := do
+  if byte < 2#u8
+  then let b ← util.transmute_unchecked Bool byte
+       ok (some b)
+  else ok none
+
+/-- [zerocopy::util::safety_checks::checked_copy]:
+    Source: 'src/util/safety_checks/mod.rs', lines 51:0-61:1 -/
+def util.safety_checks.checked_copy
+  (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)
+
 end Zerocopy
diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean
index ccb87a43d6..fd2ceb84e7 100644
--- a/verification/aeneas/golden/FunsExternal_Template.lean
+++ b/verification/aeneas/golden/FunsExternal_Template.lean
@@ -50,3 +50,12 @@ 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 310:0-325: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 337:0-366:1 -/
+axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst
+
diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean
index 8a7e3d6b0a..084929939d 100644
--- a/verification/aeneas/lean/Check.lean
+++ b/verification/aeneas/lean/Check.lean
@@ -63,6 +63,31 @@ run_elab do
       throwError "Missing external size read"
     unless ← Meta.isDefEq (mkConst `core.mem.size_of) sizeRead do
       throwError "External size read changed its data-input interpretation"
+  if env.contains `util.transmute_unchecked then
+    let expected ← Term.elabTerm (← `(fun {Src : Type} (Dst : Type) (src : Src) => by
+      classical
+      exact if hs : Src = Aeneas.Std.U8 then
+        if hd : Dst = Bool then
+          let byte := cast hs src
+          if byte.val < 2 then Aeneas.Std.Result.ok (cast hd.symm (decide (byte.val = 1)))
+          else Aeneas.Std.Result.fail Aeneas.Std.Error.undef
+        else Aeneas.Std.Result.fail Aeneas.Std.Error.undef
+      else Aeneas.Std.Result.fail Aeneas.Std.Error.undef)) none
+    Term.synthesizeSyntheticMVarsNoPostponing
+    unless ← Meta.isDefEq (mkConst `util.transmute_unchecked) (← instantiateMVars expected) do
+      throwError "External Boolean conversion changed its complete interpretation"
+  if env.contains `util.copy_unchecked then
+    let expected ← Term.elabTerm (← `(fun (src dst : Aeneas.Std.Slice Aeneas.Std.U8) =>
+      if h : src.val.length ≤ dst.val.length then
+        Aeneas.Std.Result.ok (Aeneas.Std.Slice.from
+          (src.val ++ dst.val.drop src.val.length) (by
+            have := dst.property
+            simp only [List.length_append, List.length_drop]
+            omega))
+      else Aeneas.Std.Result.fail Aeneas.Std.Error.undef)) none
+    Term.synthesizeSyntheticMVarsNoPostponing
+    unless ← Meta.isDefEq (mkConst `util.copy_unchecked) (← instantiateMVars expected) do
+      throwError "External byte copy changed its complete interpretation"
   -- Module indices identify declarations by compiled ownership. A matching
   -- namespace is insufficient: a generated or unrelated module could otherwise
   -- install a theorem under a handwritten proof's expected name.
diff --git a/verification/aeneas/lean/Obligations/SafetyChecks.lean b/verification/aeneas/lean/Obligations/SafetyChecks.lean
new file mode 100644
index 0000000000..13e489adef
--- /dev/null
+++ b/verification/aeneas/lean/Obligations/SafetyChecks.lean
@@ -0,0 +1,32 @@
+/- 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
+@[expose] public section
+open Aeneas Aeneas.Std
+namespace Zerocopy.Obligations
+
+-- The independent expectations describe all inputs, including rejected bytes
+-- and insufficient destinations. They are propositions, not trusted axioms.
+def checked_bool_spec_contract (byte : U8) (run : Result (Option Bool)) : Prop :=
+  run ⦃ out => out = if byte.val < 2 then some (decide (byte.val = 1)) else none ⦄
+
+def checked_bool_spec : Prop :=
+  ∀ byte, checked_bool_spec_contract byte (util.safety_checks.checked_bool byte)
+
+def checked_copy_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 checked_copy_spec : Prop :=
+  ∀ src dst, checked_copy_spec_contract src dst (util.safety_checks.checked_copy src dst)
+
+end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/Proofs/SafetyChecks.lean b/verification/aeneas/lean/Proofs/SafetyChecks.lean
new file mode 100644
index 0000000000..ae2b1edcaa
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/SafetyChecks.lean
@@ -0,0 +1,80 @@
+/- 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 ModelLemmas
+@[expose] public section
+
+/-!
+The callers establish the guards of the trusted conversion and copying helpers.
+These are proofs of composition, not proofs of the opaque Rust helper bodies.
+The result witnesses additionally check that the actual returned representation,
+including the updated mutable slice, decodes successfully.
+-/
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+private theorem decode_bool_option (value : Option Bool) :
+    (inferInstance : RustModel (Option Bool)).decode value = some value := by
+  cases value <;> rfl
+
+private theorem decode_unsigned_list (values : List U8) :
+    decodeList (modelUScalar .U8).decode values = some (values.map unsignedWord) := by
+  induction values with
+  | nil => rfl
+  | cons head tail ih => simp [decodeList, ih]
+
+def byteSlice (raw : Slice U8) : SliceValue (UnsignedWord .U8) :=
+  ⟨raw.val.map unsignedWord, by simpa only [List.length_map] using raw.property⟩
+
+theorem decode_byte_slice (raw : Slice U8) :
+    (modelSlice (α := U8)).decode raw = some (byteSlice raw) := by
+  apply (decodeSlice_iff (modelUScalar .U8) raw (byteSlice raw)).mpr
+  exact decode_unsigned_list raw.val
+
+private theorem decode_copy_result (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 checked_bool_raw (byte : U8) :
+    util.safety_checks.checked_bool byte ⦃ out =>
+      out = if byte.val < 2 then some (decide (byte.val = 1)) else none ⦄ := by
+  by_cases valid : byte.val < 2
+  · simp [util.safety_checks.checked_bool, UScalar.lt_equiv,
+      UScalar.ofNatCore_val_eq, util.transmute_unchecked, valid, bind_ok]
+  · simp [util.safety_checks.checked_bool, UScalar.lt_equiv,
+      UScalar.ofNatCore_val_eq, valid]
+
+theorem checked_bool_spec : Specs.checked_bool_spec := by
+  intro byte _ _
+  apply WP.spec_mono (checked_bool_raw byte)
+  intro result same
+  exact ⟨result, decode_bool_option result, same⟩
+
+theorem checked_copy_raw (src dst : Slice U8) :
+    util.safety_checks.checked_copy 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.safety_checks.checked_copy, Slice.len, UScalar.le_equiv,
+      util.copy_unchecked, fits, bind_ok]
+  · simp [util.safety_checks.checked_copy, Slice.len, UScalar.le_equiv,
+      fits]
+
+theorem checked_copy_spec : Specs.checked_copy_spec := by
+  intro src dst _ _ _ _
+  apply WP.spec_mono (checked_copy_raw src dst)
+  intro result facts
+  exact ⟨(result.1, byteSlice result.2), decode_copy_result result, facts⟩
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/RequiredModelContracts/SafetyChecks.lean b/verification/aeneas/lean/RequiredModelContracts/SafetyChecks.lean
new file mode 100644
index 0000000000..e43962075b
--- /dev/null
+++ b/verification/aeneas/lean/RequiredModelContracts/SafetyChecks.lean
@@ -0,0 +1,37 @@
+/- 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 Specs
+public import Proofs.SafetyChecks
+public import Obligations.SafetyChecks
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+-- These implications quantify over an arbitrary execution. They do not use
+-- the successful behavior of the extracted caller to strengthen its contract.
+@[contract_simps] theorem required_checked_bool (byte : U8)
+    (run : Result (Option Bool))
+    (provided : Specs.checked_bool_spec_contract byte run) :
+    Obligations.checked_bool_spec_contract byte run := by
+  apply WP.spec_mono (provided (unsignedWord byte) rfl)
+  rintro output ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_checked_copy (src dst : Slice U8)
+    (run : Result (Bool × Slice U8))
+    (provided : Specs.checked_copy_spec_contract src dst run) :
+    Obligations.checked_copy_spec_contract src dst run := by
+  apply WP.spec_mono (provided (byteSlice src) (decode_byte_slice src)
+    (byteSlice dst) (decode_byte_slice dst))
+  rintro output ⟨_, _, facts⟩
+  exact facts
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/SafetyTests.lean b/verification/aeneas/lean/SafetyTests.lean
new file mode 100644
index 0000000000..ec86c7c89e
--- /dev/null
+++ b/verification/aeneas/lean/SafetyTests.lean
@@ -0,0 +1,58 @@
+/- 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 SpecsSyntax
+public import Zerocopy.Funs
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace SafetyTests
+
+-- Sequencing cannot convert forbidden execution into either a value or
+-- divergence. In particular, discarding a callee's result is still sequencing.
+theorem forbidden_bind {α β : Type} (next : α → Result β) :
+    (Result.fail .undef >>= next) = Result.fail .undef := bind_fail .undef next
+
+theorem total_rejects_forbidden {α : Type} (post : α → Prop) :
+    ¬ WP.spec (.fail .undef) post := by simp
+
+theorem partial_rejects_forbidden {α : Type} (post : α → Prop) :
+    ¬ WP.dspec (.fail .undef) post := by simp
+
+-- Every oversized copy is forbidden, rather than success with truncated
+-- output or a recoverable None. The caller proves this branch unreachable.
+theorem copy_rejects_oversize (src dst : Slice U8)
+    (oversize : dst.val.length < src.val.length) :
+    util.copy_unchecked src dst = .fail .undef := by
+  simp [util.copy_unchecked, Zerocopy.forbiddenExecution, 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)
+
+theorem bad_bool_forbidden : badBool = .fail .undef := by
+  simp [badBool, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val]
+
+noncomputable def discardCall : Result Unit := do let _ ← badBool; Result.ok ()
+noncomputable def failThenDiverge : Result Unit := do let _ ← badBool; Result.div
+def diverge : Result Unit := .div
+spec discarded for discardCall with 0 type parameters
+  ensures _ => True
+partial spec beforeDivergence for failThenDiverge with 0 type parameters
+  ensures _ => True
+
+example : ¬discarded := by simp [discarded, discardCall, bad_bool_forbidden]
+example : ¬beforeDivergence := by simp [beforeDivergence, failThenDiverge, bad_bool_forbidden]
+
+-- Even a contract that says nothing about the output must prove its execution
+-- judgment. Partial contracts permit divergence, but never preceding UB.
+partial spec diverges for diverge with 0 type parameters
+  ensures _ => True
+example : diverges := WP.dspec.div _
+
+end SafetyTests
diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean
index c820466380..23aed8ce7f 100644
--- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean
+++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean
@@ -19,6 +19,41 @@ def core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone
     (x : core.num.niche_types.NonZeroUsizeInner) :
     Result core.num.niche_types.NonZeroUsizeInner := .ok x
 
+-- A forbidden execution cannot be accepted as an ordinary Rust panic. The
+-- backend's existing undef tag also marks unsupported models, so it means
+-- "no permitted execution claim", not necessarily that the Rust code has UB.
+-- Total and partial contracts both reject it. Future recovery models must
+-- propagate it rather than turn it into a successful return or divergence.
+def Zerocopy.forbiddenExecution {α : Type} : Result α := .fail .undef
+
+-- This is an interpretation of the whole Rust helper, whose raw-pointer body
+-- is deliberately opaque to extraction. Valid input references supply separate
+-- readable source and exclusive destination regions. The additional length
+-- guard belongs to execution: violating it must fail even if the caller ignores
+-- the result. Payload bytes have no padding or invalid bit patterns.
+def util.copy_unchecked (src dst : Slice U8) : Result (Slice U8) :=
+  if h : src.val.length ≤ dst.val.length then
+    .ok (Slice.from (src.val ++ dst.val.drop src.val.length) (by
+      have := dst.property
+      simp only [List.length_append, List.length_drop]
+      omega))
+  else forbiddenExecution
+
+-- 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
+-- represent an invalid boolean. All other instantiations fail closed.
+noncomputable def util.transmute_unchecked {Src : Type} (Dst : Type)
+    (src : Src) : Result Dst := by
+  classical
+  exact if hs : Src = U8 then
+    if hd : Dst = Bool then
+      let byte := cast hs src
+      if byte.val < 2 then .ok (cast hd.symm (decide (byte.val = 1)))
+      else forbiddenExecution
+    else forbiddenExecution
+  else forbiddenExecution
+
 @[simp] def core.num.nonzero.NonZero.get
     {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner)
     (x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val
diff --git a/verification/aeneas/negative-control-extraction.sh b/verification/aeneas/negative-control-extraction.sh
index a8d9f8a4d3..4bac330a67 100644
--- a/verification/aeneas/negative-control-extraction.sh
+++ b/verification/aeneas/negative-control-extraction.sh
@@ -31,5 +31,9 @@ manifest = json.loads(Path(sys.argv[1]).read_text())
 if manifest.get('version') != 3 or manifest.get('mode') != 'verified-live':
     raise SystemExit('Invalid verified bindings for extraction controls')
 functions = {row['raw'] for row in manifest['bindings'].values() if row['kind'] == 'function'}
+print('storage' if 'Zerocopy.util.safety_checks.checked_bool' in functions else '')
 PY
 )
+if [[ $capabilities == *storage* ]]; then
+    run bash verification/aeneas/tests/producer-controls.sh generate "$AENEAS_CONTROL_PRODUCER_DIR"
+fi
diff --git a/verification/aeneas/negative-control-family.sh b/verification/aeneas/negative-control-family.sh
index 56f2eca8de..8db08cddac 100644
--- a/verification/aeneas/negative-control-family.sh
+++ b/verification/aeneas/negative-control-family.sh
@@ -175,6 +175,13 @@ PYCONTROL
 has_model() {
     has_binding function "Zerocopy.$1"
 }
+if [[ $AENEAS_CONTROL_FAMILY == producers ]] && has_model util.safety_checks.checked_bool; then
+    python3 -B "$repo/verification/aeneas/control_runner.py" command \
+        "$AENEAS_CONTROL_LOG_DIR/commands" -- bash \
+        "$repo/verification/aeneas/tests/producer-controls.sh" check \
+        "$PWD" "$AENEAS_CONTROL_PRODUCER_DIR"
+fi
+
 if [[ $AENEAS_CONTROL_FAMILY == trait-rounding ]]; then
 # A constrained mathematical value can still break an operation promise or its
 # required raw input domain. Probe the unchanged constructor source fence in an
@@ -254,6 +261,41 @@ if ! grep -Fq 'unsupported failure erasure' "$backup/unsafe-erasure-audit.log";
 fi
 restore_build
 
+# Each storage interpretation must reject its bad inputs even when safe callers
+# never take that branch. First establish that the mutation still compiles, then
+# require the independent complete-definition audit to reject it.
+if has_model util.safety_checks.checked_bool; then
+    for mutation in boolean copy; do
+        python3 - "$mutation" <<'PYCONTROL'
+from pathlib import Path
+import sys
+p = Path("Zerocopy/FunsExternal.lean")
+s = p.read_text()
+if sys.argv[1] == 'boolean':
+    start = s.index('noncomputable def util.transmute_unchecked')
+    end = s.index('\n\n', start)
+    before = s[start:end]
+    after = before.replace('else forbiddenExecution', 'else .ok (cast hd.symm false)', 1)
+else:
+    start = s.index('def util.copy_unchecked')
+    end = s.index('-- Only the u8-to-bool', start)
+    before = s[start:end]
+    after = before.replace('else forbiddenExecution', 'else .ok dst', 1)
+if before == after:
+    raise SystemExit('Storage boundary control no longer matches')
+p.write_text(s[:start] + after + s[end:])
+PYCONTROL
+        check_model_mutant "permitted bad $mutation input" Zerocopy.FunsExternal
+        expect_failure "permitted bad $mutation input" storage-guard-audit.log audit
+        if ! grep -Eq 'Boolean conversion changed|byte copy changed' "$backup/storage-guard-audit.log"; then
+            cat "$backup/storage-guard-audit.log" >&2; exit 1
+        fi
+        expect_failure "permitted bad $mutation input" storage-guard-proof.log \
+            aeneas_lake env lean -DwarningAsError=true SafetyTests.lean
+        restore_build
+    done
+fi
+
 fi # unsafe
 
 if [[ $AENEAS_CONTROL_FAMILY == coverage ]]; then
diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean
index f21d391a3a..0651aba92d 100644
--- a/verification/aeneas/projections/Specs.lean
+++ b/verification/aeneas/projections/Specs.lean
@@ -50,4 +50,22 @@ spec min_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.min_spec for Zerocopy.util.min with 2
 
+check_model_inputs Zerocopy.util.safety_checks.checked_bool with 0 type parameters
+aeneas_spec_begin
+spec checked_bool_spec
+  for @Zerocopy.util.safety_checks.checked_bool with 0 type parameters
+  ensures(raw) r => r = if byte.val < 2 then some (decide (byte.val = 1)) else none
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.checked_bool_spec for Zerocopy.util.safety_checks.checked_bool with 1
+
+check_model_inputs Zerocopy.util.safety_checks.checked_copy with 0 type parameters
+aeneas_spec_begin
+spec checked_copy_spec
+  for @Zerocopy.util.safety_checks.checked_copy 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.checked_copy_spec for Zerocopy.util.safety_checks.checked_copy with 2
+
 end Zerocopy.Specs
diff --git a/verification/aeneas/tests/producer-controls.sh b/verification/aeneas/tests/producer-controls.sh
new file mode 100755
index 0000000000..c1729890b6
--- /dev/null
+++ b/verification/aeneas/tests/producer-controls.sh
@@ -0,0 +1,106 @@
+#!/usr/bin/env bash
+# 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.
+
+# Compile deliberately invalid producers; never execute their Rust code.
+set -euo pipefail
+case "${1:-}" in
+    generate)
+        [[ $# == 2 ]] || { echo "Usage: $0 generate FIXTURES" >&2; exit 1; }
+        mode=generate
+        mkdir -p "$2"
+        work=$(cd "$2" && pwd)
+        ;;
+    check)
+        [[ $# == 3 && -f "$2/bindings.json" && -d "$3/Controls" ]] || {
+            echo "Usage: $0 check VERIFIED_PROJECT FIXTURES" >&2; exit 1;
+        }
+        mode=check
+        project=$(cd "$2" && pwd)
+        work=$(cd "$3" && pwd)
+        ;;
+    *)
+        # Preserve the original standalone interface and its complete coverage.
+        [[ $# == 1 && -f "$1/bindings.json" ]] || { echo "Usage: $0 VERIFIED_PROJECT" >&2; exit 1; }
+        mode=both
+        project=$(cd "$1" && pwd)
+        work="$project/producer-controls"
+        ;;
+esac
+cd "$(dirname "$0")/../../.."
+repo=$PWD
+source verification/aeneas/toolchain.sh
+tools_dir=${AENEAS_TOOLCHAIN_DIR:-"$repo/target/aeneas/toolchain"}
+fixture="$repo/verification/aeneas/tests/producer-controls"
+if [[ $mode != check ]]; then
+mkdir -p "$work/Controls"
+roots=aeneas_admission_controls::valid,aeneas_admission_controls::ignored,aeneas_admission_controls::before_divergence
+boundary=aeneas_admission_controls::util::transmute_unchecked
+# These are the same reviewed exclusions as the production extraction. The
+# toy crate defines none of those methods, but admission checks the full profile.
+excluded_args=()
+while IFS= read -r method; do
+    [[ -z "$method" ]] || excluded_args+=(--exclude "$method")
+done < <(python3 -B verification/aeneas/admission.py exclude)
+(
+    cd "$fixture"
+    CHARON_ADMISSION_SNAPSHOT="$work/controls.before.ullbc" \
+    CARGO_TARGET_DIR="$work/rust" \
+        "$tools_dir/charon" cargo --preset=aeneas --sysroot default \
+        --mir promoted --no-dedup-serialized-ast --opaque "$boundary" \
+        "${excluded_args[@]}" \
+        --start-from "$roots" --dest-file "$work/controls.llbc" \
+        --abort-on-error --error-on-warnings -- --lib --locked --offline
+)
+# Exercise the same admission traversal, with the fixture's exact callable
+# identity. This does not mint a production binding manifest or certify the
+# toy helper body: its opaque interpretation is deliberately a test premise.
+python3 - "$repo" "$work" "$roots" "$boundary" <<'PY'
+import json, sys
+from pathlib import Path
+repo, work = map(Path, sys.argv[1:3])
+sys.path.insert(0, str(repo / 'verification/aeneas'))
+import admission
+registry = json.loads((repo / 'verification/aeneas/external.json').read_text())
+entry = next(row.copy() for row in registry if row['rust'] == 'zerocopy::util::transmute_unchecked')
+entry['rust'] = sys.argv[4]
+for filename, before in [('controls.before.ullbc', True), ('controls.llbc', False)]:
+    checker = admission.Admission(json.loads((work / filename).read_text()), [entry])
+    if checker.before != before:
+        raise SystemExit('Producer control has the wrong inspection stage')
+    checker.audit(sys.argv[3].split(','))
+PY
+"$tools_dir/aeneas" -backend lean -namespace Controls \
+    -dest "$work/Controls" -split-files -abort-on-error \
+    -warnings-as-errors -no-progress-bar -use-tuple-structs false "$work/controls.llbc"
+cat > "$work/Controls/TypesExternal.lean" <<'LEAN'
+module
+public import Aeneas
+LEAN
+cat > "$work/Controls/FunsExternal.lean" <<'LEAN'
+module
+public import Controls.Types
+public import Zerocopy.FunsExternal
+LEAN
+fi
+if [[ $mode != generate ]]; then
+mkdir -p "$project/.lake/build/lib/lean/Controls"
+(
+    cd "$project"
+    # Compile every fixture module freshly. A cached caller from another model
+    # cannot make a missing or erased unsafe call look forbidden.
+    for name in TypesExternal Types FunsExternal Funs; do
+        aeneas_lake env lean --root="$work" -DwarningAsError=true \
+            "$work/Controls/$name.lean" \
+            -o "$project/.lake/build/lib/lean/Controls/$name.olean"
+    done
+    aeneas_lake env lean -DwarningAsError=true "$fixture/Check.lean"
+)
+echo 'Confirmed: generated callers retain forbidden production before discard and divergence'
+
+fi
diff --git a/verification/aeneas/tests/producer-controls/Cargo.lock b/verification/aeneas/tests/producer-controls/Cargo.lock
new file mode 100644
index 0000000000..3b37b58e9c
--- /dev/null
+++ b/verification/aeneas/tests/producer-controls/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 4
+
+[[package]]
+name = "aeneas_admission_controls"
+version = "0.0.0"
diff --git a/verification/aeneas/tests/producer-controls/Cargo.toml b/verification/aeneas/tests/producer-controls/Cargo.toml
new file mode 100644
index 0000000000..2d2a38298e
--- /dev/null
+++ b/verification/aeneas/tests/producer-controls/Cargo.toml
@@ -0,0 +1,7 @@
+[package]
+name = "aeneas_admission_controls"
+version = "0.0.0"
+edition = "2021"
+publish = false
+
+[workspace]
diff --git a/verification/aeneas/tests/producer-controls/Check.lean b/verification/aeneas/tests/producer-controls/Check.lean
new file mode 100644
index 0000000000..3e8a1fd7bc
--- /dev/null
+++ b/verification/aeneas/tests/producer-controls/Check.lean
@@ -0,0 +1,29 @@
+/- 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. -/
+
+import Controls.Funs
+open Aeneas Aeneas.Std Controls
+
+-- Start with a successful generated call: a missing module, wrong namespace,
+-- or broken interpretation cannot count as rejecting an invalid execution.
+example : valid (1#u8) ⦃ out => out = some true ⦄ := by
+  simp [valid, util.transmute_unchecked, UScalar.val]
+
+-- These are real Aeneas-generated callers, not handwritten monadic witnesses.
+-- The invalid call must survive filtering even when its result is unused.
+example : ignored = Result.fail .undef := by
+  simp [ignored, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val]
+
+example : before_divergence false = Result.fail .undef := by
+  simp [before_divergence, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val]
+
+example : ¬ WP.spec ignored (fun _ => True) := by
+  simp [ignored, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val]
+
+example : ¬ WP.dspec (before_divergence false) (fun _ => True) := by
+  simp [before_divergence, util.transmute_unchecked, Zerocopy.forbiddenExecution, UScalar.val]
diff --git a/verification/aeneas/tests/producer-controls/src/lib.rs b/verification/aeneas/tests/producer-controls/src/lib.rs
new file mode 100644
index 0000000000..2206dc748c
--- /dev/null
+++ b/verification/aeneas/tests/producer-controls/src/lib.rs
@@ -0,0 +1,60 @@
+// 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.
+
+//! Extraction controls, never executed as Rust.
+//!
+//! The invalid producers intentionally violate Boolean bit validity. We prove
+//! that their extracted executions are forbidden, rather than running Rust UB.
+//! The helper is opaque, with the same u8-to-bool interpretation as production.
+//! This fixture tests translation of calls, not certification of its union body.
+#![allow(dead_code)]
+
+pub mod util {
+    use core::mem::ManuallyDrop;
+
+    /// The caller must supply a bit-valid representation of `Dst` with equal
+    /// size. Only `u8` to `bool` is selected in these extraction controls.
+    pub const unsafe fn transmute_unchecked<Src, Dst>(src: Src) -> Dst {
+        union Bits<Src, Dst> {
+            src: ManuallyDrop<Src>,
+            dst: ManuallyDrop<Dst>,
+        }
+        // SAFETY: This requires the documented caller obligations. The bad
+        // fixtures below deliberately violate them and must never be executed.
+        ManuallyDrop::into_inner(unsafe { Bits { src: ManuallyDrop::new(src) }.dst })
+    }
+}
+
+pub fn valid(byte: u8) -> Option<bool> {
+    if byte < 2 {
+        // SAFETY: Both one-byte types have equal size; 0 and 1 are valid bools.
+        Some(unsafe { util::transmute_unchecked(byte) })
+    } else {
+        None
+    }
+}
+
+/// No call to this extraction fixture is permitted.
+pub unsafe fn ignored() {
+    // Deliberate UB for a negative control. Do not execute this Rust function.
+    let _ = unsafe { util::transmute_unchecked::<u8, bool>(2u8) };
+}
+
+/// No call to this extraction fixture is permitted, including when its caller
+/// would accept divergence. UB happens before the loop begins.
+pub unsafe fn before_divergence(escape: bool) {
+    // Deliberate UB for a negative control. Do not execute this Rust function.
+    let _ = unsafe { util::transmute_unchecked::<u8, bool>(2u8) };
+    // Keep a syntactic exit: the pinned extractor rejects loops with no break.
+    // The Lean control chooses false, so an accepted execution could not exit.
+    loop {
+        if escape {
+            break;
+        }
+    }
+}
diff --git a/verification/aeneas/tests/test_control_runner.py b/verification/aeneas/tests/test_control_runner.py
index 13e9b360ea..b1b8e92be8 100644
--- a/verification/aeneas/tests/test_control_runner.py
+++ b/verification/aeneas/tests/test_control_runner.py
@@ -268,6 +268,54 @@ def test_suite_interruption_during_baseline_stops_descendants_and_keeps_roster(s
                     process.kill()
                     process.wait()
 
+    def test_shared_producer_fixtures_are_recompiled_against_each_model(self):
+        lake = shutil.which('lake')
+        if lake is None:
+            self.skipTest('Requires the pinned Lean installation')
+        with tempfile.TemporaryDirectory() as temporary:
+            root = Path(temporary)
+            scripts = root / 'verification/aeneas/tests'
+            scripts.mkdir(parents=True)
+            shutil.copyfile(AENEAS / 'tests/producer-controls.sh', scripts / 'producer-controls.sh')
+            (scripts / 'producer-controls').mkdir()
+            (scripts / 'producer-controls/Check.lean').write_text(
+                'import Controls.Funs\nexample : translated = 0 := rfl\n')
+            (root / 'verification/aeneas/toolchain.sh').write_text(
+                'AENEAS_TOOLCHAIN_DIR=/unused-for-replay\naeneas_lake() ( unset CI; command lake --old "$@"; )\n')
+            shared = root / 'shared'
+            (shared / 'Controls').mkdir(parents=True)
+            for name, text in {
+                'TypesExternal': 'module\n',
+                'Types': 'module\npublic import Controls.TypesExternal\n',
+                'FunsExternal': 'module\npublic import Controls.Types\npublic import Zerocopy.FunsExternal\n',
+                'Funs': 'module\npublic import Controls.FunsExternal\n@[expose] public section\ndef translated : Nat := modelValue\n',
+            }.items():
+                (shared / 'Controls' / (name + '.lean')).write_text(text)
+            original = {p.name: p.read_bytes() for p in (shared / 'Controls').iterdir()}
+            env = dict(os.environ)
+            env.pop('CI', None)
+            for model, value in [('golden', 0), ('live', 0), ('changed-live', 1)]:
+                project = root / model
+                (project / 'Zerocopy').mkdir(parents=True)
+                (project / 'lean-toolchain').write_bytes((AENEAS.parents[1] / 'anneal/lean/lean-toolchain').read_bytes())
+                (project / 'bindings.json').write_text('{}')
+                (project / 'lakefile.lean').write_text(
+                    'import Lake\nopen Lake DSL\npackage producerReplay\nlean_lib Zerocopy\n')
+                (project / 'Zerocopy/FunsExternal.lean').write_text(f'module\n@[expose] public section\ndef modelValue : Nat := {value}\n')
+                built = subprocess.run([lake, '--old', 'build', '+Zerocopy.FunsExternal'],
+                                       cwd=project, env=env, capture_output=True)
+                self.assertEqual(built.returncode, 0, built.stdout + built.stderr)
+                replay = subprocess.run(['bash', str(scripts / 'producer-controls.sh'),
+                    'check', str(project), str(shared)], env=env, capture_output=True)
+                if value == 0:
+                    self.assertEqual(replay.returncode, 0, replay.stdout + replay.stderr)
+                    for module in ('TypesExternal', 'Types', 'FunsExternal', 'Funs'):
+                        self.assertTrue((project / '.lake/build/lib/lean/Controls' / (module + '.olean')).exists())
+                else:
+                    self.assertNotEqual(replay.returncode, 0)
+                    self.assertIn(b'Check.lean', replay.stdout + replay.stderr)
+            self.assertEqual({p.name: p.read_bytes() for p in (shared / 'Controls').iterdir()}, original)
+
     def test_ci_preflight_accepts_native_trait_laws_and_rejects_projection_edits(self):
         sys.path.insert(0, str(AENEAS))
         with tempfile.TemporaryDirectory() as temporary:
diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py
index 927b1ef31e..8390f37afd 100644
--- a/verification/aeneas/tests/test_inline.py
+++ b/verification/aeneas/tests/test_inline.py
@@ -194,6 +194,15 @@ def test_inherent_and_generic_ownership_automatically_introduces_rust_names(self
         with self.assertRaises(ValueError):
             self.parse('impl S { ' + BLOCK + 'fn f(&mut self, x: usize) {} }')
 
+    def test_only_explicit_mutable_byte_slice_inputs_are_supported(self):
+        found = self.parse(BLOCK + 'fn f(x: &mut [u8]) {}')[0]
+        self.assertEqual(found['inputs'], ['x'])
+        for signature in ('fn f(x: &mut [u16]) {}', 'fn f(x: &mut bool) {}',
+                          'fn f(x: Option<&mut [u8]>) {}',
+                          'fn f(x: &mut [u8]) -> &mut [u8] { x }'):
+            with self.subTest(signature=signature), self.assertRaises(ValueError):
+                self.parse(BLOCK + signature)
+
     def test_ghosts_and_requirements_cannot_shadow_original_parameters(self):
         for header in ('(x : Nat)', '(T : Type)', '(ghost ghost : Nat)'):
             block = BLOCK.replace('spec f_spec', 'spec f_spec ' + header)
diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs
index a09045dccd..8235c0f3d1 100644
--- a/zerocopy/src/util/mod.rs
+++ b/zerocopy/src/util/mod.rs
@@ -14,6 +14,8 @@ pub(crate) mod macros;
 #[doc(hidden)]
 pub mod macro_util;
 
+mod safety_checks;
+
 use core::{
     marker::PhantomData,
     mem::{self, ManuallyDrop},
diff --git a/zerocopy/src/util/safety_checks/mod.rs b/zerocopy/src/util/safety_checks/mod.rs
new file mode 100644
index 0000000000..29bde56082
--- /dev/null
+++ b/zerocopy/src/util/safety_checks/mod.rs
@@ -0,0 +1,96 @@
+// 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.
+
+//! Small callers of the trusted storage boundaries.
+//!
+//! The proofs check the callers' guards and results. The interpretations of
+//! `transmute_unchecked::<u8, bool>` and `copy_unchecked` remain explicit trusted
+//! premises; these harnesses do not prove the union or raw-pointer operations
+//! inside those helpers. Both boundaries reject forbidden execution before
+//! producing a typed value, even when that value is subsequently discarded.
+
+#![allow(dead_code)]
+
+/// Converts precisely the two valid boolean encodings.
+///
+/// ```aeneas
+/// spec checked_bool_spec
+///   ensures(raw) r => r = if byte.val < 2 then some (decide (byte.val = 1)) else none
+/// ```
+fn checked_bool(byte: u8) -> Option<bool> {
+    if byte < 2 {
+        // SAFETY: The branch restricts `byte` to 0 or 1, the two boolean bit
+        // patterns. Both types have size one, satisfying the helper's size
+        // assertion. The trusted interpretation checks this same condition
+        // before producing a bool; it cannot silently accept another byte.
+        Some(unsafe { super::transmute_unchecked(byte) })
+    } else {
+        None
+    }
+}
+
+/// Copies a fitting prefix; failure leaves the destination unchanged.
+///
+/// The returned state in the extracted model includes the updated destination.
+/// Its suffix must be preserved, including when the source is empty.
+///
+/// ```aeneas
+/// spec checked_copy_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
+/// ```
+fn checked_copy(src: &[u8], dst: &mut [u8]) -> bool {
+    if src.len() <= dst.len() {
+        // SAFETY: This branch establishes the helper's sole additional
+        // requirement, `src.len() <= dst.len()`. The valid input references
+        // supply initialized source bytes and an exclusive destination.
+        unsafe { super::copy_unchecked(src, dst) };
+        true
+    } else {
+        false
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn all_boolean_bytes() {
+        for byte in 0..=u8::MAX {
+            assert_eq!(
+                checked_bool(byte),
+                match byte {
+                    0 => Some(false),
+                    1 => Some(true),
+                    _ => None,
+                }
+            );
+        }
+    }
+
+    #[test]
+    fn copy_boundaries() {
+        for len in 0..=4 {
+            let mut dst = [9; 3];
+            let src = &[1, 2, 3, 4][..len];
+            let fits = checked_copy(src, &mut dst);
+            assert_eq!(fits, len <= dst.len());
+            if fits {
+                assert_eq!(&dst[..len], src);
+                assert!(dst[len..].iter().all(|byte| *byte == 9));
+            } else {
+                assert_eq!(dst, [9; 3]);
+            }
+        }
+    }
+}