diff --git a/src/boot/vmm.c b/src/boot/vmm.c
index 902f61b41c..e571a3990d 100644
--- a/src/boot/vmm.c
+++ b/src/boot/vmm.c
@@ -225,14 +225,10 @@ static bool detect_sev(void) {
 }
 
 static bool detect_tdx(void) {
-        uint32_t eax, ebx, ecx, edx;
         char sig[13] = {};
 
-        __cpuid(CPUID_GET_HIGHEST_FUNCTION, eax, ebx, ecx, edx);
-
-        if (eax < CPUID_INTEL_TDX_ENUMERATION)
-                return false;
-
+        /* Querying an unsupported CPUID leaf is harmless (it returns the highest basic leaf's data rather
+         * than faulting), so reading this leaf and matching the IntelTDX signature is sufficient. */
         cpuid_leaf(CPUID_INTEL_TDX_ENUMERATION, sig, true);
 
         if (memcmp(sig, CPUID_SIG_INTEL_TDX, sizeof(sig)) == 0)