diff --git a/doc/source/conf.py b/doc/source/conf.py
index 1f44ea46b..760b811cf 100644
--- a/doc/source/conf.py
+++ b/doc/source/conf.py
@@ -123,7 +123,6 @@
 try:
     import sphinx_rtd_theme
     html_theme = 'sphinx_rtd_theme'
-    html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]
     def setup(app):
 #        app.add_stylesheet('style.css')
         app.add_css_file('style.css')
diff --git a/doc/source/user_guide.rst b/doc/source/user_guide.rst
index 357973109..6451313ca 100644
--- a/doc/source/user_guide.rst
+++ b/doc/source/user_guide.rst
@@ -38,7 +38,7 @@ prevent annoying warnings:
 
    sudo apt-get install bison flex
 
-Files and directroy organisation
+Files and directory organization
 ********************************
 
 SO3 root directory (main subdirs)::
@@ -67,7 +67,7 @@ SO3 root directory (main subdirs)::
 Build of the environment
 ************************
 
-kernel toolchain
+Kernel toolchain
 ================
  
 We use the ``arm-none-eabi`` toolchain which has no dependencies on a libc.
@@ -78,22 +78,22 @@ The following package can be installed:
    
    apt install gcc-arm-none-eabi
 
-usr-space toolchain
-===================
+User space toolchain
+====================
 
-The usr-space uses MUSL as libc. The Musl toolchains can be generated with
+The user space uses MUSL as libc. The Musl toolchains can be generated with
 ``toolchains/build-toolchain.sh`` script.
 
 .. code-block:: bash
 
-   $ ./build-toolchain.sh
+   $ sudo ./build-toolchain.sh
 
 By default, it generates ``aarch64-linux-musl`` and ``arm-linux-musleabihf``
 folder in the ``toolchains`` directory
 
 .. note::
 
-   The output directory (by default ``toolchains`` floder) can be changed by setting
+   The output directory (by default ``toolchains`` folder) can be changed by setting
    the ``OUTPUT_PATH`` variable in the ``build-toolchain.sh`` script
 
 Quick setup & early test
@@ -309,4 +309,4 @@ The, starting the execution of the container:
 
 
 
