diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index 03c3449e5..1de87228d 100644
--- a/tool/microkit/src/sdf.rs
+++ b/tool/microkit/src/sdf.rs
@@ -372,6 +372,39 @@ pub fn parse(
         }
     }
 
+    if config.arch == Arch::X86_64 {
+        let mut all_ioapic_irqs = BTreeSet::new();
+        let mut all_msis = BTreeSet::new();
+        for pd in pds.values() {
+            for sysirq in &pd.irqs {
+                if let SysIrqKind::IOAPIC { ioapic, pin, .. } = sysirq.kind {
+                    if all_ioapic_irqs.contains(&(ioapic, pin)) {
+                        return Err(format!(
+                            "Error: duplicate I/O APIC IRQ chip {}, pin {} in protection domain: '{}' @ {}",
+                            ioapic,
+                            pin,
+                            pd.name,
+                            loc_string(&xml_sdf, pd.text_pos.unwrap()),
+                        ));
+                    }
+                    all_ioapic_irqs.insert((ioapic, pin));
+                }
+
+                if let SysIrqKind::MSI { pci_device, .. } = sysirq.kind {
+                    if all_msis.contains(&pci_device) {
+                        return Err(format!(
+                            "Error: duplicate MSI {} in protection domain: '{}' @ {}",
+                            pci_device,
+                            pd.name,
+                            loc_string(&xml_sdf, pd.text_pos.unwrap())
+                        ));
+                    }
+                    all_msis.insert(pci_device);
+                }
+            }
+        }
+    }
+
     // Ensure no duplicate channel identifiers.
     // This means checking that no interrupt IDs clash with any channel IDs
     let mut ch_ids = BTreeMap::new();
diff --git a/tool/microkit/src/sdf/pci.rs b/tool/microkit/src/sdf/pci.rs
index 9a909a020..423d3661e 100644
--- a/tool/microkit/src/sdf/pci.rs
+++ b/tool/microkit/src/sdf/pci.rs
@@ -4,6 +4,7 @@
 // SPDX-License-Identifier: BSD-2-Clause
 //
 
+use std::cmp::Ordering;
 use std::fmt;
 use std::ops::Deref;
 
@@ -22,6 +23,29 @@ impl Deref for PciDevice {
     }
 }
 
+// This should be removed once https://github.com/seL4/rust-sel4/pull/374 is merged
+impl Ord for PciDevice {
+    fn cmp(&self, other: &Self) -> Ordering {
+        let object::PCIDevice {
+            bus,
+            device,
+            function,
+        } = &self.0;
+        let object::PCIDevice {
+            bus: other_bus,
+            device: other_device,
+            function: other_function,
+        } = &other.0;
+        (bus, device, function).cmp(&(other_bus, other_device, other_function))
+    }
+}
+
+impl PartialOrd for PciDevice {
+    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
+        Some(self.cmp(other))
+    }
+}
+
 impl From<PciDevice> for object::PCIDevice {
     fn from(device: PciDevice) -> Self {
         device.0
diff --git a/tool/microkit/tests/sdf/irq_ioapic_duplicate_pin.system b/tool/microkit/tests/sdf/irq_ioapic_duplicate_pin.system
new file mode 100644
index 000000000..7461352db
--- /dev/null
+++ b/tool/microkit/tests/sdf/irq_ioapic_duplicate_pin.system
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW.
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="test1">
+        <program_image path="test" />
+        <irq id="0" pin="2" vector="99"/>
+        <irq id="1" pin="2" vector="100"/>
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/sdf/irq_msi_pci_duplicate_device.system b/tool/microkit/tests/sdf/irq_msi_pci_duplicate_device.system
new file mode 100644
index 000000000..099c2f11a
--- /dev/null
+++ b/tool/microkit/tests/sdf/irq_msi_pci_duplicate_device.system
@@ -0,0 +1,13 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2026, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="test1">
+        <program_image path="test" />
+        <irq pcidev="1:2.3" handle="0" vector="0" id="0" />
+        <irq pcidev="1:2.3" handle="1" vector="1" id="1" />
+    </protection_domain>
+</system>
\ No newline at end of file
diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs
index 8f9a2fbb4..d9f5a6a99 100644
--- a/tool/microkit/tests/test.rs
+++ b/tool/microkit/tests/test.rs
@@ -562,6 +562,15 @@ mod protection_domain {
         )
     }
 
+    #[test]
+    fn test_irq_ioapic_duplicate_pin() {
+        check_error(
+            &DEFAULT_X86_64_KERNEL_CONFIG,
+            "irq_ioapic_duplicate_pin.system",
+            "Error: duplicate I/O APIC IRQ chip 0, pin 2 in protection domain: 'test1'",
+        )
+    }
+
     #[test]
     fn test_irq_ioapic_vector_greater_than_107() {
         check_error(
@@ -661,6 +670,15 @@ mod protection_domain {
         )
     }
 
+    #[test]
+    fn test_irq_msi_pci_duplicate_device() {
+        check_error(
+            &DEFAULT_X86_64_KERNEL_CONFIG,
+            "irq_msi_pci_duplicate_device.system",
+            "Error: duplicate MSI 01:02.3 in protection domain: 'test1'",
+        )
+    }
+
     #[test]
     fn test_irq_msi_msi_pci_valid() {
         check_success(&DEFAULT_X86_64_KERNEL_CONFIG, "irq_msi_pci_valid.system")