diff --git a/CHANGES b/CHANGES
index b79f4e46d..456efc0d9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,6 +29,7 @@ Upcoming release: BREAKING
 * Added extended bootinfo header for device tree (SEL4_BOOTINFO_HEADER_FDT).
 * Support added for passing a device tree from the bootloader to the root task on ARM.
 * Add seL4_VSpaceBits, the size of the top level page table.
+* The root cnode size is now a minimum of 4K.
 
 ## Upgrade Notes
 ---
diff --git a/config.cmake b/config.cmake
index 159e543e0..27e343eb0 100644
--- a/config.cmake
+++ b/config.cmake
@@ -72,12 +72,13 @@ include(src/config.cmake)
 config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}")
 
 # System parameters
-config_string(KernelRootCNodeSizeBits ROOT_CNODE_SIZE_BITS "Root CNode Size (2^n slots) \
-    The acceptable range is 4-27, based on the kernel-supplied caps.\
-    The root CNode needs at least enough space to contain up to\
-    BI_CAP_DYN_START. Note that in practice your root CNode will need\
-    to be several bits larger than 4 to fit untyped caps and\
-    cannot be 27 bits as it won't fit in memory." DEFAULT 12 UNQUOTE)
+config_string(
+    KernelRootCNodeSizeBits ROOT_CNODE_SIZE_BITS "Root CNode Size (2^n slots) \
+    The acceptable range is 8-27 and 7-26, for 32-bit and 64-bit respectively. \
+    The root CNode needs at least enough space to contain up to BI_CAP_DYN_START."
+    DEFAULT 12
+    UNQUOTE
+)
 
 config_string(KernelTimerTickMS TIMER_TICK_MS "Timer tick period in milliseconds" DEFAULT 2 UNQUOTE)
 config_string(
diff --git a/src/kernel/boot.c b/src/kernel/boot.c
index f8d185558..737b7c782 100644
--- a/src/kernel/boot.c
+++ b/src/kernel/boot.c
@@ -126,7 +126,8 @@ BOOT_CODE void write_slot(slot_ptr_t slot_ptr, cap_t cap)
  */
 compile_assert(root_cnode_size_valid,
                CONFIG_ROOT_CNODE_SIZE_BITS < 32 - seL4_SlotBits &&
-               (1U << CONFIG_ROOT_CNODE_SIZE_BITS) >= seL4_NumInitialCaps)
+               BIT(CONFIG_ROOT_CNODE_SIZE_BITS) >= seL4_NumInitialCaps &&
+               BIT(CONFIG_ROOT_CNODE_SIZE_BITS) >= (seL4_PageBits - seL4_SlotBits))
 
 BOOT_CODE cap_t
 create_root_cnode(void)