diff --git a/Hardware/Star64/index.md b/Hardware/Star64/index.md
index 786ecdc54fb..d1c239e651e 100644
--- a/Hardware/Star64/index.md
+++ b/Hardware/Star64/index.md
@@ -7,7 +7,7 @@ arch: RV64GBC, RV64IMAC, RV32IMAFBC
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: "Community"
 Maintained: "seL4 Foundation"
 soc: StarFive JH7110
diff --git a/Hardware/ariane.md b/Hardware/ariane.md
index 664cdfc1439..2ebc1b4f222 100644
--- a/Hardware/ariane.md
+++ b/Hardware/ariane.md
@@ -7,7 +7,7 @@ arch: RV64IMAC
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: "Data61"
 Maintained: "Hensoldt Cyber"
 cpu: Ariane (CVA6)
diff --git a/Hardware/bananapi-f3.md b/Hardware/bananapi-f3.md
index dbc2717e23f..25648cc98ad 100644
--- a/Hardware/bananapi-f3.md
+++ b/Hardware/bananapi-f3.md
@@ -7,7 +7,7 @@ arch: RV64GCVB
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: "Community"
 Maintained: "10xEngineers"
 soc: SpacemiT K1
diff --git a/Hardware/cheshire.md b/Hardware/cheshire.md
index 6aeb52e5ac3..48a1c666ed9 100644
--- a/Hardware/cheshire.md
+++ b/Hardware/cheshire.md
@@ -7,7 +7,7 @@ arch: RV64IMAFDC
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: "UNSW"
 Maintained: "UNSW"
 cpu: Cheshire
diff --git a/Hardware/hifive-p550.md b/Hardware/hifive-p550.md
index d34286803e7..e74e640ad9c 100644
--- a/Hardware/hifive-p550.md
+++ b/Hardware/hifive-p550.md
@@ -7,7 +7,7 @@ arch: RV64GC
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: "Community"
 Maintained: "seL4 Foundation"
 soc: ESWIN EIC7700X
diff --git a/Hardware/polarfire.md b/Hardware/polarfire.md
index 96fa62dfcad..f2c74b08162 100644
--- a/Hardware/polarfire.md
+++ b/Hardware/polarfire.md
@@ -7,7 +7,7 @@ arch: RV64IMAC, RV64GC
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: '<a href="https://dornerworks.com">DornerWorks</a>'
 Maintained: '<a href="https://dornerworks.com">DornerWorks</a>'
 soc: PolarFire SoC FPGA
diff --git a/Hardware/rocketchip-zcu102.md b/Hardware/rocketchip-zcu102.md
index 4d90174eec6..6be691931d9 100644
--- a/Hardware/rocketchip-zcu102.md
+++ b/Hardware/rocketchip-zcu102.md
@@ -2,12 +2,12 @@
 riscv_hardware: true
 cmake_plat: rocketchip-zcu102
 xcompiler_arg: -DRISCV64=1
-platform: Rocketchip
+platform: Rocketchip (zcu102)
 arch: RV64IMAFDC
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: '<a href="https://dornerworks.com">DornerWorks</a>'
 Maintained: '<a href="https://dornerworks.com">DornerWorks</a>'
 cpu: Rocket
diff --git a/Hardware/rocketchip.md b/Hardware/rocketchip.md
index 3f9dd82b31f..52e75312782 100644
--- a/Hardware/rocketchip.md
+++ b/Hardware/rocketchip.md
@@ -7,7 +7,7 @@ arch: RV64IMAFDC
 virtualization: false
 iommu: false
 simulation_target: false
-verification: []
+verification: [RISCV64]
 Contrib: Data61
 Maintained: seL4 Foundation
 cpu: Rocket
diff --git a/Hardware/spike.md b/Hardware/spike.md
index 907169ec712..bf08ac886c7 100644
--- a/Hardware/spike.md
+++ b/Hardware/spike.md
@@ -7,6 +7,7 @@ arch: RV32GC, RV64IMAFDC
 virtualization: false
 iommu: false
 simulation_target: true
+simulation_only: true
 verification: []
 Contrib: 'Data61, <a href="https://github.com/heshamelmatary">Hesham Almatary</a>'
 Maintained: "seL4 Foundation"
