diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md
index adae7cf864..f61ff87f51 100644
--- a/verification/aeneas/README.md
+++ b/verification/aeneas/README.md
@@ -728,6 +728,14 @@ requires an available physical decoder and initialization over its entire
 accepted domain. Absence is `False`; rejection by the library's mathematical
 `RustModel.decode` cannot reduce this domain.
 
+The law also requires **source realizability**: each raw value admitted by the
+mathematical decoder has at least one physical byte representation. Initialization
+alone cannot provide those bytes; an always-rejecting physical decoder would
+satisfy it vacuously. The reusable proofs in
+[`RustRealizability.lean`](lean/RustRealizability.lean) cover the same primitive,
+array, and wrapper families. No default source value, unique encoder, or
+inhabitedness assumption is introduced.
+
 There are 59 authored implementation markers: `()`, `bool`, `char`; all twelve
 signed/unsigned integer carriers; all twelve corresponding `NonZero` carriers
 and their `Option` forms; `PhantomData`; arrays; `Wrapping`, `ManuallyDrop`,
diff --git a/verification/aeneas/golden/Types.lean b/verification/aeneas/golden/Types.lean
index e5c868118c..2b8e48c0a6 100644
--- a/verification/aeneas/golden/Types.lean
+++ b/verification/aeneas/golden/Types.lean
@@ -346,13 +346,13 @@ structure FromBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
 /-- Trait declaration: [zerocopy::IntoBytes]
-    Source: 'src/lib.rs', lines 6017:0-6490:1
+    Source: 'src/lib.rs', lines 6018:0-6491:1
     Visibility: public -/
 structure IntoBytes (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
 
 /-- Trait declaration: [zerocopy::Unaligned]
-    Source: 'src/lib.rs', lines 6628:0-6635:1
+    Source: 'src/lib.rs', lines 6629:0-6636:1
     Visibility: public -/
 structure Unaligned (Self : Type) where
   only_derive_is_allowed_to_implement_this_trait : Result Unit
diff --git a/verification/aeneas/lean/Proofs/IntoBytes.lean b/verification/aeneas/lean/Proofs/IntoBytes.lean
index 7cc9f8408f..e8542c972c 100644
--- a/verification/aeneas/lean/Proofs/IntoBytes.lean
+++ b/verification/aeneas/lean/Proofs/IntoBytes.lean
@@ -10,6 +10,8 @@ those terms. -/
 module
 public import Specs
 public import TraitLaws
+public import RustRealizability
+public import RustRealizabilityModels
 public import Proofs.TraitChecks
 @[expose] public section
 
@@ -26,52 +28,52 @@ namespace Zerocopy.Proofs
 
 @[instance] theorem I8.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized I8 Zerocopy.I8.Insts.ZerocopyIntoBytes :=
-  ⟨initializedIScalar .I8⟩
+  ⟨⟨initializedIScalar .I8, realizableIScalar .I8⟩⟩
 
 @[instance] theorem U16.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized U16 Zerocopy.U16.Insts.ZerocopyIntoBytes :=
-  ⟨initializedUScalar .U16⟩
+  ⟨⟨initializedUScalar .U16, realizableUScalar .U16⟩⟩
 
 @[instance] theorem I16.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized I16 Zerocopy.I16.Insts.ZerocopyIntoBytes :=
-  ⟨initializedIScalar .I16⟩
+  ⟨⟨initializedIScalar .I16, realizableIScalar .I16⟩⟩
 
 @[instance] theorem U32.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized U32 Zerocopy.U32.Insts.ZerocopyIntoBytes :=
-  ⟨initializedUScalar .U32⟩
+  ⟨⟨initializedUScalar .U32, realizableUScalar .U32⟩⟩
 
 @[instance] theorem I32.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized I32 Zerocopy.I32.Insts.ZerocopyIntoBytes :=
-  ⟨initializedIScalar .I32⟩
+  ⟨⟨initializedIScalar .I32, realizableIScalar .I32⟩⟩
 
 @[instance] theorem U64.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized U64 Zerocopy.U64.Insts.ZerocopyIntoBytes :=
-  ⟨initializedUScalar .U64⟩
+  ⟨⟨initializedUScalar .U64, realizableUScalar .U64⟩⟩
 
 @[instance] theorem I64.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized I64 Zerocopy.I64.Insts.ZerocopyIntoBytes :=
-  ⟨initializedIScalar .I64⟩
+  ⟨⟨initializedIScalar .I64, realizableIScalar .I64⟩⟩
 
 @[instance] theorem U128.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized U128 Zerocopy.U128.Insts.ZerocopyIntoBytes :=
-  ⟨initializedUScalar .U128⟩
+  ⟨⟨initializedUScalar .U128, realizableUScalar .U128⟩⟩
 
 @[instance] theorem I128.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized I128 Zerocopy.I128.Insts.ZerocopyIntoBytes :=
-  ⟨initializedIScalar .I128⟩
+  ⟨⟨initializedIScalar .I128, realizableIScalar .I128⟩⟩
 
 @[instance] theorem Usize.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized Usize Zerocopy.Usize.Insts.ZerocopyIntoBytes :=
-  ⟨initializedUScalar .Usize⟩
+  ⟨⟨initializedUScalar .Usize, realizableUScalar .Usize⟩⟩
 
 @[instance] theorem Isize.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized Isize Zerocopy.Isize.Insts.ZerocopyIntoBytes :=
-  ⟨initializedIScalar .Isize⟩
+  ⟨⟨initializedIScalar .Isize, realizableIScalar .Isize⟩⟩
 
 @[instance] theorem Char.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized Char Zerocopy.Char.Insts.ZerocopyIntoBytes :=
-  ⟨Rust.Storage.BitDecoder.filterMap_initialized _ _
-    (Rust.Storage.integerDecoder_initialized 4 .little)⟩
+  ⟨⟨Rust.Storage.BitDecoder.filterMap_initialized _ _
+    (Rust.Storage.integerDecoder_initialized 4 .little), realizableChar⟩⟩
 
 -- Zero rejects NonZero construction; for Option it denotes a successfully
 -- decoded None. Initialization follows the same full integer carrier.
@@ -79,62 +81,62 @@ namespace Zerocopy.Proofs
 @[instance] theorem core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U8 core.num.niche_types.NonZeroU8Inner)
       Zerocopy.core.num.nonzero.NonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩
