diff --git a/verification/aeneas/admission.py b/verification/aeneas/admission.py
index d450560b26..8189e05d4a 100644
--- a/verification/aeneas/admission.py
+++ b/verification/aeneas/admission.py
@@ -117,7 +117,7 @@ def __init__(self, data, registry, law_traits=()):
             if options[key] != expected:
                 raise ValueError(f'Unreviewed extraction option {key}: {options[key]!r}')
         stages = {variant(f['body'])[0] for f in self.functions.values()
-                  if f['body'] != 'Opaque'}
+                  if f['body'] != 'Opaque' and variant(f['body'])[0] != 'Intrinsic'}
         if len(stages) != 1 or not stages <= {'Unstructured', 'Structured'}:
             raise ValueError('Missing or mixed admission body stages')
         self.before = stages == {'Unstructured'}
@@ -263,6 +263,10 @@ def visit(self, index):
                 continue
             if kind == 'Builtin':
                 tag, _ = variant(detail)
+                if tag == 'RustcIntrinsic' and name == 'core::intrinsics::transmute':
+                    if function['body'] != {'Intrinsic': {'name': 'transmute', 'arg_names': ['src']}}:
+                        raise ValueError('Standard transmute intrinsic body changed')
+                    continue
                 if tag in {'Inline', 'TrackCaller'}:
                     continue
             elif kind == 'Unknown':
@@ -279,6 +283,17 @@ def visit(self, index):
         if matches:
             if len(matches) != 1:
                 raise ValueError(f'External interpretation signature changed: {name}')
+            if name == 'core::intrinsics::transmute':
+                expected_providers = {
+                    'u32->[u8;4]': 'Zerocopy.stdTransmuteU32ToBytes',
+                    '[u8;4]->u32': 'Zerocopy.stdTransmuteBytesToU32',
+                    'u8->bool': 'Zerocopy.stdTransmuteU8ToBool',
+                }
+                if (matches[0].get('interpretation_extension') != 'closed-implicit-owned-provider-v1'
+                        or matches[0].get('providers') != expected_providers
+                        or meta['is_local'] or function['body'] != {
+                            'Intrinsic': {'name': 'transmute', 'arg_names': ['src']}}):
+                    raise ValueError('Standard transmute reviewed boundary extension changed')
             # A builtin may replace a visible Rust body. Always select the
             # interpretation first, rather than approving the unused body.
             self.visited[index] = {'rust': name, 'origin': 'interpretation',
@@ -721,7 +736,22 @@ def block(self, block, unwind=False):
                         'usize', 'core::num::niche_types::NonZeroUsizeInner']
                     if actual != expected:
                         raise ValueError(f'Unsupported NonZero::new_unchecked instantiation {actual}')
-                self.calls.append({'caller': self.current, 'callee': name})
+                call_evidence = {'caller': self.current, 'callee': name}
+                if name == 'core::intrinsics::transmute':
+                    actual = [self.ty_name(ty) for ty in fn['generics']['types']]
+                    providers = {
+                        ('u32', '[u8;4]'): 'Zerocopy.stdTransmuteU32ToBytes',
+                        ('[u8;4]', 'u32'): 'Zerocopy.stdTransmuteBytesToU32',
+                        ('u8', 'bool'): 'Zerocopy.stdTransmuteU8ToBool',
+                    }
+                    if tuple(actual) not in providers:
+                        raise ValueError(f'Unsupported standard transmute instantiation {actual}')
+                    if fn['generics']['regions'] or fn['generics']['const_generics'] or fn['generics']['trait_refs']:
+                        raise ValueError('Standard transmute acquired additional generic arguments')
+                    call_evidence.update(type_arguments=actual,
+                                         provider=providers[tuple(actual)],
+                                         caller_def_id=self.current_function['def_id'])
+                self.calls.append(call_evidence)
                 self.visit(callee)
                 self.block(body['on_unwind'], True)
             elif tag == 'Assert':
@@ -837,7 +867,7 @@ def input_identity(root):
     for name, value in os.environ.items():
         if value and (name in {'RUSTFLAGS', 'CARGO_ENCODED_RUSTFLAGS',
                 'CARGO_BUILD_RUSTFLAGS', 'RUSTC', 'RUSTC_WRAPPER',
-                'RUSTC_WORKSPACE_WRAPPER', 'CHARON_ARGS'} or
+                'RUSTC_WORKSPACE_WRAPPER', 'CHARON_ARGS', 'CARGO_BUILD_TARGET'} or
                 re.fullmatch(r'CARGO_TARGET_.*_RUSTFLAGS', name)):
             raise ValueError(f'Unreviewed compiler override {name}')
     configs = []
@@ -856,7 +886,7 @@ def input_identity(root):
         # Conservative lexical check avoids implementing Cargo's precedence
         # rules. Even a dormant override is rejected, rather than guessed safe.
         text = '\n'.join(line.split('#', 1)[0] for line in path.read_text().splitlines())
-        if re.search(r'\b(rustflags|rustc|rustc-wrapper|rustc-workspace-wrapper)\b', text):
+        if re.search(r'\b(rustflags|rustc|rustc-wrapper|rustc-workspace-wrapper)\b|\b(?:build\.)?target\s*=', text):
             raise ValueError(f'Unreviewed Cargo compiler configuration: {path}')
     # Discovery and freshness use the same unconditional source inventory.
     # Cache-like names under src cannot hide newly added Rust specifications.
@@ -909,7 +939,7 @@ def inspect(root, work, roots, sources, body_digests=None, law_traits=()):
     guarded = {row['rust'] for row in registry
                if row.get('opaque') or row['signature']['unsafe']}
     def guarded_calls(stage):
