diff --git a/libsel4/arch_include/arm/interfaces/sel4arch.xml b/libsel4/arch_include/arm/interfaces/sel4arch.xml
index a101b0611f0..911dc5cfa4b 100644
--- a/libsel4/arch_include/arm/interfaces/sel4arch.xml
+++ b/libsel4/arch_include/arm/interfaces/sel4arch.xml
@@ -26,6 +26,7 @@
                 <description>
                     VM Attributes for the mapping. <docref>Possible values for this type are given in <autoref label="ch:vspace"/>  .</docref>
                 </description>
+            </param>
             <error name="seL4_DeleteFirst">
                 <description>
                     A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
@@ -54,7 +55,6 @@
                     Or, <texttt text="_service"/> is already mapped in a VSpace.
                 </description>
             </error>
-            </param>
         </method>
         <method id="ARMPageTableUnmap" name="Unmap" manual_label="pagetable_unmap">
             <brief>
@@ -526,7 +526,7 @@
         <method id="ARMVCPUSetTCB" name="SetTCB" manual_name="Set TCB">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Bind a TCB to a virtual CPU
+                Bind a TCB to a virtual CPU.
             </brief>
              <description>
                  There is a 1:1 relationship between a virtual CPU and a TCB. If either (or both) of them is
@@ -549,10 +549,14 @@
         <method id="ARMVCPUInjectIRQ" name="InjectIRQ" manual_name="Inject IRQ">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Inject an IRQ to a virtual CPU
+                Inject an IRQ to a virtual CPU.
             </brief>
             <description>
-                TODO
+                Used to queue IRQs towards the VCPU.
+                Writes <texttt text="ICH_LRn_EL2"/> for GICv3 or <texttt text="LRn"/> for GICv2,
+                where <texttt text="n"/> is determined by <texttt text="index"/>.
+                The list register becomes available again when the guest acknowledges
+                the injected interrupt.
             </description>
             <param dir="in" name="virq" type="seL4_Uint16"
             description="Virtual IRQ ID"/>
@@ -561,10 +565,10 @@
             <param dir="in" name="group" type="seL4_Uint8"
             description="IRQ group"/>
             <param dir="in" name="index" type="seL4_Uint8"
-            description="IRQ index"/>
+            description="VGIC list register"/>
             <error name="seL4_DeleteFirst">
                 <description>
-                    The <texttt text="index"/> is in use.
+                    The <texttt text="index"/> is in use and not yet handled by the guest.
                 </description>
             </error>
             <error name="seL4_IllegalOperation">
@@ -586,12 +590,19 @@
         <method id="ARMVCPUReadReg" name="ReadRegs" manual_name="Read Registers">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Read a virtual CPU register
+                Read a virtual CPU register.
             </brief>
             <description>
-                TODO
+                Provides a way to read EL1 system registers, as well as <texttt text='VMPIDR_EL2'/>.
             </description>
-            <param dir="in" name="field" type="seL4_Word"
+            <return>
+                A <texttt text='seL4_ARM_VCPU_ReadRegs_t'/> struct that contains a
+                <texttt text='seL4_Word value'/>, which holds the value of the system register,
+                and <texttt text='int error'/>, which will be non-zero when an error occurred.
+                <docref>See <autoref label='sec:errors'/> for a description
+                of the message register and tag contents upon error.</docref>
+            </return>
+            <param dir="in" name="field" type="seL4_VCPUReg"
             description="Register to read from a VCPU"/>
             <param dir="out" name="value" type="seL4_Word"
             description="Returned value of the VCPU register"/>
@@ -614,12 +625,12 @@
         <method id="ARMVCPUWriteReg" name="WriteRegs" manual_name="Write Registers">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Write a virtual CPU register
+                Write a virtual CPU register.
             </brief>
             <description>
-                TODO
+                Provides a way to write EL1 system registers, as well as <texttt text='VMPIDR_EL2'/>.
             </description>
-            <param dir="in" name="field" type="seL4_Word"
+            <param dir="in" name="field" type="seL4_VCPUReg"
             description="Register ID to write to a VCPU"/>
             <param dir="in" name="value" type="seL4_Word"
             description="Value to be written to the VCPU register"/>
@@ -642,7 +653,7 @@
         <method id="ARMVCPUAckVPPI" name="AckVPPI" manual_name="Acknowledge Virtual PPI IRQ">
             <condition><config var="CONFIG_ARM_HYPERVISOR_SUPPORT"/></condition>
             <brief>
-                Acknowledge a PPI IRQ previously forwarded from a VPPIEvent fault
+                Acknowledge a PPI IRQ previously forwarded from a VPPIEvent fault.
             </brief>
             <description>
                 Acknowledge and unmask the PPI interrupt so that further interrupts can be forwarded
