diff --git a/config.cmake b/config.cmake
index 48023e8f8..a61812c9f 100644
--- a/config.cmake
+++ b/config.cmake
@@ -330,6 +330,15 @@ config_option(
     DEPENDS "NOT KernelVerificationBuild"
     DEFAULT_DISABLED OFF
 )
+
+config_option(
+    KernelInvocationReportErrorIPC KERNEL_INVOCATION_REPORT_ERROR_IPC
+    "Allows the kernel to write the userError to the IPC buffer"
+    DEFAULT OFF
+    DEPENDS "KernelPrinting"
+    DEFAULT_DISABLED OFF
+)
+
 config_choice(
     KernelBenchmarks
     KERNEL_BENCHMARK
diff --git a/include/api/failures.h b/include/api/failures.h
index bbd0f8046..b84de75bc 100644
--- a/include/api/failures.h
+++ b/include/api/failures.h
@@ -36,13 +36,15 @@ struct syscall_error {
 };
 typedef struct syscall_error syscall_error_t;
 
+#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
 struct debug_syscall_error {
     word_t errorMessage[DEBUG_MESSAGE_MAXLEN];
 };
 typedef struct debug_syscall_error debug_syscall_error_t;
 
+extern debug_syscall_error_t current_debug_error;
+#endif
 extern lookup_fault_t current_lookup_fault;
 extern seL4_Fault_t current_fault;
 extern syscall_error_t current_syscall_error;
-extern debug_syscall_error_t current_debug_error;
 
diff --git a/include/api/types.h b/include/api/types.h
index 05e97ad2c..df01660b4 100644
--- a/include/api/types.h
+++ b/include/api/types.h
@@ -110,24 +110,29 @@ static inline word_t CONST wordFromMessageInfo(seL4_MessageInfo_t mi)
 #define THREAD_NAME ""
 #endif
 
+#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
 extern struct debug_syscall_error current_debug_error;
 
+#define out_error(...) \
+    snprintf((char *)current_debug_error.errorMessage, \
+            DEBUG_MESSAGE_MAXLEN * sizeof(word_t), __VA_ARGS__);
+#else
+#define out_error printf
+#endif
+
 /*
  * Print to serial a message helping userspace programmers to determine why the
  * kernel is not performing their requested operation.
  */
-#define userError(...) \
+#define userError(M, ...) \
     do {                                                                     \
-        printf(ANSI_DARK "<<" ANSI_GREEN "seL4(CPU %lu)" ANSI_DARK           \
-                " [%s/%d T%p \"%s\" @%lx]: ",                                \
+        out_error(ANSI_DARK "<<" ANSI_GREEN "seL4(CPU %lu)" ANSI_DARK        \
+                " [%s/%d T%p \"%s\" @%lx]: " M ">>" ANSI_RESET "\n",         \
                 SMP_TERNARY(getCurrentCPUIndex(), 0lu),                      \
                 __func__, __LINE__, NODE_STATE(ksCurThread),                 \
                 THREAD_NAME,                                                 \
-                (word_t)getRestartPC(NODE_STATE(ksCurThread)));              \
-        printf(__VA_ARGS__);                                                 \
-        printf(">>" ANSI_RESET "\n");                                        \
-        snprintf((char *)current_debug_error.errorMessage,                   \
-                DEBUG_MESSAGE_MAXLEN * sizeof(word_t), __VA_ARGS__);         \
+                (word_t)getRestartPC(NODE_STATE(ksCurThread)),               \
+                ## __VA_ARGS__);                                             \
     } while (0)
 #else /* !CONFIG_PRINTING */
 #define userError(...)
diff --git a/libsel4/CMakeLists.txt b/libsel4/CMakeLists.txt
index 665d7bd10..d6ca94801 100644
--- a/libsel4/CMakeLists.txt
+++ b/libsel4/CMakeLists.txt
@@ -35,6 +35,14 @@ config_option(
     DEFAULT OFF
 )
 
+config_string(
+    LibSel4PrintInvocationErrors LIB_SEL4_PRINT_INVOCATION_ERRORS
+    "Generated stubs on error will print the message contained in the IPC buffer"
+    DEFAULT 1
+    DEPENDS "KernelInvocationReportErrorIPC" DEFAULT_DISABLED 0
+    UNQUOTE
+)
+
 if(LibSel4StubsUseIPCBufferOnly)
     set(buffer "--buffer")
 endif()
diff --git a/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h
index 45b9bfc57..eb31dc8a6 100644
--- a/libsel4/arch_include/arm/sel4/arch/syscalls.h
+++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h
@@ -584,6 +584,14 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
     arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
 }
 
+LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str)
+{
+    for (char *s = str; *s; s++) {
+        seL4_DebugPutChar(*s);
+    }
+    return;
+}
+
 LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
 {
     seL4_Word unused0 = 0;
diff --git a/libsel4/arch_include/riscv/sel4/arch/syscalls.h b/libsel4/arch_include/riscv/sel4/arch/syscalls.h
index 58c84ba8c..00f393e36 100644
--- a/libsel4/arch_include/riscv/sel4/arch/syscalls.h
+++ b/libsel4/arch_include/riscv/sel4/arch/syscalls.h
@@ -786,6 +786,14 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
                         &unused4, &unused5, 0);
 }
 
+LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str)
+{
+    for (char *s = str; *s; s++) {
+        seL4_DebugPutChar(*s);
+    }
+    return;
+}
+
 LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
 {
     seL4_Word unused0 = 0;
diff --git a/libsel4/include/sel4/constants.h b/libsel4/include/sel4/constants.h
index a68f7a68f..dbeb557e7 100644
--- a/libsel4/include/sel4/constants.h
+++ b/libsel4/include/sel4/constants.h
@@ -97,6 +97,7 @@ static inline seL4_Word seL4_MaxExtraRefills(seL4_Word size)
 #endif /* !__ASSEMBLER__ */
 #endif /* CONFIG_KERNEL_MCS */
 
+#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
 #define DEBUG_MESSAGE_START 6
 #define DEBUG_MESSAGE_MAXLEN 50
-
+#endif
diff --git a/libsel4/include/sel4/functions.h b/libsel4/include/sel4/functions.h
index 0bceb5654..e66b439f3 100644
--- a/libsel4/include/sel4/functions.h
+++ b/libsel4/include/sel4/functions.h
@@ -13,6 +13,26 @@
 extern __thread seL4_IPCBuffer *__sel4_ipc_buffer;
 __thread __attribute__((weak)) seL4_IPCBuffer *__sel4_ipc_buffer;
 
+#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
+extern __thread char __sel4_print_error;
+
+LIBSEL4_INLINE_FUNC char *seL4_GetDebugError(void)
+{
+    return (char *)(__sel4_ipc_buffer->msg + DEBUG_MESSAGE_START);
+}
+
+LIBSEL4_INLINE_FUNC void seL4_SetPrintError(char print_error)
+{
+    __sel4_print_error = print_error;
+    return;
+}
+
+LIBSEL4_INLINE_FUNC char seL4_CanPrintError(void)
+{
+    return __sel4_print_error;
+}
+#endif
+
 LIBSEL4_INLINE_FUNC void seL4_SetIPCBuffer(seL4_IPCBuffer *ipc_buffer)
 {
     __sel4_ipc_buffer = ipc_buffer;
diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
index f2f807cc4..0ba7aa949 100644
--- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
@@ -815,6 +815,15 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
     x86_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3));
 }
 
+LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str)
+{
+    for (char *s = str; *s; s++) {
+        seL4_DebugPutChar(*s);
+    }
+    return;
+}
+
+
 LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
 {
     seL4_Word unused0 = 0;
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
index c254c2c54..516f413c3 100644
--- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
@@ -588,6 +588,14 @@ LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
     x64_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
 }
 
+LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str)
+{
+    for (char *s = str; *s; s++) {
+        seL4_DebugPutChar(*s);
+    }
+    return;
+}
+
 LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
 {
     seL4_Word unused0 = 0;
diff --git a/libsel4/src/sel4_bootinfo.c b/libsel4/src/sel4_bootinfo.c
index 03e3e94e2..afee42729 100644
--- a/libsel4/src/sel4_bootinfo.c
+++ b/libsel4/src/sel4_bootinfo.c
@@ -6,6 +6,10 @@
 
 #include <sel4/sel4.h>
 
+#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
+__thread char __sel4_print_error = CONFIG_LIB_SEL4_PRINT_INVOCATION_ERRORS;
+#endif
+
 /** Userland per-thread IPC buffer address **/
 __thread seL4_IPCBuffer *__sel4_ipc_buffer;
 
diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py
index a2b6ced17..0ca4ed5d6 100644
--- a/libsel4/tools/syscall_stub_gen.py
+++ b/libsel4/tools/syscall_stub_gen.py
@@ -715,6 +715,11 @@ def generate_stub(arch, wordsize, interface_name, method_name, method_id, input_
         result.append("\tif (%s != seL4_NoError) {" % label)
         for i in range(num_mrs):
             result.append("\t\tseL4_SetMR(%d, mr%d);" % (i, i))
+        result.append("#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC")
+        result.append("\t\tif (seL4_CanPrintError()) {")
+        result.append("\t\t\tseL4_DebugPutString(seL4_GetDebugError());")
+        result.append("\t\t}")
+        result.append("#endif")
         if returning_struct:
             result.append("\t\treturn result;")
         result.append("\t}")
diff --git a/src/inlines.c b/src/inlines.c
index 42b61af5b..a93984a0c 100644
--- a/src/inlines.c
+++ b/src/inlines.c
@@ -10,4 +10,7 @@
 lookup_fault_t current_lookup_fault;
 seL4_Fault_t current_fault;
 syscall_error_t current_syscall_error;
+#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
 debug_syscall_error_t current_debug_error;
+#endif
+
diff --git a/src/object/endpoint.c b/src/object/endpoint.c
index 9b126ba92..308deabf1 100644
--- a/src/object/endpoint.c
+++ b/src/object/endpoint.c
@@ -262,11 +262,13 @@ void replyFromKernel_error(tcb_t *thread)
     setRegister(thread, badgeRegister, 0);
     len = setMRs_syscall_error(thread, ipcBuffer);
 
+#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
     char *debugBuffer = (char *)(ipcBuffer + DEBUG_MESSAGE_START + 1);
     word_t add = strlcpy(debugBuffer, (char *)current_debug_error.errorMessage,
                          DEBUG_MESSAGE_MAXLEN * sizeof(word_t));
 
     len += (add / sizeof(word_t)) + 1;
+#endif
 
     setRegister(thread, msgInfoRegister, wordFromMessageInfo(
                     seL4_MessageInfo_new(current_syscall_error.type, 0, 0, len)));