+  ⟨⟨initializedNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner, realizableNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I8 core.num.niche_types.NonZeroI8Inner)
       Zerocopy.core.num.nonzero.NonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩
+  ⟨⟨initializedNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner, realizableNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U16 core.num.niche_types.NonZeroU16Inner)
       Zerocopy.core.num.nonzero.NonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩
+  ⟨⟨initializedNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner, realizableNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I16 core.num.niche_types.NonZeroI16Inner)
       Zerocopy.core.num.nonzero.NonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩
+  ⟨⟨initializedNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner, realizableNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U32 core.num.niche_types.NonZeroU32Inner)
       Zerocopy.core.num.nonzero.NonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩
+  ⟨⟨initializedNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner, realizableNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I32 core.num.niche_types.NonZeroI32Inner)
       Zerocopy.core.num.nonzero.NonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩
+  ⟨⟨initializedNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner, realizableNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U64 core.num.niche_types.NonZeroU64Inner)
       Zerocopy.core.num.nonzero.NonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩
+  ⟨⟨initializedNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner, realizableNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I64 core.num.niche_types.NonZeroI64Inner)
       Zerocopy.core.num.nonzero.NonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩
+  ⟨⟨initializedNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner, realizableNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero U128 core.num.niche_types.NonZeroU128Inner)
       Zerocopy.core.num.nonzero.NonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩
+  ⟨⟨initializedNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner, realizableNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero I128 core.num.niche_types.NonZeroI128Inner)
       Zerocopy.core.num.nonzero.NonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩
+  ⟨⟨initializedNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner, realizableNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner)
       Zerocopy.core.num.nonzero.NonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩
+  ⟨⟨initializedNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner, realizableNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩⟩
 
 @[instance] theorem core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (core.num.nonzero.NonZero Isize core.num.niche_types.NonZeroIsizeInner)
       Zerocopy.core.num.nonzero.NonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩
+  ⟨⟨initializedNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner, realizableNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩⟩
 
 -- Zero rejects NonZero construction; for Option it denotes a successfully
 -- decoded None. Initialization follows the same full integer carrier.
@@ -142,69 +144,69 @@ namespace Zerocopy.Proofs
 @[instance] theorem core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U8 core.num.niche_types.NonZeroU8Inner))
       Zerocopy.core.option.OptionNonZeroU8NonZeroU8Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩
+  ⟨⟨initializedOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner, realizableOptionNonZeroUScalar .U8 core.num.niche_types.NonZeroU8Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I8 core.num.niche_types.NonZeroI8Inner))
       Zerocopy.core.option.OptionNonZeroI8NonZeroI8Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩
+  ⟨⟨initializedOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner, realizableOptionNonZeroIScalar .I8 core.num.niche_types.NonZeroI8Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U16 core.num.niche_types.NonZeroU16Inner))
       Zerocopy.core.option.OptionNonZeroU16NonZeroU16Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩
+  ⟨⟨initializedOptionNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner, realizableOptionNonZeroUScalar .U16 core.num.niche_types.NonZeroU16Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I16 core.num.niche_types.NonZeroI16Inner))
       Zerocopy.core.option.OptionNonZeroI16NonZeroI16Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩
+  ⟨⟨initializedOptionNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner, realizableOptionNonZeroIScalar .I16 core.num.niche_types.NonZeroI16Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U32 core.num.niche_types.NonZeroU32Inner))
       Zerocopy.core.option.OptionNonZeroU32NonZeroU32Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩
+  ⟨⟨initializedOptionNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner, realizableOptionNonZeroUScalar .U32 core.num.niche_types.NonZeroU32Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I32 core.num.niche_types.NonZeroI32Inner))
       Zerocopy.core.option.OptionNonZeroI32NonZeroI32Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩
+  ⟨⟨initializedOptionNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner, realizableOptionNonZeroIScalar .I32 core.num.niche_types.NonZeroI32Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U64 core.num.niche_types.NonZeroU64Inner))
       Zerocopy.core.option.OptionNonZeroU64NonZeroU64Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩
+  ⟨⟨initializedOptionNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner, realizableOptionNonZeroUScalar .U64 core.num.niche_types.NonZeroU64Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I64 core.num.niche_types.NonZeroI64Inner))
       Zerocopy.core.option.OptionNonZeroI64NonZeroI64Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩
+  ⟨⟨initializedOptionNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner, realizableOptionNonZeroIScalar .I64 core.num.niche_types.NonZeroI64Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero U128 core.num.niche_types.NonZeroU128Inner))
       Zerocopy.core.option.OptionNonZeroU128NonZeroU128Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩
+  ⟨⟨initializedOptionNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner, realizableOptionNonZeroUScalar .U128 core.num.niche_types.NonZeroU128Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero I128 core.num.niche_types.NonZeroI128Inner))
       Zerocopy.core.option.OptionNonZeroI128NonZeroI128Inner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩
+  ⟨⟨initializedOptionNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner, realizableOptionNonZeroIScalar .I128 core.num.niche_types.NonZeroI128Inner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner))
       Zerocopy.core.option.OptionNonZeroUsizeNonZeroUsizeInner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩
+  ⟨⟨initializedOptionNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner, realizableOptionNonZeroUScalar .Usize core.num.niche_types.NonZeroUsizeInner⟩⟩
 
 @[instance] theorem core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized (Option (core.num.nonzero.NonZero Isize core.num.niche_types.NonZeroIsizeInner))
       Zerocopy.core.option.OptionNonZeroIsizeNonZeroIsizeInner.Insts.ZerocopyIntoBytes :=
-  ⟨initializedOptionNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩
+  ⟨⟨initializedOptionNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner, realizableOptionNonZeroIScalar .Isize core.num.niche_types.NonZeroIsizeInner⟩⟩
 
 -- No value of T is stored in PhantomData, so this law needs no model or
 -- trait promise for T, including when T is uninhabited.
 @[instance] theorem core.marker.PhantomData.Insts.ZerocopyIntoBytes_law (T : Type) :
     TraitLaws.into_bytes_initialized (Zerocopy.core.marker.PhantomData T)
       (Zerocopy.core.marker.PhantomData.Insts.ZerocopyIntoBytes T) :=
