diff --git a/Hardware/CEI_TK1_SOM/index.md b/Hardware/CEI_TK1_SOM/index.md
index 9eaaccedd5..fe416df32e 100644
--- a/Hardware/CEI_TK1_SOM/index.md
+++ b/Hardware/CEI_TK1_SOM/index.md
@@ -8,7 +8,7 @@ virtualization: ARM HYP
 iommu: System MMU
 soc: NVIDIA Tegra K1
 cpu: Cortex-A15
-Status: "[FC (without System MMU)](/projects/sel4/verified-configurations.html#arm_hyp)"
+Status: "[FC with HYP, no SMMU](/projects/sel4/verified-configurations.html#arm_hyp-tk1)"
 Contrib: Data61
 Maintained: seL4 Foundation
 SPDX-License-Identifier: CC-BY-SA-4.0
diff --git a/Hardware/OdroidXU4.md b/Hardware/OdroidXU4.md
index bc836505ed..52f8339bb9 100644
--- a/Hardware/OdroidXU4.md
+++ b/Hardware/OdroidXU4.md
@@ -8,7 +8,7 @@ virtualization: ARM HYP
 iommu: limited System MMU
 soc: Exynos5
 cpu: Cortex-A15
-Status: Unverified
+Status: "[FC with HYP, no SMMU](/projects/sel4/verified-configurations.html#arm_hyp-exynos5)"
 Contrib: Data61
 Maintained: seL4 Foundation
 SPDX-License-Identifier: CC-BY-SA-4.0
diff --git a/Hardware/imx8mm.md b/Hardware/imx8mm.md
index bb341822c1..904764f0b8 100644
--- a/Hardware/imx8mm.md
+++ b/Hardware/imx8mm.md
@@ -9,7 +9,7 @@ virtualization: "No"
 iommu: "No"
 soc: IMX8MM-EVK
 cpu: Cortex-A53 Quad 1.8 GHz
-Status: "FC, unmaintained"
+Status: "[FC](/projects/sel4/verified-configurations.html#arm-imx8mm-evk)"
 Contrib: Data61
 Maintained: seL4 Foundation
 SPDX-License-Identifier: CC-BY-SA-4.0
diff --git a/Hardware/sabreLite.md b/Hardware/sabreLite.md
index 30e2c076e7..5fba6310f3 100644
--- a/Hardware/sabreLite.md
+++ b/Hardware/sabreLite.md
@@ -9,7 +9,7 @@ virtualization: "No"
 iommu: "No"
 soc: i.MX6
 cpu: Cortex-A9
-Status: "[Verified](/projects/sel4/verified-configurations.html#arm)"
+Status: "[Verified](/projects/sel4/verified-configurations.html#arm-sabre-lite)"
 Contrib: Data61
 Maintained: seL4 Foundation
 SPDX-License-Identifier: CC-BY-SA-4.0
diff --git a/projects/sel4/verified-configurations.md b/projects/sel4/verified-configurations.md
index 8056f32c12..c858e2e49d 100644
--- a/projects/sel4/verified-configurations.md
+++ b/projects/sel4/verified-configurations.md
@@ -67,26 +67,35 @@ The proofs for RISCV64\_MCS/ARM\_MCS (mixed-criticality extensions to real-time
 seL4 features), as well as proofs for AARCH64 are in progress. Refer to the
 [roadmap](/projects/roadmap.html) for status and upcoming features.
 
-## ARM
+## ARM Sabre Lite
 
 | File | `ARM_verified.cmake`
 | Architecture | ARMv7
-| Platform | iMX.6 (e.g. Sabre Lite)
+| Platform | i.MX 6 (Sabre Lite)
 | Floating-point support | No
 | Hypervisor mode | No
 | **Verified properties** | functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation
 
+## ARM IMX8MM-EVK
+
+| File | `ARM_imx8mm_verified.cmake`
+| Architecture | ARMv7
+| Platform | IMX8MM-EVK
+| Floating-point support | Yes
+| Hypervisor mode | No
+| **Verified properties** | functional correctness incl fast path
+
 ## ARM_MCS
 
 File | `ARM_MCS_verified.cmake`
 Architecture | ARMv7
-Platform | iMX.6 (e.g. Sabre Lite)
+Platform | i.MX 6 (Sabre Lite)
 Floating-point support | No
 Hypervisor mode | No
 Mixed-Criticality-Systems API | Yes
 **Verified properties** | in progress (design-level functional correctness completed)
 
-## ARM\_HYP
+## ARM\_HYP TK1
 
 File | `ARM_HYP_verified.cmake`
 Architecture | ARMv7
@@ -95,11 +104,20 @@ Floating-point support | No
 Hypervisor mode | Yes
 **Verified properties** | functional correctness, incl fast path
 
+## ARM\_HYP Exynos5
+
+File | `ARM_HYP_exynos5_verified.cmake`
+Architecture | ARMv7
+Platform | Odroid XU4
+Floating-point support | No
+Hypervisor mode | Yes
+**Verified properties** | functional correctness, incl fast path
+
 ## AARCH64
 
 | File | `AARCH64_verified.cmake`
 | Architecture | ARMv8
-| Platform | Tegra X2 (e.g. Jetson TX2)
+| Platform | Tegra X2 (Jetson TX2)
 | Floating-point support | Yes
 | Hypervisor mode | Yes
 | **Verified properties** | in progress