-        return Counter((call['caller'], call['callee']) for call in stage['calls']
+        return Counter((call['caller'], call['callee'], tuple(call.get('type_arguments', []))) for call in stage['calls']
                        if call.get('callee') in guarded)
     missing = guarded_calls(reports['before']) - guarded_calls(reports['llbc'])
     if missing:
@@ -932,6 +962,8 @@ def guarded_calls(stage):
 def check_translation(work, evidence):
     text = (work / 'Zerocopy/FunsExternal_Template.lean').read_text()
     signatures = {
+        'core.intrinsics.transmute':
+            'axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst',
         'util.transmute_unchecked':
             'axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst',
         'util.copy_unchecked':
diff --git a/verification/aeneas/control_runner.py b/verification/aeneas/control_runner.py
index e5f67ee322..a4efbe3b3a 100644
--- a/verification/aeneas/control_runner.py
+++ b/verification/aeneas/control_runner.py
@@ -27,9 +27,9 @@
 import time
 
 FAMILIES = ('producers', 'authoring', 'trait-rounding', 'unsafe', 'coverage', 'abi',
-            'contracts', 'dependencies', 'admission', 'semantics')
+            'contracts', 'dependencies', 'admission', 'semantics', 'owned-std')
 MODELS = ('golden-verification', 'verification')
-FIXTURES = ('NegativeControl.lean', 'WeakOutcome.lean',
+FIXTURES = ('StdTransmuteAuditProbe.lean', 'NegativeControl.lean', 'WeakOutcome.lean',
             'RoundingConstructorControl.lean', 'RoundingDomainControl.lean',
             'Zerocopy/ScopeControl.lean', 'Zerocopy/ShapeControl.lean',
             'Zerocopy/ModelControl.lean', 'Proofs/WitnessOwnerControl.lean',
diff --git a/verification/aeneas/external.json b/verification/aeneas/external.json
index 2ce379ce23..d3c0e0f1ce 100644
--- a/verification/aeneas/external.json
+++ b/verification/aeneas/external.json
@@ -33,5 +33,6 @@
   {"rust": "core::num::{u32}::to_le_bytes", "signature": {"unsafe": false, "inputs": ["u32"], "output": "[u8;4]", "types": 0, "consts": 0}, "lean": "core.num.U32.to_le_bytes"},
   {"rust": "core::num::{usize}::MAX", "signature": {"unsafe": false, "inputs": [], "output": "usize", "types": 0, "consts": 0}, "lean": "Usize.MAX"},
   {"rust": "core::clone::impls::{core::clone::Clone<usize>}::clone", "signature": {"unsafe": false, "inputs": ["&usize"], "output": "usize", "types": 0, "consts": 0}, "lean": "core.clone.CloneUsize"},
-  {"rust": "core::num::niche_types::{core::clone::Clone<core::num::niche_types::NonZeroUsizeInner>}::clone", "signature": {"unsafe": false, "inputs": ["&core::num::niche_types::NonZeroUsizeInner"], "output": "core::num::niche_types::NonZeroUsizeInner", "types": 0, "consts": 0}, "lean": "core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone"}
+  {"rust": "core::num::niche_types::{core::clone::Clone<core::num::niche_types::NonZeroUsizeInner>}::clone", "signature": {"unsafe": false, "inputs": ["&core::num::niche_types::NonZeroUsizeInner"], "output": "core::num::niche_types::NonZeroUsizeInner", "types": 0, "consts": 0}, "lean": "core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone"},
+  {"rust": "core::intrinsics::transmute", "signature": {"unsafe": true, "inputs": ["T0"], "output": "T1", "types": 2, "consts": 0}, "lean": "core.intrinsics.transmute", "interpretation_extension": "closed-implicit-owned-provider-v1", "providers": {"u32->[u8;4]": "Zerocopy.stdTransmuteU32ToBytes", "[u8;4]->u32": "Zerocopy.stdTransmuteBytesToU32", "u8->bool": "Zerocopy.stdTransmuteU8ToBool"}}
 ]
diff --git a/verification/aeneas/golden/Funs.lean b/verification/aeneas/golden/Funs.lean
index 6b3f6d2cfc..e9976c0c69 100644
--- a/verification/aeneas/golden/Funs.lean
+++ b/verification/aeneas/golden/Funs.lean
@@ -792,7 +792,7 @@ def trait_checks.check_array_into_bytes : Result Unit := do
     (Array.Insts.ZerocopyIntoBytes 2#usize Bool.Insts.ZerocopyIntoBytes))
 
 /-- [zerocopy::util::padding_needed_for]:
-    Source: 'src/util/mod.rs', lines 163:0-223:1 -/
+    Source: 'src/util/mod.rs', lines 166:0-226:1 -/
 def util.padding_needed_for
   (len : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -808,7 +808,7 @@ def util.padding_needed_for
   ok (i2 &&& mask)
 
 /-- [zerocopy::util::round_down_to_next_multiple_of_alignment]:
-    Source: 'src/util/mod.rs', lines 250:0-268:1 -/
+    Source: 'src/util/mod.rs', lines 253:0-271:1 -/
 def util.round_down_to_next_multiple_of_alignment
   (n : Std.Usize)
   (align : core.num.nonzero.NonZero Std.Usize
@@ -825,7 +825,7 @@ def util.round_down_to_next_multiple_of_alignment
   ok (n &&& mask)
 
 /-- [zerocopy::util::max]:
-    Source: 'src/util/mod.rs', lines 277:0-283:1 -/
+    Source: 'src/util/mod.rs', lines 280:0-286:1 -/
 def util.max
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -845,7 +845,7 @@ def util.max
   else ok a
 
 /-- [zerocopy::util::min]:
-    Source: 'src/util/mod.rs', lines 292:0-298:1 -/
+    Source: 'src/util/mod.rs', lines 295:0-301:1 -/
 def util.min
   (a : core.num.nonzero.NonZero Std.Usize
   core.num.niche_types.NonZeroUsizeInner)
@@ -864,6 +864,41 @@ def util.min
   then ok b
   else ok a
 
+/-- [zerocopy::util::owned_transmute::to_bytes_native]:
+    Source: 'src/util/owned_transmute.rs', lines 29:0-33:1 -/
+def util.owned_transmute.to_bytes_native
+  (value : Std.U32) : Result (Array Std.U8 4#usize) := do
+  core.intrinsics.transmute (Array Std.U8 4#usize) value
+
+/-- [zerocopy::util::owned_transmute::to_bytes]:
+    Source: 'src/util/owned_transmute.rs', lines 22:0-24:1 -/
+def util.owned_transmute.to_bytes
+  (value : Std.U32) : Result (Array Std.U8 4#usize) := do
+  util.owned_transmute.to_bytes_native value
+
+/-- [zerocopy::util::owned_transmute::from_bytes]:
+    Source: 'src/util/owned_transmute.rs', lines 44:0-48:1 -/
+def util.owned_transmute.from_bytes
+  (bytes : Array Std.U8 4#usize) : Result Std.U32 := do
+  core.intrinsics.transmute Std.U32 bytes
+
+/-- [zerocopy::util::owned_transmute::checked_bool]:
+    Source: 'src/util/owned_transmute.rs', lines 59:0-67:1 -/
+def util.owned_transmute.checked_bool
+  (byte : Std.U8) : Result (Option Bool) := do
+  if byte < 2#u8
+  then let b ← core.intrinsics.transmute Bool byte
+       ok (some b)
+  else ok none
+
+/-- [zerocopy::util::owned_transmute::round_trip_checks]:
+    Source: 'src/util/owned_transmute.rs', lines 75:0-79:1 -/
+def util.owned_transmute.round_trip_checks
+  (value : Std.U32) : Result Unit := do
+  let bytes ← util.owned_transmute.to_bytes value
+  let restored ← util.owned_transmute.from_bytes bytes
+  massert (restored = value)
+
 /-- [zerocopy::util::safety_checks::checked_bool]:
     Source: 'src/util/safety_checks/mod.rs', lines 28:0-38:1 -/
 def util.safety_checks.checked_bool
diff --git a/verification/aeneas/golden/FunsExternal_Template.lean b/verification/aeneas/golden/FunsExternal_Template.lean
index fd2ceb84e7..2a05df9bda 100644
--- a/verification/aeneas/golden/FunsExternal_Template.lean
+++ b/verification/aeneas/golden/FunsExternal_Template.lean
@@ -28,6 +28,13 @@ set_option maxHeartbeats 1000000
 set_option maxRecDepth 2048
 open Zerocopy
 
+/-- [core::intrinsics::transmute]:
+    Source: '/rustc/library/core/src/intrinsics/mod.rs', lines 898:0-898:57
+    Name pattern: [core::intrinsics::transmute]
+    Visibility: public -/
+@[rust_fun "core::intrinsics::transmute"]
+axiom core.intrinsics.transmute {Src : Type} (Dst : Type) : Src → Result Dst
+
 /-- [core::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}::clone]:
     Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22
     Name pattern: [core::num::niche_types::{core::clone::Clone<core::num::niche_types::NonZeroUsizeInner>}::clone]
@@ -51,11 +58,11 @@ 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 310:0-325:1 -/
+    Source: 'src/util/mod.rs', lines 313:0-328:1 -/
 axiom util.copy_unchecked
   : Slice Std.U8 → Slice Std.U8 → Result (Slice Std.U8)
 
 /-- [zerocopy::util::transmute_unchecked]:
-    Source: 'src/util/mod.rs', lines 337:0-366:1 -/
+    Source: 'src/util/mod.rs', lines 340:0-369:1 -/
 axiom util.transmute_unchecked {Src : Type} (Dst : Type) : Src → Result Dst
 
diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean
index d40e9c042a..29ef24344a 100644
--- a/verification/aeneas/lean/Check.lean
+++ b/verification/aeneas/lean/Check.lean
@@ -72,6 +72,132 @@ private def checkUnemittedNativeType (env : Environment) (row : Json) : TermElab
       unless (generics.getObjValAs? (Array Json) field).toOption == some #[] do
         throwError "Unemitted native type has unsupported generic obligations: {rust}"
 
+-- This closed boundary adds an interpretation-only provider to the std
+-- primitive. Compare whole definitions independently of the functional proofs,
+-- then bind each reached native call (including unannotated helpers) to its
+-- original Rust endpoints and exact canonical provider.
+private partial def stdTransmuteCalls (expression : Expr) : Array Expr :=
+  if expression.getAppFn.isConstOf `core.intrinsics.transmute then
+    #[expression] ++ expression.getAppArgs.foldl
+      (fun found arg => found ++ stdTransmuteCalls arg) #[]
+  else
+    match expression with
+    | .app fn arg => stdTransmuteCalls fn ++ stdTransmuteCalls arg
+    | .lam _ ty body _ | .forallE _ ty body _ => stdTransmuteCalls ty ++ stdTransmuteCalls body
+    | .letE _ ty value body _ => stdTransmuteCalls ty ++ stdTransmuteCalls value ++ stdTransmuteCalls body
+    | .mdata _ body | .proj _ _ body => stdTransmuteCalls body
+    | _ => #[]
+
+private def auditStdTransmute (bindings : Json) : TermElabM Unit := do
+  let env ← getEnv
+  unless env.contains `core.intrinsics.transmute do return
+  let ctor ← Term.elabType (← `(∀ (Src Dst : Type),
+    (Src → Aeneas.Std.Result Dst) → Zerocopy.StdOwnedTransmute Src Dst))
+  let some (.ctorInfo classCtor) := env.find? `Zerocopy.StdOwnedTransmute.mk
+    | throwError "Standard transmute provider must retain its reviewed one-field carrier"
+  unless ← Meta.isDefEq classCtor.type ctor do
+    throwError "Standard transmute provider carrier changed"
+  let expectedType ← Term.elabType (← `(∀ {Src : Type} (Dst : Type)
+    [Zerocopy.StdOwnedTransmute Src Dst], Src → Aeneas.Std.Result Dst))
+  let expectedBody ← Term.elabTerm (← `(fun {Src : Type} (Dst : Type)
+    [provider : Zerocopy.StdOwnedTransmute Src Dst] (src : Src) => provider.run src)) none
+  Term.synthesizeSyntheticMVarsNoPostponing
+  let some (.defnInfo primitive) := env.find? `core.intrinsics.transmute
+    | throwError "Standard transmute interpretation must be a definition"
+  unless (← Meta.isDefEq primitive.type expectedType) &&
+      (← Meta.isDefEq primitive.value (← instantiateMVars expectedBody)) do
+    throwError "Standard transmute extended signature or whole interpretation changed"
+  let forward ← Term.elabTerm (← `(
+    ({ run := fun value => Aeneas.Std.Result.ok (Aeneas.Std.core.num.U32.to_le_bytes value) } :
+      Zerocopy.StdOwnedTransmute Aeneas.Std.U32 (Aeneas.Std.Array Aeneas.Std.U8 4#usize)))) none
+  let backward ← Term.elabTerm (← `(
+    ({ run := fun bytes => Aeneas.Std.Result.ok (Aeneas.Std.core.num.U32.from_le_bytes bytes) } :
+      Zerocopy.StdOwnedTransmute (Aeneas.Std.Array Aeneas.Std.U8 4#usize) Aeneas.Std.U32))) none
+  let boolean ← Term.elabTerm (← `(
+    ({ run := fun byte => if byte.val < 2 then Aeneas.Std.Result.ok (decide (byte.val = 1))
+        else Aeneas.Std.Result.fail Aeneas.Std.Error.undef } :
+      Zerocopy.StdOwnedTransmute Aeneas.Std.U8 Bool))) none
+  Term.synthesizeSyntheticMVarsNoPostponing
+  for (providerName, providerValue) in #[(`Zerocopy.stdTransmuteU32ToBytes, forward),
+      (`Zerocopy.stdTransmuteBytesToU32, backward), (`Zerocopy.stdTransmuteU8ToBool, boolean)] do
+    let some (.defnInfo provider) := env.find? providerName
+      | throwError "Standard transmute provider {providerName} must be a definition"
+    unless ← Meta.isDefEq provider.value (← instantiateMVars providerValue) do
+      throwError "Standard transmute provider {providerName} changed its whole interpretation"
+  let .ok admission := bindings.getObjVal? "admission"
+    | throwError "Standard transmute requires original compiler admission"
+  let .ok stages := admission.getObjVal? "stages"
+    | throwError "Standard transmute requires both compiler admission stages"
+  let .ok original := stages.getObjVal? "before"
+    | throwError "Standard transmute lacks original admission"
+  let .ok lowered := stages.getObjVal? "llbc"
+    | throwError "Standard transmute lacks lowered admission"
+  let .ok originalCalls := original.getObjValAs? (Array Json) "calls"
+    | throwError "Standard transmute lacks original call evidence"
+  let .ok loweredCalls := lowered.getObjValAs? (Array Json) "calls"
+    | throwError "Standard transmute lacks lowered call evidence"
+  let originalStd := originalCalls.filter fun row => row.getObjValAs? String "callee" == .ok "core::intrinsics::transmute"
+  let loweredStd := loweredCalls.filter fun row => row.getObjValAs? String "callee" == .ok "core::intrinsics::transmute"
+  -- Ordered type arguments identify source and destination independently;
+  -- preserve each call, its owner, and its multiplicity through lowering.
+  unless originalStd == loweredStd do
+    throwError "Standard transmute changed original ordered Rust endpoints or call ownership"
+  let .ok executions := lowered.getObjValAs? (Array Json) "executions"
+    | throwError "Standard transmute lacks the complete execution closure"
+  let nativeText ← IO.FS.readFile "Zerocopy/translation.json"
+  let .ok native := Json.parse nativeText | throwError "Invalid native primitive call map"
+  let .ok functions := native.getObjValAs? (Array Json) "functions"
+    | throwError "Missing native primitive function map"
+  for execution in executions do
+    if execution.getObjValAs? String "origin" != .ok "body" then continue
+    let .ok rust := execution.getObjValAs? String "rust" | throwError "Missing primitive call owner"
+    let expected := loweredStd.filter fun row => row.getObjValAs? String "caller" == .ok rust
+    let selected := functions.filter fun row => row.getObjValAs? String "rust_name" == .ok rust
+    -- General dictionary owners can have a different native spelling. Owners
+    -- with this boundary must have an exact producer identity from their call.
+    if expected.isEmpty && selected.isEmpty then continue
+    let candidates := if expected.isEmpty then selected else functions.filter fun row =>
+      expected.any (fun call => call.getObjValAs? Nat "caller_def_id" == row.getObjValAs? Nat "def_id")
+    unless !candidates.isEmpty do throwError "Missing compiled standard transmute owner {rust}"
+    -- Native loop splitting can emit several bodies for one Rust owner. Audit
+    -- their aggregate inventory rather than silently omitting the loop helper.
+    let mut actual : Array Expr := #[]
+    let mut names : Array Name := #[]
+    for candidate in candidates do
+      let .ok raw := candidate.getObjValAs? String "lean_name" | throwError "Missing native owner name"
+      unless !names.contains raw.toName do throwError "Repeated native primitive owner {raw}"
+      names := names.push raw.toName
+      let some (.defnInfo owner) := env.find? raw.toName
+        | throwError "Reached primitive owner {rust} must retain its compiled body"
+      actual := actual ++ stdTransmuteCalls owner.value
+    unless actual.size == expected.size do
+      throwError "Compiled standard transmute call inventory differs for {rust}"
+    -- Consume one original witness per compiled call. Repeated calls with the
+    -- same endpoints are legal, but neither omission nor duplication is legal.
+    let mut remaining := expected
+    for call in actual do
+      let args := call.getAppArgs
+      unless args.size == 4 do throwError "Standard transmute acquired unsupported compiled arguments"
+      let matching ← remaining.filterM fun row => do
+        let .ok types := row.getObjValAs? (Array String) "type_arguments" | throwError "Missing Rust endpoints"
+        let (source, target, canonical) ← match types.toList with
+          | ["u32", "[u8;4]"] => pure ((← Term.elabType (← `(Aeneas.Std.U32))),
+              (← Term.elabType (← `(Aeneas.Std.Array Aeneas.Std.U8 4#usize))), `Zerocopy.stdTransmuteU32ToBytes)
+          | ["[u8;4]", "u32"] => pure ((← Term.elabType (← `(Aeneas.Std.Array Aeneas.Std.U8 4#usize))),
+              (← Term.elabType (← `(Aeneas.Std.U32))), `Zerocopy.stdTransmuteBytesToU32)
+          | ["u8", "bool"] => pure ((← Term.elabType (← `(Aeneas.Std.U8))),
+              (← Term.elabType (← `(Bool))), `Zerocopy.stdTransmuteU8ToBool)
+          | _ => throwError "Unsupported original Rust standard transmute endpoints"
+        unless row.getObjValAs? String "provider" == .ok canonical.toString do
+          throwError "Original Rust endpoint provider binding changed"
+        return (← Meta.isDefEq args[0]! source) && (← Meta.isDefEq args[1]! target) &&
+          args[2]! == mkConst canonical
+      unless !matching.isEmpty do
+        throwError "Compiled standard transmute did not retain its canonical endpoint provider in {rust}"
+      let some selectedIndex := remaining.findIdx? (· == matching[0]!)
+        | throwError "Missing matched standard transmute call"
+      remaining := remaining.extract 0 selectedIndex ++ remaining.extract (selectedIndex + 1) remaining.size
+
 run_elab do
   let env ← getEnv
   let layoutInputs := #[`Zerocopy.RustLayout.size, `Zerocopy.RustLayout.alignInput]
@@ -301,6 +427,7 @@ run_elab do
         | throwError "Invalid {stage} execution admission roots"
       unless roots.size == rootNames.size && rootNames.all roots.contains do
         throwError "Execution admission roots disagree with the function binding table"
+  auditStdTransmute bindings
   let some typesModule := env.getModuleIdx? `Zerocopy.Types
     | throwError "Raw extracted types must be imported"
   let some shapesModule := env.getModuleIdx? `ModelShapes
diff --git a/verification/aeneas/lean/Obligations/OwnedTransmute.lean b/verification/aeneas/lean/Obligations/OwnedTransmute.lean
new file mode 100644
index 0000000000..242eaa11a4
--- /dev/null
+++ b/verification/aeneas/lean/Obligations/OwnedTransmute.lean
@@ -0,0 +1,40 @@
+/- Copyright 2026 The Fuchsia Authors
+SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT -/
+
+module
+public import Obligations.Byteorder
+@[expose] public section
+open Aeneas Aeneas.Std
+namespace Zerocopy.Obligations
+
+-- Retain the independent positional digit expectations used for numerical
+-- byteorder. These expectations inspect arbitrary outcomes, not executions.
+def owned_transmute_to_bytes_spec_contract (value : U32)
+    (run : Result (Aeneas.Std.Array U8 4#usize)) : Prop :=
+  write_u32_le_spec_contract value run
+
+def owned_transmute_to_bytes_spec : Prop :=
+  ∀ value, owned_transmute_to_bytes_spec_contract value (util.owned_transmute.to_bytes value)
+
+def owned_transmute_from_bytes_spec_contract (bytes : Aeneas.Std.Array U8 4#usize)
+    (run : Result U32) : Prop := read_u32_le_spec_contract bytes run
+
+def owned_transmute_from_bytes_spec : Prop :=
+  ∀ bytes, owned_transmute_from_bytes_spec_contract bytes (util.owned_transmute.from_bytes bytes)
+
+def owned_transmute_bool_spec_contract (byte : U8) (run : Result (Option Bool)) : Prop :=
+  run ⦃ output => match output with
+    | none => 2 ≤ byte.val
+    | some value => byte.val < 2 ∧ value = decide (byte.val = 1) ⦄
+
+def owned_transmute_bool_spec : Prop :=
+  ∀ byte, owned_transmute_bool_spec_contract byte (util.owned_transmute.checked_bool byte)
+
+def owned_transmute_round_trip_checks_spec_contract (_value : U32) (run : Result Unit) : Prop :=
+  run ⦃ _ => True ⦄
+
+def owned_transmute_round_trip_checks_spec : Prop :=
+  ∀ value, owned_transmute_round_trip_checks_spec_contract value
+    (util.owned_transmute.round_trip_checks value)
+
+end Zerocopy.Obligations
diff --git a/verification/aeneas/lean/Proofs/OwnedTransmute.lean b/verification/aeneas/lean/Proofs/OwnedTransmute.lean
new file mode 100644
index 0000000000..50cd71ebf5
--- /dev/null
+++ b/verification/aeneas/lean/Proofs/OwnedTransmute.lean
@@ -0,0 +1,108 @@
+/- Copyright 2026 The Fuchsia Authors
+SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT -/
+
+module
+public import Specs
+public import BytesAdapter
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs.Raw
+
+theorem owned_transmute_to_bytes (value : U32) :
+    util.owned_transmute.to_bytes value ⦃ bytes =>
+      bytes.val.map U8.bv = Rust.Bytes.encodeLE 4 value.val ⦄ := by
+  have actual : util.owned_transmute.to_bytes value =
+      .ok (core.num.U32.to_le_bytes value) := rfl
+  rw [actual]
+  simp only [WP.spec_ok]
+  have digits : (core.num.U32.to_le_bytes value).val.map U8.bv = value.bv.toLEBytes := by
+    simp only [core.num.U32.to_le_bytes, Array.from_val, List.map_map,
+      ↓U8.bv_UScalar_mk, List.map_id]
+  rw [digits]
+  exact Rust.Bytes.AeneasAdapter.toLEBytes_eq_encodeLE (by decide) value.bv
+
+theorem owned_transmute_from_bytes (bytes : Aeneas.Std.Array U8 4#usize) :
+    util.owned_transmute.from_bytes bytes ⦃ value =>
+      value.val = Rust.Bytes.decodeLE (bytes.val.map U8.bv) ⦄ := by
+  have actual : util.owned_transmute.from_bytes bytes =
+      .ok (core.num.U32.from_le_bytes bytes) := rfl
+  rw [actual]
+  simp only [WP.spec_ok, core.num.U32.from_le_bytes, UScalar.val, BitVec.toNat_cast]
+  exact Rust.Bytes.AeneasAdapter.fromLEBytes_toNat _
+
+theorem owned_transmute_bool (byte : U8) :
+    util.owned_transmute.checked_bool byte ⦃ output => match output with
+      | none => 2 ≤ byte.val
+      | some value => byte.val < 2 ∧ value = decide (byte.val = 1) ⦄ := by
+  have actual : core.intrinsics.transmute Bool byte =
+      if byte.val < 2 then .ok (decide (byte.val = 1)) else forbiddenExecution := rfl
+  unfold util.owned_transmute.checked_bool
+  simp only [UScalar.lt_equiv, UScalar.ofNatCore_val_eq]
+  by_cases below : byte.val < 2
+  · simp only [if_pos below]
+    rw [actual]
+    simp only [if_pos below, bind_ok, WP.spec_ok]
+    exact ⟨below, trivial⟩
+  · simp only [if_neg below, WP.spec_ok]
+    omega
+
+theorem owned_transmute_round_trip_checks (value : U32) :
+    util.owned_transmute.round_trip_checks value ⦃ _ => True ⦄ := by
+  have digits : (core.num.U32.to_le_bytes value).val.map U8.bv = value.bv.toLEBytes := by
+    simp only [core.num.U32.to_le_bytes, Array.from_val, List.map_map,
+      ↓U8.bv_UScalar_mk, List.map_id]
+  have identical : core.num.U32.from_le_bytes (core.num.U32.to_le_bytes value) = value := by
+    apply UScalar.eq_of_val_eq
+    change (BitVec.fromLEBytes ((core.num.U32.to_le_bytes value).val.map U8.bv)).toNat = value.bv.toNat
+    rw [digits, Rust.Bytes.AeneasAdapter.fromLEBytes_toNat]
+    exact Rust.Bytes.AeneasAdapter.decodeLE_toLEBytes (by decide) value.bv
+  have actualTo : util.owned_transmute.to_bytes value =
+      .ok (core.num.U32.to_le_bytes value) := rfl
+  have actualFrom : util.owned_transmute.from_bytes (core.num.U32.to_le_bytes value) =
+      .ok (core.num.U32.from_le_bytes (core.num.U32.to_le_bytes value)) := rfl
+  simp [util.owned_transmute.round_trip_checks, actualTo, actualFrom, identical, bind_ok]
+
+end Zerocopy.Proofs.Raw
+namespace Zerocopy.Proofs
+
+theorem owned_transmute_to_bytes_spec : Specs.owned_transmute_to_bytes_spec := by
+  intro value mathValue decoded
+  have same := (decodeUScalar_iff value mathValue).mp decoded
+  apply WP.spec_mono (Raw.owned_transmute_to_bytes value)
+  intro bytes facts
+  refine ⟨unsignedArray bytes, decodeArray_unsigned bytes, ?_⟩
+  change _ = Rust.Bytes.encodeLE 4 mathValue.value
+  rw [decodedArray_bytes_eq bytes (unsignedArray bytes) (decodeArray_unsigned bytes), ← same]
+  exact facts
+
+theorem owned_transmute_from_bytes_spec : Specs.owned_transmute_from_bytes_spec := by
+  intro bytes mathBytes decoded
+  apply WP.spec_mono (Raw.owned_transmute_from_bytes bytes)
+  intro value facts
+  refine ⟨unsignedWord value, rfl, ?_⟩
+  change value.val = _
+  rw [decodedArray_bytes_eq bytes mathBytes decoded]
+  exact facts
+
+theorem owned_transmute_bool_spec : Specs.owned_transmute_bool_spec := by
+  intro byte mathByte decoded
+  have same := (decodeUScalar_iff byte mathByte).mp decoded
+  apply WP.spec_mono (Raw.owned_transmute_bool byte)
+  intro output facts
+  refine ⟨output, ?_, ?_⟩
+  · cases output <;> rfl
+  · cases output <;> simpa only [← same] using facts
+
+theorem owned_transmute_round_trip_checks_spec : Specs.owned_transmute_round_trip_checks_spec := by
+  intro value _ _
+  apply WP.spec_mono (Raw.owned_transmute_round_trip_checks value)
+  intro _ _
+  exact ⟨(), rfl, trivial⟩
+
+-- Invalid representations must fail before constructing a Boolean, even for
+-- a True postcondition. Discarding the result cannot erase forbidden execution.
+example : ¬ (core.intrinsics.transmute Bool 2#u8 ⦃ _ => True ⦄) := by
+  change ¬ (Result.fail Error.undef : Result Bool) ⦃ _ => True ⦄
+  simp
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/RequiredModelContracts/OwnedTransmute.lean b/verification/aeneas/lean/RequiredModelContracts/OwnedTransmute.lean
new file mode 100644
index 0000000000..c2bc1ec339
--- /dev/null
+++ b/verification/aeneas/lean/RequiredModelContracts/OwnedTransmute.lean
@@ -0,0 +1,42 @@
+/- Copyright 2026 The Fuchsia Authors
+SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT -/
+
+module
+public import RequiredModelContracts.Byteorder
+public import Obligations.OwnedTransmute
+@[expose] public section
+open Aeneas Aeneas.Std AeneasSpecs
+namespace Zerocopy.Proofs
+
+-- These bridges reuse positional digit expectations, not implementation
+-- correctness. Every provided hypothesis is about the same arbitrary run.
+@[contract_simps] theorem required_owned_transmute_to_bytes (value : U32)
+    (run : Result (Aeneas.Std.Array U8 4#usize))
+    (provided : Specs.owned_transmute_to_bytes_spec_contract value run) :
+    Obligations.owned_transmute_to_bytes_spec_contract value run := by
+  exact required_write_u32_le value run provided
+
+@[contract_simps] theorem required_owned_transmute_from_bytes (bytes : Aeneas.Std.Array U8 4#usize)
+    (run : Result U32) (provided : Specs.owned_transmute_from_bytes_spec_contract bytes run) :
+    Obligations.owned_transmute_from_bytes_spec_contract bytes run := by
+  exact required_read_u32_le bytes run provided
+
+@[contract_simps] theorem required_owned_transmute_bool (byte : U8)
+    (run : Result (Option Bool)) (provided : Specs.owned_transmute_bool_spec_contract byte run) :
+    Obligations.owned_transmute_bool_spec_contract byte run := by
+  apply WP.spec_mono (provided (unsignedWord byte) rfl)
+  rintro output ⟨value, decoded, facts⟩
+  have identityDecode : RustModel.decode output = some output := by
+    cases output <;> rfl
+  have same : value = output := Option.some.inj (decoded.symm.trans identityDecode)
+  subst value
+  cases output <;> exact facts
+
+@[contract_simps] theorem required_owned_transmute_round_trip_checks (value : U32)
+    (run : Result Unit) (provided : Specs.owned_transmute_round_trip_checks_spec_contract value run) :
+    Obligations.owned_transmute_round_trip_checks_spec_contract value run := by
+  apply WP.spec_mono (provided (unsignedWord value) rfl)
+  rintro _ ⟨_, _, _⟩
+  trivial
+
+end Zerocopy.Proofs
diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean
index 23aed8ce7f..68313fb2df 100644
--- a/verification/aeneas/lean/Zerocopy/FunsExternal.lean
+++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean
@@ -54,6 +54,34 @@ noncomputable def util.transmute_unchecked {Src : Type} (Dst : Type)
     else forbiddenExecution
   else forbiddenExecution
 
+-- The standard primitive uses a closed, interpretation-only provider. Original
+-- Rust endpoint admission and compiled call auditing bind every reached use to
+-- one of these fixed providers; no arbitrary dictionary enters a Rust root.
+-- This preserves endpoint identity without testing equality of erased Types.
+class Zerocopy.StdOwnedTransmute (Src Dst : Type) where
+  run : Src → Result Dst
+
+instance Zerocopy.stdTransmuteU32ToBytes :
+    Zerocopy.StdOwnedTransmute U32 (Array U8 4#usize) where
+  run value := .ok (core.num.U32.to_le_bytes value)
+
+instance Zerocopy.stdTransmuteBytesToU32 :
+    Zerocopy.StdOwnedTransmute (Array U8 4#usize) U32 where
+  run bytes := .ok (core.num.U32.from_le_bytes bytes)
+
+instance Zerocopy.stdTransmuteU8ToBool : Zerocopy.StdOwnedTransmute U8 Bool where
+  run byte := if byte.val < 2 then .ok (decide (byte.val = 1)) else forbiddenExecution
+
+-- The additional implicit parameter is explicitly part of the reviewed std
+-- boundary, not a translated Rust trait argument. Other endpoints are rejected
+-- by admission and have no registered provider. The numeric cases require the
+-- independently checked little-endian compiler profile; Boolean validity does
+-- not depend on byte order.
+def core.intrinsics.transmute {Src : Type} (Dst : Type)
+    [provider : Zerocopy.StdOwnedTransmute Src Dst] (src : Src) : Result Dst :=
+  provider.run src
+
+
 @[simp] def core.num.nonzero.NonZero.get
     {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner)
     (x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val
diff --git a/verification/aeneas/negative-control-family.sh b/verification/aeneas/negative-control-family.sh
index 77cc4aa6d2..3db0053065 100644
--- a/verification/aeneas/negative-control-family.sh
+++ b/verification/aeneas/negative-control-family.sh
@@ -24,7 +24,7 @@ echo "Testing failure controls in $1"
 # suite starts and is removed on exit. Use the same roster for both decisions
 # so cleanup cannot delete a source that belonged to an earlier editor session.
 control_files=(
-    NegativeControl.lean WeakOutcome.lean
+    StdTransmuteAuditProbe.lean NegativeControl.lean WeakOutcome.lean
     RoundingConstructorControl.lean RoundingDomainControl.lean
     Zerocopy/ScopeControl.lean Zerocopy/ShapeControl.lean Zerocopy/ModelControl.lean
     Proofs/WitnessOwnerControl.lean Proofs/PaddingDependencyControl.lean
@@ -822,13 +822,16 @@ if grep -Fq 'def core.mem.align_of' Zerocopy/FunsExternal.lean; then
     python3 - <<'PYCONTROL'
 from pathlib import Path
 s = Path("Check.lean").read_text()
-begin = '  let env ← getEnv\n'
+# Select the top-level audit command. The standalone probe consumes the carrier
+# set because its normal consumer follows this prefix in the full audit.
+begin = 'run_elab do\n  let env ← getEnv\n'
 end = '  let mut proofModules : Array ModuleIdx := #[]'
 if s.count(begin) != 1 or s.count(end) != 1:
     raise SystemExit("External-input audit control boundaries no longer match")
-body = s[s.index(begin):s.index(end)]
+body = s[s.index(begin) + len('run_elab do\n'):s.index(end)]
 Path("NegativeControl.lean").write_text(
-    'import Lean\nimport Zerocopy.FunsExternal\nopen Lean Elab Command\nrun_elab do\n' + body)
+    'import Lean\nimport Zerocopy.FunsExternal\nopen Lean Elab Command\nrun_elab do\n' + body +
+    '  let _ := opaqueCarriers\n  pure ()\n')
 PYCONTROL
     aeneas_lake env lean -DwarningAsError=true NegativeControl.lean \
         > "$backup/abi-baseline.log" 2>&1 || {
@@ -1572,6 +1575,15 @@ expect_failure "a min implementation with its comparison reversed" min-build.log
 restore_build
 audit
 fi # semantics
+if [[ $AENEAS_CONTROL_FAMILY == owned-std ]] && has_model util.owned_transmute.to_bytes; then
+    # This family has its own frozen project and preserves exact command logs.
+    # Standard-boundary controls inspect original endpoints in both compiler
+    # stages, then challenge whole definitions and canonical native providers.
+    python3 -B "$repo/verification/aeneas/control_runner.py" command \
+        "$AENEAS_CONTROL_LOG_DIR/commands" -- python3 -B \
+        "$repo/verification/aeneas/tests/std_transmute_controls.py" \
+        --work "$PWD" --runtime "$tools_dir" --evidence "$backup/owned-std-evidence"
+fi
 control_complete=yes
 )
 check_workspace "$AENEAS_CONTROL_MODEL"
diff --git a/verification/aeneas/projections/Specs.lean b/verification/aeneas/projections/Specs.lean
index 5911ea7f12..8992e2fb55 100644
--- a/verification/aeneas/projections/Specs.lean
+++ b/verification/aeneas/projections/Specs.lean
@@ -184,6 +184,42 @@ spec min_spec
 aeneas_spec_end
 check_spec_binding Zerocopy.Specs.min_spec for Zerocopy.util.min with 2
 
+check_model_inputs Zerocopy.util.owned_transmute.to_bytes with 0 type parameters
+aeneas_spec_begin
+spec owned_transmute_to_bytes_spec
+  for @Zerocopy.util.owned_transmute.to_bytes with 0 type parameters
+  ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) =
+    Rust.Bytes.encodeLE 4 (value : Nat)
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.owned_transmute_to_bytes_spec for Zerocopy.util.owned_transmute.to_bytes with 1
+
+check_model_inputs Zerocopy.util.owned_transmute.from_bytes with 0 type parameters
+aeneas_spec_begin
+spec owned_transmute_from_bytes_spec
+  for @Zerocopy.util.owned_transmute.from_bytes with 0 type parameters
+  ensures value => (value : Nat) = Rust.Bytes.decodeLE
+    (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)))
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.owned_transmute_from_bytes_spec for Zerocopy.util.owned_transmute.from_bytes with 1
+
+check_model_inputs Zerocopy.util.owned_transmute.checked_bool with 0 type parameters
+aeneas_spec_begin
+spec owned_transmute_bool_spec
+  for @Zerocopy.util.owned_transmute.checked_bool with 0 type parameters
+  ensures output => match output with
+    | none => 2 ≤ (byte : Nat)
+    | some value => (byte : Nat) < 2 ∧ value = decide ((byte : Nat) = 1)
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.owned_transmute_bool_spec for Zerocopy.util.owned_transmute.checked_bool with 1
+
+check_model_inputs Zerocopy.util.owned_transmute.round_trip_checks with 0 type parameters
+aeneas_spec_begin
+spec owned_transmute_round_trip_checks_spec
+  for @Zerocopy.util.owned_transmute.round_trip_checks with 0 type parameters
+  ensures _ => True
+aeneas_spec_end
+check_spec_binding Zerocopy.Specs.owned_transmute_round_trip_checks_spec for Zerocopy.util.owned_transmute.round_trip_checks with 1
+
 check_model_inputs Zerocopy.util.safety_checks.checked_bool with 0 type parameters
 aeneas_spec_begin
 spec checked_bool_spec
diff --git a/verification/aeneas/tests/std_transmute_controls.py b/verification/aeneas/tests/std_transmute_controls.py
new file mode 100644
index 0000000000..3b32c4eef9
--- /dev/null
+++ b/verification/aeneas/tests/std_transmute_controls.py
@@ -0,0 +1,173 @@
+# Copyright 2026 The Fuchsia Authors
+# SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+
+"""Challenge standard-transmute endpoint admission and compiled providers.
+
+Compiler mutations stay in memory. Lean mutations affect only a disposable
+project and are restored and rebuilt. No invalid Rust execution is performed.
+"""
+
+import argparse
+import copy
+import json
+import os
+from pathlib import Path
+import subprocess
+import sys
+
+ROOT = Path(__file__).resolve().parents[3]
+sys.path.insert(0, str(ROOT / 'verification/aeneas'))
+import admission
+import toolchain
+
+
+def nodes(value):
+    if isinstance(value, dict):
+        yield value
+        for child in value.values():
+            yield from nodes(child)
+    elif isinstance(value, list):
+        for child in value:
+            yield from nodes(child)
+
+
+def admission_controls(work, evidence):
+    registry = json.loads((ROOT / 'verification/aeneas/external.json').read_text())
+    manifest = json.loads((work / 'bindings.json').read_text())
+    laws = [row['rust'] for row in manifest['trait_laws']]
+    owner = 'zerocopy::util::owned_transmute::to_bytes'
+    for stage, filename in [('before', 'zerocopy.before.ullbc'), ('llbc', 'zerocopy.llbc')]:
+        data = json.loads((work / filename).read_text())
+        baseline = admission.Admission(data, registry, laws)
+        baseline.audit([owner])
+        helper = next(f for f in baseline.functions.values()
+                      if baseline.name(f['item_meta']['name']) == owner + '_native')
+        intrinsic = next(i for i, f in baseline.functions.items()
+                         if baseline.name(f['item_meta']['name']) == 'core::intrinsics::transmute')
+        calls = [node['Regular'] for node in nodes(helper['body'])
+                 if node.get('Regular', {}).get('kind', {}).get('Fun') == intrinsic]
+        if len(calls) != 1:
+            raise ValueError('Expected one standard call in the actual unannotated helper')
+        original = copy.deepcopy(calls[0]['generics']['types'])
+        calls[0]['generics']['types'][0] = {'Untagged': {'Scalar': {
+            'Integer': {'Unsigned': 'U16'}}}}
+        try:
+            admission.Admission(data, registry, laws).audit([owner])
+        except ValueError as error:
+            if 'Unsupported standard transmute instantiation' not in str(error):
+                raise ValueError('Endpoint mutation failed outside its intended guard') from error
+            evidence.append({'case': stage + '-unsupported-endpoint', 'rejection': str(error)})
+        else:
+            raise ValueError('Accepted an unsupported original Rust endpoint')
+        finally:
+            calls[0]['generics']['types'] = original
+        for key, bad in [('is_little_endian', False), ('target_pointer_size', 4)]:
+            target = data['translated']['target_information'][0]['value']
+            old = target[key]
+            target[key] = bad
+            try:
+                admission.Admission(data, registry, laws)
+            except ValueError as error:
+                if 'little-endian 64-bit target' not in str(error):
+                    raise
+                evidence.append({'case': stage + '-' + key, 'rejection': str(error)})
+            else:
+                raise ValueError('Accepted an unsupported original target profile')
+            finally:
+                target[key] = old
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--work', type=Path, required=True)
+    parser.add_argument('--runtime', type=Path, required=True)
+    parser.add_argument('--evidence', type=Path, required=True)
+    args = parser.parse_args()
+    work, runtime, output = args.work.resolve(), args.runtime.resolve(), args.evidence.resolve()
+    standard = work in [ROOT / 'target/aeneas/verification', ROOT / 'target/aeneas/golden-verification']
+    private = (work.name == 'project' and work.parent.parent.name.startswith('control-sandboxes-')
+               and work.parent.parent.parent == ROOT / 'target/aeneas'
+               and os.environ.get('AENEAS_CONTROL_PROJECT') == str(work)
+               and os.environ.get('AENEAS_CONTROL_REPO') == str(ROOT))
+    if not (standard or private):
+        raise ValueError('Controls require a disposable verification project')
+    toolchain.validate(ROOT, runtime)
+    output.mkdir(parents=True, exist_ok=False)
+    environment = toolchain.runtime_env(runtime)
+    environment['LEAN_NUM_THREADS'] = '2'
+    results = []
+    admission_controls(work, results)
+    source = (ROOT / 'verification/aeneas/lean/Check.lean').read_text()
+    begin = source.index('-- This closed boundary')
+    end = source.index('run_elab do\n')
+    probe = work / 'StdTransmuteAuditProbe.lean'
+    if probe.exists() or probe.is_symlink():
+        raise ValueError('Control probe already belongs to an earlier session')
+    probe.write_text('import Lean\nimport Zerocopy.Funs\nopen Lean Elab Command\n' + source[begin:end] +
+        'run_elab do\n  let contents ← IO.FS.readFile "bindings.json"\n'
+        '  let .ok bindings := Json.parse contents | throwError "Invalid control bindings"\n'
+        '  auditStdTransmute bindings\n')
+    external, native = work / 'Zerocopy/FunsExternal.lean', work / 'Zerocopy/Funs.lean'
+    originals = {external: external.read_text(), native: native.read_text()}
+    start = originals[external].index('instance Zerocopy.stdTransmuteU8ToBool :')
+    end = originals[external].index('\n-- The additional implicit parameter', start)
+    boolean = originals[external][start:end]
+    if boolean.count('else forbiddenExecution') != 1:
+        raise ValueError('Boolean provider control boundary changed')
+
+    def run(label, command, expected=''):
+        log = output / (label + '.log')
+        with log.open('w') as stream:
+            result = subprocess.run(command, cwd=work, env=environment,
+                                    stdout=stream, stderr=subprocess.STDOUT)
+        contents = log.read_text()
+        results.append({'case': label, 'command': command, 'exit_code': result.returncode,
+                        'log': str(log), 'expected_rejection': expected})
+        if expected:
+            if result.returncode == 0 or expected not in contents:
+                raise ValueError(f'{label} did not fail at its intended audit: {log}')
+        elif result.returncode:
+            raise ValueError(f'{label} failed: {log}')
+
+    build = ['lake', '--old', 'build', '+Zerocopy.Funs:olean']
+    audit = ['lake', '--old', 'env', 'lean', '-DwarningAsError=true', probe.name]
+    try:
+        run('positive-audit', audit)
+        for case in ['failure-erasure', 'opaque-provider', 'shadow-provider']:
+            for path, text in originals.items():
+                path.write_text(text)
+            if case == 'failure-erasure':
+                external.write_text(originals[external][:start] +
+                    boolean.replace('else forbiddenExecution', 'else .ok false') + originals[external][end:])
+                rejection = 'changed its whole interpretation'
+            elif case == 'opaque-provider':
+                external.write_text(originals[external][:start] +
+                    'axiom Zerocopy.stdTransmuteU8ToBool : Zerocopy.StdOwnedTransmute U8 Bool\n'
+                    'attribute [instance] Zerocopy.stdTransmuteU8ToBool\n' + originals[external][end:])
+                rejection = 'must be a definition'
+            else:
+                external.write_text(originals[external] +
+                    '\n@[reducible] def Zerocopy.shadowStdProvider :\n'
+                    '    Zerocopy.StdOwnedTransmute U32 (Array U8 4#usize) :=\n'
+                    '  Zerocopy.stdTransmuteU32ToBytes\n')
+                needle = 'core.intrinsics.transmute (Array Std.U8 4#usize) value'
+                if originals[native].count(needle) != 1:
+                    raise ValueError('Expected one native primitive call in the unannotated helper')
+                native.write_text(originals[native].replace(needle,
+                    'core.intrinsics.transmute (Array Std.U8 4#usize) (provider := Zerocopy.shadowStdProvider) value'))
+                rejection = 'did not retain its canonical endpoint provider'
+            run(case + '-elaboration', build)
+            run(case + '-rejection', audit, rejection)
+    finally:
+        for path, text in originals.items():
+            path.write_text(text)
+        try:
+            run('restored-native-elaboration', build)
+            run('restored-positive-audit', audit)
+        finally:
+            probe.unlink(missing_ok=True)
+            (output / 'evidence.json').write_text(json.dumps({'restored': True, 'results': results}, indent=2) + '\n')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/verification/aeneas/tests/test_admission.py b/verification/aeneas/tests/test_admission.py
index eaef9e4f31..de8ef8409f 100644
--- a/verification/aeneas/tests/test_admission.py
+++ b/verification/aeneas/tests/test_admission.py
@@ -240,6 +240,18 @@ def test_compiler_override_is_rejected_before_compilation(self):
             with self.assertRaisesRegex(ValueError, 'compiler override RUSTFLAGS'):
                 admission.input_identity(ROOT)
 
+    def test_target_override_is_rejected_before_compilation(self):
+        with mock.patch.dict(os.environ, {'CARGO_BUILD_TARGET': 'aarch64-apple-darwin'}, clear=True):
+            with self.assertRaisesRegex(ValueError, 'compiler override CARGO_BUILD_TARGET'):
+                admission.input_identity(ROOT)
+        with tempfile.TemporaryDirectory() as directory:
+            root = Path(directory)
+            (root / '.cargo').mkdir()
+            (root / '.cargo/config.toml').write_text('[build]\ntarget = "powerpc64-unknown-linux-gnu"\n')
+            with mock.patch.dict(os.environ, {'CARGO_HOME': str(root / 'cargo')}, clear=True):
+                with self.assertRaisesRegex(ValueError, 'Cargo compiler configuration'):
+                    admission.input_identity(root)
+
     def test_nonzero_constructor_template_preserves_guarded_result_and_dictionary(self):
         leaf = 'core.num.nonzero.NonZero.new_unchecked'
         evidence = {'stages': {'llbc': {'executions': [{'rust': 'std constructor', 'lean': leaf}]}}}
diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs
index 8235c0f3d1..e9167686c1 100644
--- a/zerocopy/src/util/mod.rs
+++ b/zerocopy/src/util/mod.rs
@@ -14,6 +14,9 @@ pub(crate) mod macros;
 #[doc(hidden)]
 pub mod macro_util;
 
+#[cfg(target_endian = "little")]
+#[allow(dead_code)]
+mod owned_transmute;
 mod safety_checks;
 
 use core::{
diff --git a/zerocopy/src/util/owned_transmute.rs b/zerocopy/src/util/owned_transmute.rs
new file mode 100644
index 0000000000..1f5eb2d5f2
--- /dev/null
+++ b/zerocopy/src/util/owned_transmute.rs
@@ -0,0 +1,104 @@
+// Copyright 2026 The Fuchsia Authors
+// SPDX-License-Identifier: BSD-2-Clause OR Apache-2.0 OR MIT
+//
+// 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.
+
+//! Concrete owned conversions through the standard transmute primitive.
+//!
+//! This private verification module is selected only on little-endian targets.
+//! Verification separately checks the original compiler target and rejects
+//! unsupported target overrides. These types have no padding or pointer fields.
+
+/// Preserves all four bytes of the original integer.
+///
+/// ```aeneas
+/// spec owned_transmute_to_bytes_spec
+///   ensures bytes => bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)) =
+///     Rust.Bytes.encodeLE 4 (value : Nat)
+/// ```
+fn to_bytes(value: u32) -> [u8; 4] {
+    to_bytes_native(value)
+}
+
+// This unannotated helper remains in the checked execution closure.
+#[allow(unknown_lints)] // unnecessary_transmutes is newer than the MSRV.
+#[allow(unnecessary_transmutes)]
+fn to_bytes_native(value: u32) -> [u8; 4] {
+    // SAFETY: Both types have size four, contain no padding, and accept every
+    // bit pattern. Transmute moves the representation into the owned result.
+    unsafe { core::mem::transmute::<u32, [u8; 4]>(value) }
+}
+
+/// Interprets every initialized four-byte representation as an integer.
+///
+/// ```aeneas
+/// spec owned_transmute_from_bytes_spec
+///   ensures value => (value : Nat) = Rust.Bytes.decodeLE
+///     (bytes.val.map (fun b => BitVec.ofNat 8 (b : Nat)))
+/// ```
+#[allow(unknown_lints)] // unnecessary_transmutes is newer than the MSRV.
+#[allow(unnecessary_transmutes)]
+fn from_bytes(bytes: [u8; 4]) -> u32 {
+    // SAFETY: Both types have size four, contain no padding, and accept every
+    // bit pattern. No pointer, borrow, or destructor crosses this conversion.
+    unsafe { core::mem::transmute::<[u8; 4], u32>(bytes) }
+}
+
+/// Checks Boolean validity before invoking the standard primitive.
+///
+/// ```aeneas
+/// spec owned_transmute_bool_spec
+///   ensures output => match output with
+///     | none => 2 ≤ (byte : Nat)
+///     | some value => (byte : Nat) < 2 ∧ value = decide ((byte : Nat) = 1)
+/// ```
+#[allow(clippy::transmute_int_to_bool)] // Exercise the standard primitive itself.
+fn checked_bool(byte: u8) -> Option<bool> {
+    if byte < 2 {
+        // SAFETY: u8 and bool have size one and no padding. The guard admits
+        // exactly Boolean representations zero and one before construction.
+        Some(unsafe { core::mem::transmute::<u8, bool>(byte) })
+    } else {
+        None
+    }
+}
+
+/// Checks the complete owned integer round trip.
+///
+/// ```aeneas
+/// spec owned_transmute_round_trip_checks_spec
+///   ensures _ => True
+/// ```
+fn round_trip_checks(value: u32) {
+    let bytes = to_bytes(value);
+    let restored = from_bytes(bytes);
+    assert!(restored == value);
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn concrete_examples() {
+        for value in [0, 1, 0x1234_5678, u32::MAX] {
+            assert_eq!(to_bytes(value), value.to_le_bytes());
+            assert_eq!(from_bytes(value.to_le_bytes()), value);
+            round_trip_checks(value);
+        }
+        for byte in 0..=u8::MAX {
+            assert_eq!(
+                checked_bool(byte),
+                match byte {
+                    0 => Some(false),
+                    1 => Some(true),
+                    _ => None,
+                }
+            );
+        }
+    }
+}