diff --git a/docs/manual.md b/docs/manual.md
index d5717ed7..5503162a 100644
--- a/docs/manual.md
+++ b/docs/manual.md
@@ -624,6 +624,13 @@ To find the full list of possible faults that could occur and details regarding
 kind of fault, please see the 'Faults' section of the
 [seL4 reference manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf).
 
+For x86 VCPU fault specifically:
+Only the `child` argument will contain a valid value. The return value of `fault()` is ignored. To resume a VCPU from
+a fault, `fault()` must call `microkit_vcpu_x86_deferred_resume()` with the intended values before returning.
+
+To deduce the VM Exit reason, read the `SEL4_VMENTER_FAULT_REASON_MR` message register. For more details,
+please see the 'Virtualisation' section of the [seL4 reference manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf).
+
 ## `microkit_msginfo microkit_ppcall(microkit_channel ch, microkit_msginfo msginfo)`
 
 Performs a call to a protected procedure in a different PD.
@@ -958,6 +965,15 @@ virtual CPU with ID `vcpu`.
 Write the registers of a given virtual CPU with ID `vcpu`. The `regs` argument is the pointer to
 the struct of registers `seL4_VCPUContext` that are written from.
 
+## `void microkit_vcpu_x86_deferred_resume(seL4_Word rip, seL4_Word ppc, seL4_Word irq)`
+
+Resume the bound vCPU when current execution returns to libmicrokit's event handler (see [Internals](#Internals)).
+It switches the PD's thread from regular execution mode into the guest execution mode whenever it is scheduled thereafter.
+
+This will set the program counter of the vCPU to `entry_point`, the Primary Processor-Based VM-Execution Controls to `ppc`
+and the VM-Entry Interruption-Information Field to `irq`. Any previous value of these vCPU fields set by
+`microkit_vcpu_x86_write_vmcs()` will be overwritten.
+
 # System Description File {#sysdesc}
 
 This section describes the format of the System Description File (SDF).
diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h
index 90155d21..924262e5 100644
--- a/libmicrokit/include/microkit.h
+++ b/libmicrokit/include/microkit.h
@@ -45,6 +45,12 @@ extern char microkit_name[MICROKIT_PD_NAME_LENGTH];
 extern seL4_Bool microkit_have_signal;
 extern seL4_CPtr microkit_signal_cap;
 extern seL4_MessageInfo_t microkit_signal_msg;
+#if defined(CONFIG_VTX)
+extern seL4_Bool microkit_x86_do_vcpu_resume;
+extern seL4_Word microkit_x86_vcpu_resume_rip;
+extern seL4_Word microkit_x86_vcpu_resume_ppc;
+extern seL4_Word microkit_x86_vcpu_resume_irq;
+#endif
 
 /* Symbols for error checking libmicrokit API calls. Patched by the Microkit tool
  * to set bits corresponding to valid channels for this PD. */
@@ -188,13 +194,8 @@ static inline void microkit_vcpu_restart(microkit_child vcpu, seL4_Word entry_po
 {
     seL4_Error err;
     seL4_UserContext ctxt = {0};
-#if defined(CONFIG_ARCH_AARCH64)
     ctxt.pc = entry_point;
-#elif defined(CONFIG_ARCH_X86_64)
-    ctxt.rip = entry_point;
-#else
-#error "unknown architecture for 'microkit_vcpu_restart'"
-#endif
+
     err = seL4_TCB_WriteRegisters(
               BASE_VM_TCB_CAP + vcpu,
               seL4_True,
@@ -218,9 +219,7 @@ static inline void microkit_vcpu_stop(microkit_child vcpu)
         microkit_internal_crash(err);
     }
 }
-#endif
 
-#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
 static inline void microkit_vcpu_arm_inject_irq(microkit_child vcpu, seL4_Uint16 irq, seL4_Uint8 priority,
                                                 seL4_Uint8 group, seL4_Uint8 index)
 {
@@ -263,7 +262,7 @@ static inline void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word re
         microkit_internal_crash(err);
     }
 }
