diff --git a/configs/seL4Config.cmake b/configs/seL4Config.cmake
index 6346a32d6..bf1bdabf4 100644
--- a/configs/seL4Config.cmake
+++ b/configs/seL4Config.cmake
@@ -143,6 +143,7 @@ foreach(
         KernelArmCortexA55
         KernelArmCortexA57
         KernelArmCortexA72
+        KernelArmCortexA76
         KernelArchArmV7a
         KernelArchArmV7ve
         KernelArchArmV8a
@@ -194,6 +195,7 @@ config_set(KernelArmCortexA53 ARM_CORTEX_A53 "${KernelArmCortexA53}")
 config_set(KernelArmCortexA55 ARM_CORTEX_A55 "${KernelArmCortexA55}")
 config_set(KernelArmCortexA57 ARM_CORTEX_A57 "${KernelArmCortexA57}")
 config_set(KernelArmCortexA72 ARM_CORTEX_A72 "${KernelArmCortexA72}")
+config_set(KernelArmCortexA76 ARM_CORTEX_A76 "${KernelArmCortexA76}")
 config_set(KernelArchArmV7a ARCH_ARM_V7A "${KernelArchArmV7a}")
 config_set(KernelArchArmV7ve ARCH_ARM_V7VE "${KernelArchArmV7ve}")
 config_set(KernelArchArmV8a ARCH_ARM_V8A "${KernelArchArmV8a}")
@@ -232,6 +234,8 @@ elseif(KernelArmCortexA57)
   set(KernelArmCPU "cortex-a57" CACHE INTERNAL "")
 elseif(KernelArmCortexA72)
   set(KernelArmCPU "cortex-a72" CACHE INTERNAL "")
+elseif(KernelArmCortexA76)
+  set(KernelArmCPU "cortex-a76" CACHE INTERNAL "")
 endif()
 if(KernelArchARM)
   config_set(KernelArmMach ARM_MACH "${KernelArmMach}")
diff --git a/libsel4/arch_include/arm/sel4/arch/constants_cortex_a76.h b/libsel4/arch_include/arm/sel4/arch/constants_cortex_a76.h
new file mode 100644
index 000000000..dfc963ac3
--- /dev/null
+++ b/libsel4/arch_include/arm/sel4/arch/constants_cortex_a76.h
@@ -0,0 +1,28 @@
+/*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#pragma once
+
+#include <sel4/config.h>
+
+#if !defined(CONFIG_ARM_CORTEX_A76)
+#error CONFIG_ARM_CORTEX_A76 is not defined
+#endif
+
+/* Cortex-A76 Manual, Section 17.2.2 */
+#define seL4_NumHWBreakpoints           10
+#define seL4_NumExclusiveBreakpoints     6
+#define seL4_NumExclusiveWatchpoints     4
+
+#ifdef CONFIG_HARDWARE_DEBUG_API
+
+#define seL4_FirstBreakpoint             0
+#define seL4_FirstWatchpoint             6
+
+#define seL4_NumDualFunctionMonitors     0
+#define seL4_FirstDualFunctionMonitor    (-1)
+
+#endif /* CONFIG_HARDWARE_DEBUG_API */
diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake
index 36e7a4022..bc042cc21 100644
--- a/src/arch/arm/config.cmake
+++ b/src/arch/arm/config.cmake
@@ -30,6 +30,9 @@ elseif(KernelArmCortexA72)
   # (https://developer.arm.com/documentation/100095/0001/memory-management-unit/about-the-mmu)
   set(KernelArmPASizeBits44 ON)
   math(EXPR KernelPaddrUserTop "(1 << 44)")
+elseif(KernelArmCortexA76)
+  set(KernelArmPASizeBits40 ON)
+  math(EXPR KernelPaddrUserTop "(1 << 40)")
 endif()
 config_set(KernelArmPASizeBits40 ARM_PA_SIZE_BITS_40 "${KernelArmPASizeBits40}")
 config_set(KernelArmPASizeBits44 ARM_PA_SIZE_BITS_44 "${KernelArmPASizeBits44}")
@@ -78,7 +81,7 @@ config_option(
   "Build as Hypervisor. Utilise ARM virtualisation extensions to build the kernel as a hypervisor"
   DEFAULT ${KernelSel4ArchArmHyp}
   DEPENDS
-    "KernelArmCortexA15 OR KernelArmCortexA35 OR KernelArmCortexA57 OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA72"
+    "KernelArmCortexA15 OR KernelArmCortexA35 OR KernelArmCortexA57 OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA72 OR KernelArmCortexA76"
 )
 
 config_option(KernelArmGicV3 ARM_GIC_V3_SUPPORT "Build support for GICv3" DEFAULT OFF)
@@ -234,7 +237,8 @@ if(KernelAArch32FPUEnableContextSwitch OR KernelSel4ArchAarch64)
 endif()
 
 if(KernelArmCortexA7 OR KernelArmCortexA8 OR KernelArmCortexA15 OR KernelArmCortexA35
-   OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA57 OR KernelArmCortexA72)
+   OR KernelArmCortexA53 OR KernelArmCortexA55 OR KernelArmCortexA57 OR KernelArmCortexA72
+   OR KernelArmCortexA76)
   # According to https://developer.arm.com/documentation/100095/0001/functional-description/about-the-cortex-a72-processor-functions/components-of-the-processor
   # the L1 instruction on the Cortex-A72 cache has a 64-byte cache line.
   # Thus, 6 bits are needed.