diff --git a/verification/aeneas/ADMISSION_DESIGN.md b/verification/aeneas/ADMISSION_DESIGN.md
index 16a1ff1a1b..22755945b3 100644
--- a/verification/aeneas/ADMISSION_DESIGN.md
+++ b/verification/aeneas/ADMISSION_DESIGN.md
@@ -65,6 +65,18 @@ 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.
 
+`util::validity::read_byte` reads one initialized byte with a bounds check. It
+returns `.fail .panic` out of bounds; it never constructs the type whose bit
+validity is being tested. Its exact source body and complete model are checked.
+This narrow boundary avoids importing the generic indexing dictionary's unused
+pointer operations. It supplies no premise about arbitrary raw-pointer reads,
+uninitialized storage, or padding. Boolean and nonzero-word predicates are
+extracted from the helpers used by the production `TryFromBytes` implementations.
+The checked scalar/pair conversions and slice validator retain all raw integer
+and byte inputs, including rejected encodings. Native regression tests compare
+them with the public conversions; the generic `Maybe` pointer path still relies
+on its existing Rust safety arguments.
+
 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 8f79f04bda..4b04e20b84 100644
--- a/verification/aeneas/external.json
+++ b/verification/aeneas/external.json
@@ -24,6 +24,7 @@
   {"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": "zerocopy::util::validity::read_byte", "signature": {"unsafe": false, "inputs": ["&[u8]", "usize"], "output": "u8", "types": 0, "consts": 0}, "lean": "util.validity.read_byte", "opaque": true, "source_body_sha256": "35941f898b8ec4684e6f36fefab11d0804ad0c9baa4f151becfaa20ad862976b"},
   {"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 a8d818d0c1..c6237d79f3 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -2073,7 +2073,7 @@ def core.cell.UnsafeCell.Insts.ZerocopyIntoBytes {T : Type} (IntoBytesInst :
 }
 
 /-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 167:0-227:1 -/
