diff --git a/.github/workflows/nightly-validation.yml b/.github/workflows/nightly-validation.yml
index f4daced79..bec816438 100644
--- a/.github/workflows/nightly-validation.yml
+++ b/.github/workflows/nightly-validation.yml
@@ -844,3 +844,97 @@ jobs:
 
       - name: Run build script unit tests
         run: python -m unittest discover -s scripts/tests -p "test_*.py" -v
+
+  # ============================================================================
+  # DOTNET MANAGED WRAPPER ARCHITECTURE VALIDATION
+  # ============================================================================
+
+  validate-dotnet-anycpu:
+    name: "Validate Microsoft.Z3.dll is AnyCPU (issue #9863)"
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 15
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6.0.3
+
+      - name: Download NuGet package from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
+
+      - name: Extract managed DLL from NuGet package
+        run: |
+          # NuGet packages are ZIP archives; exclude the symbols package
+          NUPKG=$(ls nuget-packages/*.nupkg | grep -v '\.symbols\.' | grep -v '\.snupkg' | head -n 1)
+          echo "Checking package: $NUPKG"
+          unzip -q "$NUPKG" "lib/netstandard2.0/Microsoft.Z3.dll" -d nupkg-extracted
+
+      - name: Check PE Machine field is AnyCPU (not architecture-specific)
+        run: |
+          python3 - <<'EOF'
+          import struct
+          import sys
+
+          dll_path = "nupkg-extracted/lib/netstandard2.0/Microsoft.Z3.dll"
+
+          with open(dll_path, 'rb') as f:
+              # Verify MZ magic
+              if f.read(2) != b'MZ':
+                  print("ERROR: Not a valid PE file (missing MZ header)")
+                  sys.exit(1)
+
+              # Read PE header offset stored at 0x3C in the DOS stub
+              f.seek(0x3C)
+              pe_offset = struct.unpack('<I', f.read(4))[0]
+
+              # Verify PE signature
+              f.seek(pe_offset)
+              if f.read(4) != b'PE\x00\x00':
+                  print("ERROR: Missing PE\\0\\0 signature")
+                  sys.exit(1)
+
+              # COFF Machine field is the 2 bytes immediately after the PE signature
+              machine = struct.unpack('<H', f.read(2))[0]
+
+          machine_names = {
+              0x0000: "Unknown/AnyCPU",
+              0x014C: "i386 (AnyCPU for managed assemblies)",
+              0x8664: "AMD64/x64",
+              0xAA64: "ARM64",
+              0x01C0: "ARM",
+              0x01C4: "ARM Thumb-2",
+          }
+          machine_name = machine_names.get(machine, f"0x{machine:04X}")
+          print(f"Machine field: 0x{machine:04X} = {machine_name}")
+
+          if machine == 0x8664:
+              print()
+              print("FAIL: Machine is AMD64 (0x8664).")
+              print("This prevents loading on arm64 .NET hosts even though the assembly")
+              print("contains only pure IL (CorFlags.ILONLY=True).")
+              print("The DLL must be built as AnyCPU (Machine=0x014C) so the CLR loader")
+              print("accepts it on every host architecture.")
+              print("See issue #9863 for details.")
+              sys.exit(1)
+          elif machine == 0xAA64:
+              print()
+              print("FAIL: Machine is ARM64 (0xAA64).")
+              print("This prevents loading on x64 .NET hosts.")
+              print("The DLL must be built as AnyCPU (Machine=0x014C).")
+              sys.exit(1)
+          elif machine in (0x014C, 0x0000):
+              print()
+              print("PASS: Machine field indicates AnyCPU.")
+              print("Microsoft.Z3.dll will load on any .NET host architecture.")
+          else:
+              print()
+              print(f"FAIL: Unexpected Machine field 0x{machine:04X}.")
+              print("Expected 0x014C (i386/AnyCPU) for a managed-only assembly.")
+              sys.exit(1)
+          EOF