diff --git a/config.cmake b/config.cmake
index 6c87ee0a0..0e1080164 100644
--- a/config.cmake
+++ b/config.cmake
@@ -240,19 +240,6 @@ config_string(
     UNQUOTE
 )
 
-config_string(
-    KernelFPUMaxRestoresSinceSwitch
-    FPU_MAX_RESTORES_SINCE_SWITCH
-    "This option is a heuristic to attempt to detect when the FPU is no longer in use,\
-    allowing the kernel to save the FPU state out so that the FPU does not have to be\
-    enabled/disabled every thread switch. Every time we restore a thread and there is\
-    active FPU state, we increment this setting and if it exceeds this threshold we\
-    switch to the NULL state."
-    DEFAULT 64
-    DEPENDS "KernelHaveFPU"
-    UNDEF_DISABLED UNQUOTE
-)
-
 config_option(
     KernelVerificationBuild
     VERIFICATION_BUILD
diff --git a/include/arch/arm/arch/kernel/traps.h b/include/arch/arm/arch/kernel/traps.h
index b19368ad8..90b37bf52 100644
--- a/include/arch/arm/arch/kernel/traps.h
+++ b/include/arch/arm/arch/kernel/traps.h
@@ -57,8 +57,3 @@ void c_handle_vcpu_fault(word_t hsr)
 VISIBLE SECTION(".vectors.text");
 #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
 
-#ifdef CONFIG_HAVE_FPU
-void c_handle_enfp(void)
-VISIBLE SECTION(".vectors.text");
-#endif /* CONFIG_HAVE_FPU */
-
diff --git a/include/arch/arm/armv/armv7-a/armv/vcpu.h b/include/arch/arm/armv/armv7-a/armv/vcpu.h
index 3e34d0816..95ecabb05 100644
--- a/include/arch/arm/armv/armv7-a/armv/vcpu.h
+++ b/include/arch/arm/armv/armv7-a/armv/vcpu.h
@@ -703,9 +703,8 @@ static inline void armv_vcpu_save(vcpu_t *vcpu, bool_t active)
 #endif
     isb();
 #ifdef CONFIG_HAVE_FPU
-    /* Other FPU registers are still lazily saved and restored when
-     * handleFPUFault is called. See the comments in vcpu_enable
-     * for more information.
+    /* Other FPU registers are still lazily saved and restored.
+     * See the comments in vcpu_enable for more information.
      */
     if (active && nativeThreadUsingFPU(vcpu->vcpuTCB)) {
         access_fpexc(vcpu, false);
@@ -849,15 +848,6 @@ static inline void armv_vcpu_init(vcpu_t *vcpu)
 
 static inline bool_t armv_handleVCPUFault(word_t hsr)
 {
-#ifdef CONFIG_HAVE_FPU
-    if (hsr == HSR_FPU_FAULT || hsr == HSR_TASE_FAULT) {
-        assert(!isFpuEnable());
-        handleFPUFault();
-        setNextPC(NODE_STATE(ksCurThread), getRestartPC(NODE_STATE(ksCurThread)));
-        return true;
-    }
-#endif
-
     return false;
 }
 
diff --git a/include/arch/arm/armv/armv8-a/64/armv/vcpu.h b/include/arch/arm/armv/armv8-a/64/armv/vcpu.h
index ff5813182..2f0b83a30 100644
--- a/include/arch/arm/armv/armv8-a/64/armv/vcpu.h
+++ b/include/arch/arm/armv/armv8-a/64/armv/vcpu.h
@@ -714,12 +714,6 @@ static inline void armv_vcpu_init(vcpu_t *vcpu)
 
 static inline bool_t armv_handleVCPUFault(word_t hsr)
 {
-    if ((ESR_EC(hsr) == ESR_EC_TFP || ESR_EC(hsr) == ESR_EC_CPACR) && !isFpuEnable()) {
-        handleFPUFault();
-        setNextPC(NODE_STATE(ksCurThread), getRestartPC(NODE_STATE(ksCurThread)));
-        return true;
-    }
-
 #ifdef CONFIG_HARDWARE_DEBUG_API
     if (isDebugFault(hsr)) {
         handleDebugFaultEvent(hsr);
diff --git a/include/machine/fpu.h b/include/machine/fpu.h
index f05efe960..3e6f11f75 100644
--- a/include/machine/fpu.h
+++ b/include/machine/fpu.h
@@ -16,9 +16,6 @@
 /* Perform any actions required for the deletion of the given thread. */
 void fpuThreadDelete(tcb_t *thread);
 
-/* Handle an FPU exception. */
-exception_t handleFPUFault(void);
-
 void switchLocalFpuOwner(user_fpu_state_t *new_owner);
 
 /* Switch the current owner of the FPU state on the core specified by 'cpu'. */
@@ -31,28 +28,15 @@ static inline bool_t nativeThreadUsingFPU(tcb_t *thread)
            NODE_STATE_ON_CORE(ksActiveFPUState, thread->tcbAffinity);
 }
 
+/* Called without global lock held! */
 static inline void FORCE_INLINE lazyFPURestore(tcb_t *thread)
 {
-    if (unlikely(NODE_STATE(ksActiveFPUState))) {
-        /* If we have enabled/disabled the FPU too many times without
-         * someone else trying to use it, we assume it is no longer
-         * in use and switch out its state. */
-        if (unlikely(NODE_STATE(ksFPURestoresSinceSwitch) > CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH)) {
-            switchLocalFpuOwner(NULL);
-            NODE_STATE(ksFPURestoresSinceSwitch) = 0;
-        } else {
-            if (likely(nativeThreadUsingFPU(thread))) {
-                /* We are using the FPU, make sure it is enabled */
-                enableFpu();
-            } else {
-                /* Someone is using the FPU and it might be enabled */
-                disableFpu();
-            }
-            NODE_STATE(ksFPURestoresSinceSwitch)++;
-        }
+    if (thread->tcbFlags & seL4_TCBFlag_fpuDisabled) {
+        disableFpu();
+    } else if (nativeThreadUsingFPU(thread)) {
+        enableFpu();
     } else {
-        /* No-one (including us) is using the FPU, so we assume it
-         * is currently disabled */
+        switchLocalFpuOwner(&thread->tcbArch.tcbContext.fpuState);
     }
 }
 
diff --git a/include/model/statedata.h b/include/model/statedata.h
index ee0a467b1..f7eaa0e9b 100644
--- a/include/model/statedata.h
+++ b/include/model/statedata.h
@@ -75,9 +75,8 @@ NODE_STATE_DECLARE(sched_context_t, *ksIdleSC);
 #ifdef CONFIG_HAVE_FPU
 /* Current state installed in the FPU, or NULL if the FPU is currently invalid */
 NODE_STATE_DECLARE(user_fpu_state_t *, ksActiveFPUState);
-/* Number of times we have restored a user context with an active FPU without switching it */
-NODE_STATE_DECLARE(word_t, ksFPURestoresSinceSwitch);
 #endif /* CONFIG_HAVE_FPU */
+
 #ifdef CONFIG_DEBUG_BUILD
 NODE_STATE_DECLARE(tcb_t *, ksDebugTCBs);
 #endif /* CONFIG_DEBUG_BUILD */
diff --git a/src/arch/arm/64/traps.S b/src/arch/arm/64/traps.S
index 6320d54c0..d3f410f92 100644
--- a/src/arch/arm/64/traps.S
+++ b/src/arch/arm/64/traps.S
@@ -171,8 +171,6 @@ BEGIN_FUNC(lower_el_sync)
     mov     x0, x25
     b       c_handle_vcpu_fault
 #else
-    cmp     x24, #ESR_EL1_EC_ENFP
-    b.eq    el0_enfp
     b       el0_user
 #endif
 
@@ -214,12 +212,6 @@ lel_syscall:
     mov     x2, x7
     b       c_handle_syscall
 
-el0_enfp:
-#ifdef CONFIG_HAVE_FPU
-    lsp_i   x19
-    b       c_handle_enfp
-#endif /* CONFIG_HAVE_FPU */
-
 el0_user:
     mrs     x20, ELR
     str     x20, [sp, #PT_FaultIP]
diff --git a/src/arch/arm/c_traps.c b/src/arch/arm/c_traps.c
index 94cc3a4cf..8104d73df 100644
--- a/src/arch/arm/c_traps.c
+++ b/src/arch/arm/c_traps.c
@@ -27,21 +27,6 @@ void VISIBLE NORETURN c_handle_undefined_instruction(void)
     ksKernelEntry.word = getRegister(NODE_STATE(ksCurThread), NextIP);
 #endif
 
-#if defined(CONFIG_HAVE_FPU) && defined(CONFIG_ARCH_AARCH32)
-    /* We assume the first fault is a FP exception and enable FPU, if not already enabled */
-    if (!isFpuEnable()) {
-        handleFPUFault();
-
-        /* Restart the FP instruction that cause the fault */
-        setNextPC(NODE_STATE(ksCurThread), getRestartPC(NODE_STATE(ksCurThread)));
-    } else {
-        handleUserLevelFault(0, 0);
-    }
-
-    restore_user_context();
-    UNREACHABLE();
-#endif
-
     /* There's only one user-level fault on ARM, and the code is (0,0) */
 #ifdef CONFIG_ARCH_AARCH32
     handleUserLevelFault(0, 0);
@@ -60,17 +45,6 @@ void VISIBLE NORETURN c_handle_undefined_instruction(void)
     UNREACHABLE();
 }
 
-#if defined(CONFIG_HAVE_FPU) && defined(CONFIG_ARCH_AARCH64)
-void VISIBLE NORETURN c_handle_enfp(void)
-{
-    c_entry_hook();
-
-    handleFPUFault();
-    restore_user_context();
-    UNREACHABLE();
-}
-#endif /* CONFIG_HAVE_FPU */
-
 #ifdef CONFIG_EXCEPTION_FASTPATH
 void NORETURN vm_fault_slowpath(vm_fault_type_t type)
 {
diff --git a/src/arch/riscv/c_traps.c b/src/arch/riscv/c_traps.c
index 86c7ebe90..8a805e0f2 100644
--- a/src/arch/riscv/c_traps.c
+++ b/src/arch/riscv/c_traps.c
@@ -133,14 +133,6 @@ void VISIBLE NORETURN c_handle_exception(void)
         handleVMFaultEvent(scause);
         break;
     default:
-#ifdef CONFIG_HAVE_FPU
-        if (!isFpuEnable()) {
-            /* we assume the illegal instruction is caused by FPU first */
-            handleFPUFault();
-            setNextPC(NODE_STATE(ksCurThread), getRestartPC(NODE_STATE(ksCurThread)));
-            break;
-        }
-#endif
         handleUserLevelFault(scause, 0);
         break;
     }
diff --git a/src/arch/x86/c_traps.c b/src/arch/x86/c_traps.c
index 330967144..c1ed5bce8 100644
--- a/src/arch/x86/c_traps.c
+++ b/src/arch/x86/c_traps.c
@@ -42,13 +42,7 @@ void VISIBLE NORETURN c_handle_interrupt(int irq, int syscall)
 
     c_entry_hook();
 
-    if (irq == int_unimpl_dev) {
-        handleFPUFault();
-#ifdef TRACK_KERNEL_ENTRIES
-        ksKernelEntry.path = Entry_UnimplementedDevice;
-        ksKernelEntry.word = irq;
-#endif
-    } else if (irq == int_page_fault) {
+    if (irq == int_page_fault) {
         /* Error code is in Error. Pull out bit 5, which is whether it was instruction or data */
         vm_fault_type_t type = (NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers[Error] >> 4u) & 1u;
 #ifdef TRACK_KERNEL_ENTRIES
diff --git a/src/kernel/thread.c b/src/kernel/thread.c
index d1d44be00..11f66be35 100644
--- a/src/kernel/thread.c
+++ b/src/kernel/thread.c
@@ -29,6 +29,7 @@ transferCaps(seL4_MessageInfo_t info,
 
 BOOT_CODE void configureIdleThread(tcb_t *tcb)
 {
+    tcb->tcbFlags = seL4_TCBFlag_fpuDisabled;
     Arch_configureIdleThread(tcb);
     setThreadState(tcb, ThreadState_IdleThreadState);
 }
diff --git a/src/machine/fpu.c b/src/machine/fpu.c
index 79c400bb1..17537bffb 100644
--- a/src/machine/fpu.c
+++ b/src/machine/fpu.c
@@ -19,7 +19,6 @@ void switchLocalFpuOwner(user_fpu_state_t *new_owner)
         saveFpuState(NODE_STATE(ksActiveFPUState));
     }
     if (new_owner) {
-        NODE_STATE(ksFPURestoresSinceSwitch) = 0;
         loadFpuState(new_owner);
     } else {
         disableFpu();
@@ -39,24 +38,6 @@ void switchFpuOwner(user_fpu_state_t *new_owner, word_t cpu)
     }
 }
 
-/* Handle an FPU fault.
- *
- * This CPU exception is thrown when userspace attempts to use the FPU while
- * it is disabled. We need to save the current state of the FPU, and hand
- * it over. */
-exception_t handleFPUFault(void)
-{
-    /* If we have already given the FPU to the user, we should not reach here.
-     * This should only be able to occur on CPUs without an FPU at all, which
-     * we presumably are happy to assume will not be running seL4. */
-    assert(!nativeThreadUsingFPU(NODE_STATE(ksCurThread)));
-
-    /* Otherwise, lazily switch over the FPU. */
-    switchLocalFpuOwner(&NODE_STATE(ksCurThread)->tcbArch.tcbContext.fpuState);
-
-    return EXCEPTION_NONE;
-}
-
 /* Prepare for the deletion of the given thread. */
 void fpuThreadDelete(tcb_t *thread)
 {
diff --git a/src/model/statedata.c b/src/model/statedata.c
index 8ae02c6bf..471919026 100644
--- a/src/model/statedata.c
+++ b/src/model/statedata.c
@@ -44,9 +44,8 @@ UP_STATE_DEFINE(tcb_t *, ksSchedulerAction);
 #ifdef CONFIG_HAVE_FPU
 /* Currently active FPU state, or NULL if there is no active FPU state */
 UP_STATE_DEFINE(user_fpu_state_t *, ksActiveFPUState);
-
-UP_STATE_DEFINE(word_t, ksFPURestoresSinceSwitch);
 #endif /* CONFIG_HAVE_FPU */
+
 #ifdef CONFIG_KERNEL_MCS
 /* the amount of time passed since the kernel time was last updated */
 UP_STATE_DEFINE(ticks_t, ksConsumed);