-#endif
+#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
 
 #if defined(CONFIG_ALLOW_SMC_CALLS)
 static inline void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMCContext *response)
@@ -275,7 +274,7 @@ static inline void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMC
         microkit_internal_crash(err);
     }
 }
-#endif
+#endif /* CONFIG_ALLOW_SMC_CALLS */
 
 #if defined(CONFIG_ARCH_X86_64)
 static inline void microkit_x86_ioport_write_8(microkit_ioport ioport_id, seL4_Word port_addr, seL4_Word data)
@@ -391,9 +390,8 @@ static inline seL4_Uint32 microkit_x86_ioport_read_32(microkit_ioport ioport_id,
 
     return ret.result;
 }
-#endif
 
-#if defined(CONFIG_ARCH_X86_64) && defined(CONFIG_VTX)
+#if defined(CONFIG_VTX)
 static inline seL4_Word microkit_vcpu_x86_read_vmcs(microkit_child vcpu, seL4_Word field)
 {
     seL4_X86_VCPU_ReadVMCS_t ret;
@@ -477,7 +475,16 @@ static inline void microkit_vcpu_x86_write_regs(microkit_child vcpu, seL4_VCPUCo
     }
 }
 
-#endif
+static inline void microkit_vcpu_x86_deferred_resume(seL4_Word rip, seL4_Word ppc, seL4_Word irq) {
+    /* On x86, a TCB can only have one bound VCPU at any given time.
+     * So we don't take a `microkit_child vcpu` here. */
+    microkit_x86_do_vcpu_resume = seL4_True;
+    microkit_x86_vcpu_resume_rip = rip;
+    microkit_x86_vcpu_resume_ppc = ppc;
+    microkit_x86_vcpu_resume_irq = irq;
+}
+#endif /* CONFIG_VTX */
+#endif /* CONFIG_ARCH_X86_64 */
 
 static inline void microkit_deferred_notify(microkit_channel ch)
 {
diff --git a/libmicrokit/src/main.c b/libmicrokit/src/main.c
index cff14f64..a9e635ca 100644
--- a/libmicrokit/src/main.c
+++ b/libmicrokit/src/main.c
@@ -27,6 +27,13 @@ seL4_Bool microkit_have_signal = seL4_False;
 seL4_CPtr microkit_signal_cap;
 seL4_MessageInfo_t microkit_signal_msg;
 
+#if defined(CONFIG_VTX)
+seL4_Bool microkit_x86_do_vcpu_resume = seL4_False;
+seL4_Word microkit_x86_vcpu_resume_rip;
+seL4_Word microkit_x86_vcpu_resume_ppc; /* "Primary Processor-Based VM-Execution Controls" */
+seL4_Word microkit_x86_vcpu_resume_irq; /* "VM-Entry Interruption-Information Field" */
+#endif /* CONFIG_VTX */
+
 seL4_Word microkit_irqs;
 seL4_Word microkit_notifications;
 seL4_Word microkit_pps;
@@ -63,6 +70,18 @@ static void run_init_funcs(void)
     }
 }
 
