diff --git a/docs/getting_started/build-options.rst b/docs/getting_started/build-options.rst
index de0e8cc9..805482b8 100644
--- a/docs/getting_started/build-options.rst
+++ b/docs/getting_started/build-options.rst
@@ -282,6 +282,7 @@ The |RMM| build system supports the following CMake build options.
    RMM_COVERAGE 		,ON | OFF		,OFF			,"Enable coverage analysis"
    RMM_HTML_COV_REPORT		,ON | OFF		,ON			,"Enable HTML output report for coverage analysis"
    RMM_CBMC_VIEWER_OUTPUT	,ON | OFF		,OFF			,"Generate report of CBMC results using the tool cbmc-viewer"
+   RMM_CBMC_SINGLE_TESTBENCH	,			,OFF			,"Run CBMC on a single testbench instead on all of them"
 
 .. _llvm_build:
 
diff --git a/docs/resources/application-notes/cbmc.rst b/docs/resources/application-notes/cbmc.rst
index 0564ef35..60569bec 100644
--- a/docs/resources/application-notes/cbmc.rst
+++ b/docs/resources/application-notes/cbmc.rst
@@ -53,6 +53,12 @@ each build.
 
 For an example build command please refer to :ref:`RMM Build Examples`
 
+The CMake system by default runs CBMC on all the testbenches. This can take a
+long time, and it can be convenient to run a single testcase at once. This can
+be achieved using the option ``-DRMM_CBMC_SINGLE_TESTBENCH="testbench_name"``.
+The list of possible ``testbench_name``s can be listed by using the option
+``-DRMM_CBMC_SINGLE_TESTBENCH="help"``.
+
 The CMake system provides different modes in which CBMC can be called, along
 with their respective build targets.
 
diff --git a/lib/arch/include/arch_features.h b/lib/arch/include/arch_features.h
index d8468096..7d16f570 100644
--- a/lib/arch/include/arch_features.h
+++ b/lib/arch/include/arch_features.h
@@ -111,6 +111,13 @@ static inline bool is_feat_hpmn0_present(void)
 		read_id_aa64dfr0_el1()) == 1UL);
 }
 
+#ifndef CBMC
 unsigned int arch_feat_get_pa_width(void);
+#else /* CBMC */
+static inline unsigned int arch_feat_get_pa_width(void)
+{
+	return 32U;
+}
+#endif /* CBMC */
 
 #endif /* ARCH_FEATURES_H */
diff --git a/lib/arch/include/simd.h b/lib/arch/include/simd.h
index 848179ec..89f2d267 100644
--- a/lib/arch/include/simd.h
+++ b/lib/arch/include/simd.h
@@ -187,7 +187,15 @@ COMPILER_ASSERT((U(offsetof(struct sve_regs, ffr))) == SVE_REGS_OFFSET_FFR);
 void simd_init(void);
 
 /* Returns the CPU SIMD config discovered during the init time */
+#ifndef CBMC
 int simd_get_cpu_config(struct simd_config *simd_cfg);
