diff --git a/checkct/driver/Cargo.toml b/checkct/driver/Cargo.toml
index 00437a00..f82d92cd 100644
--- a/checkct/driver/Cargo.toml
+++ b/checkct/driver/Cargo.toml
@@ -6,7 +6,7 @@ edition = "2024"
 
 [dependencies]
 checkct_macros = { path = "../checkct_macros" }
-rsa = { path = "../..", default-features = false }
+rsa = { path = "../..", default-features = false, features = ["hazmat"] }
 crypto-bigint = { version = "0.7", default-features = false, features = ["alloc", "zeroize"] }
 zeroize = { version = "1.8", default-features = false, features = ["alloc"] }
 # RNG traits supplied by cargo-checkct's generated rng.rs.
diff --git a/checkct/driver/src/main.rs b/checkct/driver/src/main.rs
index 5a889d9b..238a7140 100644
--- a/checkct/driver/src/main.rs
+++ b/checkct/driver/src/main.rs
@@ -6,6 +6,9 @@ extern crate alloc;
 
 mod allocator;
 mod driver;
+// BINSEC 0.11.3 does not decode the RISC-V amoadd.w used by Arc::clone.
+#[cfg(not(target_arch = "riscv32"))]
+mod raw_rsa;
 
 // Compile the actual private helper without adding a public API for the harness.
 pub use rsa::errors;
diff --git a/checkct/driver/src/raw_rsa.rs b/checkct/driver/src/raw_rsa.rs
new file mode 100644
index 00000000..85caa376
--- /dev/null
+++ b/checkct/driver/src/raw_rsa.rs
@@ -0,0 +1,99 @@
+//! Small unblinded, non-CRT private operation through the public hazmat API.
+
+use crate::rng::{PrivateRng, PublicRng};
+use checkct_macros::checkct;
+use core::hint::black_box;
+use crypto_bigint::{
+    modular::{BoxedMontyForm, BoxedMontyParams, MontyParams},
+    BoxedUint, NonZero,
+};
+use rsa::{
+    hazmat::rsa_decrypt,
+    traits::{PrivateKeyParts, PublicKeyParts},
+    CrtValue, RsaPublicKey,
+};
+use zeroize::Zeroizing;
+
+#[checkct]
+pub fn rsa_decrypt_unblinded_non_crt_128() {
+    // SAFETY: This independent, single-threaded analysis has no live allocations.
+    unsafe { crate::allocator::reset() };
+
+    // Public modulus (2^64 - 59) * (2^64 - 83), with fixed 128-bit precision.
+    let n = BoxedUint::from_be_hex("FFFFFFFFFFFFFF720000000000001321", 128).unwrap();
+    let public = RsaPublicKey::new(n, BoxedUint::from(65537u64)).unwrap();
+
+    let mut bytes = [0u8; 16];
+    PrivateRng.fill_bytes(&mut bytes);
+    let key = NonCrtKey {
+        public,
+        d: Zeroizing::new(BoxedUint::from_be_slice(&bytes, 128).unwrap()),
+    };
+
+    PublicRng.fill_bytes(&mut bytes);
+    bytes[0] &= 0x7f; // Public ciphertext below 2^127 is below the modulus.
+    let c = BoxedUint::from_be_slice(&bytes, 128).unwrap();
+
+    // `None` disables blinding. The API processes all 128 exponent bits, including leading zeros.
+    // The fixture below selects the non-CRT path.
+    let m = rsa_decrypt::<PrivateRng>(None, &key, &c).unwrap();
+    black_box(m.as_limbs());
+    drop(m);
+    drop(key);
+}
+
+// Leave `d` unconstrained without including key validation or CRT precomputation in the analysis.
+// This fixture checks the private operation's arithmetic, not whether the supplied exponent forms a
+// valid RSA key.
+struct NonCrtKey {
+    public: RsaPublicKey,
+    d: Zeroizing<BoxedUint>,
+}
+
+impl PublicKeyParts for NonCrtKey {
+    fn n(&self) -> &NonZero<BoxedUint> {
+        self.public.n()
+    }
+
+    fn e(&self) -> &BoxedUint {
+        self.public.e()
+    }
+
+    fn n_params(&self) -> &BoxedMontyParams {
+        self.public.n_params()
+    }
+}
+
+impl PrivateKeyParts for NonCrtKey {
+    fn d(&self) -> &BoxedUint {
+        &self.d
+    }
+
+    fn primes(&self) -> &[BoxedUint] {
+        &[]
+    }
+
+    fn p(&self) -> Option<&MontyParams<BoxedUint>> {
+        None
+    }
+
+    fn q(&self) -> Option<&MontyParams<BoxedUint>> {
+        None
+    }
+
+    fn dp(&self) -> Option<&BoxedUint> {
+        None
+    }
+
+    fn dq(&self) -> Option<&BoxedUint> {
+        None
+    }
+
+    fn qinv(&self) -> Option<&BoxedMontyForm> {
+        None
+    }
+
+    fn crt_values(&self) -> Option<&[CrtValue]> {
+        None
+    }
+}