diff --git a/projects/sel4/verified-configurations.md b/projects/sel4/verified-configurations.md
index e0d38f1c56b..e171ccae750 100644
--- a/projects/sel4/verified-configurations.md
+++ b/projects/sel4/verified-configurations.md
@@ -29,23 +29,28 @@ Current verified configurations can be found in seL4 sources in the
 ```sh
 cd configs/
 ls *_verified.cmake
-# AARCH64_bcm2711_verified.cmake    ARM_exynos5410_verified.cmake
-# AARCH64_hikey_verified.cmake      ARM_exynos5422_verified.cmake
-# AARCH64_imx8mm_verified.cmake     ARM_hikey_verified.cmake
-# AARCH64_imx8mq_verified.cmake     ARM_HYP_exynos5_verified.cmake
-# AARCH64_imx93_verified.cmake      ARM_HYP_exynos5410_verified.cmake
-# AARCH64_maaxboard_verified.cmake  ARM_HYP_verified.cmake
-# AARCH64_odroidc2_verified.cmake   ARM_imx8mm_verified.cmake
-# AARCH64_odroidc4_verified.cmake   ARM_MCS_verified.cmake
-# AARCH64_rockpro64_verified.cmake  ARM_omap3_verified.cmake
-# AARCH64_tqma_verified.cmake       ARM_tk1_verified.cmake
-# AARCH64_tx1_verified.cmake        ARM_verified.cmake
-# AARCH64_ultra96v2_verified.cmake  ARM_zynq7000_verified.cmake
-# AARCH64_verified.cmake            ARM_zynqmp_verified.cmake
-# AARCH64_zynqmp_verified.cmake     RISCV64_MCS_verified.cmake
-# ARM_am335x_verified.cmake         RISCV64_verified.cmake
-# ARM_bcm2837_verified.cmake        X64_verified.cmake
-# ARM_exynos4_verified.cmake
+# AARCH64_bcm2711_verified.cmake           ARM_hikey_verified.cmake
+# AARCH64_bcm2712_verified.cmake           ARM_HYP_exynos5_verified.cmake
+# AARCH64_hikey_verified.cmake             ARM_HYP_exynos5410_verified.cmake
+# AARCH64_imx8mm_verified.cmake            ARM_HYP_verified.cmake
+# AARCH64_imx8mq_verified.cmake            ARM_imx8mm_verified.cmake
+# AARCH64_imx93_verified.cmake             ARM_MCS_verified.cmake
+# AARCH64_maaxboard_verified.cmake         ARM_omap3_verified.cmake
+# AARCH64_MCS_verified.cmake               ARM_tk1_verified.cmake
+# AARCH64_odroidc2_verified.cmake          ARM_verified.cmake
+# AARCH64_odroidc4_verified.cmake          ARM_zynq7000_verified.cmake
+# AARCH64_rockpro64_verified.cmake         ARM_zynqmp_verified.cmake
+# AARCH64_stm32mp2_verified.cmake          RISCV64_ariane_verified.cmake
+# AARCH64_tqma_verified.cmake              RISCV64_bananapi-f3_verified.cmake
+# AARCH64_tx1_verified.cmake               RISCV64_cheshire_verified.cmake
+# AARCH64_ultra96v2_verified.cmake         RISCV64_hifive-p550_verified.cmake
+# AARCH64_verified.cmake                   RISCV64_MCS_verified.cmake
+# AARCH64_zynqmp_verified.cmake            RISCV64_polarfire_verified.cmake
+# ARM_am335x_verified.cmake                RISCV64_rocketchip_verified.cmake
+# ARM_bcm2837_verified.cmake               RISCV64_rocketchip-zcu102_verified.cmake
+# ARM_exynos4_verified.cmake               RISCV64_star64_verified.cmake
+# ARM_exynos5410_verified.cmake            RISCV64_verified.cmake
+# ARM_exynos5422_verified.cmake            X64_verified.cmake
 ```
 
 To obtain specific source code and build for a given configuration (e.g.
@@ -73,10 +78,9 @@ At present, none of our verified configurations take into account
 address translation for devices (System MMU or IOMMU), debug/profiling/printing
 interfaces, or the kernel startup at boot.
 
-The proofs for RISCV64\_MCS/ARM\_MCS (mixed-criticality extensions to real-time
-seL4 features), as well as confidentiality proofs for AARCH64 are in progress.
-Refer to the [roadmap](https://sel4.systems/roadmap.html) for status and
-upcoming features.
+The proofs for AARCH64\_MCS/ARM\_MCS (mixed-criticality extensions to real-time
+seL4 features) are in progress. Refer to the
+[roadmap](https://sel4.systems/roadmap.html) for status and upcoming features.
 
 ### Arm Aarch32 (`ARM`) {#ARM}
 
@@ -156,6 +160,7 @@ The following properties are verified:
 
 - C-level functional correctness, including fast path
 - integrity and availability (access control)
+- confidentiality (information flow)
 
 Further properties are under development. See also the
 [roadmap](https://sel4.systems/roadmap.html) for status and schedule.