diff --git a/libsel4/tools/sel4_idl.xsd b/libsel4/tools/sel4_idl.xsd
index 187a324cbc0..2118fb238ab 100644
--- a/libsel4/tools/sel4_idl.xsd
+++ b/libsel4/tools/sel4_idl.xsd
@@ -128,7 +128,6 @@
     <xsd:complexType name="ParamType">
         <xsd:sequence>
             <xsd:element name="description" minOccurs="0" maxOccurs="1" type="DescriptionType"/>
-            <xsd:element name="error" minOccurs="0" maxOccurs="unbounded" type="ErrorType"/>
         </xsd:sequence>
         <xsd:attribute name="type" type="xsd:string" use="required"/>
         <xsd:attribute name="name" type="xsd:string" use="required"/>
diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py
index cbba6e4b43a..d692e85267b 100644
--- a/libsel4/tools/syscall_stub_gen.py
+++ b/libsel4/tools/syscall_stub_gen.py
@@ -280,6 +280,7 @@ def init_arch_types(wordsize, args):
             CapType("seL4_ARM_IOSpace", wordsize),
             CapType("seL4_ARM_IOPageTable", wordsize),
             StructType("seL4_UserContext", wordsize * 19, wordsize),
+            Type("seL4_VCPUReg", wordsize, wordsize),
         ] + arm_smmu,
 
         "aarch64": [
@@ -295,6 +296,7 @@ def init_arch_types(wordsize, args):
             CapType("seL4_ARM_SMC", wordsize),
             StructType("seL4_UserContext", wordsize * 36, wordsize),
             StructType("seL4_ARM_SMCContext", wordsize * 8, wordsize),
+            Type("seL4_VCPUReg", wordsize, wordsize),
         ] + arm_smmu,
 
         "arm_hyp": [
@@ -308,6 +310,7 @@ def init_arch_types(wordsize, args):
             CapType("seL4_ARM_IOSpace", wordsize),
             CapType("seL4_ARM_IOPageTable", wordsize),
             StructType("seL4_UserContext", wordsize * 19, wordsize),
+            Type("seL4_VCPUReg", wordsize, wordsize),
         ] + arm_smmu,
 
         "ia32": [
diff --git a/manual/manual.tex b/manual/manual.tex
index 2d106954cc7..28924c9f6bb 100644
--- a/manual/manual.tex
+++ b/manual/manual.tex
@@ -154,7 +154,7 @@
 Toby Murray.
 
 The authors and contributors can be contacted via the seL4 Developer Mailing
-List or the seL4 Discourse Forums. See \url{https://sel4.systems/contact.html}
+List or the seL4 Discourse Forums. See \url{https://sel4.systems/contact/}
 for details.
   \end{abstract}
   \thispagestyle{empty}
diff --git a/manual/parts/threads.tex b/manual/parts/threads.tex
index b493a00c33f..d6ffef4c48c 100644
--- a/manual/parts/threads.tex
+++ b/manual/parts/threads.tex
@@ -658,11 +658,28 @@ \section{Virtualisation}
 
 \subsection{Arm}
 
-When a \obj{TCB} has a bound \obj{VCPU} it is allowed to have the mode portion of the
-\texttt{cpsr} register set to values other than \texttt{user}. Specifically it may have any value other than
-\texttt{hypervisor}.
+When a \obj{TCB} has a bound \obj{VCPU} it will have access to (virtualised) system registers,
+cache and TLB maintenance instructions and be able to handle some exceptions itself.
+The virtual GIC will be enabled, allowing virtual interrupt delivery.
 
-TODO: this section needs more detail
+The vitualised system registers can be modified with \apifunc{seL4\_ARM\_VCPU\_WriteRegs}{arm_vcpu_write_registers}.
+By configuring the mode portion of the \texttt{SPSR\_EL1} or \texttt{cpsr} register,
+for ARMv8 and ARMv7 respectively, the thread can run in guest kernel mode.
+
+Interrupts are virtualised through the virtual GIC and need to be forwarded, which can be done
+with \apifunc{seL4\_ARM\_VCPU\_InjectIRQ}{arm_vcpu_inject_irq}, which provides a way to manage
+Virtual GIC List Registers, a queue of pending IRQs to be delivered to the guest. To help
+with managing the list, the Virtual GIC will send GIC maintenance interrupts as PPIs.
+
+Shared Peripheral Interrupts (SPIs) can be handled like any normal IRQs and forwarded as required.
+
+However, Virtual Private Peripheral Interrupts (PPI) are trapped and delivered as faults instead and
+need to be acknowledged with \apifunc{seL4\_ARM\_VCPU\_AckVPPI}{arm_vcpu_acknowledge_virtual_ppi_irq}.
+
+Stage 2 translation is enabled when the kernel supports virtualisation, but only for \obj{VCPUs}.
+Practically this means that there is an ASID limit of 256 for non-virtualised threads running in EL0.
+If more ASIDs are used, ASIDs will be dynamically re-used, with the associated cache flushing and
+slow downs.
 
 \subsection{x86}