diff --git a/CHANGES.md b/CHANGES.md
index 8a6000d11..af0fbc440 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -34,6 +34,7 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
   the highest available address available to user level. The existing constant
   `seL4_UserTop` is a mix of inclusive and exclusive across existing platforms, however,
   changing this to be consistent would break userspace and require proof updates.
+  The existing `seL4_UserTop` define is deprecated.
 
 ### Platforms
 
diff --git a/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
index 68bc4316e..4db7e16ff 100644
--- a/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
@@ -243,7 +243,7 @@ SEL4_SIZE_SANITY(seL4_VSpaceEntryBits, seL4_VSpaceIndexBits, seL4_VSpaceBits);
  * Anything address above the range above triggers an
  * address size fault.
  */
-/* Last address in the virtual address space that is accessible to user level */
+/* (Deprecated) Last address in the virtual address space that is accessible to user level */
 #if defined(CONFIG_ARM_PA_SIZE_BITS_44)
 #define seL4_UserTop 0x00000fffffffffff
 #elif defined(CONFIG_ARM_PA_SIZE_BITS_40)
@@ -253,7 +253,7 @@ SEL4_SIZE_SANITY(seL4_VSpaceEntryBits, seL4_VSpaceIndexBits, seL4_VSpaceBits);
 #endif
 
 #else
-/* Last address in the virtual address space that is accessible to user level */
+/* (Deprecated) Last address in the virtual address space that is accessible to user level */
 #define seL4_UserTop 0x00007fffffffffff
 #endif
 
diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
index 4110554c5..e47e7971b 100644
--- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/constants.h
@@ -143,7 +143,7 @@ typedef enum {
 /* IPC buffer is 512 bytes, giving size bits of 9 */
 #define seL4_IPCBufferSizeBits 9
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_arch_include/riscv32/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/riscv32/sel4/sel4_arch/constants.h
index 76af64ac6..2391324f4 100644
--- a/libsel4/sel4_arch_include/riscv32/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/riscv32/sel4/sel4_arch/constants.h
@@ -124,7 +124,7 @@ typedef enum {
 #endif
 #endif /* __ASSEMBLER__ */
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0x80000000lu
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h
index d80dca400..32b5446fd 100644
--- a/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/riscv64/sel4/sel4_arch/constants.h
@@ -125,7 +125,7 @@ typedef enum {
 #endif
 #endif /* __ASSEMBLER__ */
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0x0000003ffffff000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
index 1cd5e1363..ecbcb688b 100644
--- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/constants.h
@@ -153,7 +153,7 @@ typedef enum {
 /* IPC buffer is 1024 bytes, giving size bits of 10 */
 #define seL4_IPCBufferSizeBits 10
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0x00007ffffffff000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/allwinnerA20/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/allwinnerA20/sel4/plat/api/constants.h
index 19039299a..1d864a422 100644
--- a/libsel4/sel4_plat_include/allwinnerA20/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/allwinnerA20/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a7.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xa0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/am335x/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/am335x/sel4/plat/api/constants.h
index 95d4cb717..eca6edc04 100644
--- a/libsel4/sel4_plat_include/am335x/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/am335x/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a8.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/apq8064/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/apq8064/sel4/plat/api/constants.h
index 76312530f..ccf72ffc9 100644
--- a/libsel4/sel4_plat_include/apq8064/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/apq8064/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a15.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/bcm2711/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/bcm2711/sel4/plat/api/constants.h
index 604916436..0571efb4e 100644
--- a/libsel4/sel4_plat_include/bcm2711/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/bcm2711/sel4/plat/api/constants.h
@@ -11,7 +11,7 @@
 #include <sel4/arch/constants_cortex_a72.h>
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xa0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/bcm2837/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/bcm2837/sel4/plat/api/constants.h
index 7d0446608..6f3cf6d49 100644
--- a/libsel4/sel4_plat_include/bcm2837/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/bcm2837/sel4/plat/api/constants.h
@@ -11,7 +11,7 @@
 #include <sel4/arch/constants_cortex_a53.h>
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/exynos4/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/exynos4/sel4/plat/api/constants.h
index 03108ecd4..b7a7d676c 100644
--- a/libsel4/sel4_plat_include/exynos4/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/exynos4/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a9.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/exynos5/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/exynos5/sel4/plat/api/constants.h
index c46e3f024..95bf9b805 100644
--- a/libsel4/sel4_plat_include/exynos5/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/exynos5/sel4/plat/api/constants.h
@@ -22,7 +22,7 @@
 #error "unsupported core"
 #endif
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/hikey/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/hikey/sel4/plat/api/constants.h
index a16b94f17..f9aac3ff5 100644
--- a/libsel4/sel4_plat_include/hikey/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/hikey/sel4/plat/api/constants.h
@@ -11,7 +11,7 @@
 #include <sel4/arch/constants_cortex_a53.h>
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/imx6/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/imx6/sel4/plat/api/constants.h
index 03108ecd4..b7a7d676c 100644
--- a/libsel4/sel4_plat_include/imx6/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/imx6/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a9.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/imx7/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/imx7/sel4/plat/api/constants.h
index d527f2198..1970116ab 100644
--- a/libsel4/sel4_plat_include/imx7/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/imx7/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a7.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/imx8mm-evk/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/imx8mm-evk/sel4/plat/api/constants.h
index ebe3e7713..511e9eefb 100644
--- a/libsel4/sel4_plat_include/imx8mm-evk/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/imx8mm-evk/sel4/plat/api/constants.h
@@ -10,7 +10,7 @@
 #include <sel4/arch/constants_cortex_a53.h>
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/imx8mp-evk/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/imx8mp-evk/sel4/plat/api/constants.h
index 82c2563c6..9c2e15842 100644
--- a/libsel4/sel4_plat_include/imx8mp-evk/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/imx8mp-evk/sel4/plat/api/constants.h
@@ -10,7 +10,7 @@
 #include <sel4/arch/constants_cortex_a53.h>
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/imx8mq-evk/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/imx8mq-evk/sel4/plat/api/constants.h
index ebe3e7713..511e9eefb 100644
--- a/libsel4/sel4_plat_include/imx8mq-evk/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/imx8mq-evk/sel4/plat/api/constants.h
@@ -10,7 +10,7 @@
 #include <sel4/arch/constants_cortex_a53.h>
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/maaxboard/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/maaxboard/sel4/plat/api/constants.h
index c2475671b..71cfb8e0f 100644
--- a/libsel4/sel4_plat_include/maaxboard/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/maaxboard/sel4/plat/api/constants.h
@@ -11,7 +11,7 @@
 #include <sel4/arch/constants_cortex_a53.h>
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/omap3/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/omap3/sel4/plat/api/constants.h
index 26fe85134..8e3b7a87a 100644
--- a/libsel4/sel4_plat_include/omap3/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/omap3/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a8.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xf0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/qemu-arm-virt/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/qemu-arm-virt/sel4/plat/api/constants.h
index 6f683d0da..bd676991e 100644
--- a/libsel4/sel4_plat_include/qemu-arm-virt/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/qemu-arm-virt/sel4/plat/api/constants.h
@@ -23,7 +23,7 @@
 
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop CONFIG_USER_TOP
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/tk1/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/tk1/sel4/plat/api/constants.h
index 76312530f..ccf72ffc9 100644
--- a/libsel4/sel4_plat_include/tk1/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/tk1/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a15.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/zynq7000/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/zynq7000/sel4/plat/api/constants.h
index 03108ecd4..b7a7d676c 100644
--- a/libsel4/sel4_plat_include/zynq7000/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/zynq7000/sel4/plat/api/constants.h
@@ -9,7 +9,7 @@
 #include <sel4/config.h>
 #include <sel4/arch/constants_cortex_a9.h>
 
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */
diff --git a/libsel4/sel4_plat_include/zynqmp/sel4/plat/api/constants.h b/libsel4/sel4_plat_include/zynqmp/sel4/plat/api/constants.h
index 1f782c4a5..47b8e1b8f 100644
--- a/libsel4/sel4_plat_include/zynqmp/sel4/plat/api/constants.h
+++ b/libsel4/sel4_plat_include/zynqmp/sel4/plat/api/constants.h
@@ -15,7 +15,7 @@
 #include <sel4/arch/constants_cortex_a53.h>
 
 #if CONFIG_WORD_SIZE == 32
-/* First address in the virtual address space that is not accessible to user level */
+/* (Deprecated) First address in the virtual address space that is not accessible to user level */
 #define seL4_UserTop 0xe0000000
 
 /* Last address in the virtual address space that is accessible to user level */