+static seL4_MessageInfo_t receive_event(bool have_reply, seL4_MessageInfo_t reply_tag, seL4_Word *badge)
+{
+    if (have_reply) {
+        return seL4_ReplyRecv(INPUT_CAP, reply_tag, badge, REPLY_CAP);
+    } else if (microkit_have_signal) {
+        return seL4_NBSendRecv(microkit_signal_cap, microkit_signal_msg, INPUT_CAP, badge, REPLY_CAP);
+        microkit_have_signal = seL4_False;
+    } else {
+        return seL4_Recv(INPUT_CAP, badge, REPLY_CAP);
+    }
+}
+
 static void handler_loop(void)
 {
     bool have_reply = false;
@@ -89,25 +108,67 @@ static void handler_loop(void)
         seL4_Word badge;
         seL4_MessageInfo_t tag;
 
-        if (have_reply) {
-            tag = seL4_ReplyRecv(INPUT_CAP, reply_tag, &badge, REPLY_CAP);
-        } else if (microkit_have_signal) {
-            tag = seL4_NBSendRecv(microkit_signal_cap, microkit_signal_msg, INPUT_CAP, &badge, REPLY_CAP);
-            microkit_have_signal = seL4_False;
+#if defined(CONFIG_VTX)
+        seL4_Word x86_vmenter_result;
+        seL4_Bool x86_vmenter_result_valid = seL4_False;
+        if (microkit_x86_do_vcpu_resume) {
+            /* There isn't a syscall that atomically send signal or reply, perform vmenter while waiting for
+               incoming notifications. So we have to dispatch any signal or reply first. Then switch execution
+               to the bound VCPU. */
+            if (have_reply) {
+                seL4_Send(REPLY_CAP, reply_tag);
+            } else if (microkit_have_signal) {
+                seL4_NBSend(microkit_signal_cap, microkit_signal_msg);
+            }
+
+            microkit_mr_set(SEL4_VMENTER_CALL_EIP_MR, microkit_x86_vcpu_resume_rip);
+            microkit_mr_set(SEL4_VMENTER_CALL_CONTROL_PPC_MR, microkit_x86_vcpu_resume_ppc);
+            microkit_mr_set(SEL4_VMENTER_CALL_INTERRUPT_INFO_MR, microkit_x86_vcpu_resume_irq);
+
+            x86_vmenter_result = seL4_VMEnter(&badge);
+
+            x86_vmenter_result_valid = seL4_True;
+            microkit_x86_do_vcpu_resume = seL4_False;
         } else {
-            tag = seL4_Recv(INPUT_CAP, &badge, REPLY_CAP);
+            tag = receive_event(have_reply, reply_tag, &badge);
         }
+#else
+        tag = receive_event(have_reply, reply_tag, &badge);
+#endif /* CONFIG_VTX */
 
         uint64_t is_endpoint = badge >> 63;
         uint64_t is_fault = (badge >> 62) & 1;
 
+#if defined(CONFIG_VTX)
+        if (x86_vmenter_result_valid) {
+            if (x86_vmenter_result == SEL4_VMENTER_RESULT_FAULT) {
+                is_fault = 1;
+                tag = seL4_MessageInfo_new(0, 0, 0, 0);
+            } else if (x86_vmenter_result == SEL4_VMENTER_RESULT_NOTIF) {
+                /* VCPU was interrupted while executing from a notification. Saves the instruction pointer,
+                 * Primary Processor-Based VM-Execution Controls and VM-Entry Interruption-Information Field.
+                 * So we can resume automatically with the correct values on the next event loop iteration. */
+                microkit_vcpu_x86_deferred_resume(microkit_mr_get(SEL4_VMENTER_CALL_EIP_MR), microkit_mr_get(SEL4_VMENTER_CALL_CONTROL_PPC_MR), microkit_mr_get(SEL4_VMENTER_CALL_INTERRUPT_INFO_MR));
+            }
+        }
+#endif /* CONFIG_VTX */
+
         have_reply = false;
 
         if (is_fault) {
             seL4_Bool reply_to_fault = fault(badge & PD_MASK, tag, &reply_tag);
-            if (reply_to_fault) {
+
+#if defined(CONFIG_VTX)
+            if (x86_vmenter_result_valid == seL4_False && reply_to_fault == seL4_True) {
+                /* Fault from child PD rather than from bound VCPU */
+                have_reply = true;
+            }
+#else
+            if (reply_to_fault == seL4_True) {
                 have_reply = true;
             }
+#endif /* CONFIG_VTX */
+
         } else if (is_endpoint) {
             have_reply = true;
             reply_tag = protected(badge & CHANNEL_MASK, tag);