diff --git a/core/debug/src/debug_box.c b/core/debug/src/debug_box.c
index 0a3c3f2c..1f88b688 100644
--- a/core/debug/src/debug_box.c
+++ b/core/debug/src/debug_box.c
@@ -92,9 +92,7 @@ void debug_halt_error(THaltError reason)
     if (!g_debug_box.initialized || debugged_once_before) {
         while (1);
     } else {
-        /* Remember that debug_deprivilege_and_return() has been called once.
-         * We'll reboot after the debug handler is run, so this will go back to
-         * zero after the reboot. */
+        /* Remember that debug_deprivilege_and_return() has been called once. */
         debugged_once_before = 1;
 
         /* The following arguments are passed to the destination function:
diff --git a/docs/api/DEBUGGING.md b/docs/api/DEBUGGING.md
index 10d87932..a5fb72c9 100644
--- a/docs/api/DEBUGGING.md
+++ b/docs/api/DEBUGGING.md
@@ -122,12 +122,14 @@ Instead, debug events and messages are forwarded to a special unprivileged box,
 
 The debug box driver is encoded in a standard table (a C `struct`) that must be populated by a debug box at initialization time. A debug box can decide to implement only some of the available handlers, although they must all exist at least as empty functions, otherwise the program behaviour might be unpredictable.
 
-Currently, only one debug handler is provided. A debug box driver will always expect a `get_version()` handler in position 0 of the function table:
+Currently, only one debug handler — `halt_error` — is provided. This handler only executes once, so if another fault occurs during its execution, the uVisor does not de-privilege again, halting instead. A debug box driver will also expect a `get_version()` handler in position 0 of the function table:
+
+Debug box handlers can also reset the device by calling the `NVIC_SystemReset()` API. This API cannot be called from other secure boxes.
 
 ```C
 typedef struct TUvisorDebugDriver {
   uint32_t (*get_version)(void);      /* 0. Return the implemented driver version. */
-  void (*halt_error)(int);            /* 1. Halt on error. Reboot upon return. */
+  void (*halt_error)(int);            /* 1. Halt on error. Halt upon return. */
 }
 ```
 
@@ -137,20 +139,17 @@ The following is an example of how to implement and configure a debug box.
 #include "mbed.h"
 #include "uvisor-lib/uvisor-lib.h"
 
-struct box_context {
-    uint32_t unused;
-};
-
 static const UvisorBoxAclItem acl[] = {
+    /* No specific ACL required. */
 };
 
 static void box_debug_main(const void *);
 
 /* Configure the debug box. */
 UVISOR_BOX_NAMESPACE(NULL);
-UVISOR_BOX_CONFIG(box_debug, UVISOR_BOX_STACK_SIZE);
-UVISOR_BOX_MAIN(box_debug_main, osPriorityNormal, UVISOR_BOX_STACK_SIZE);
-UVISOR_BOX_CONFIG(box_debug, acl, UVISOR_BOX_STACK_SIZE, box_context);
+UVISOR_BOX_HEAPSIZE(2048);
+UVISOR_BOX_MAIN(box_debug_main, osPriorityNormal, 1024);
+UVISOR_BOX_CONFIG(box_debug, 1024);
 
 static uint32_t get_version(void) {
     return 0;
@@ -158,7 +157,11 @@ static uint32_t get_version(void) {
 
 static void halt_error(int reason) {
     printf("We halted with reason %i\r\n", reason);
-    /* We will now reboot. */
+
+    /* If we don't do anything, the system will halt upon return. */
+    /* A debug box handler like this one can also decide to reboot the whole
+     * system. This is only allowed from the debug box. */
+    NVIC_SystemReset();
 }
 
 static void box_debug_main(const void *)
@@ -176,12 +179,7 @@ static void box_debug_main(const void *)
 
 ## Platform-specific details
 
-Currently the following platforms are officially supported by uVisor:
-
-* [NXP FRDM-K64F](http://developer.mbed.org/platforms/FRDM-K64F/).
-* [STMicorelectronics STM32F429I-DISCO](http://www.st.com/web/catalog/tools/FM116/SC959/SS1532/PF259090).
-
-This section provides details on how to enable debug on these platforms.
+This section provides details on how to enable debug on some specific hardware platforms.
 
 #### NXP FRDM-K64F