diff --git a/docs/manual.md b/docs/manual.md
index d50e1f6d2..97e0c96d2 100644
--- a/docs/manual.md
+++ b/docs/manual.md
@@ -988,6 +988,7 @@ It supports the following attributes:
   Must be be between 4KiB and 16MiB and be 4K page-aligned. Defaults to 8KiB.
 * `cpu`: (optional) set the physical CPU core this PD will run on. Defaults to zero.
 * `smc`: (optional, only on ARM) Allow the PD to give an SMC call for the kernel to perform.. Defaults to false.
+* `fpu`: (optional) disable the FPU support for this PD. Defaults to true.
 
 Additionally, it supports the following child elements:
 
diff --git a/tool/microkit/src/capdl/builder.rs b/tool/microkit/src/capdl/builder.rs
index c40575871..9d57564d6 100644
--- a/tool/microkit/src/capdl/builder.rs
+++ b/tool/microkit/src/capdl/builder.rs
@@ -322,6 +322,7 @@ impl CapDLSpecContainer {
             prio: 0,
             max_prio: 0,
             resume: false,
+            fpu: true,
             ip: entry_point.into(),
             sp: 0.into(),
             gprs: Vec::new(),
@@ -468,7 +469,7 @@ pub fn build_capdl_spec(
     )
     .unwrap();
 
-    // At this point, all of the required objects for the monitor have been created and it caps inserted into
+    // At this point, all of the required objects for the monitor have been created and its caps inserted into
     // the correct slot in the CSpace. We need to bind those objects into the TCB for the monitor to use them.
     // In addition, `add_elf_to_spec()` doesn't fill most the details in the TCB.
     // Now fill them in: stack ptr, priority, ipc buf vaddr, etc.
@@ -911,6 +912,7 @@ pub fn build_capdl_spec(
                             affinity: Word(vcpu.cpu.0.into()),
                             prio: virtual_machine.priority,
                             max_prio: virtual_machine.priority,
+                            fpu: true,
                             resume: false,
                             // VMs do not have program images associated with them so these are always zero.
                             ip: Word(0),
@@ -979,6 +981,7 @@ pub fn build_capdl_spec(
             pd_tcb.extra.master_fault_ep = None; // Not used on MCS kernel.
             pd_tcb.extra.prio = pd.priority;
             pd_tcb.extra.max_prio = pd.priority;
+            pd_tcb.extra.fpu = pd.fpu;
             pd_tcb.extra.resume = true;
 
             pd_tcb.slots.extend(caps_to_bind_to_tcb);
diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs
index 17b5adbae..935ad11e0 100644
--- a/tool/microkit/src/sdf.rs
+++ b/tool/microkit/src/sdf.rs
@@ -257,6 +257,8 @@ pub struct ProtectionDomain {
     pub smc: bool,
     pub cpu: CpuCore,
     pub program_image: PathBuf,
+    /// Enable FPU for this PD.
+    pub fpu: bool,
     pub maps: Vec<SysMap>,
     pub irqs: Vec<SysIrq>,
     pub ioports: Vec<IOPort>,
@@ -456,6 +458,7 @@ impl ProtectionDomain {
             // but we do the error-checking further down.
             "smc",
             "cpu",
+            "fpu",
         ];
         if is_child {
             attrs.push("id");
@@ -607,6 +610,19 @@ impl ProtectionDomain {
             ));
         }
 
+        // FPU is enabled by default
+        let fpu = if let Some(xml_fpu) = node.attribute("fpu") {
+            match str_to_bool(xml_fpu) {
+                Some(val) => val,
+                None => {
+                    return Err(value_error(xml_sdf, node, "fpu must be 'true' or 'false'".to_string(),))
+                }
+            }
+        } else {
+            // Default to fpu enabled
+            true
+        };
+
         for child in node.children() {
             if !child.is_element() {
                 continue;
@@ -1074,6 +1090,7 @@ impl ProtectionDomain {
             smc,
             cpu,
             program_image: program_image.unwrap(),
+            fpu,
             maps,
             irqs,
             ioports,
diff --git a/tool/microkit/tests/sdf/wrong_fpu_flag_value.system b/tool/microkit/tests/sdf/wrong_fpu_flag_value.system
new file mode 100644
index 000000000..f85a3c257
--- /dev/null
+++ b/tool/microkit/tests/sdf/wrong_fpu_flag_value.system
@@ -0,0 +1,10 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!--
+ Copyright 2025, UNSW
+
+ SPDX-License-Identifier: BSD-2-Clause
+-->
+<system>
+    <protection_domain name="test" fpu="foo">
+    </protection_domain>
+</system>
diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs
index 2ae153b24..459236f59 100644
--- a/tool/microkit/tests/test.rs
+++ b/tool/microkit/tests/test.rs
@@ -828,4 +828,13 @@ mod system {
             "Error: too many protection domains (64) defined. Maximum is 63.",
         )
     }
+
+    #[test]
+    fn test_fpu_flag_wrong_value() {
+        check_error(
+            &DEFAULT_AARCH64_KERNEL_CONFIG,
+            "wrong_fpu_flag_value.system",
+            "Error: fpu must be 'true' or 'false'",
+        )
+    }
 }