+#else /* CBMC */
+static inline int simd_get_cpu_config(struct simd_config *simd_cfg)
+{
+	memset(simd_cfg, 0, sizeof(*simd_cfg));
+	return 0;
+}
+#endif /* CBMC */
 
 /* Initialize the SIMD context in RMM corresponding to NS world or Realm */
 int simd_context_init(simd_owner_t owner, struct simd_context *simd_ctx,
diff --git a/lib/measurement/include/measurement.h b/lib/measurement/include/measurement.h
index 1254b28c..9b4288eb 100644
--- a/lib/measurement/include/measurement.h
+++ b/lib/measurement/include/measurement.h
@@ -41,11 +41,15 @@ enum hash_algo {
 #define MEASURE_DESC_TYPE_REC		0x1
 #define MEASURE_DESC_TYPE_RIPAS		0x2
 
+#ifndef CBMC
 /*
  * Size in bytes of the largest measurement type that can be supported.
  * This macro needs to be updated accordingly if new algorithms are supported.
  */
 #define MAX_MEASUREMENT_SIZE		SHA512_SIZE
+#else
+#define MAX_MEASUREMENT_SIZE		sizeof(uint64_t)
+#endif
 
 /* RmmMeasurementDescriptorData type as per RMM spec */
 struct measurement_desc_data {
diff --git a/lib/realm/include/realm.h b/lib/realm/include/realm.h
index c2dd30ba..f8ec50fd 100644
--- a/lib/realm/include/realm.h
+++ b/lib/realm/include/realm.h
@@ -12,9 +12,9 @@
 #include <rec.h>
 #include <table.h>
 
-#define REALM_STATE_NEW		0U
-#define REALM_STATE_ACTIVE	1U
-#define REALM_STATE_SYSTEM_OFF	2U
+#define REALM_NEW		0U
+#define REALM_ACTIVE		1U
+#define REALM_SYSTEM_OFF	2U
 
 /*
  * Stage 2 configuration of the Realm
diff --git a/lib/smc/include/smc-rmi.h b/lib/smc/include/smc-rmi.h
index f89f7dfd..78b610c4 100644
--- a/lib/smc/include/smc-rmi.h
+++ b/lib/smc/include/smc-rmi.h
@@ -366,7 +366,15 @@
 #define SMC_RMM_RTT_SET_RIPAS			SMC64_RMI_FID(U(0x19))
 
 /* Size of Realm Personalization Value */
+#ifndef CBMC
 #define RPV_SIZE		64
+#else
+/*
+ * Small RPV size so that `struct rd` fits in the reduced sized granule defined
+ * for CBMC
+ */
+#define RPV_SIZE		1
+#endif
 
 /* RmiRealmFlags format */
 #define RMI_REALM_FLAGS_LPA2_SHIFT	UL(0)
diff --git a/plat/host/host_cbmc/CMakeLists.txt b/plat/host/host_cbmc/CMakeLists.txt
index 38bf6dfe..7a94ea55 100644
--- a/plat/host/host_cbmc/CMakeLists.txt
+++ b/plat/host/host_cbmc/CMakeLists.txt
@@ -19,6 +19,9 @@ target_sources(rmm-plat-host_cbmc
         "src/host_harness.c"
         "src/tb_common.c"
         "src/tb_granules.c"
+        "src/tb_measurement.c"
+        "src/tb_realm.c"
+        "src/tb_rtt.c"
         "src/tb.c"
         )
 
diff --git a/plat/host/host_cbmc/include/tb.h b/plat/host/host_cbmc/include/tb.h
index fd598e1f..6bddf41c 100644
--- a/plat/host/host_cbmc/include/tb.h
+++ b/plat/host/host_cbmc/include/tb.h
@@ -9,6 +9,7 @@
 #include "smc-rmi.h"
 #include "tb_common.h"
 #include "tb_granules.h"
+#include "tb_realm.h"
 
 typedef uint64_t rmi_interface_version_t;
 
diff --git a/plat/host/host_cbmc/include/tb_common.h b/plat/host/host_cbmc/include/tb_common.h
index c77462f3..db84b986 100644
--- a/plat/host/host_cbmc/include/tb_common.h
+++ b/plat/host/host_cbmc/include/tb_common.h
@@ -106,6 +106,8 @@ bool valid_pa(uint64_t addr);
 bool valid_granule_metadata_ptr(struct granule *p);
 struct granule *pa_to_granule_metadata_ptr(uint64_t addr);
 uint64_t granule_metadata_ptr_to_pa(struct granule *g_ptr);
+void *pa_to_granule_buffer_ptr(uint64_t addr);
+
 /* TODO change the function name */
 void init_pa_page(const void *content, size_t size);
 
diff --git a/plat/host/host_cbmc/include/tb_granules.h b/plat/host/host_cbmc/include/tb_granules.h
index b5fc79f6..a1971faa 100644
--- a/plat/host/host_cbmc/include/tb_granules.h
+++ b/plat/host/host_cbmc/include/tb_granules.h
@@ -39,7 +39,12 @@ struct SPEC_granule {
 	enum granule_state state;
 };
 
+/*
+ * CBMC needs access to the below data structures which are not otherwise
+ * visible outside their respective files.
+ */
 extern unsigned char granules_buffer[HOST_MEM_SIZE];
+extern struct granule granules[RMM_MAX_GRANULES];
 
 /*
  * Declare nondet_* functions.
diff --git a/plat/host/host_cbmc/include/tb_measurement.h b/plat/host/host_cbmc/include/tb_measurement.h
new file mode 100644
index 00000000..6aa5c2f4
--- /dev/null
+++ b/plat/host/host_cbmc/include/tb_measurement.h
@@ -0,0 +1,13 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_MEASUREMENT_H
+#define TB_MEASUREMENT_H
+
+#include "measurement.h"
+
+bool valid_hash_algo(enum hash_algo value);
+
+#endif /* !TB_MEASUREMENT_H */
diff --git a/plat/host/host_cbmc/include/tb_realm.h b/plat/host/host_cbmc/include/tb_realm.h
new file mode 100644
index 00000000..52dc876e
--- /dev/null
+++ b/plat/host/host_cbmc/include/tb_realm.h
@@ -0,0 +1,65 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_REALM_H
+#define TB_REALM_H
+
+#include <measurement.h>
+#include <realm.h>
+#include <smc-rmi.h>
+#include <tb_granules.h>
+
+#define DESTROYED RIPAS_DESTROYED
+#define EMPTY RIPAS_EMPTY
+#define RAM RIPAS_RAM
+
+extern unsigned long vmids[];
+
+enum rmm_rtt_entry_state {
+	ASSIGNED,
+	ASSIGNED_NS,
+	TABLE,
+	UNASSIGNED,
+	UNASSIGNED_NS,
+};
+
+struct rmm_realm {
+	uint64_t ipa_width;
+	uint64_t measurements[MEASUREMENT_SLOT_NR];
+	uint64_t hash_algo;
+	uint64_t rec_index;
+	uint64_t rtt_base;
+	uint64_t rtt_level_start;
+	uint64_t rtt_num_start;
+	uint64_t state;
+	uint64_t vmid;
+	uint8_t rpv[RPV_SIZE];
+};
+
+struct rmi_realm_params_buffer {
+	uint8_t flags;
+	uint8_t s2sz;
+	uint8_t sve_vl;
+	uint8_t num_bps;
+	uint8_t num_wps;
+	uint8_t pmu_num_ctrs;
+	uint8_t hash_algo;
+	uint8_t rpv[RPV_SIZE];
+	uint16_t vmid;
+	uint64_t rtt_base;
+	int64_t rtt_level_start;
+	uint32_t rtt_num_start;
+};
+
+bool VmidIsFree(uint16_t vmid);
+struct rmm_realm Realm(uint64_t rd);
+
+struct rd nondet_struct_rd(void);
+struct rmm_realm nondet_struct_rmm_realm(void);
+
+struct granule *init_realm_descriptor_page(void);
+
+#endif /* TB_REALM_H */
+
diff --git a/plat/host/host_cbmc/include/tb_rtt.h b/plat/host/host_cbmc/include/tb_rtt.h
new file mode 100644
index 00000000..81ffe2fd
--- /dev/null
+++ b/plat/host/host_cbmc/include/tb_rtt.h
@@ -0,0 +1,12 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#ifndef TB_RTT_H
+#define TB_RTT_H
+
+bool valid_num_root_rtts(unsigned int num_root_rtts);
+struct granule *init_rtt_root_page(unsigned int num_root_rtts);
+
+#endif
diff --git a/plat/host/host_cbmc/src/tb.c b/plat/host/host_cbmc/src/tb.c
index 27728037..945bbc26 100644
--- a/plat/host/host_cbmc/src/tb.c
+++ b/plat/host/host_cbmc/src/tb.c
@@ -11,6 +11,7 @@
 #include "tb.h"
 #include "tb_common.h"
 #include "tb_granules.h"
+#include "tb_realm.h"
 
 void __init_global_state(unsigned long cmd)
 {
@@ -24,6 +25,10 @@ void __init_global_state(unsigned long cmd)
 			init_granule_and_page();
 			return;
 		}
+	case SMC_RMM_REALM_ACTIVATE:{
+			init_realm_descriptor_page();
+			return;
+	}
 	case SMC_RMM_FEATURES:
 	case SMC_RMM_VERSION: {
 			/* No state to initialize */
@@ -52,6 +57,9 @@ void tb_handle_smc(struct tb_regs *config)
 	case SMC_RMM_GRANULE_UNDELEGATE:
 		result = smc_granule_undelegate(config->X1);
 		break;
+	case SMC_RMM_REALM_ACTIVATE:
+		result = smc_realm_activate(config->X1);
+		break;
 	case SMC_RMM_VERSION:
 		smc_version(config->X1, &res);
 		result = res.x[0];
diff --git a/plat/host/host_cbmc/src/tb_common.c b/plat/host/host_cbmc/src/tb_common.c
index 4f941745..629c43d5 100644
--- a/plat/host/host_cbmc/src/tb_common.c
+++ b/plat/host/host_cbmc/src/tb_common.c
@@ -94,6 +94,28 @@ struct granule *pa_to_granule_metadata_ptr(uint64_t addr)
 	return &granules[idx];
 }
 
+uint64_t granule_metadata_ptr_to_pa(struct granule *g_ptr)
+{
+	return (uint64_t)granules_buffer + (g_ptr - granules) * GRANULE_SIZE;
+}
+
+void *pa_to_granule_buffer_ptr(uint64_t addr)
+{
+	__ASSERT((unsigned char *)addr - granules_buffer >= 0,
+		"internal: `_pa_to_granule_buffer_ptr`, addr is in lower range");
+	/*
+	 * CBMC has difficulty doing an integer->object mapping, when the
+	 * integer is the address of the expected object, and the integer is not
+	 * derived from a pointer.
+	 * So instead of simply returning addr we need to tell CBMC that the
+	 * object we are looking for is in the `granules_buffer` array, at an
+	 * offset. To calculate the offset we can use `addr`, and the address of
+	 * `granules_buffer`.
+	 * For details see https://github.com/diffblue/cbmc/issues/8103
+	 */
+	return (void *)granules_buffer + ((unsigned char *)addr - granules_buffer);
+}
+
 bool valid_granule_metadata_ptr(struct granule *p)
 {
 	return p >= granules
@@ -140,6 +162,13 @@ struct granule *inject_granule_at(const struct granule *granule_metadata,
 {
 	size_t offset = index * GRANULE_SIZE;
 
+	if (granule_metadata->state == GRANULE_STATE_NS) {
+		/* initialise the granules as either secure or non-secure */
+		granule_gpt_array[index] = nondet_bool() ? GPT_SECURE : GPT_NS;
+	} else {
+		granule_gpt_array[index] = GPT_REALM;
+	}
+
 	granules[index] = *granule_metadata;
 	(void)memcpy(granules_buffer + offset, src_page, src_size);
 	used_granules_buffer[index] = true;
@@ -152,13 +181,6 @@ struct granule *inject_granule(const struct granule *granule_metadata,
 {
 	size_t index = next_index();
 
-	if (granule_metadata->state == GRANULE_STATE_NS) {
-		/* initialise the granules as either secure or non-secure */
-		granule_gpt_array[index] = nondet_bool() ? GPT_SECURE : GPT_NS;
-	} else {
-		granule_gpt_array[index] = GPT_REALM;
-	}
-
 	return inject_granule_at(granule_metadata, src_page, src_size, index);
 }
 
diff --git a/plat/host/host_cbmc/src/tb_granules.c b/plat/host/host_cbmc/src/tb_granules.c
index d66e2ad6..a7281cd2 100644
--- a/plat/host/host_cbmc/src/tb_granules.c
+++ b/plat/host/host_cbmc/src/tb_granules.c
@@ -14,8 +14,6 @@
 #include "tb_common.h"
 #include "tb_granules.h"
 
-extern struct granule granules[RMM_MAX_GRANULES];
-
 /* Chooses an arbitrary granule state. */
 bool valid_granule_state(enum granule_state value)
 {
diff --git a/plat/host/host_cbmc/src/tb_measurement.c b/plat/host/host_cbmc/src/tb_measurement.c
new file mode 100644
index 00000000..cb21e032
--- /dev/null
+++ b/plat/host/host_cbmc/src/tb_measurement.c
@@ -0,0 +1,13 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include "measurement.h"
+#include "tb_measurement.h"
+
+bool valid_hash_algo(enum hash_algo value)
+{
+	return value == RMI_HASH_SHA_256 ||
+	       value == RMI_HASH_SHA_512;
+}
diff --git a/plat/host/host_cbmc/src/tb_realm.c b/plat/host/host_cbmc/src/tb_realm.c
new file mode 100644
index 00000000..bc0aadb5
--- /dev/null
+++ b/plat/host/host_cbmc/src/tb_realm.c
@@ -0,0 +1,150 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include "granule.h"
+#include "realm.h"
+#include "ripas.h"
+#include "tb_common.h"
+#include "tb_granules.h"
+#include "tb_measurement.h"
+#include "tb_realm.h"
+#include "tb_rtt.h"
+
+#define VMID8_COUNT		(U(1) << 8)
+#define VMID16_COUNT		(U(1) << 16)
+
+bool VmidIsFree(uint16_t vmid)
+{
+	unsigned int offset = vmid / BITS_PER_UL;
+	unsigned int vmid_bit = vmid % BITS_PER_UL;
+	uint64_t bit_mask = (uint64_t)(1UL << vmid_bit);
+	/* return TRUE if the bit at the bit_mask is ZERO. */
+	return (vmids[offset] & bit_mask) == 0;
+}
+
+struct rmm_realm Realm(uint64_t addr)
+{
+	size_t i;
+
+	/*
+	 * TODO: change to a unified function call
+	 * Find the realm ptr related to `addr`.
+	 * If it is NULL, return the `nondet_realm` realm.
+	 */
+	if (!valid_pa(addr)) {
+		return nondet_struct_rmm_realm();
+	}
+
+	struct rd *rd_ptr = pa_to_granule_buffer_ptr(addr);
+
+	__CPROVER_assert(rd_ptr, "internal: `_Realm` rd_ptr is not null");
+
+
+	/* convert the type */
+	struct rmm_realm spec_rd = {
+		.ipa_width = rd_ptr->s2_ctx.ipa_bits,
+		.hash_algo = rd_ptr->algorithm,
+		.rec_index = rd_ptr->rec_count,
+		.rtt_base = granule_metadata_ptr_to_pa(rd_ptr->s2_ctx.g_rtt),
+		.rtt_level_start = rd_ptr->s2_ctx.s2_starting_level,
+		.rtt_num_start = rd_ptr->s2_ctx.num_root_rtts,
+		.state = rd_ptr->state,
+		.vmid = rd_ptr->s2_ctx.vmid
+	};
+
+	for (i = 0; i < MEASUREMENT_SLOT_NR; ++i) {
+		spec_rd.measurements[i] = (uint64_t)(rd_ptr->measurement[i]);
+	}
+	for (i = 0; i < sizeof(spec_rd.rpv); ++i) {
+		spec_rd.rpv[i] = rd_ptr->rpv[i];
+	}
+
+	return spec_rd;
+}
+
+bool valid_realm_state(uint64_t value)
+{
+	return value == (uint64_t)REALM_NEW
+		|| value == (uint64_t)REALM_ACTIVE
+		|| value == (uint64_t)REALM_SYSTEM_OFF;
+}
+
+/* Detail of the valid state */
+bool valid_realm_s2_context(struct realm_s2_context value)
+{
+	unsigned int vmid_count = is_feat_vmid16_present() ? VMID16_COUNT : VMID8_COUNT;
+
+	return  value.s2_starting_level >= 0
+		&& value.s2_starting_level <= 3
+		/* TODO focus on standard size of root rtt for now */
+		&& value.num_root_rtts >= 1
+		/* && value.num_root_rtts <= 16 */
+		&& value.num_root_rtts <= 2
+		&& valid_granule_metadata_ptr(value.g_rtt)
+		&& value.g_rtt->state == GRANULE_STATE_RTT
+		/* TODO: what is the ranges here */
+		&& value.ipa_bits == (3 - value.s2_starting_level + 1) *
+			S2TTE_STRIDE + value.num_root_rtts
+		/* TODO check */
+		&& value.vmid < vmid_count;
+}
+
+bool valid_rd(struct rd value)
+{
+	return valid_realm_state(value.state)
+		&& valid_realm_s2_context(value.s2_ctx)
+		&& valid_hash_algo(value.algorithm)
+		&& value.num_rec_aux <= MAX_REC_AUX_GRANULES;
+}
+
+struct rd init_rd(void)
+{
+	struct rd value = nondet_struct_rd();
+
+	unsigned int num_root_rtts = nondet_unsigned_int();
+
+	__CPROVER_assume(valid_num_root_rtts(num_root_rtts));
+	struct granule *g_root_rtt = init_rtt_root_page(num_root_rtts);
+
+	value.s2_ctx.num_root_rtts = num_root_rtts;
+	value.s2_ctx.g_rtt = g_root_rtt;
+	value.rpv[0] = 0;
+	/*
+	 * If the `g_root_rtt` does not satisfy the assume condition, all
+	 * following `cover` checks fail.
+	 */
+	__CPROVER_assume(valid_rd(value));
+
+	/* Non-deterministically if the vmid is registered. */
+	uint64_t vmid = value.s2_ctx.vmid;
+	unsigned int offset = vmid / BITS_PER_UL;
+
+	vmid %= BITS_PER_UL;
+	uint64_t bit_mask = (uint64_t)(1UL << vmid);
+
+	if (nondet_bool()) {
+		vmids[offset] |= bit_mask;
+	}
+
+	return value;
+}
+
+struct granule *init_realm_descriptor_page(void)
+{
+	struct granule g = init_granule();
+
+	__CPROVER_assume(g.state == GRANULE_STATE_RD);
+	struct rd rd = init_rd();
+
+	/*
+	 * This assert is necessary because the COMPILER_ASSERT in realm.h is
+	 * disabled for CBMC.
+	 */
+	__CPROVER_assert(sizeof(struct rd) <= GRANULE_SIZE, "check size");
+
+	struct granule *rd_granule = inject_granule(&g, &rd, sizeof(rd));
+
+	return rd_granule;
+}
diff --git a/plat/host/host_cbmc/src/tb_rtt.c b/plat/host/host_cbmc/src/tb_rtt.c
new file mode 100644
index 00000000..4872fe75
--- /dev/null
+++ b/plat/host/host_cbmc/src/tb_rtt.c
@@ -0,0 +1,36 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ */
+
+#include <tb_common.h>
+#include <tb_granules.h>
+
+/* The valid range is smaller than in the specification */
+bool valid_num_root_rtts(unsigned int num_root_rtts)
+{
+	return num_root_rtts >= 1 && num_root_rtts <= 2;
+}
+
+struct granule *init_rtt_root_page(unsigned int num_root_rtts)
+{
+	__CPROVER_assert(valid_num_root_rtts(num_root_rtts),
+		"Internal: `_init_rtt_root_page` valid numbers of root rtt");
+
+	/* The first root rtt granule is granules[index]. */
+	size_t index = next_index();
+	struct granule *before = &granules[index];
+
+	for (size_t i = index; i < index + num_root_rtts && i < index + 16; ++i) {
+		__CPROVER_assume(unused_index(i));
+		struct granule g = init_granule();
+
+		__CPROVER_assume(g.state == GRANULE_STATE_RTT);
+		/* We assume there are at least one unused slot. */
+		__CPROVER_assume(g.refcount < (GRANULE_SIZE / sizeof(uint64_t)));
+
+		char rtt_content[GRANULE_SIZE] = { 0 };
+		struct granule *after = inject_granule_at(&g, rtt_content, sizeof(rtt_content), i);
+	}
+	return &granules[index];
+}
diff --git a/runtime/core/vmid.c b/runtime/core/vmid.c
index 22e3e7ab..ba9738aa 100644
--- a/runtime/core/vmid.c
+++ b/runtime/core/vmid.c
@@ -7,6 +7,7 @@
 #include <assert.h>
 #include <atomics.h>
 #include <sizes.h>
+#include <utils_def.h>
 #include <vmid.h>
 
 #define VMID8_COUNT		(U(1) << 8)
@@ -17,7 +18,7 @@
 /*
  * The bitmap for the reserved/used VMID values.
  */
-static unsigned long vmids[VMID_ARRAY_LONG_SIZE];
+IF_NCBMC(static) unsigned long vmids[VMID_ARRAY_LONG_SIZE];
 
 /*
  * Marks the VMID value to be in use. It returns:
diff --git a/runtime/rmi/realm.c b/runtime/rmi/realm.c
index f4554e7b..78c94247 100644
--- a/runtime/rmi/realm.c
+++ b/runtime/rmi/realm.c
@@ -35,8 +35,8 @@ unsigned long smc_realm_activate(unsigned long rd_addr)
 	rd = granule_map(g_rd, SLOT_RD);
 	assert(rd != NULL);
 
-	if (get_rd_state_locked(rd) == REALM_STATE_NEW) {
-		set_rd_state(rd, REALM_STATE_ACTIVE);
+	if (get_rd_state_locked(rd) == REALM_NEW) {
+		set_rd_state(rd, REALM_ACTIVE);
 		ret = RMI_SUCCESS;
 	} else {
 		ret = RMI_ERROR_REALM;
@@ -376,7 +376,7 @@ unsigned long smc_realm_create(unsigned long rd_addr,
 	rd = granule_map(g_rd, SLOT_RD);
 	assert(rd != NULL);
 
-	set_rd_state(rd, REALM_STATE_NEW);
+	set_rd_state(rd, REALM_NEW);
 	set_rd_rec_count(rd, 0UL);
 	rd->s2_ctx.g_rtt = find_granule(p.rtt_base);
 	rd->s2_ctx.ipa_bits = p.s2sz;
diff --git a/runtime/rmi/rec.c b/runtime/rmi/rec.c
index c6b39c58..be830349 100644
--- a/runtime/rmi/rec.c
+++ b/runtime/rmi/rec.c
@@ -282,7 +282,7 @@ unsigned long smc_rec_create(unsigned long rd_addr,
 	rd = granule_map(g_rd, SLOT_RD);
 	assert(rd != NULL);
 
-	if (get_rd_state_locked(rd) != REALM_STATE_NEW) {
+	if (get_rd_state_locked(rd) != REALM_NEW) {
 		ret = RMI_ERROR_REALM;
 		goto out_unmap;
 	}
diff --git a/runtime/rmi/rtt.c b/runtime/rmi/rtt.c
index a4fd65db..6afbef99 100644
--- a/runtime/rmi/rtt.c
+++ b/runtime/rmi/rtt.c
@@ -861,7 +861,7 @@ static unsigned long validate_data_create_unknown(unsigned long map_addr,
 static unsigned long validate_data_create(unsigned long map_addr,
 					  struct rd *rd)
 {
-	if (get_rd_state_locked(rd) != REALM_STATE_NEW) {
+	if (get_rd_state_locked(rd) != REALM_NEW) {
 		return RMI_ERROR_REALM;
 	}
 
@@ -1220,7 +1220,7 @@ void smc_rtt_init_ripas(unsigned long rd_addr,
 		return;
 	}
 
-	if (get_rd_state_locked(rd) != REALM_STATE_NEW) {
+	if (get_rd_state_locked(rd) != REALM_NEW) {
 		buffer_unmap(rd);
 		granule_unlock(g_rd);
 		res->x[0] = RMI_ERROR_REALM;
diff --git a/runtime/rmi/run.c b/runtime/rmi/run.c
index 7eaa1413..eed04ef0 100644
--- a/runtime/rmi/run.c
+++ b/runtime/rmi/run.c
@@ -223,12 +223,12 @@ unsigned long smc_rec_enter(unsigned long rec_addr,
 	buffer_unmap(rd);
 
 	switch (realm_state) {
-	case REALM_STATE_NEW:
+	case REALM_NEW:
 		ret = pack_return_code(RMI_ERROR_REALM, 0U);
 		goto out_unmap_buffers;
-	case REALM_STATE_ACTIVE:
+	case REALM_ACTIVE:
 		break;
-	case REALM_STATE_SYSTEM_OFF:
+	case REALM_SYSTEM_OFF:
 		ret = pack_return_code(RMI_ERROR_REALM, 1U);
 		goto out_unmap_buffers;
 	default:
diff --git a/runtime/rsi/psci.c b/runtime/rsi/psci.c
index 4769e369..1b42da17 100644
--- a/runtime/rsi/psci.c
+++ b/runtime/rsi/psci.c
@@ -231,7 +231,7 @@ static void system_off_reboot(struct rec *rec)
 	rd = granule_map(rec->realm_info.g_rd, SLOT_RD);
 	assert(rd != NULL);
 
-	set_rd_state(rd, REALM_STATE_SYSTEM_OFF);
+	set_rd_state(rd, REALM_SYSTEM_OFF);
 
 	buffer_unmap(rd);
 	granule_unlock(g_rd);
diff --git a/tools/cbmc/CMakeLists.txt b/tools/cbmc/CMakeLists.txt
index d6218dbf..7d11b72f 100644
--- a/tools/cbmc/CMakeLists.txt
+++ b/tools/cbmc/CMakeLists.txt
@@ -9,12 +9,36 @@ arm_config_option(
   HELP "Use XML format for CBMC output and generate cbmc-viewer report."
   DEFAULT OFF)
 
+arm_config_option(
+    NAME RMM_CBMC_SINGLE_TESTBENCH
+    HELP "Run CBMC on a single testbench instead on all of them."
+    DEFAULT OFF)
+
 if("${RMM_CBMC_STATIC_ANALYSIS}")
 
+  set (TESTBENCH_DIR "${CMAKE_CURRENT_SOURCE_DIR}/testbenches")
+
   if (NOT (${HOST_VARIANT} STREQUAL "host_cbmc"))
     message(FATAL_ERROR "cbmc analysis requires host variant `host_cbmc`. (Add `-DHOST_VARIANT=host_cbmc`)")
   endif()
 
+  file(GLOB_RECURSE TESTBENCH_FILES "${TESTBENCH_DIR}/*.c")
+  if(RMM_CBMC_SINGLE_TESTBENCH)
+    set(TESTBENCH_NAMES ${TESTBENCH_FILES})
+    list(TRANSFORM TESTBENCH_NAMES REPLACE "\\.c" "")
+    list(TRANSFORM TESTBENCH_NAMES REPLACE "${TESTBENCH_DIR}/" "")
+    if (NOT "${RMM_CBMC_SINGLE_TESTBENCH}" IN_LIST TESTBENCH_NAMES)
+      message(STATUS "Invalid testbench name '${RMM_CBMC_SINGLE_TESTBENCH}'")
+      message(STATUS "The valid options are: ")
+      foreach(tb ${TESTBENCH_NAMES})
+        message(STATUS "  ${tb}")
+      endforeach()
+      message(FATAL_ERROR "Invalid testbench name '${RMM_CBMC_SINGLE_TESTBENCH}'")
+    else()
+      set(TESTBENCH_FILES "${TESTBENCH_DIR}/${RMM_CBMC_SINGLE_TESTBENCH}.c")
+    endif()
+  endif()
+
   #
   # Create the list of source files and include directories that are to be
   # included in the analysis.
@@ -59,7 +83,8 @@ if("${RMM_CBMC_STATIC_ANALYSIS}")
     -DRMM_CBMC_CONFIGURATION=COVERAGE
     -DSOURCE_DIR=${CMAKE_SOURCE_DIR}
     -DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
-    -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+    -DTESTBENCH_DIR="${TESTBENCH_DIR}"
+    -DTESTBENCH_FILES="${TESTBENCH_FILES}"
     -DRMM_IMP_SRCS="${rmm_implementation_srcs}"
     -DRMM_IMP_INCS="${rmm_implementation_includes}"
     -P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
@@ -72,7 +97,8 @@ if("${RMM_CBMC_STATIC_ANALYSIS}")
     -DRMM_CBMC_VIEWER_OUTPUT=${RMM_CBMC_VIEWER_OUTPUT}
     -DSOURCE_DIR=${CMAKE_SOURCE_DIR}
     -DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
-    -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+    -DTESTBENCH_DIR="${TESTBENCH_DIR}"
+    -DTESTBENCH_FILES="${TESTBENCH_FILES}"
     -DRMM_IMP_SRCS="${rmm_implementation_srcs}"
     -DRMM_IMP_INCS="${rmm_implementation_includes}"
     -P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
@@ -85,7 +111,8 @@ if("${RMM_CBMC_STATIC_ANALYSIS}")
     -DRMM_CBMC_VIEWER_OUTPUT=${RMM_CBMC_VIEWER_OUTPUT}
     -DSOURCE_DIR=${CMAKE_SOURCE_DIR}
     -DBINARY_DIR=${CMAKE_CURRENT_BINARY_DIR}
-    -DTESTBENCH_DIR="${CMAKE_CURRENT_SOURCE_DIR}/testbenches"
+    -DTESTBENCH_DIR="${TESTBENCH_DIR}"
+    -DTESTBENCH_FILES="${TESTBENCH_FILES}"
     -DRMM_IMP_SRCS="${rmm_implementation_srcs}"
     -DRMM_IMP_INCS="${rmm_implementation_includes}"
     -P ${CMAKE_SOURCE_DIR}/tools/cbmc/CheckCBMC.cmake
diff --git a/tools/cbmc/CheckCBMC.cmake b/tools/cbmc/CheckCBMC.cmake
index 0ce1a180..e31e82fa 100644
--- a/tools/cbmc/CheckCBMC.cmake
+++ b/tools/cbmc/CheckCBMC.cmake
@@ -54,26 +54,26 @@ set(MAX_UNWIND_FLAGS "")
 # Set up cbmc command line
 #
 set(cbmc_unwinds_list
+  "--unwindset;find_lock_granules.3:${MAX_ROOT_RTT}"
   "--unwindset;find_lock_rd_granules.0:${MAX_RTT_UNWIND}"
   "--unwindset;find_lock_rd_granules.1:${MAX_RTT_UNWIND}"
-  "--unwindset;smc_realm_create.0:${MAX_RTT_UNWIND}"
-  "--unwindset;total_root_rtt_refcount.0:${MAX_RTT_UNWIND}"
-  "--unwindset;free_sl_rtts.0:${MAX_RTT_UNWIND}"
-  "--unwindset;rtt_walk_lock_unlock.0:${MAX_RTT_UNWIND}"
-  "--unwindset;RttWalk.0:${MAX_RTT_UNWIND}"
-  "--unwindset;init_walk_path.0:${MAX_RTT_UNWIND}"
-  "--unwindset;smc_rec_create.0:${MAX_AUX_REC}"
   "--unwindset;free_rec_aux_granules.0:${MAX_AUX_REC}"
-  "--unwindset;find_lock_granules.3:${MAX_ROOT_RTT}"
-  "--unwindset;RealmIsLive.0:${MAX_ROOT_RTT}"
-  "--unwindset;init_rtt_root_page.0:${MAX_ROOT_RTT}"
-  "--unwindset;init_rec.0:${MAX_AUX_REC}"
-  "--unwindset;RealmIsLive.2:${MAX_ROOT_RTT}"
+  "--unwindset;free_sl_rtts.0:${MAX_RTT_UNWIND}"
   "--unwindset;init_realm_descriptor_page.0:${MAX_ROOT_RTT}"
+  "--unwindset;init_realm_descriptor_page.1:${MAX_ROOT_RTT}"
   "--unwindset;init_rec.0:${MAX_AUX_REC}"
+  "--unwindset;init_rtt_root_page.0:${MAX_ROOT_RTT}"
+  "--unwindset;init_walk_path.0:${MAX_RTT_UNWIND}"
   "--unwindset;lock_order_invariable.0:21"
   "--unwindset;lock_order_invariable.1:11"
   "--unwindset;lock_order_invariable.2:"
+  "--unwindset;RealmIsLive.0:${MAX_ROOT_RTT}"
+  "--unwindset;RealmIsLive.2:${MAX_ROOT_RTT}"
+  "--unwindset;rtt_walk_lock_unlock.0:${MAX_RTT_UNWIND}"
+  "--unwindset;RttWalk.0:${MAX_RTT_UNWIND}"
+  "--unwindset;smc_realm_create.0:${MAX_RTT_UNWIND}"
+  "--unwindset;smc_rec_create.0:${MAX_AUX_REC}"
+  "--unwindset;total_root_rtt_refcount.0:${MAX_RTT_UNWIND}"
 )
 
 set(cbmc_defines_list
@@ -132,7 +132,8 @@ else()
   message(FATAL_ERROR "Invalid RMM_CBMC_CONFIGURATION '${RMM_CBMC_CONFIGURATION}'")
 endif()
 
-file(GLOB_RECURSE TESTBENCH_FILES "${TESTBENCH_DIR}/*.c")
+# Convert the space separated strings to a CMake list
+string(REPLACE " " ";" TESTBENCH_FILES "${TESTBENCH_FILES}")
 
 #
 # Create semi-colon separated list from white-space seperated ones.
@@ -273,10 +274,12 @@ foreach(testbench_file ${TESTBENCH_FILES})
 endforeach()
 message(STATUS "Result in ${RMM_TESTBENCH_RESULT_DIR}")
 
+list(TRANSFORM TESTBENCH_FILES REPLACE "${TESTBENCH_DIR}/" "" OUTPUT_VARIABLE TESTBENCH_FILENAMES)
 execute_process(
   WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}
   COMMAND ${CHECK_CBMC_SUMMARY_EXECUTABLE}
     ${CMAKE_SOURCE_DIR}/tools/cbmc/testbenches_results/BASELINE.${CBMC_RESULT_FILE_SUFFIX}
+    --testbench-files "${TESTBENCH_FILENAMES}"
     ${RMM_TESTBENCH_RESULT_DIR}/${SUMMARY_FILE}
   OUTPUT_VARIABLE CHECK_SUMMARY_OUTPUT
   ERROR_VARIABLE CHECK_SUMMARY_ERROR
diff --git a/tools/cbmc/compare_summary.py b/tools/cbmc/compare_summary.py
index ca4e4df5..5cec772d 100755
--- a/tools/cbmc/compare_summary.py
+++ b/tools/cbmc/compare_summary.py
@@ -16,6 +16,7 @@
 
 import argparse
 import logging
+import ntpath
 import re
 import sys
 
@@ -158,12 +159,20 @@ def compare_assert_summary(testbench_name, baseline_results, current_results):
     # The number of asserts in the code can change frequently, so don't do a check on it.
 
 
-def compare_summary_lists(baseline_list, actual_list, comparator):
+def compare_summary_lists(baseline_list, actual_list, comparator, testbench_list):
     """
     Compare two summary lists.
 
-    List items are expected to be in the format of a tuple:
-    (testbench name, first integer value, second integer value)
+    Arguments:
+    baseline_list -- List of testbench baseline results
+    actual_list -- List of testbench actual results
+    comparator -- A function that can compare 2 testbench result items
+    testbench_list -- A list of testbenches to be considered. If None, all
+                      testbenches are considered
+
+    baseline_list and  actual_list items are expected to be in the format of a
+    tuple: (testbench name, first integer value, second integer value)
+
     """
     # TODO: check for duplicated lines
     baseline = {summary[0]: summary[1:] for summary in baseline_list}
@@ -174,6 +183,10 @@ def compare_summary_lists(baseline_list, actual_list, comparator):
     # that was triggered by a tetsbench addition/deletion.
     actual_extra = {}
 
+    if testbench_list is not None:
+        baseline = {k: v for k, v in baseline.items() if k in testbench_list}
+        actual_list = [e for e in actual_list if e[0] in testbench_list]
+
     for summary in actual_list:
         testbench_name = summary[0]
         if testbench_name not in baseline.keys():
@@ -191,7 +204,7 @@ def compare_summary_lists(baseline_list, actual_list, comparator):
         )
 
 
-def compare_summary_files(baseline_filename, actual_filename):
+def compare_summary_files(baseline_filename, actual_filename, testbench_list):
     """
     Compare two summary files.
     """
@@ -213,7 +226,7 @@ def compare_summary_files(baseline_filename, actual_filename):
         raise ParseException(f"Unknown summary type {base_type}")
 
     compare_summary_lists(
-        base_summary_list, actual_summary_list, comparators[base_type]
+        base_summary_list, actual_summary_list, comparators[base_type], testbench_list
     )
 
 
@@ -223,10 +236,9 @@ def main():
     """
     parser = argparse.ArgumentParser(description="compare CBMC summary siles")
     parser.add_argument(
-        "-v", "--verbosity",
+        "--testbench-files",
         type=str,
-        choices='',
-        help="The path of the baseline summary file.",
+        help="A semicolon (;) separated list of files to check in the summaries.",
     )
     parser.add_argument(
         "baseline",
@@ -238,8 +250,13 @@ def main():
     )
     args = parser.parse_args()
 
+    if args.testbench_files:
+        testbench_list = [ntpath.basename(p) for p in args.testbench_files.split(";")]
+    else:
+        testbench_list = None
+
     try:
-        compare_summary_files(args.baseline, args.actual)
+        compare_summary_files(args.baseline, args.actual, testbench_list)
     except ParseException as exc:
         logging.error("Failed to compare summaries:")
         logging.error(f"{str(exc)}")
diff --git a/tools/cbmc/testbenches/tb_rmi_realm_activate.c b/tools/cbmc/testbenches/tb_rmi_realm_activate.c
new file mode 100644
index 00000000..b29e2754
--- /dev/null
+++ b/tools/cbmc/testbenches/tb_rmi_realm_activate.c
@@ -0,0 +1,145 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ *
+ * This file was AUTOGENERATED from the RMM specification.
+ * RMM specification source version: 790fd539
+ */
+
+#include "tb.h"
+#include "tb_rmi_realm_activate.h"
+
+bool tb_rmi_realm_activate(
+	uint64_t rd)
+{
+	/*
+	 * Initialize registers
+	 */
+
+	struct tb_regs __tb_regs = __tb_arb_regs();
+
+	__tb_regs.X0 = SMC_RMM_REALM_ACTIVATE;
+	__tb_regs.X1 = (uint64_t)rd;
+
+	/*
+	 * Initialize global state
+	 */
+
+	__init_global_state(__tb_regs.X0);
+
+	/*
+	 * Pre-conditions
+	 */
+
+	bool failure_rd_align_pre = !AddrIsGranuleAligned(rd);
+	bool failure_rd_bound_pre = !PaIsDelegable(rd);
+	bool failure_rd_state_pre = Granule(rd).state != RD;
+	bool failure_realm_state_pre = Realm(rd).state != REALM_NEW;
+	bool no_failures_pre = !failure_rd_align_pre
+		&& !failure_rd_bound_pre
+		&& !failure_rd_state_pre
+		&& !failure_realm_state_pre;
+
+	/*
+	 * Execute command and read the result.
+	 */
+
+	tb_handle_smc(&__tb_regs);
+	uint64_t result = __tb_regs.X0;
+
+	/*
+	 * Post-conditions
+	 */
+
+	bool failure_rd_align_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+	bool failure_rd_bound_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+	bool failure_rd_state_post = ResultEqual_2(result, RMI_ERROR_INPUT);
+	bool failure_realm_state_post = ResultEqual_2(result, RMI_ERROR_REALM);
+	bool success_realm_state_post = Realm(rd).state == REALM_ACTIVE;
+
+	/*
+	 * Failure condition assertions
+	 */
+
+	bool prop_failure_rd_align_ante = failure_rd_align_pre;
+
+	__COVER(prop_failure_rd_align_ante);
+	if (prop_failure_rd_align_ante) {
+		bool prop_failure_rd_align_cons = failure_rd_align_post;
+
+		__COVER(prop_failure_rd_align_cons);
+		__ASSERT(prop_failure_rd_align_cons, "prop_failure_rd_align_cons");
+	}
+
+	bool prop_failure_rd_bound_ante = !failure_rd_align_pre
+		&& failure_rd_bound_pre;
+
+	__COVER(prop_failure_rd_bound_ante);
+	if (prop_failure_rd_bound_ante) {
+		bool prop_failure_rd_bound_cons = failure_rd_bound_post;
+
+		__COVER(prop_failure_rd_bound_cons);
+		__ASSERT(prop_failure_rd_bound_cons, "prop_failure_rd_bound_cons");
+	}
+
+	bool prop_failure_rd_state_ante = !failure_rd_align_pre
+		&& !failure_rd_bound_pre
+		&& failure_rd_state_pre;
+
+	__COVER(prop_failure_rd_state_ante);
+	if (prop_failure_rd_state_ante) {
+		bool prop_failure_rd_state_cons = failure_rd_state_post;
+
+		__COVER(prop_failure_rd_state_cons);
+		__ASSERT(prop_failure_rd_state_cons, "prop_failure_rd_state_cons");
+	}
+
+	bool prop_failure_realm_state_ante = !failure_rd_align_pre
+		&& !failure_rd_bound_pre
+		&& !failure_rd_state_pre
+		&& failure_realm_state_pre;
+
+	__COVER(prop_failure_realm_state_ante);
+	if (prop_failure_realm_state_ante) {
+		bool prop_failure_realm_state_cons = failure_realm_state_post;
+
+		__COVER(prop_failure_realm_state_cons);
+		__ASSERT(prop_failure_realm_state_cons, "prop_failure_realm_state_cons");
+	}
+
+	/*
+	 * Result assertion
+	 */
+
+	bool prop_result_ante = no_failures_pre;
+
+	__COVER(prop_result_ante);
+	if (prop_result_ante) {
+		bool prop_result_cons = result == RMI_SUCCESS;
+
+		__COVER(prop_result_cons);
+		__ASSERT(prop_result_cons, "prop_result_cons");
+	}
+
+	/*
+	 * Success condition assertions
+	 */
+
+	bool prop_success_realm_state_ante = no_failures_pre;
+
+	__COVER(prop_success_realm_state_ante);
+	if (prop_success_realm_state_ante) {
+		bool prop_success_realm_state_cons = success_realm_state_post
+		&& (result == RMI_SUCCESS);
+
+		__COVER(prop_success_realm_state_cons);
+		__ASSERT(prop_success_realm_state_cons, "prop_success_realm_state_cons");
+	}
+
+	/*
+	 * Assertion used to check consistency of the testbench
+	 */
+	__tb_expect_fail();
+
+	return no_failures_pre;
+}
diff --git a/tools/cbmc/testbenches/tb_rmi_realm_activate.h b/tools/cbmc/testbenches/tb_rmi_realm_activate.h
new file mode 100644
index 00000000..5a9076fb
--- /dev/null
+++ b/tools/cbmc/testbenches/tb_rmi_realm_activate.h
@@ -0,0 +1,28 @@
+/*
+ * SPDX-License-Identifier: BSD-3-Clause
+ * SPDX-FileCopyrightText: Copyright TF-RMM Contributors.
+ *
+ * This file was AUTOGENERATED from the RMM specification.
+ * RMM specification source version: 790fd539
+ */
+
+#ifndef __TB_RMI_REALM_ACTIVATE_H
+#define __TB_RMI_REALM_ACTIVATE_H
+
+#include "stdbool.h"
+#include "stdint.h"
+
+/*
+ * Testbench for RMI_REALM_ACTIVATE command. Check via CBMC with flag
+ * `--entry-point tb_rmi_realm_activate`.
+ *
+ * Arguments:
+ *     rd: PA of the RD.
+ *
+ * Returns:
+ *     bool: Output value.
+ */
+bool tb_rmi_realm_activate(
+	uint64_t rd);
+
+#endif /* __TB_RMI_REALM_ACTIVATE_H */
diff --git a/tools/cbmc/testbenches_results/BASELINE.analysis b/tools/cbmc/testbenches_results/BASELINE.analysis
index 5b0f5eaa..20c95f5e 100644
--- a/tools/cbmc/testbenches_results/BASELINE.analysis
+++ b/tools/cbmc/testbenches_results/BASELINE.analysis
@@ -1,11 +1,13 @@
 +--------------------------------------+--------------------------------------+
 |               FILENAME               |               ANALYSIS               |
 +--------------------------------------+--------------------------------------+
-|          tb_rmi_features.c           |    0 of 796 failed (1 iterations)    |
+|          tb_rmi_features.c           |    0 of 855 failed (1 iterations)    |
 +--------------------------------------+--------------------------------------+
-|      tb_rmi_granule_delegate.c       |    0 of 844 failed (1 iterations)    |
+|      tb_rmi_granule_delegate.c       |    0 of 903 failed (1 iterations)    |
 +--------------------------------------+--------------------------------------+
-|     tb_rmi_granule_undelegate.c      |    0 of 842 failed (1 iterations)    |
+|     tb_rmi_granule_undelegate.c      |    0 of 901 failed (1 iterations)    |
 +--------------------------------------+--------------------------------------+
-|           tb_rmi_version.c           |    0 of 794 failed (1 iterations)    |
+|       tb_rmi_realm_activate.c        |    11 of 966 failed (7 iterations)   |
++--------------------------------------+--------------------------------------+
+|           tb_rmi_version.c           |    0 of 853 failed (1 iterations)    |
 +--------------------------------------+--------------------------------------+
diff --git a/tools/cbmc/testbenches_results/BASELINE.assert b/tools/cbmc/testbenches_results/BASELINE.assert
index 969f22d0..c714696a 100644
--- a/tools/cbmc/testbenches_results/BASELINE.assert
+++ b/tools/cbmc/testbenches_results/BASELINE.assert
@@ -1,11 +1,13 @@
 +--------------------------------------+--------------------------------------+
 |               FILENAME               |                ASSERT                |
 +--------------------------------------+--------------------------------------+
-|          tb_rmi_features.c           |     0 of 35 failed (1 iterations)    |
+|          tb_rmi_features.c           |     0 of 68 failed (1 iterations)    |
 +--------------------------------------+--------------------------------------+
-|      tb_rmi_granule_delegate.c       |     0 of 42 failed (1 iterations)    |
+|      tb_rmi_granule_delegate.c       |     0 of 75 failed (1 iterations)    |
 +--------------------------------------+--------------------------------------+
-|     tb_rmi_granule_undelegate.c      |     0 of 42 failed (1 iterations)    |
+|     tb_rmi_granule_undelegate.c      |     0 of 75 failed (1 iterations)    |
 +--------------------------------------+--------------------------------------+
-|           tb_rmi_version.c           |     0 of 33 failed (1 iterations)    |
+|       tb_rmi_realm_activate.c        |     0 of 76 failed (1 iterations)    |
++--------------------------------------+--------------------------------------+
+|           tb_rmi_version.c           |     0 of 66 failed (1 iterations)    |
 +--------------------------------------+--------------------------------------+
diff --git a/tools/cbmc/testbenches_results/BASELINE.coverage b/tools/cbmc/testbenches_results/BASELINE.coverage
index e9e0baac..5d371ad7 100644
--- a/tools/cbmc/testbenches_results/BASELINE.coverage
+++ b/tools/cbmc/testbenches_results/BASELINE.coverage
@@ -7,5 +7,7 @@
 +--------------------------------------+--------------------------------------+
 |     tb_rmi_granule_undelegate.c      |       16 of 16 covered (100.0%)      |
 +--------------------------------------+--------------------------------------+
+|       tb_rmi_realm_activate.c        |       14 of 14 covered (100.0%)      |
++--------------------------------------+--------------------------------------+
 |           tb_rmi_version.c           |        2 of 2 covered (100.0%)       |
 +--------------------------------------+--------------------------------------+