-  ⟨Rust.Storage.emptyDecoder_initialized _⟩
+  ⟨⟨Rust.Storage.emptyDecoder_initialized _, realizablePhantomData T⟩⟩
 
 
 -- Transparent wrappers inherit the exact incoming dictionary promise.
@@ -215,48 +217,54 @@ namespace Zerocopy.Proofs
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (Zerocopy.core.num.wrapping.Wrapping T)
       (Zerocopy.core.num.wrapping.Wrapping.Insts.ZerocopyIntoBytes dictionary) :=
-  ⟨initializedWrapping T
-    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩
+  ⟨⟨initializedWrapping T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableWrapping T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
 @[instance] theorem core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes_law
     {T : Type} (dictionary : IntoBytes T)
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (core.mem.manually_drop.ManuallyDrop T)
       (Zerocopy.core.mem.manually_drop.ManuallyDrop.Insts.ZerocopyIntoBytes dictionary) :=
-  ⟨initializedManuallyDrop T
-    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩
+  ⟨⟨initializedManuallyDrop T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableManuallyDrop T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
 @[instance] theorem core.cell.Cell.Insts.ZerocopyIntoBytes_law
     {T : Type} (dictionary : IntoBytes T)
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (core.cell.Cell T)
       (Zerocopy.core.cell.Cell.Insts.ZerocopyIntoBytes dictionary) :=
-  ⟨initializedCell T
-    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩
+  ⟨⟨initializedCell T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableCell T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
 @[instance] theorem core.cell.UnsafeCell.Insts.ZerocopyIntoBytes_law
     {T : Type} (dictionary : IntoBytes T)
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (core.cell.UnsafeCell T)
       (Zerocopy.core.cell.UnsafeCell.Insts.ZerocopyIntoBytes dictionary) :=
-  ⟨initializedUnsafeCell T
-    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩
+  ⟨⟨initializedUnsafeCell T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableUnsafeCell T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
 @[instance] theorem wrappers.Unalign.Insts.ZerocopyIntoBytes_law
     {T : Type} (dictionary : IntoBytes T)
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (Zerocopy.wrappers.Unalign T)
       (Zerocopy.wrappers.Unalign.Insts.ZerocopyIntoBytes dictionary) :=
-  ⟨initializedWrapperRepresentation Zerocopy.wrappers.Unalign.mk
-    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩
+  ⟨⟨initializedWrapperRepresentation Zerocopy.wrappers.Unalign.mk
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableUnalign T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
 @[instance] theorem wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes_law
     {T : Type} (dictionary : IntoBytes T)
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (Zerocopy.wrappers.read_only_def.ReadOnly T)
       (Zerocopy.wrappers.read_only_def.ReadOnly.Insts.ZerocopyIntoBytes dictionary) :=
-  ⟨initializedWrapperRepresentation Zerocopy.wrappers.read_only_def.ReadOnly.mk
-    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩
+  ⟨⟨initializedWrapperRepresentation Zerocopy.wrappers.read_only_def.ReadOnly.mk
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1, realizableReadOnly T
+    (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
 -- The byte-order parameter is phantom. Only the byte array contributes
 -- storage, and its elements inherit the u8 initialization theorem.
@@ -265,96 +273,96 @@ namespace Zerocopy.Proofs
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U16 O)
       (Zerocopy.byteorder.U16.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.U16.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8)), realizableByteorderU16 O⟩⟩
 
 @[instance] theorem byteorder.U32.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U32 O)
       (Zerocopy.byteorder.U32.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.U32.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderU32 O⟩⟩
 
 @[instance] theorem byteorder.U64.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U64 O)
       (Zerocopy.byteorder.U64.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.U64.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderU64 O⟩⟩
 
 @[instance] theorem byteorder.U128.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.U128 O)
       (Zerocopy.byteorder.U128.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.U128.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8)), realizableByteorderU128 O⟩⟩
 
 @[instance] theorem byteorder.Usize.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.Usize O)
       (Zerocopy.byteorder.Usize.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.Usize.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderUsize O⟩⟩
 
 @[instance] theorem byteorder.I16.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I16 O)
       (Zerocopy.byteorder.I16.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.I16.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (2#usize) (initializedUScalar .U8)), realizableByteorderI16 O⟩⟩
 
 @[instance] theorem byteorder.I32.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I32 O)
       (Zerocopy.byteorder.I32.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.I32.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderI32 O⟩⟩
 
 @[instance] theorem byteorder.I64.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I64 O)
       (Zerocopy.byteorder.I64.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.I64.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderI64 O⟩⟩
 
 @[instance] theorem byteorder.I128.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.I128 O)
       (Zerocopy.byteorder.I128.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.I128.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (16#usize) (initializedUScalar .U8)), realizableByteorderI128 O⟩⟩
 
 @[instance] theorem byteorder.Isize.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.Isize O)
       (Zerocopy.byteorder.Isize.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.Isize.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderIsize O⟩⟩
 
 @[instance] theorem byteorder.F32.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.F32 O)
       (Zerocopy.byteorder.F32.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.F32.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (4#usize) (initializedUScalar .U8)), realizableByteorderF32 O⟩⟩
 
 @[instance] theorem byteorder.F64.Insts.ZerocopyIntoBytes_law
     (O : Type) [meaning : RustModel O] :
     TraitLaws.into_bytes_initialized (Zerocopy.byteorder.F64 O)
       (Zerocopy.byteorder.F64.Insts.ZerocopyIntoBytes O) :=
-  ⟨initializedWrapperRepresentation
+  ⟨⟨initializedWrapperRepresentation
     (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk)
-    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8))⟩
+    (RustModel.initialized_array U8 (8#usize) (initializedUScalar .U8)), realizableByteorderF64 O⟩⟩
 
 end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Proofs/TraitChecks.lean b/verification/aeneas/lean/Proofs/TraitChecks.lean
index e70eca529f..22b03b51ff 100644
--- a/verification/aeneas/lean/Proofs/TraitChecks.lean
+++ b/verification/aeneas/lean/Proofs/TraitChecks.lean
@@ -9,6 +9,7 @@ those terms. -/
 module
 public import Specs
 public import TraitLaws
+public import RustRealizability
 @[expose] public section
 
 /-!
@@ -50,15 +51,15 @@ namespace Zerocopy.Proofs
 -- library decoder's (possibly smaller) admission domain.
 @[instance] theorem Bool.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized Bool Zerocopy.Bool.Insts.ZerocopyIntoBytes :=
-  ⟨Rust.Storage.boolDecoder_initialized⟩
+  ⟨⟨Rust.Storage.boolDecoder_initialized, realizableBool⟩⟩
 
 @[instance] theorem U8.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized U8 Zerocopy.U8.Insts.ZerocopyIntoBytes :=
-  ⟨initializedUScalar .U8⟩
+  ⟨⟨initializedUScalar .U8, realizableUScalar .U8⟩⟩
 
 @[instance] theorem Tuple.Insts.ZerocopyIntoBytes_law :
     TraitLaws.into_bytes_initialized Unit Zerocopy.Tuple.Insts.ZerocopyIntoBytes :=
-  ⟨Rust.Storage.unitDecoder_initialized⟩
+  ⟨⟨Rust.Storage.unitDecoder_initialized, realizableUnit⟩⟩
 
 -- The original type, const length, and computational dictionary remain the
 -- native implementation's prefix. Only the element's provider and law are
@@ -68,7 +69,10 @@ namespace Zerocopy.Proofs
     [meaning : RustModel T] [law : TraitLaws.into_bytes_initialized T dictionary] :
     TraitLaws.into_bytes_initialized (Aeneas.Std.Array T N)
       (Zerocopy.Array.Insts.ZerocopyIntoBytes N dictionary) :=
-  ⟨RustModel.initialized_array T N (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law)⟩
+  ⟨⟨RustModel.initialized_array T N
+      (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).1,
+    RustModel.realizable_array T N
+      (@TraitLaws.into_bytes_initialized.holds T dictionary meaning law).2⟩⟩
 
 -- Calling the real Rust helper selects the existing unsafe impls in Charon.
 -- The generic impl law proves all lengths; these concrete cases additionally
@@ -79,20 +83,20 @@ theorem array_into_bytes_spec : Specs.array_into_bytes_spec := by
   refine ⟨(), rfl, ?_, ?_, ?_, ?_, ?_⟩
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)
-      _ inferInstance)
+      _ inferInstance).1
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.U8.Insts.ZerocopyIntoBytes)
-      _ inferInstance)
+      _ inferInstance).1
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Tuple.Insts.ZerocopyIntoBytes)
-      _ inferInstance)
+      _ inferInstance).1
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes)
-      _ inferInstance)
+      _ inferInstance).1
   · exact (@TraitLaws.into_bytes_initialized.holds _
       (Zerocopy.Array.Insts.ZerocopyIntoBytes _
         (Zerocopy.Array.Insts.ZerocopyIntoBytes _ Zerocopy.Bool.Insts.ZerocopyIntoBytes))
-      _ inferInstance)
+      _ inferInstance).1
 
 theorem unaligned_alignment_spec : Specs.unaligned_alignment_spec := by
   intro T dictionary _ law