- 
\ No newline at end of file
+ 
diff --git a/so3/arch/arm64/domain.c b/so3/arch/arm64/domain.c
index 6cd3cad13..1b6402f94 100644
--- a/so3/arch/arm64/domain.c
+++ b/so3/arch/arm64/domain.c
@@ -116,9 +116,9 @@ void __setup_dom_pgtable(struct domain *d, addr_t paddr_start, unsigned long map
 	__create_mapping(new_pt, memslot[slotID].ipa_addr, paddr_start, map_size, false, S2);
 
 	if (d->avz_shared->domID == DOMID_AGENCY)
-		do_ipamap(new_pt, linux_ipamap, ARRAY_SIZE(linux_ipamap));
+		do_ipamap(new_pt, agency_ipamap, ARRAY_SIZE(agency_ipamap));
 	else
-		do_ipamap(new_pt, guest_ipamap, ARRAY_SIZE(guest_ipamap));
+		do_ipamap(new_pt, capsule_ipamap, ARRAY_SIZE(capsule_ipamap));
 
 	/* Map the shared page in the IPA space; the shared page is located right after the domain area
 	 * in the IPA space, and if any, the RT shared page follows the shared page (in IPA space).
diff --git a/so3/arch/arm64/exception.S b/so3/arch/arm64/exception.S
index 114010d43..ddee4bf02 100644
--- a/so3/arch/arm64/exception.S
+++ b/so3/arch/arm64/exception.S
@@ -209,17 +209,17 @@ ENTRY(__vectors)
 
 #ifdef CONFIG_CPU_SPIN_TABLE
 
-ENTRY(pre_ret_to_el1_with_spin)
+ENTRY(pre_ret_to_el1_spin)
 
-	mov	x1, x0
+	mov		x1, x0
 	str 	xzr, [x1]
 1:
 	wfe
  	ldr 	x0, [x1]
 
-    	cbz 	x0, 1b
+    cbz 	x0, 1b
 
-    	// Branch to the given address
+    // Branch to the given address
 	msr	elr_el2, x0
 
 	// Set the CPU in EL1 mode to proceed with
@@ -239,7 +239,7 @@ ENTRY(pre_ret_to_el1_with_spin)
 	mov	x2, #0
 	mov	x3, #0
 
-	// Ready to jump into the Linux domain...
+	// Ready to jump into the Agency domain...
 
 	eret
 
@@ -264,7 +264,7 @@ ENTRY(pre_ret_to_el1)
 
 	wfi
 
-	ldr 	x0, cpu_entrypoint
+	ldr x0, cpu_entrypoint
 	msr	elr_el2, x0
 
 	// Set the CPU in EL1 mode to proceed with
diff --git a/so3/arch/arm64/include/asm/processor.h b/so3/arch/arm64/include/asm/processor.h
index b04e79589..1b8ca3d1a 100644
--- a/so3/arch/arm64/include/asm/processor.h
+++ b/so3/arch/arm64/include/asm/processor.h
@@ -1263,7 +1263,7 @@ void __switch_domain_to(struct domain *prev, struct domain *next);
 void ret_to_user(void);
 void pre_ret_to_user(void);
 void pre_ret_to_el1(void);
-void pre_ret_to_el1_with_spin(addr_t release_addr);
+void pre_ret_to_el1_spin(addr_t release_addr);
 
 #endif /* CONFIG_AVZ */
 
diff --git a/so3/arch/arm64/rpi4_64/include/mach/ipamap.h b/so3/arch/arm64/rpi4_64/include/mach/ipamap.h
index e9293975b..d7d67ca3e 100644
--- a/so3/arch/arm64/rpi4_64/include/mach/ipamap.h
+++ b/so3/arch/arm64/rpi4_64/include/mach/ipamap.h
@@ -21,51 +21,37 @@
 
 #include <asm/mmu.h>
 
-ipamap_t ipamap[] = {
+ipamap_t agency_ipamap[] = {
+
+	/* I/O Memory space*/
 	{
 		.ipa_addr = 0xf0000000,
 		.phys_addr = 0xf0000000,
 		.size = 0x10000000,
 	},
-	{
-		.ipa_addr = 0x1faf0000,
-		.phys_addr = 0x1faf0000,
-		.size = 0x1000,
-	},
-	{
-		.ipa_addr = 0x1faf1000,
-		.phys_addr = 0x1faf1000,
-		.size = 0x9000,
-	},
-	{
-		.ipa_addr = 0x1fafa000,
-		.phys_addr = 0x1fafa000,
-		.size = 0x2000,
-	},
-	{
-		.ipa_addr = 0x1fafc000,
-		.phys_addr = 0x1fafc000,
-		.size = 0x2000,
-	},
-	{
-		.ipa_addr = 0x1fafe000,
-		.phys_addr = 0x1fafe000,
-		.size = 0x2000,
-	},
+
+	/* Null pointer exception */
 	{
 		.ipa_addr = 0x0,
 		.phys_addr = 0x0,
 		.size = 0x1000,
 	},
+};
+
+/**
+ * In the guest environment, the access to the GIC distributor must lead to a data abort
+ * which will be trapped and handled by the hypervisor.
+ */
+
+ipamap_t capsule_ipamap[] = {
+
 	{
-		.ipa_addr = 0x50000000,
-		.phys_addr = 0x50000000,
-		.size = 0x10000000,
-	},
-	{
-		.ipa_addr = 0x600000000,
-		.phys_addr = 0x600000000,
-		.size = 0x1000,
+		/* Only mapping the CPU interface to the vGIC CPU interface.
+	 * Access to the distributor must lead to a trap and be handled by the hypervisor.
+	 */
+		.ipa_addr = 0x08010000,
+		.phys_addr = 0x08040000,
+		.size = 0x10000,
 	},
 };
 
diff --git a/so3/arch/arm64/virt64/include/mach/ipamap.h b/so3/arch/arm64/virt64/include/mach/ipamap.h
index 985ba5f95..b4b0a85a2 100644
--- a/so3/arch/arm64/virt64/include/mach/ipamap.h
+++ b/so3/arch/arm64/virt64/include/mach/ipamap.h
@@ -21,7 +21,7 @@
 
 #include <asm/mmu.h>
 
-ipamap_t linux_ipamap[] = {
+ipamap_t agency_ipamap[] = {
 	{
 		.ipa_addr = 0x08000000,
 		.phys_addr = 0x08000000,
@@ -34,7 +34,7 @@ ipamap_t linux_ipamap[] = {
  * which will be trapped and handled by the hypervisor.
  */
 
-ipamap_t guest_ipamap[] = {
+ipamap_t capsule_ipamap[] = {
 
 	{
 		/* Only mapping the CPU interface to the vGIC CPU interface.
diff --git a/so3/avz/kernel/smp.c b/so3/avz/kernel/smp.c
index bdbeebbfe..283b4e96d 100644
--- a/so3/avz/kernel/smp.c
+++ b/so3/avz/kernel/smp.c
@@ -114,23 +114,25 @@ void secondary_start_kernel(void)
 #ifdef CONFIG_CPU_SPIN_TABLE
 	switch (cpu) {
 	case 1:
-		pre_ret_to_el1_with_spin(CPU1_RELEASE_ADDR);
+		pre_ret_to_el1_spin(CPU1_RELEASE_ADDR);
 		break;
 	case 2:
-		pre_ret_to_el1_with_spin(CPU2_RELEASE_ADDR);
+		pre_ret_to_el1_spin(CPU2_RELEASE_ADDR);
 		break;
 	case 3:
-		pre_ret_to_el1_with_spin(CPU3_RELEASE_ADDR);
+		pre_ret_to_el1_spin(CPU3_RELEASE_ADDR);
 		break;
 	default:
 		printk("%s: trying to start CPU %d that is not supported.\n", __func__, cpu);
 	}
 #endif
 
+#ifdef CONFIG_CPU_PSCI
 #ifdef CONFIG_SOO
 	if (cpu != ME_CPU)
-#endif
+#endif /* CONFIG_SOO */
 		pre_ret_to_el1();
+#endif /* CONFIG_CPU_PCSI */
 
 	secondary_timer_init();
 
diff --git a/so3/devices/fdt.c b/so3/devices/fdt.c
index 0ebdfd3a8..4b23137e4 100644
--- a/so3/devices/fdt.c
+++ b/so3/devices/fdt.c
@@ -1,5 +1,5 @@
 /*
- * Copyright (C) 2014-2019 Daniel Rossier <daniel.rossier@heig-vd.ch>
+ * Copyright (C) 2014-2026 Daniel Rossier <daniel.rossier@heig-vd.ch>
  *
  *
  * This program is free software; you can redistribute it and/or modify
@@ -55,7 +55,13 @@ static void init_dev_info(dev_t *dev)
 	dev->fdt = 0;
 }
 
-/* Get memory informations from a device tree */
+/**
+ * @brief Get memory informations from a device tree 
+ * 
+ * @param fdt Virtual address of the device tree
+ * @param info Memory info structure which will be filled up by this function
+ * @return int Offset of the memory node in the device tree
+ */
 int get_mem_info(const void *fdt, mem_info_t *info)
 {
 	int offset;
@@ -81,6 +87,9 @@ int get_mem_info(const void *fdt, mem_info_t *info)
 
 	/* For some platform, address-cells and size-cells are set to 2 (64-bit)
 	 * even for a 32-bit platform, probably to support LPAE.
+	 * Additionally, on Raspberry Pi 4, the device tree has its memory node 
+	 * with a 64-bit address cell and a 32-bit size cell. That's why we need
+	 * to consider a 12 bytes <reg> property.
 	 */
 
 	if (prop) {
@@ -88,7 +97,7 @@ int get_mem_info(const void *fdt, mem_info_t *info)
 			info->phys_base = fdt32_to_cpu(((const fdt32_t *) prop->data)[0]);
 			info->size = fdt32_to_cpu(((const fdt32_t *) prop->data)[1]);
 		} else {
-			BUG_ON(prop_len != 16);
+			BUG_ON((prop_len != 16) && (prop_len != 12));
 
 			/* Keep a possible conversion from 64-bit to 32-bit if the address & size are
 			 * on 64-bit for aarch32 platforms.
@@ -110,10 +119,15 @@ int get_mem_info(const void *fdt, mem_info_t *info)
 
 			info->phys_base = fdt64_to_cpu(val);
 
-			for (i = 0; i < 8; i++)
-				*(((char *) &val) + i) = *ptr++;
-
-			info->size = fdt64_to_cpu(val);
+			if (prop_len == 16) {
+				for (i = 0; i < 8; i++)
+					*(((char *) &val) + i) = *ptr++;
+				info->size = fdt64_to_cpu(val);
+			} else {
+				for (i = 0; i < 4; i++)
+					*(((char *) &val) + i) = *ptr++;
+				info->size = fdt32_to_cpu(val);
+			}
 
 #endif /* !CONFIG_ARCH_ARM32 */
 		}
diff --git a/so3/devices/irq/gic.c b/so3/devices/irq/gic.c
index 9c70f7c9c..04dacd444 100644
--- a/so3/devices/irq/gic.c
+++ b/so3/devices/irq/gic.c
@@ -431,12 +431,9 @@ void gich_init(void)
 
 void gicc_init(void)
 {
-	unsigned int cpu = smp_processor_id();
 	u32 bypass = 0;
 	int i;
 
-	spin_lock_init(&per_cpu(intc_lock, cpu));
-
 	/*
          * Deal with the banked PPI and SGI interrupts - disable all
          * PPI interrupts, ensure all SGI interrupts are enabled.
@@ -659,6 +656,11 @@ static int gic_init(dev_t *dev, int fdt_offset)
 {
 	const struct fdt_property *prop;
 	int prop_len;
+	int cpu;
+
+	for (cpu = 0; cpu < CONFIG_NR_CPUS; cpu++) {
+		spin_lock_init(&per_cpu(intc_lock, cpu));
+	}
 
 	gic = (gic_t *) malloc(sizeof(gic_t));
 	BUG_ON(!gic);
diff --git a/so3/dts/Makefile b/so3/dts/Makefile
index 2ba411c3a..e0acd87d9 100644
--- a/so3/dts/Makefile
+++ b/so3/dts/Makefile
@@ -1,6 +1,6 @@
 
 dtb-$(CONFIG_RPI4) += rpi4.dtb
-dtb-$(CONFIG_RPI4_64) += rpi4_64.dtb rpi4_64_avz_vt.dtb
+dtb-$(CONFIG_RPI4_64) += rpi4_64.dtb rpi4_64_avz.dtb
 dtb-$(CONFIG_VIRT64) += virt64.dtb virt64_avz.dtb virt64_capsule.dtb virt64_lvperf.dtb
 dtb-$(CONFIG_VIRT32) += virt32.dtb virt32_lvperf.dtb
 
diff --git a/so3/dts/rpi4_64.dts b/so3/dts/rpi4_64.dts
index 0e8b46ef1..1f3cbd30f 100644
--- a/so3/dts/rpi4_64.dts
+++ b/so3/dts/rpi4_64.dts
@@ -32,11 +32,7 @@
 	
 	memory@0 {
 		device_type = "memory";
-		reg = <0x0 0x01000000 0x0 0x20000000>; /* 512 MB */
-	};
-
-	agency {
-		domain-size = <0x10000000>;
+		reg = <0x0 0x10000000 0x0 0x20000000>; /* 512 MB */
 	};
 
 	mem {
diff --git a/so3/dts/rpi4_64_avz_vt.dts b/so3/dts/rpi4_64_avz.dts
similarity index 100%
rename from so3/dts/rpi4_64_avz_vt.dts
rename to so3/dts/rpi4_64_avz.dts
diff --git a/so3/fs/elf.c b/so3/fs/elf.c
index 5baa087a1..b37272bda 100644
--- a/so3/fs/elf.c
+++ b/so3/fs/elf.c
@@ -219,8 +219,9 @@ void elf_load_segments(elf_img_info_t *elf_img_info)
 		elf_img_info->segment_end_vaddr = 0;
 	}
 
+#ifndef CONFIG_AVZ
 	LOG_DEBUG("segments use %d virtual pages\n", elf_img_info->segment_page_count);
-
+#endif
 	for (i = 0; i < elf_img_info->header->e_phnum; i++) {
 		LOG_DEBUG("[0x%08x] vaddr: 0x%08x; paddr: 0x%08x; filesize: 0x%08x; memsize: 0x%08x flags: 0x%08x\n",
 			  elf_img_info->segments[i].p_offset, elf_img_info->segments[i].p_vaddr,
diff --git a/so3/kernel/process.c b/so3/kernel/process.c
index 2646e5113..a6973aa56 100644
--- a/so3/kernel/process.c
+++ b/so3/kernel/process.c
@@ -329,8 +329,9 @@ void create_root_process(void)
 
 	allocate_page(pcb, pcb->stack_top - (pcb->page_count * PAGE_SIZE), pcb->page_count, true);
 
+#ifndef CONFIG_AVZ
 	LOG_DEBUG("Stack mapped at 0x%08x (size: %d bytes)\n", pcb->stack_top - (pcb->page_count * PAGE_SIZE), PROC_STACK_SIZE);
-
+#endif
 	/* First map the code in the user space so that
          * the initial code can run normally in user mode.
          */
@@ -589,8 +590,9 @@ int setup_proc_image_replace(elf_img_info_t *elf_img_info, pcb_t *pcb, int argc,
 
 	allocate_page(pcb, pcb->stack_top - (pcb->page_count * PAGE_SIZE), pcb->page_count, true);
 
+#ifndef CONFIG_AVZ
 	LOG_DEBUG("stack mapped at 0x%08x (size: %d bytes)\n", pcb->stack_top - (pcb->page_count * PAGE_SIZE), PROC_STACK_SIZE);
-
+#endif
 	/* Initialize the pc register */
 	pcb->bin_image_entry = (uint32_t) elf_img_info->header->e_entry;
 
diff --git a/so3/soo/include/soo/uapi/soo.h b/so3/soo/include/soo/uapi/soo.h
index 8564ead45..e5f56463e 100644
--- a/so3/soo/include/soo/uapi/soo.h
+++ b/so3/soo/include/soo/uapi/soo.h
@@ -175,7 +175,7 @@ extern atomic_t dc_incoming_domID[DC_EVENT_MAX];
  */
 typedef struct {
 	unsigned int slotID;
-	unsigned int capsuleID;
+	unsigned int capsuleID; /* ID handled by emiso engine */
 	uint64_t spid;
 
 	ME_state_t state;
diff --git a/target/rpi4_64_avz_so3.its b/target/rpi4_64_avz_so3.its
new file mode 100644
index 000000000..002d0872e
--- /dev/null
+++ b/target/rpi4_64_avz_so3.its
@@ -0,0 +1,91 @@
+/*
+ * Copyright (C) 2020-2026 Daniel Rossier <daniel.rossier@heig-vd.ch>
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License version 2 as
+ * published by the Free Software Foundation.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
+ *
+ */
+
+/dts-v1/;
+
+/ {
+	description = "Kernel and rootfs components for virt64 (armv8) environment";
+
+	images {
+
+		avz {
+			description = "AVZ Hypervisor (64-bit) Polymorphic SO3";
+			data = /incbin/("../avz/so3.bin");
+			type = "kernel";
+			os = "linux";
+			arch = "arm64";
+			compression = "none";
+			load = <0x00080000>;
+			entry = <0x00080000>;
+		};
+
+		avz_dt {
+			description = "Flattened Device Tree blob";
+			data = /incbin/("../avz/dts/rpi4_64_avz.dtb");
+			type = "avz_dt";
+			arch = "arm64";
+			compression = "none";
+			load = <0x03000000>;
+		};
+
+		so3 {
+			description = "SO3 OS kernel";
+			data = /incbin/("../so3/so3.bin");
+			type = "guest";
+			arch = "arm64";
+			os = "linux";
+			compression = "none";
+			load = <0x10080000>;
+			entry = <0x10080000>;
+		};
+
+		fdt {
+			description = "Flattened Device Tree blob";
+			data = /incbin/("../so3/dts/rpi4_64.dtb");
+			type = "flat_dt";
+			arch = "arm64";
+			compression = "none";
+			load = <0x15000000>;
+		};
+
+		ramfs {
+				description = "SO3 environment minimal rootfs";
+				data = /incbin/("../rootfs/rootfs.fat");
+				type = "ramdisk";
+				arch = "arm64";
+				os = "linux";
+				compression = "none";
+				load = <0x15c00000>;
+		};
+
+	};
+
+	configurations {
+		default = "so3_guest";
+
+		so3_guest {
+			description = "SO3/AVZ on RPi4 64-bit";
+			kernel = "avz";
+			loadables = "avz_dt", "so3";
+			fdt = "fdt";
+			ramdisk = "ramfs";
+		};
+
+	};
+
+};