diff --git a/lean/VerifiedGarbage/TCB/AArch64/Target.lean b/lean/VerifiedGarbage/TCB/AArch64/Target.lean
index d02c420bb..dd1ab4de9 100644
--- a/lean/VerifiedGarbage/TCB/AArch64/Target.lean
+++ b/lean/VerifiedGarbage/TCB/AArch64/Target.lean
@@ -96,7 +96,10 @@ abbrev target : Target where
   isa := isa
   printer := printer
   abiPreserved := abiPreserved
-  rustCfg := "target_arch = \"aarch64\""
+  -- `aarch64_be` targets are big-endian, and ILP32 ones (`aarch64-unknown-linux-gnu_ilp32`)
+  -- have 32-bit pointers.
+  rustCfg := "all(target_arch = \"aarch64\", target_endian = \"little\", \
+    target_pointer_width = \"64\")"
   rustAbi := "C"
   abi := abi
 
diff --git a/lean/VerifiedGarbage/TCB/Arm/Target.lean b/lean/VerifiedGarbage/TCB/Arm/Target.lean
index bf381c2f8..f9665701b 100644
--- a/lean/VerifiedGarbage/TCB/Arm/Target.lean
+++ b/lean/VerifiedGarbage/TCB/Arm/Target.lean
@@ -114,7 +114,8 @@ abbrev target : Target where
   isa := isa
   printer := printer
   abiPreserved := abiPreserved
-  rustCfg := "target_arch = \"arm\""
+  -- `armeb` targets are big-endian.
+  rustCfg := "all(target_arch = \"arm\", target_endian = \"little\")"
   rustAbi := "C"
   abi := abi
 
diff --git a/lean/VerifiedGarbage/TCB/Artifact.lean b/lean/VerifiedGarbage/TCB/Artifact.lean
index 41498ae2c..d871652a5 100644
--- a/lean/VerifiedGarbage/TCB/Artifact.lean
+++ b/lean/VerifiedGarbage/TCB/Artifact.lean
@@ -43,7 +43,11 @@ structure Target where
   returns, relating the entry state to the exit state (callee-saved
   registers and the stack pointer restored, return address intact). -/
   abiPreserved : isa.State → isa.State → Prop
-  /-- The Rust `cfg` predicate under which this target's functions are compiled. -/
+  /-- The Rust `cfg` predicate under which this target's functions are
+  compiled. It must exclude every configuration of the architecture that the
+  model does not describe: memory is little-endian in every ISA model
+  (`TCB/Mem.lean`), and pointers have `abi`'s width (`Abi.ptrBits`), which
+  the contracts assume. -/
   rustCfg : String
   /-- The Rust ABI string of the generated functions (e.g. `sysv64`). -/
   rustAbi : String
diff --git a/lean/VerifiedGarbage/TCB/X86_64/Target.lean b/lean/VerifiedGarbage/TCB/X86_64/Target.lean
index b25434294..ce11cb0a5 100644
--- a/lean/VerifiedGarbage/TCB/X86_64/Target.lean
+++ b/lean/VerifiedGarbage/TCB/X86_64/Target.lean
@@ -103,7 +103,8 @@ abbrev target : Target where
   isa := isa
   printer := printer
   abiPreserved := abiPreserved
-  rustCfg := "target_arch = \"x86_64\""
+  -- x32 targets (`x86_64-unknown-linux-gnux32`) have 32-bit pointers.
+  rustCfg := "all(target_arch = \"x86_64\", target_pointer_width = \"64\")"
   rustAbi := "sysv64"
   abi := abi
 
diff --git a/src/asm/mod.rs b/src/asm/mod.rs
index b758e2b71..2ff1de918 100644
--- a/src/asm/mod.rs
+++ b/src/asm/mod.rs
@@ -5,11 +5,11 @@
 //! whose machine code has been proven correct, memory safe and constant time
 //! against its contract.
 
-#[cfg(target_arch = "aarch64")]
+#[cfg(all(target_arch = "aarch64", target_endian = "little", target_pointer_width = "64"))]
 #[rustfmt::skip]
 pub(crate) mod aarch64;
 
-#[cfg(target_arch = "arm")]
+#[cfg(all(target_arch = "arm", target_endian = "little"))]
 #[rustfmt::skip]
 pub(crate) mod arm;
 
@@ -17,6 +17,6 @@ pub(crate) mod arm;
 #[rustfmt::skip]
 pub(crate) mod x86;
 
-#[cfg(target_arch = "x86_64")]
+#[cfg(all(target_arch = "x86_64", target_pointer_width = "64"))]
 #[rustfmt::skip]
 pub(crate) mod x86_64;
diff --git a/src/lib.rs b/src/lib.rs
index 8c7c4c909..6b3991786 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -32,6 +32,25 @@ use asm::x86 as arch;
 #[cfg(target_arch = "x86_64")]
 use asm::x86_64 as arch;
 
+// The ISA models are little-endian, and the contracts assume the pointer
+// width of each architecture's calling convention: the verified assembly is
+// compiled only where both hold (each target's `rustCfg`, in
+// `lean/VerifiedGarbage/TCB/<Target>/Target.lean`), not on aarch64_be, armeb
+// or x32.
+#[cfg(any(
+    all(
+        any(target_arch = "aarch64", target_arch = "arm"),
+        target_endian = "big"
+    ),
+    all(
+        any(target_arch = "aarch64", target_arch = "x86_64"),
+        target_pointer_width = "32"
+    ),
+))]
+compile_error!(
+    "the verified assembly needs a little-endian target with its architecture's usual pointer width (not, e.g., aarch64_be or x32)"
+);
+
 // The 32-bit x86 model's baseline is i686 with SSE2 (see
 // `lean/VerifiedGarbage/TCB/X86/Isa.lean`): older CPUs' `mul` is not constant
 // time.