+    Source: 'src/util/mod.rs', lines 168:0-228:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -2089,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 254:0-272:1 -/
+    Source: 'src/util/mod.rs', lines 255:0-273:1 -/
 def util.round_down_to_next_multiple_of_alignment
   (n : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -2106,7 +2106,7 @@ def util.round_down_to_next_multiple_of_alignment
   ok (n &&& mask)
 
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 281:0-287:1 -/
+    Source: 'src/util/mod.rs', lines 282:0-288:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -2126,7 +2126,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 296:0-302:1 -/
+    Source: 'src/util/mod.rs', lines 297:0-303:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -2180,13 +2180,19 @@ def util.owned_transmute.round_trip_checks
   let restored ← util.owned_transmute.from_bytes bytes
   massert (restored = value)
 
+/-- [zerocopy::util::validity::bool_encoding]:
+    Source: 'src/util/validity/mod.rs', lines 26:0-28:1 -/
+def util.validity.bool_encoding (byte : Std.U8) : Result Bool := do
+  ok (byte < 2#u8)
+
 /-- [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)
+  let b ← util.validity.bool_encoding byte
+  if b
+  then let b1 ← util.transmute_unchecked Bool byte
+       ok (some b1)
   else ok none
 
 /-- [zerocopy::util::safety_checks::checked_copy]:
@@ -2202,4 +2208,74 @@ def util.safety_checks.checked_copy
        ok (true, dst1)
   else ok (false, dst)
 
+/-- [zerocopy::util::validity::nonzero_encoding]:
+    Source: 'src/util/validity/mod.rs', lines 37:0-39:1 -/
+def util.validity.nonzero_encoding (n : Std.Usize) : Result Bool := do
+  ok (n != 0#usize)
+
+/-- [zerocopy::util::safety_checks::checked_nonzero]:
+    Source: 'src/util/safety_checks/mod.rs', lines 72:0-78:1 -/
+def util.safety_checks.checked_nonzero
+  (n : Std.Usize) :
+  Result (Option (core.num.nonzero.NonZero Std.Usize
+    core.num.niche_types.NonZeroUsizeInner))
+  := do
+  let b ← util.validity.nonzero_encoding n
+  if b
+  then
+    core.num.nonzero.NonZero.new
+      Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner n
+  else ok none
+
+/-- [zerocopy::util::safety_checks::checked_bool_pair]:
+    Source: 'src/util/safety_checks/mod.rs', lines 91:0-97:1 -/
+def util.safety_checks.checked_bool_pair
+  (bytes : Array Std.U8 2#usize) : Result (Option (Array Bool 2#usize)) := do
+  let s ← lift (Array.to_slice bytes)
+  let left ← util.validity.read_byte s 0#usize
+  let s1 ← lift (Array.to_slice bytes)
+  let right ← util.validity.read_byte s1 1#usize
+  let o ← util.safety_checks.checked_bool left
+  match o with
+  | none => ok none
+  | some left1 =>
+    let o1 ← util.safety_checks.checked_bool right
+    match o1 with
+    | none => ok none
+    | some right1 => ok (some (Array.make 2#usize [ left1, right1 ]))
+
+/-- [zerocopy::util::safety_checks::bool_slice_valid]: loop body 0:
+    Source: 'src/util/safety_checks/mod.rs', lines 108:4-115:1 -/
+@[rust_loop_body]
+def util.safety_checks.bool_slice_valid_loop.body
+  (bytes : Slice Std.U8) (i : Std.Usize) :
+  Result (ControlFlow Std.Usize Bool)
+  := do
+  let i1 := Slice.len bytes
+  if i < i1
+  then
+    let i2 ← util.validity.read_byte bytes i
+    let b ← util.validity.bool_encoding i2
+    if b
+    then let i3 ← i + 1#usize
+         ok (cont i3)
+    else ok (done false)
+  else ok (done true)
+
+/-- [zerocopy::util::safety_checks::bool_slice_valid]: loop 0:
+    Source: 'src/util/safety_checks/mod.rs', lines 108:4-115:1 -/
+@[rust_loop]
+def util.safety_checks.bool_slice_valid_loop
+  (bytes : Slice Std.U8) (i : Std.Usize) : Result Bool := do
+  loop
+    (fun i1 => util.safety_checks.bool_slice_valid_loop.body bytes i1)
+    i
+
+/-- [zerocopy::util::safety_checks::bool_slice_valid]:
+    Source: 'src/util/safety_checks/mod.rs', lines 106:0-115:1 -/
+@[reducible]
+def util.safety_checks.bool_slice_valid
+  (bytes : Slice Std.U8) : Result Bool := do
+  util.safety_checks.bool_slice_valid_loop bytes 0#usize
+
 end Zerocopy
diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean
index ce24b5be06..5b4246f474 100644
--- a/verification/aeneas/golden/FunsExternal_Template.lean
+++ b/verification/aeneas/golden/FunsExternal_Template.lean
@@ -52,6 +52,17 @@ axiom core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone
   core.num.niche_types.NonZeroUsizeInner → Result
     core.num.niche_types.NonZeroUsizeInner
 
+/-- [core::num::nonzero::{core::num::nonzero::NonZero<T, Clause0_NonZeroInner>}::new]:
+    Source: '/rustc/library/core/src/num/nonzero.rs', lines 388:4-388:42
+    Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new]
+    Visibility: public -/
+@[rust_fun
+  "core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::new"]
+axiom core.num.nonzero.NonZero.new
+  {T : Type} {Clause0_NonZeroInner : Type} (ZeroablePrimitiveInst :
+  core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) :
+  T → Result (Option (core.num.nonzero.NonZero T Clause0_NonZeroInner))
+
 /-- [core::num::nonzero::{core::num::nonzero::NonZero<T, Clause0_NonZeroInner>}::get]:
     Source: '/rustc/library/core/src/num/nonzero.rs', lines 467:4-467:31
     Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::get]
@@ -64,12 +75,12 @@ axiom core.num.nonzero.NonZero.get
   core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T
 
 /-- [zerocopy::util::copy_unchecked]:
-    Source: 'src/util/mod.rs', lines 314:0-329:1 -/
+    Source: 'src/util/mod.rs', lines 315:0-330: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 -/
+    Source: 'src/util/mod.rs', lines 344:0-355:1 -/
 axiom util.copy_unchecked_at
   : Slice Std.U8 → Slice Std.U8 → Std.Usize → Result (Slice Std.U8)
 
@@ -130,6 +141,10 @@ axiom Array.Insts.ZerocopyTryFromBytes.is_safe
     Bool
 
 /-- [zerocopy::util::transmute_unchecked]:
-    Source: 'src/util/mod.rs', lines 366:0-395:1 -/
+    Source: 'src/util/mod.rs', lines 367:0-396:1 -/
 axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst
 
+/-- [zerocopy::util::validity::read_byte]:
+    Source: 'src/util/validity/mod.rs', lines 49:0-51:1 -/
+axiom util.validity.read_byte : Slice Std.U8 → Std.Usize → Result Std.U8
+
diff --git a/verification/aeneas/lean/Obligations/Validity.lean b/verification/aeneas/lean/Obligations/Validity.lean
new file mode 100644
index 0000000000..2a779c984a
--- /dev/null
+++ b/verification/aeneas/lean/Obligations/Validity.lean
@@ -0,0 +1,50 @@
+/- 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
+
+-- These expectations retain all raw candidate values. A decoder rejecting bad
+-- candidates at the INPUT would conceal precisely the cases being validated.
+def bool_encoding_spec_contract (byte : U8) (run : Result Bool) : Prop :=
+  run ⦃ out => out = decide (byte.val = 0 ∨ byte.val = 1) ⦄
+def bool_encoding_spec : Prop :=
+  ∀ byte, bool_encoding_spec_contract byte (util.validity.bool_encoding byte)
+
+def nonzero_encoding_spec_contract (n : Usize) (run : Result Bool) : Prop :=
+  run ⦃ out => out = decide (n.val ≠ 0) ⦄
+def nonzero_encoding_spec : Prop :=
+  ∀ n, nonzero_encoding_spec_contract n (util.validity.nonzero_encoding n)
+
+def checked_nonzero_spec_contract (n : Usize)
+    (run : Result (Option (core.num.nonzero.NonZero Usize
+      core.num.niche_types.NonZeroUsizeInner))) : Prop :=
+  run ⦃ out => match out with
+    | none => n.val = 0
+    | some value => value.val = n ∧ 0 < value.val.val ⦄
+def checked_nonzero_spec : Prop :=
+  ∀ n, checked_nonzero_spec_contract n (util.safety_checks.checked_nonzero n)
+
+def checked_bool_pair_spec_contract (bytes : Aeneas.Std.Array U8 2#usize)
+    (run : Result (Option (Aeneas.Std.Array Bool 2#usize))) : Prop :=
+  run ⦃ out => match out with
+    | none => ∃ byte ∈ bytes.val, 2 ≤ byte.val
+    | some values => values.val = bytes.val.map (fun byte => decide (byte.val = 1)) ∧
+        ∀ byte ∈ bytes.val, byte.val < 2 ⦄
+def checked_bool_pair_spec : Prop :=
+  ∀ bytes, checked_bool_pair_spec_contract bytes (util.safety_checks.checked_bool_pair bytes)
+
+def bool_slice_valid_spec_contract (bytes : Slice U8) (run : Result Bool) : Prop :=
+  run ⦃ out => out = decide (∀ byte ∈ bytes.val, byte.val < 2) ⦄
+def bool_slice_valid_spec : Prop :=
+  ∀ bytes, bool_slice_valid_spec_contract bytes (util.safety_checks.bool_slice_valid bytes)
+
+end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/Proofs/SafetyChecks.lean b/verification/aeneas/lean/Proofs/SafetyChecks.lean
index ae2b1edcaa..5ca62b7a0e 100644
--- a/verification/aeneas/lean/Proofs/SafetyChecks.lean
+++ b/verification/aeneas/lean/Proofs/SafetyChecks.lean
@@ -49,9 +49,9 @@ 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,
+  · simp [util.safety_checks.checked_bool, util.validity.bool_encoding, UScalar.lt_equiv,
       UScalar.ofNatCore_val_eq, util.transmute_unchecked, valid, bind_ok]
-  · simp [util.safety_checks.checked_bool, UScalar.lt_equiv,
+  · simp [util.safety_checks.checked_bool, util.validity.bool_encoding, UScalar.lt_equiv,
       UScalar.ofNatCore_val_eq, valid]
 
 theorem checked_bool_spec : Specs.checked_bool_spec := by
diff --git a/verification/aeneas/lean/Proofs/Validity.lean b/verification/aeneas/lean/Proofs/Validity.lean
new file mode 100644
index 0000000000..61abee7e12
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/Validity.lean
@@ -0,0 +1,168 @@
+/- 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 BytesAdapter
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+-- These are the predicates called by the production scalar validators. The
+-- raw candidates include every u8/usize value, not just valid encodings.
+theorem bool_encoding_raw (byte : U8) :
+    util.validity.bool_encoding byte ⦃ out =>
+      out = decide (byte.val = 0 ∨ byte.val = 1) ⦄ := by
+  simp only [util.validity.bool_encoding, WP.spec_ok]
+  apply Bool.eq_iff_iff.mpr
+  simp only [UScalar.lt_equiv, UScalar.ofNatCore_val_eq, decide_eq_true_eq]
+  omega
+
+theorem nonzero_encoding_raw (n : Usize) :
+    util.validity.nonzero_encoding n ⦃ out => out = decide (n.val ≠ 0) ⦄ := by
+  simp only [util.validity.nonzero_encoding, WP.spec_ok]
+  apply Bool.eq_iff_iff.mpr
+  simp [bne_iff_ne, UScalar.eq_equiv]
+
+theorem bool_encoding_spec : Specs.bool_encoding_spec := by
+  intro byte _ _
+  apply WP.spec_mono (bool_encoding_raw byte)
+  intro out facts
+  exact ⟨out, rfl, facts⟩
+
+theorem nonzero_encoding_spec : Specs.nonzero_encoding_spec := by
+  intro n _ _
+  apply WP.spec_mono (nonzero_encoding_raw n)
+  intro out facts
+  exact ⟨out, rfl, facts⟩
+
+-- Successful construction must return the original word, with a nonzero raw
+-- representation. The decoder therefore cannot hide an invalid zero result.
+theorem checked_nonzero_raw (n : Usize) :
+    util.safety_checks.checked_nonzero n ⦃ out => match out with
+      | none => n.val = 0
+      | some value => value.val = n ∧ 0 < value.val.val ⦄ := by
+  by_cases zero : n.val = 0
+  · simp [util.safety_checks.checked_nonzero, util.validity.nonzero_encoding,
+      UScalar.eq_equiv, zero, bind_ok]
+  · have positive : 0 < n.val := by omega
+    simp [util.safety_checks.checked_nonzero, util.validity.nonzero_encoding,
+      core.num.nonzero.NonZero.new, bne_iff_ne, UScalar.eq_equiv, zero,
+      positive, bind_ok]
+
+theorem checked_nonzero_spec : Specs.checked_nonzero_spec := by
+  intro n _ _
+  apply WP.spec_mono (checked_nonzero_raw n)
+  intro out facts
+  cases out with
+  | none => exact ⟨none, rfl, facts⟩
+  | some value =>
+    refine ⟨some ⟨unsignedWord value.val, facts.2⟩, ?_, facts⟩
+    simp only [RustModel.decode, facts.2, ↓reduceDIte, Option.map_some]
+
+-- The fixed array bridge reads bytes before their Boolean validity is known.
+-- Both reads have statically proved bounds; construction uses the checked
+-- scalar conversion, so no invalid Bool can disappear through the carrier.
+theorem checked_bool_pair_raw (bytes : Aeneas.Std.Array U8 2#usize) :
+    util.safety_checks.checked_bool_pair bytes ⦃ out => match out with
+      | none => ∃ byte ∈ bytes.val, 2 ≤ byte.val
+      | some values => values.val = bytes.val.map (fun byte => decide (byte.val = 1)) ∧
+          ∀ byte ∈ bytes.val, byte.val < 2 ⦄ := by
+  obtain ⟨left, right, same⟩ := List.length_eq_two.mp
+    (show bytes.val.length = 2 by simp)
+  by_cases hl : left.val ≤ 1 <;> by_cases hr : right.val ≤ 1 <;>
+    simp [util.safety_checks.checked_bool_pair, Array.to_slice,
+      util.validity.read_byte, util.safety_checks.checked_bool,
+      util.validity.bool_encoding, util.transmute_unchecked,
+      UScalar.lt_equiv, UScalar.ofNatCore_val_eq, lift, bind_ok, same, hl, hr] <;> omega
+
+private theorem decode_bool_list (values : List Bool) :
+    decodeList (modelBool).decode values = some values := by
+  change decodeList some values = some values
+  induction values with
+  | nil => rfl
+  | cons head tail ih => simp [decodeList, ih]
+
+private def boolArray (raw : Aeneas.Std.Array Bool 2#usize) : ArrayValue Bool 2#usize :=
+  ⟨raw.val, raw.property⟩
+
+private theorem decode_bool_array (raw : Aeneas.Std.Array Bool 2#usize) :
+    (modelArray 2#usize).decode raw = some (boolArray raw) := by
+  apply (decodeArray_iff modelBool 2#usize raw (boolArray raw)).mpr
+  exact decode_bool_list raw.val
+
+theorem checked_bool_pair_spec : Specs.checked_bool_pair_spec := by
+  intro bytes _ _
+  apply WP.spec_mono (checked_bool_pair_raw bytes)
+  intro out facts
+  cases out with
+  | none => exact ⟨none, rfl, facts⟩
+  | some values =>
+    exact ⟨some (boolArray values), by
+      change Option.map some ((modelArray 2#usize).decode values) =
+        some (some (boolArray values))
+      rw [decode_bool_array values]
+      rfl, facts⟩
+
+-- Unlike the layout adapter, this loop may finish early with false. Use the
+-- upstream decreasing-natural rule directly, retaining the checked prefix.
+theorem bool_slice_loop_raw (bytes : Slice U8) (i : Usize)
+    (bound : i.val ≤ bytes.val.length)
+    (checked : ∀ j, j < i.val → (bytes.val[j]!).val < 2) :
+    util.safety_checks.bool_slice_valid_loop bytes i ⦃ out =>
+      out = decide (∀ byte ∈ bytes.val, byte.val < 2) ⦄ := by
+  unfold util.safety_checks.bool_slice_valid_loop
+  apply loop.spec_decr_nat
+    (fun i : Usize => bytes.val.length - i.val)
+    (fun i => i.val ≤ bytes.val.length ∧ ∀ j, j < i.val → (bytes.val[j]!).val < 2)
+  · intro idx ⟨bound, checked⟩
+    unfold util.safety_checks.bool_slice_valid_loop.body
+    simp only [UScalar.lt_equiv, Slice.len_val, Slice.length]
+    split
+    · rename_i inside
+      simp only [util.validity.read_byte, inside, ↓reduceIte, bind_ok,
+        util.validity.bool_encoding, UScalar.lt_equiv, UScalar.ofNatCore_val_eq, decide_eq_true_eq]
+      split
+      · rename_i valid
+        step with Usize.add_spec (x := idx) (y := 1#usize) (by
+          have := bytes.property
+          simp only [UScalar.ofNatCore_val_eq]
+          omega) as ⟨next, advanced⟩
+        refine ⟨by omega, ?_, by omega⟩
+        intro j before
+        by_cases earlier : j < idx.val
+        · exact checked j earlier
+        · have same : j = idx.val := by omega
+          simpa only [same] using valid
+      · rename_i invalid
+        have rejected : ¬ (∀ byte ∈ bytes.val, byte.val < 2) := by
+          intro all
+          have member : bytes.val[idx.val]! ∈ bytes.val := by
+            simpa only [getElem!_pos bytes.val idx.val inside] using List.getElem_mem inside
+          exact invalid (all _ member)
+        simp only [WP.spec_ok]
+        exact (decide_eq_false rejected).symm
+    · rename_i finished
+      have at_end : idx.val = bytes.val.length := by omega
+      have all : ∀ byte ∈ bytes.val, byte.val < 2 := by
+        intro byte member
+        obtain ⟨j, hj, same⟩ := List.getElem_of_mem member
+        have good := checked j (by omega)
+        simpa only [getElem!_pos bytes.val j hj, same] using good
+      simp only [WP.spec_ok]
+      exact (decide_eq_true all).symm
+  · exact ⟨bound, checked⟩
+
+theorem bool_slice_valid_spec : Specs.bool_slice_valid_spec := by
+  intro bytes _ _
+  apply WP.spec_mono (bool_slice_loop_raw bytes 0#usize (by simp) (by simp))
+  intro out facts
+  exact ⟨out, rfl, facts⟩
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/RequiredModelContracts/Validity.lean b/verification/aeneas/lean/RequiredModelContracts/Validity.lean
new file mode 100644
index 0000000000..94da37a22f
--- /dev/null
+++ b/verification/aeneas/lean/RequiredModelContracts/Validity.lean
@@ -0,0 +1,57 @@
+/- 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.Validity
+public import Obligations.Validity
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+-- Supply an independent admission witness for EVERY raw input. The subsequent
+-- implications consume only the authored postcondition, for any execution.
+@[contract_simps] theorem required_bool_encoding (byte : U8) (run : Result Bool)
+    (provided : Specs.bool_encoding_spec_contract byte run) :
+    Obligations.bool_encoding_spec_contract byte run := by
+  apply WP.spec_mono (provided (unsignedWord byte) rfl)
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_nonzero_encoding (n : Usize) (run : Result Bool)
+    (provided : Specs.nonzero_encoding_spec_contract n run) :
+    Obligations.nonzero_encoding_spec_contract n run := by
+  apply WP.spec_mono (provided (unsignedWord n) rfl)
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_checked_nonzero (n : Usize)
+    (run : Result (Option (core.num.nonzero.NonZero Usize
+      core.num.niche_types.NonZeroUsizeInner)))
+    (provided : Specs.checked_nonzero_spec_contract n run) :
+    Obligations.checked_nonzero_spec_contract n run := by
+  apply WP.spec_mono (provided (unsignedWord n) rfl)
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_checked_bool_pair (bytes : Aeneas.Std.Array U8 2#usize)
+    (run : Result (Option (Aeneas.Std.Array Bool 2#usize)))
+    (provided : Specs.checked_bool_pair_spec_contract bytes run) :
+    Obligations.checked_bool_pair_spec_contract bytes run := by
+  apply WP.spec_mono (provided (unsignedArray bytes) (decodeArray_unsigned bytes))
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+@[contract_simps] theorem required_bool_slice_valid (bytes : Slice U8) (run : Result Bool)
+    (provided : Specs.bool_slice_valid_spec_contract bytes run) :
+    Obligations.bool_slice_valid_spec_contract bytes run := by
+  apply WP.spec_mono (provided (byteSlice bytes) (decode_byte_slice bytes))
+  rintro out ⟨_, _, facts⟩
+  exact facts
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/SafetyTests.lean b/verification/aeneas/lean/SafetyTests.lean
index e374074266..554daab40a 100644
--- a/verification/aeneas/lean/SafetyTests.lean
+++ b/verification/aeneas/lean/SafetyTests.lean
@@ -38,6 +38,11 @@ theorem offset_copy_rejects_oversize (src dst : Slice U8) (start : Usize)
   simp [util.copy_unchecked_at, Zerocopy.forbiddenExecution, inside,
     Nat.not_le.mpr oversize]
 
+theorem byte_read_rejects_outside (bytes : Slice U8) (index : Usize)
+    (outside : bytes.val.length ≤ index.val) :
+    util.validity.read_byte bytes index = .fail .panic := by
+  simp [util.validity.read_byte, Nat.not_lt.mpr outside]
+
 -- 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 6b58a42033..89b3bc79de 100644
--- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean
+++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean
@@ -107,6 +107,11 @@ def util.copy_unchecked_at (src dst : Slice U8) (start : Usize) : Result (Slice
     else forbiddenExecution
   else .fail .panic
 
+-- Reading bytes never assumes the validity of the type they might encode.
+-- Bounds are checked at execution, including when the caller discards the byte.
+def util.validity.read_byte (bytes : Slice U8) (index : Usize) : Result U8 :=
+  if index.val < bytes.val.length then .ok bytes.val[index.val]! 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
@@ -153,3 +158,13 @@ def core.intrinsics.transmute {Src : Type} (Dst : Type)
 @[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
+
+-- The extracted call sites instantiate this primitive only at Usize. Other
+-- types are unsupported, so the model cannot promise a recoverable panic.
+@[simp] noncomputable def core.num.nonzero.NonZero.new
+    {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner)
+    (x : T) : Result (Option (core.num.nonzero.NonZero T Inner)) := by
+  classical
+  exact if h : T = Usize then
+    if (cast h x : Usize) = 0#usize then .ok none else .ok (some ⟨x⟩)
+  else forbiddenExecution
diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean
index febac5a7e4..3c31859ab8 100644
--- a/verification/aeneas/projections/Specs.lean
+++ b/verification/aeneas/projections/Specs.lean
@@ -287,4 +287,49 @@ spec checked_copy_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.checked_copy_spec for Zerocopy.util.safety_checks.checked_copy with 2
 
+check_model_inputs Zerocopy.util.safety_checks.checked_nonzero with 0 type parameters
+aeneas_spec_begin
+spec checked_nonzero_spec
+  for @Zerocopy.util.safety_checks.checked_nonzero with 0 type parameters
+  ensures(raw) r => match r with
+    | none => n.val = 0
+    | some value => value.val = n ∧ 0 < value.val.val
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.checked_nonzero_spec for Zerocopy.util.safety_checks.checked_nonzero with 1
+
+check_model_inputs Zerocopy.util.safety_checks.checked_bool_pair with 0 type parameters
+aeneas_spec_begin
+spec checked_bool_pair_spec
+  for @Zerocopy.util.safety_checks.checked_bool_pair with 0 type parameters
+  ensures(raw) r => match r with
+    | none => ∃ byte ∈ bytes.val, 2 ≤ byte.val
+    | some values => values.val = bytes.val.map (fun byte => decide (byte.val = 1)) ∧
+        ∀ byte ∈ bytes.val, byte.val < 2
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.checked_bool_pair_spec for Zerocopy.util.safety_checks.checked_bool_pair with 1
+
+check_model_inputs Zerocopy.util.safety_checks.bool_slice_valid with 0 type parameters
+aeneas_spec_begin
+spec bool_slice_valid_spec
+  for @Zerocopy.util.safety_checks.bool_slice_valid with 0 type parameters
+  ensures(raw) r => r = decide (∀ byte ∈ bytes.val, byte.val < 2)
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.bool_slice_valid_spec for Zerocopy.util.safety_checks.bool_slice_valid with 1
+
+check_model_inputs Zerocopy.util.validity.bool_encoding with 0 type parameters
+aeneas_spec_begin
+spec bool_encoding_spec
+  for @Zerocopy.util.validity.bool_encoding with 0 type parameters
+  ensures(raw) r => r = decide (byte.val = 0 ∨ byte.val = 1)
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.bool_encoding_spec for Zerocopy.util.validity.bool_encoding with 1
+
+check_model_inputs Zerocopy.util.validity.nonzero_encoding with 0 type parameters
+aeneas_spec_begin
+spec nonzero_encoding_spec
+  for @Zerocopy.util.validity.nonzero_encoding with 0 type parameters
+  ensures(raw) r => r = decide (n.val ≠ 0)
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.nonzero_encoding_spec for Zerocopy.util.validity.nonzero_encoding with 1
+
 end Zerocopy.Specs
diff --git a/zerocopy/src/impls.rs b/zerocopy/src/impls.rs
index 48f1f24774..87965aa194 100644
--- a/zerocopy/src/impls.rs
+++ b/zerocopy/src/impls.rs
@@ -226,7 +226,7 @@ assert_unaligned!(bool);
 const _: () = unsafe {
     unsafe_impl!(=> TryFromBytes for bool; |byte| {
         let byte = byte.transmute_with::<u8, invariant::Safe, CastSizedExact, BecauseImmutable>();
-        *byte.unaligned_as_ref() < 2
+        util::validity::bool_encoding(*byte.unaligned_as_ref())
     })
 };
 
@@ -302,11 +302,20 @@ const _: () = unsafe {
 };
 
 macro_rules! unsafe_impl_try_from_bytes_for_nonzero {
+    // Expose the word predicate to Lean without changing the other scalar
+    // implementations. Their widths and standard-library carriers can be
+    // covered separately as those models are admitted.
+    (@validate NonZeroUsize, $value:expr) => {
+        util::validity::nonzero_encoding($value)
+    };
+    (@validate $nonzero:ident, $value:expr) => {
+        $nonzero::new($value).is_some()
+    };
     ($($nonzero:ident[$prim:ty]),*) => {
         $(
             unsafe_impl!(=> TryFromBytes for $nonzero; |n| {
                 let n = n.transmute_with::<Unalign<$prim>, invariant::Safe, CastSizedExact, BecauseImmutable>();
-                $nonzero::new(n.read().into_inner()).is_some()
+                unsafe_impl_try_from_bytes_for_nonzero!(@validate $nonzero, n.read().into_inner())
             });
         )*
     }
diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs
index f4c53b4428..97d5315413 100644
--- a/zerocopy/src/util/mod.rs
+++ b/zerocopy/src/util/mod.rs
@@ -19,6 +19,7 @@ pub(crate) mod bytewrite;
 #[allow(dead_code)]
 mod owned_transmute;
 mod safety_checks;
+pub(crate) mod validity;
 
 use core::{
     marker::PhantomData,
diff --git a/zerocopy/src/util/safety_checks/mod.rs b/zerocopy/src/util/safety_checks/mod.rs
index 29bde56082..1dcdd05e8c 100644
--- a/zerocopy/src/util/safety_checks/mod.rs
+++ b/zerocopy/src/util/safety_checks/mod.rs
@@ -26,7 +26,7 @@
 ///   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 {
+    if super::validity::bool_encoding(byte) {
         // 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
@@ -60,9 +60,64 @@ fn checked_copy(src: &[u8], dst: &mut [u8]) -> bool {
     }
 }
 
+/// Checks the same scalar predicate used by `NonZero`'s validator, then
+/// constructs a nonzero word. Zero remains representable at the input boundary.
+///
+/// ```aeneas
+/// spec checked_nonzero_spec
+///   ensures(raw) r => match r with
+///     | none => n.val = 0
+///     | some value => value.val = n ∧ 0 < value.val.val
+/// ```
+fn checked_nonzero(n: usize) -> Option<core::num::NonZeroUsize> {
+    if super::validity::nonzero_encoding(n) {
+        core::num::NonZeroUsize::new(n)
+    } else {
+        None
+    }
+}
+
+/// Converts two raw candidate bytes using the checked scalar conversion.
+/// Invalid candidates are never constructed as bools, even transiently.
+///
+/// ```aeneas
+/// spec checked_bool_pair_spec
+///   ensures(raw) r => match r with
+///     | none => ∃ byte ∈ bytes.val, 2 ≤ byte.val
+///     | some values => values.val = bytes.val.map (fun byte => decide (byte.val = 1)) ∧
+///         ∀ byte ∈ bytes.val, byte.val < 2
+/// ```
+#[allow(clippy::question_mark)] // Keep branches first-order instead of using a Try dictionary.
+fn checked_bool_pair(bytes: [u8; 2]) -> Option<[bool; 2]> {
+    let left = super::validity::read_byte(&bytes, 0);
+    let right = super::validity::read_byte(&bytes, 1);
+    let left = if let Some(left) = checked_bool(left) { left } else { return None };
+    let right = if let Some(right) = checked_bool(right) { right } else { return None };
+    Some([left, right])
+}
+
+/// Validates a concrete boolean slice by checking every raw candidate byte.
+///
+/// ```aeneas
+/// spec bool_slice_valid_spec
+///   ensures(raw) r => r = decide (∀ byte ∈ bytes.val, byte.val < 2)
+/// ```
+#[allow(clippy::arithmetic_side_effects)] // i < bytes.len() rules out overflow of i + 1.
+fn bool_slice_valid(bytes: &[u8]) -> bool {
+    let mut i = 0;
+    while i < bytes.len() {
+        if !super::validity::bool_encoding(super::validity::read_byte(bytes, i)) {
+            return false;
+        }
+        i += 1;
+    }
+    true
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
+    use crate::TryFromBytes;
 
     #[test]
     fn all_boolean_bytes() {
@@ -75,6 +130,36 @@ mod tests {
                     _ => None,
                 }
             );
+            assert_eq!(checked_bool(byte), bool::try_read_from_bytes(&[byte]).ok());
+        }
+    }
+
+    #[test]
+    fn boolean_array_and_slice_candidates() {
+        for left in 0..=u8::MAX {
+            for right in 0..=u8::MAX {
+                let bytes = [left, right];
+                assert_eq!(checked_bool_pair(bytes), <[bool; 2]>::try_read_from_bytes(&bytes).ok());
+                assert_eq!(bool_slice_valid(&bytes), <[bool]>::try_ref_from_bytes(&bytes).is_ok());
+            }
+        }
+        assert!(bool_slice_valid(&[]));
+        assert!(bool_slice_valid(&[0, 1, 0, 1]));
+        for invalid_index in 0..4 {
+            let mut bytes = [0, 1, 0, 1];
+            bytes[invalid_index] = 2;
+            assert!(!bool_slice_valid(&bytes));
+            <[bool]>::try_ref_from_bytes(&bytes).unwrap_err();
+        }
+    }
+
+    #[test]
+    fn nonzero_candidates() {
+        for n in [0, 1, 2, 255, 256, usize::MAX / 2, usize::MAX] {
+            assert_eq!(
+                checked_nonzero(n),
+                core::num::NonZeroUsize::try_read_from_bytes(&n.to_ne_bytes()).ok()
+            );
         }
     }
 
diff --git a/zerocopy/src/util/validity/mod.rs b/zerocopy/src/util/validity/mod.rs
new file mode 100644
index 0000000000..60752712a4
--- /dev/null
+++ b/zerocopy/src/util/validity/mod.rs
@@ -0,0 +1,51 @@
+// 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.
+
+//! Value predicates shared by the actual scalar `TryFromBytes` implementations.
+//!
+//! Candidates retain their integer representation until these checks finish.
+//! In particular, a candidate for `bool` is a `u8`, not a Lean or Rust `bool`
+//! which would already exclude invalid encodings. Reading the candidate through
+//! `Maybe` remains the implementation's separate pointer safety argument.
+
+/// Accepts exactly the two boolean bit patterns.
+///
+/// ```aeneas
+/// spec bool_encoding_spec
+///   ensures(raw) r => r = decide (byte.val = 0 ∨ byte.val = 1)
+/// ```
+#[inline]
+pub(crate) fn bool_encoding(byte: u8) -> bool {
+    byte < 2
+}
+
+/// Accepts exactly the nonzero word representations.
+///
+/// ```aeneas
+/// spec nonzero_encoding_spec
+///   ensures(raw) r => r = decide (n.val ≠ 0)
+/// ```
+#[inline]
+pub(crate) fn nonzero_encoding(n: usize) -> bool {
+    n != 0
+}
+
+/// Reads an initialized raw byte, with the ordinary slice bounds check.
+///
+/// This narrow, source-bound interpretation avoids importing the whole generic
+/// indexing dictionary (including unsupported pointer operations) to read one
+/// byte. It does not create a bool, a reference, or a possibly invalid integer.
+/// Aeneas checks its complete guarded interpretation independently in Check.
+#[inline]
+#[allow(clippy::indexing_slicing)] // The model explicitly preserves this bounds check.
+pub(crate) fn read_byte(bytes: &[u8], index: usize) -> u8 {
+    bytes[index]
+}