diff --git a/verification/aeneas/lean/RustModel.lean b/verification/aeneas/lean/RustModel.lean
index 45c33f0d89..4a54d75ef5 100644
--- a/verification/aeneas/lean/RustModel.lean
+++ b/verification/aeneas/lean/RustModel.lean
@@ -63,6 +63,14 @@ def RustModel.initializedRepresentation (Raw : Type u) [m : RustModel Raw] : Pro
   | none => False
   | some decoder => decoder.Initialized
 
+/-- Every admitted source has some physical representation. This is vacuous
+for uninhabited sources and does not require a canonical encoding. -/
+def RustModel.realizableRepresentation (Raw : Type u) [m : RustModel Raw] : Prop :=
+  match m.representation with
+  | none => False
+  | some decoder => ∀ raw, @isValid Raw m raw →
+      ∃ bytes, decoder.run bytes = some raw
+
 /-- Every initialized representation of the physical width admits a language
 value and a mathematical value through this same provider. Missing physical
 semantics fail closed. This law does not establish Rust layout correspondence,
diff --git a/verification/aeneas/lean/RustRealizability.lean b/verification/aeneas/lean/RustRealizability.lean
new file mode 100644
index 0000000000..bb64337299
--- /dev/null
+++ b/verification/aeneas/lean/RustRealizability.lean
@@ -0,0 +1,334 @@
+/- 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 RustRepresentation
+import all RustModel
+import all ModelPrelude
+import all Rust.Storage
+import all RustAeneas.Storage
+@[expose] public section
+
+/-!
+Source realizability is conditional on mathematical admission. It supplies a
+physical representation of that particular raw value, without imposing a
+default value or a unique representation. An uninhabited raw carrier therefore
+needs no invented source value. These existence laws leave initialization and
+Rust layout correspondence as separate obligations.
+-/
+
+namespace Rust.Storage
+
+/-- Integer encoding supplies a representation for every fixed-width word. -/
+theorem integerDecoder_realizable (byteSize : Nat) (endian : Rust.Bytes.Endian)
+    (word : BitVec (8 * byteSize)) :
+    ∃ bytes, (integerDecoder byteSize endian).run bytes = some word := by
+  have bound : word.toNat < 256 ^ byteSize := by
+    rw [Rust.Bytes.radix_pow_eq_two_pow]
+    exact word.isLt
+  cases endian with
+  | little =>
+    refine ⟨(Rust.Bytes.encodeLE byteSize word.toNat).map AMByte.init, ?_⟩
+    rw [integerDecoder_run_map _ _ _ (Rust.Bytes.length_encodeLE _ _)]
+    simp only [Rust.Bytes.decode, Rust.Bytes.decodeLE_encodeLE_of_lt _ _ bound]
+    congr 1
+    simp
+  | big =>
+    refine ⟨(Rust.Bytes.encodeBE byteSize word.toNat).map AMByte.init, ?_⟩
+    rw [integerDecoder_run_map _ _ _ (Rust.Bytes.length_encodeBE _ _)]
+    simp only [Rust.Bytes.decode, Rust.Bytes.decodeBE_encodeBE_of_lt _ _ bound]
+    congr 1
+    simp
+
+namespace BitDecoder
+
+/-- A mapped decoder realizes an output whenever one realized input maps to it. -/
+theorem map_realizable (decoder : BitDecoder Raw) (f : Raw → Other)
+    (raw : Raw) (h : ∃ bytes, decoder.run bytes = some raw) :
+    ∃ bytes, (decoder.map f).run bytes = some (f raw) := by
+  obtain ⟨bytes, accepted⟩ := h
+  exact ⟨bytes, by rw [run_map, accepted]; rfl⟩
+
+/-- Filtering preserves an existing representation when the value passes. -/
+theorem filterMap_realizable (decoder : BitDecoder Raw) (f : Raw → Option Other)
+    (raw : Raw) (other : Other) (h : ∃ bytes, decoder.run bytes = some raw)
+    (passes : f raw = some other) :
+    ∃ bytes, (decoder.filterMap f).run bytes = some other := by
+  obtain ⟨bytes, accepted⟩ := h
+  exact ⟨bytes, by rw [run_filterMap, accepted]; exact passes⟩
+
+end BitDecoder
+
+/-- Concatenate one witness per admitted element. Recursion follows the value
+list, so empty arrays and zero-sized elements require no inhabited carrier. -/
+theorem arrayDecode_realizable (element : BitDecoder Raw) (admitted : Raw → Prop)
+    (realizable : ∀ raw, admitted raw → ∃ bytes, element.run bytes = some raw)
+    (raws : List Raw) (valid : ∀ raw ∈ raws, admitted raw) :
+    ∃ bytes, bytes.length = raws.length * element.byteSize ∧
+      arrayDecode element raws.length bytes = some ⟨raws, rfl⟩ := by
+  induction raws with
+  | nil => exact ⟨[], by simp, rfl⟩
+  | cons raw raws ih =>
+    obtain ⟨head, headAccepted⟩ := realizable raw (valid raw (by simp))
+    have headWidth := BitDecoder.run_length element head raw headAccepted
+    obtain ⟨tail, tailWidth, tailAccepted⟩ := ih
+      (fun raw member => valid raw (by simp [member]))
+    refine ⟨head ++ tail, ?_, ?_⟩
+    · simp only [List.length_append, List.length_cons, headWidth, tailWidth, Nat.succ_mul]
+      omega
+    · simp only [List.length_cons, arrayDecode, ← headWidth, List.take_left, List.drop_left,
+        headAccepted, tailAccepted]
+      rfl
+
+end Rust.Storage
+
+open Aeneas.Std Rust.Storage
+namespace AeneasSpecs
+
+theorem RustModel.realizableRepresentation_exists {Raw : Type u} [m : RustModel Raw]
+    (realizable : RustModel.realizableRepresentation Raw)
+    (decoder : BitDecoder Raw) (available : m.representation = some decoder)
+    (raw : Raw) (valid : isValid raw) : ∃ bytes, decoder.run bytes = some raw := by
+  simp only [RustModel.realizableRepresentation, available] at realizable
+  exact realizable raw valid
+
+theorem realizableUScalar (ty : UScalarTy) :
+    RustModel.realizableRepresentation (UScalar ty) := by
+  intro raw _
+  obtain ⟨bytes, accepted⟩ := integerDecoder_realizable (ty.numBits / 8) .little
+    (raw.bv.cast (AeneasAdapter.unsigned_byte_width ty).symm)
+  refine ⟨bytes, ?_⟩
+  change ((integerDecoder _ _).map _).run bytes = _
+  rw [BitDecoder.run_map, accepted]
+  simp
+
+theorem realizableIScalar (ty : IScalarTy) :
+    RustModel.realizableRepresentation (IScalar ty) := by
+  intro raw _
+  obtain ⟨bytes, accepted⟩ := integerDecoder_realizable (ty.numBits / 8) .little
+    (raw.bv.cast (AeneasAdapter.signed_byte_width ty).symm)
+  refine ⟨bytes, ?_⟩
+  change ((integerDecoder _ _).map _).run bytes = _
+  rw [BitDecoder.run_map, accepted]
+  simp
+
+theorem realizableBool : RustModel.realizableRepresentation Bool := by
+  intro raw _
+  cases raw
+  · exact ⟨[AMByte.init 0], boolDecoder_run_zero⟩
+  · exact ⟨[AMByte.init 1], boolDecoder_run_one⟩
+
+theorem realizableUnit : RustModel.realizableRepresentation Unit := by
+  intro raw _
+  cases raw
+  exact ⟨[], unitDecoder_run_nil⟩
+
+theorem realizablePhantomData (T : Type) :
+    RustModel.realizableRepresentation (Zerocopy.core.marker.PhantomData T) := by
+  intro raw _
+  rw [phantomData_eq_mk T raw]
+  exact ⟨[], emptyDecoder_run_nil _⟩
+
+theorem realizableChar : RustModel.realizableRepresentation Char := by
+  intro raw _
+  obtain ⟨bytes, accepted⟩ := integerDecoder_realizable 4 .little
+    (BitVec.ofNat 32 raw.val.toNat)
+  refine ⟨bytes, ?_⟩
+  change ((integerDecoder 4 .little).filterMap _).run bytes = _
+  rw [BitDecoder.run_filterMap, accepted]
+  have word : UInt32.ofNat (BitVec.ofNat 32 raw.val.toNat).toNat = raw.val := by
+    rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (UInt32.toNat_lt raw.val)]
+    exact UInt32.ofNat_toNat
+  have valid : _root_.isValidChar raw.val := by
+    simpa only [_root_.isValidChar, UInt32.lt_iff_toNat_lt, UInt32.reduceToNat,
+      UInt32.isValidChar, Nat.isValidChar] using raw.valid
+  simp only [Option.bind_some, word, dif_pos valid]
+
+theorem realizableOptionNonZeroUScalar (ty : UScalarTy) (Inner : Type) :
+    RustModel.realizableRepresentation (Option (core.num.nonzero.NonZero (UScalar ty) Inner)) := by
+  intro raw valid
+  cases raw with
+  | none =>
+    obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists
+      (realizableUScalar ty) (uScalarBitDecoder ty) rfl ⟨0⟩ ⟨_, rfl⟩
+    exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; rfl⟩
+  | some raw =>
+    have nonzero : raw.val.val ≠ 0 := by
+      obtain ⟨value, accepted⟩ := valid
+      by_cases positive : 0 < raw.val.val
+      · omega
+      · simp [RustModel.decode, positive] at accepted
+    obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists
+      (realizableUScalar ty) (uScalarBitDecoder ty) rfl raw.val ⟨_, rfl⟩
+    exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp [nonzero]⟩
+
+theorem realizableOptionNonZeroIScalar (ty : IScalarTy) (Inner : Type) :
+    RustModel.realizableRepresentation (Option (core.num.nonzero.NonZero (IScalar ty) Inner)) := by
+  intro raw valid
+  cases raw with
+  | none =>
+    obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists
+      (realizableIScalar ty) (iScalarBitDecoder ty) rfl ⟨0⟩ ⟨_, rfl⟩
+    exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp only [Option.map_some, IScalar.val, BitVec.toInt_ofNat, Int.natCast_zero, Int.zero_bmod, ite_true]⟩
+  | some raw =>
+    have nonzero : raw.val.val ≠ 0 := by
+      obtain ⟨value, accepted⟩ := valid
+      by_contra zero
+      simp [RustModel.decode, zero] at accepted
+    obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists
+      (realizableIScalar ty) (iScalarBitDecoder ty) rfl raw.val ⟨_, rfl⟩
+    exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp [nonzero]⟩
+
+theorem realizableNonZeroUScalar (ty : UScalarTy) (Inner : Type) :
+    RustModel.realizableRepresentation (core.num.nonzero.NonZero (UScalar ty) Inner) := by
+  intro raw valid
+  have nonzero : raw.val.val ≠ 0 := by
+    obtain ⟨value, accepted⟩ := valid
+    by_cases positive : 0 < raw.val.val
+    · omega
+    · simp [RustModel.decode, positive] at accepted
+  obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists
+    (realizableUScalar ty) (uScalarBitDecoder ty) rfl raw.val ⟨_, rfl⟩
+  refine ⟨bytes, ?_⟩
+  change ((uScalarBitDecoder ty).filterMap _).run bytes = _
+  rw [BitDecoder.run_filterMap, accepted]
+  simp only [Option.bind_some, nonzero, ↓reduceIte]
+
+theorem realizableNonZeroIScalar (ty : IScalarTy) (Inner : Type) :
+    RustModel.realizableRepresentation (core.num.nonzero.NonZero (IScalar ty) Inner) := by
+  intro raw valid
+  have nonzero : raw.val.val ≠ 0 := by
+    obtain ⟨value, accepted⟩ := valid
+    by_contra zero
+    simp [RustModel.decode, zero] at accepted
+  obtain ⟨bytes, accepted⟩ := RustModel.realizableRepresentation_exists
+    (realizableIScalar ty) (iScalarBitDecoder ty) rfl raw.val ⟨_, rfl⟩
+  refine ⟨bytes, ?_⟩
+  change ((iScalarBitDecoder ty).filterMap _).run bytes = _
+  rw [BitDecoder.run_filterMap, accepted]
+  simp only [Option.bind_some, nonzero, ↓reduceIte]
+
+/-- A transparent wrapper reuses its payload's bytes. The inverse and validity
+premises also cover generated wrapper providers with their retained decoder. -/
+theorem RustModel.realizable_of_wrapper {A B : Type} [ma : RustModel A] [mb : RustModel B]
+    (wrap : A → B) (unwrap : B → A) (inverse : ∀ raw, wrap (unwrap raw) = raw)
+    (representation : mb.representation = wrapperRepresentation wrap)
+    (validChild : ∀ raw, isValid raw → isValid (unwrap raw))
+    (child : RustModel.realizableRepresentation A) :
+    RustModel.realizableRepresentation B := by
+  cases available : ma.representation with
+  | none => simp [RustModel.realizableRepresentation, available] at child
+  | some decoder =>
+    simp only [RustModel.realizableRepresentation, available] at child
+    simp only [RustModel.realizableRepresentation, representation,
+      wrapperRepresentation, available, Option.map_some]
+    intro raw valid
+    obtain ⟨bytes, accepted⟩ := child (unwrap raw) (validChild raw valid)
+    exact ⟨bytes, by rw [BitDecoder.run_map, accepted]; simp [inverse]⟩
+
+theorem realizableManuallyDrop (T : Type) [ma : RustModel T]
+    (child : RustModel.realizableRepresentation T) :
+    RustModel.realizableRepresentation (core.mem.manually_drop.ManuallyDrop T) :=
+  RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl
+    (fun _ valid => valid) child
+
+theorem realizableCell (T : Type) [ma : RustModel T]
+    (child : RustModel.realizableRepresentation T) :
+    RustModel.realizableRepresentation (core.cell.Cell T) :=
+  RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl
+    (fun _ valid => valid) child
+
+theorem realizableUnsafeCell (T : Type) [ma : RustModel T]
+    (child : RustModel.realizableRepresentation T) :
+    RustModel.realizableRepresentation (core.cell.UnsafeCell T) :=
+  RustModel.realizable_of_wrapper _ (·.value) (by rintro ⟨raw⟩; rfl) rfl
+    (fun _ valid => valid) child
+
+theorem realizableWrapping (T : Type) [ma : RustModel T]
+    (child : RustModel.realizableRepresentation T) :
+    RustModel.realizableRepresentation (Zerocopy.core.num.wrapping.Wrapping T) :=
+  RustModel.realizable_of_wrapper _ (·._0) (by rintro ⟨raw⟩; rfl) rfl
+    (fun _ valid => valid) child
+
+/-- Successful list decoding admits every stored element with the same provider. -/
+theorem decodeList_valid {α : Type u} [ma : RustModel α]
+    (raws : List α) (values : List ma.Model) (accepted : decodeList ma.decode raws = some values) :
+    ∀ raw ∈ raws, isValid raw := by
+  induction raws generalizing values with
+  | nil => simp
+  | cons head tail ih =>
+    cases decodedHead : ma.decode head with
+    | none => simp [decodeList, decodedHead] at accepted
+    | some value =>
+      cases decodedTail : decodeList ma.decode tail with
+      | none => simp [decodeList, decodedHead, decodedTail] at accepted
+      | some values =>
+        intro raw member
+        rcases List.mem_cons.mp member with same | member
+        · subst raw; exact ⟨value, decodedHead⟩
+        · exact ih _ decodedTail raw member
+
+/-- Element admission constructs list admission without choosing a default. -/
+theorem decodeList_exists {α : Type u} [ma : RustModel α]
+    (raws : List α) (valid : ∀ raw ∈ raws, isValid raw) :
+    ∃ values, decodeList ma.decode raws = some values := by
+  induction raws with
+  | nil => exact ⟨[], rfl⟩
+  | cons raw raws ih =>
+    obtain ⟨value, head⟩ := valid raw (by simp)
+    obtain ⟨values, tail⟩ := ih (fun raw member => valid raw (by simp [member]))
+    exact ⟨value :: values, by simp [decodeList, head, tail]⟩
+
+theorem RustModel.valid_array {α : Type u} [ma : RustModel α] {n : Usize}
+    (raw : Aeneas.Std.Array α n) (valid : ∀ item ∈ raw.val, isValid item) : isValid raw := by
+  obtain ⟨values, decoded⟩ := decodeList_exists raw.val valid
+  unfold isValid
+  dsimp only [RustModel.decode]
+  split
+  · rename_i rejected
+    rw [decoded] at rejected
+    contradiction
+  · exact ⟨_, rfl⟩
+
+theorem RustModel.realizable_array (α : Type u) [ma : RustModel α] (n : Usize)
+    (element : RustModel.realizableRepresentation α) :
+    @RustModel.realizableRepresentation (Aeneas.Std.Array α n) (@modelArray α n ma) := by
+  cases available : ma.representation with
+  | none => simp [RustModel.realizableRepresentation, available] at element
+  | some decoder =>
+    simp only [RustModel.realizableRepresentation, available] at element
+    unfold RustModel.realizableRepresentation
+    rw [show (@modelArray α n ma).representation = ma.representation.map (fun element =>
+      (arrayDecoder element n.val).map
+        (fun values => Aeneas.Std.Array.from values.val values.property)) from rfl]
+    rw [available]
+    simp only [Option.map_some]
+    intro raw valid
+    obtain ⟨model, accepted⟩ := valid
+    have all : ∀ item ∈ raw.val, isValid item := by
+      dsimp only [RustModel.decode] at accepted
+      split at accepted
+      · contradiction
+      · rename_i values decoded
+        exact decodeList_valid raw.val values decoded
+    obtain ⟨bytes, width, physical⟩ := arrayDecode_realizable decoder isValid element raw.val all
+    refine ⟨bytes, ?_⟩
+    rw [BitDecoder.run_map]
+    have rawLength : raw.val.length = n.val := raw.property
+    have decoded : arrayDecode decoder n.val bytes = some ⟨raw.val, rawLength⟩ := by
+      have transport (count : Nat) (h : raw.val.length = count) :
+          arrayDecode decoder count bytes = some ⟨raw.val, h⟩ := by
+        cases h
+        exact physical
+      exact transport n.val rawLength
+    have fromRaw : Aeneas.Std.Array.from raw.val rawLength = raw :=
+      Aeneas.Std.Array.ext _ _ (Aeneas.Std.Array.from_val _ _)
+    simp only [rawLength] at width
+    simp [BitDecoder.run, arrayDecoder, width, decoded, fromRaw]
+
+end AeneasSpecs
diff --git a/verification/aeneas/lean/RustRealizabilityModels.lean b/verification/aeneas/lean/RustRealizabilityModels.lean
new file mode 100644
index 0000000000..7294a926ad
--- /dev/null
+++ b/verification/aeneas/lean/RustRealizabilityModels.lean
@@ -0,0 +1,139 @@
+/- 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 RustRealizability
+public import Models
+import all RustModel
+import all ModelPrelude
+@[expose] public section
+
+open Aeneas.Std Rust.Storage
+namespace AeneasSpecs
+
+/-- Generated providers retain their mathematical admission checks. A wrapper
+may restrict admission further, but must still admit its stored child. -/
+theorem realizableUnalign (T : Type) [ma : RustModel T]
+    (child : RustModel.realizableRepresentation T) :
+    RustModel.realizableRepresentation (Zerocopy.wrappers.Unalign T) := by
+  apply RustModel.realizable_of_wrapper Zerocopy.wrappers.Unalign.mk (·._0)
+    (by rintro ⟨raw⟩; rfl) rfl ?_ child
+  intro raw valid
+  obtain ⟨value, accepted⟩ := valid
+  cases decoded : ma.decode raw._0 with
+  | none => simp [RustModel.decode, Zerocopy.wrappers.Unalign.decode, decoded] at accepted
+  | some value => exact ⟨value, decoded⟩
+
+theorem realizableReadOnly (T : Type) [ma : RustModel T]
+    (child : RustModel.realizableRepresentation T) :
+    RustModel.realizableRepresentation (Zerocopy.wrappers.read_only_def.ReadOnly T) := by
+  apply RustModel.realizable_of_wrapper Zerocopy.wrappers.read_only_def.ReadOnly.mk (·.inner)
+    (by rintro ⟨raw⟩; rfl) rfl ?_ child
+  intro raw valid
+  obtain ⟨value, accepted⟩ := valid
+  cases decoded : ma.decode raw.inner with
+  | none => simp [RustModel.decode, Zerocopy.wrappers.read_only_def.ReadOnly.decode, decoded] at accepted
+  | some value => exact ⟨value, decoded⟩
+
+theorem realizableByteorderU16 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.U16 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.U16.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (2#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderU32 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.U32 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.U32.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderU64 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.U64 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.U64.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderU128 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.U128 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.U128.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (16#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderUsize (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.Usize O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.Usize.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderI16 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.I16 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.I16.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (2#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderI32 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.I32 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.I32.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderI64 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.I64 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.I64.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderI128 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.I128 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.I128.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (16#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderIsize (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.Isize O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.Isize.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderF32 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.F32 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.F32.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (4#usize) (realizableUScalar .U8))
+
+theorem realizableByteorderF64 (O : Type) [RustModel O] :
+    RustModel.realizableRepresentation (Zerocopy.byteorder.F64 O) := by
+  apply RustModel.realizable_of_wrapper
+    (fun raw => Zerocopy.byteorder.F64.mk raw Zerocopy.core.marker.PhantomData.mk)
+    (·._0) (by rintro ⟨raw, phantom⟩; cases phantom; rfl) rfl
+    (fun raw _ => RustModel.valid_array raw._0 (fun _ _ => ⟨_, rfl⟩))
+    (RustModel.realizable_array U8 (8#usize) (realizableUScalar .U8))
+
+end AeneasSpecs
diff --git a/verification/aeneas/lean/RustRealizabilityTests.lean b/verification/aeneas/lean/RustRealizabilityTests.lean
new file mode 100644
index 0000000000..cf7028d4f6
--- /dev/null
+++ b/verification/aeneas/lean/RustRealizabilityTests.lean
@@ -0,0 +1,94 @@
+/- 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 RustRealizabilityModels
+import all RustModel
+import all ModelPrelude
+import all Rust.Storage
+@[expose] public section
+
+open Aeneas.Std AeneasSpecs Rust.Storage
+namespace RustRealizabilityTests
+
+example (ty : UScalarTy) : RustModel.realizableRepresentation (UScalar ty) := realizableUScalar ty
+example (ty : IScalarTy) : RustModel.realizableRepresentation (IScalar ty) := realizableIScalar ty
+example : RustModel.realizableRepresentation Char := realizableChar
+example : RustModel.realizableRepresentation Bool := realizableBool
+example (ty : UScalarTy) (Inner : Type) :
+    RustModel.realizableRepresentation (core.num.nonzero.NonZero (UScalar ty) Inner) :=
+  realizableNonZeroUScalar ty Inner
+example (ty : IScalarTy) (Inner : Type) :
+    RustModel.realizableRepresentation (Option (core.num.nonzero.NonZero (IScalar ty) Inner)) :=
+  realizableOptionNonZeroIScalar ty Inner
+example : RustModel.realizableRepresentation
+    (Aeneas.Std.Array (Aeneas.Std.Array Bool (2#usize)) (3#usize)) :=
+  RustModel.realizable_array _ _ (RustModel.realizable_array _ _ realizableBool)
+example : RustModel.realizableRepresentation (Aeneas.Std.Array Unit (4#usize)) :=
+  RustModel.realizable_array _ _ realizableUnit
+example (T : Type) : RustModel.realizableRepresentation
+    (Aeneas.Std.Array (Zerocopy.core.marker.PhantomData T) (3#usize)) :=
+  RustModel.realizable_array _ _ (realizablePhantomData T)
+
+-- Source existence cannot be inferred from initialization alone: this
+-- initialized decoder realizes false, while the provider also admits true.
+@[reducible] def missingTrue : RustModel Bool where
+  Model := Bool
+  «decode» := some
+  representation := some (emptyDecoder false)
+
+example : @RustModel.initializedRepresentation Bool missingTrue := emptyDecoder_initialized false
+example : ¬ @RustModel.realizableRepresentation Bool missingTrue := by
+  intro realizable
+  obtain ⟨bytes, accepted⟩ := realizable true ⟨true, rfl⟩
+  have empty : bytes = [] := List.length_eq_zero_iff.mp
+    (BitDecoder.run_length (emptyDecoder false) bytes true accepted)
+  subst bytes
+  contradiction
+
+-- Missing physical semantics remain unavailable even when no raw values exist.
+@[reducible] def noPhysical : RustModel Empty where
+  Model := Empty
+  «decode» := some
+example : ¬ @RustModel.realizableRepresentation Empty noPhysical := by
+  change ¬ False
+  exact not_false
+
+-- With an explicit decoder, an uninhabited raw carrier is vacuous and needs
+-- no Inhabited instance. Empty arrays of this element carrier are realizable.
+@[reducible] def emptyPhysical : RustModel Empty where
+  Model := Empty
+  «decode» := some
+  representation := some { byteSize := 0, «decode» := fun _ => none }
+
+theorem emptyRealizable : @RustModel.realizableRepresentation Empty emptyPhysical := by
+  intro raw
+  cases raw
+
+example : @RustModel.realizableRepresentation (Aeneas.Std.Array Empty (0#usize))
+    (@modelArray Empty (0#usize) emptyPhysical) :=
+  @RustModel.realizable_array Empty emptyPhysical (0#usize) emptyRealizable
+
+-- Distinct bytes may represent the same raw value; realizability supplies
+-- existence and does not impose uniqueness or a canonical inverse.
+@[reducible] def ambiguous : RustModel Bool where
+  Model := Unit
+  «decode» raw := if raw then none else some ()
+  representation := some ((uScalarBitDecoder .U8).map fun _ => false)
+
+theorem ambiguousRealizable : @RustModel.realizableRepresentation Bool ambiguous := by
+  intro raw valid
+  cases raw with
+  | false => exact ⟨[AMByte.init 0], rfl⟩
+  | true => obtain ⟨value, accepted⟩ := valid; contradiction
+
+example : ((uScalarBitDecoder .U8).map fun _ => false).run [AMByte.init 0] = some false := rfl
+example : ((uScalarBitDecoder .U8).map fun _ => false).run [AMByte.init 1] = some false := rfl
+example : [AMByte.init 0] ≠ [AMByte.init 1] := by decide
+
+end RustRealizabilityTests
diff --git a/verification/aeneas/projections/TraitLaws.lean b/verification/aeneas/projections/TraitLaws.lean
index 152ded5181..4c7b510126 100644
--- a/verification/aeneas/projections/TraitLaws.lean
+++ b/verification/aeneas/projections/TraitLaws.lean
@@ -39,7 +39,8 @@ trait_invariant byte_roundtrip for @Zerocopy.trait_checks.ByteCodec with 1 type
       ⦃ result => result = byte ⦄
 
 trait_invariant into_bytes_initialized for @Zerocopy.IntoBytes with 1 type parameters where self =>
-  AeneasSpecs.RustModel.initializedRepresentation Self
+  AeneasSpecs.RustModel.initializedRepresentation Self ∧
+    AeneasSpecs.RustModel.realizableRepresentation Self
 
 trait_invariant from_bytes_valid for @Zerocopy.FromBytes with 1 type parameters where self =>
   AeneasSpecs.RustModel.completeRepresentation Self
diff --git a/zerocopy/src/lib.rs b/zerocopy/src/lib.rs
index 147d350695..58adfe171c 100644
--- a/zerocopy/src/lib.rs
+++ b/zerocopy/src/lib.rs
@@ -6012,7 +6012,8 @@ pub use zerocopy_derive::IntoBytes;
 )]
 /// ```aeneas
 /// invariant into_bytes_initialized for self =>
-///   AeneasSpecs.RustModel.initializedRepresentation Self
+///   AeneasSpecs.RustModel.initializedRepresentation Self ∧
+///   AeneasSpecs.RustModel.realizableRepresentation Self
 /// ```
 pub unsafe trait IntoBytes {
     // The `Self: Sized` bound makes it so that this function doesn't prevent