diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 9c5c7b9a..36ad8bc0 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -9,10 +9,10 @@ on:
 
 jobs:
   build_manual:
-    name: Build VMM manual
+    name: Build manual
     runs-on: ubuntu-20.04
     steps:
-      - name: Checkout seL4CP VMM repository
+      - name: Checkout VMM repository
         uses: actions/checkout@v3
       - name: Install pandoc/latex via apt
         run: sudo apt update && sudo apt install -y pandoc texlive-latex-base texlive-fonts-recommended texlive-formats-extra
@@ -27,13 +27,13 @@ jobs:
     name: Build and run VMM examples (Linux x86-64)
     runs-on: ubuntu-20.04
     steps:
-      - name: Checkout seL4CP VMM repository
+      - name: Checkout VMM repository
         uses: actions/checkout@v3
-      - name: Download seL4CP SDK
-        run: ./ci/acquire_sdk.sh sel4cp-sdk.zip ${{ secrets.GITHUB_TOKEN }} linux-x86-64
+      - name: Download Microkit SDK
+        run: ./ci/acquire_sdk.sh microkit-sdk.zip ${{ secrets.GITHUB_TOKEN }} linux-x86-64
         shell: bash
-      - name: Extract seL4CP SDK
-        run: unzip sel4cp-sdk.zip && tar -xf sel4cp-sdk-1.2.6.tar.gz
+      - name: Extract Microkit SDK
+        run: unzip microkit-sdk.zip && tar -xf microkit-sdk-1.2.6.tar.gz
       - name: Install VMM dependencies (via apt)
         # 'expect' is only a dependency for CI testing
         run: sudo apt update && sudo apt install -y make clang lld llvm qemu-system-arm device-tree-compiler expect
@@ -45,7 +45,7 @@ jobs:
       - name: Install Rust
         run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
       - name: Build and run VMM examples
-        run: ./ci/examples.sh ${PWD}/sel4cp-sdk-1.2.6
+        run: ./ci/examples.sh ${PWD}/microkit-sdk-1.2.6
         shell: bash
       - name: Upload built system images
         uses: actions/upload-artifact@v3
@@ -56,13 +56,13 @@ jobs:
     name: Build and run VMM examples (macOS x86-64)
     runs-on: macos-12
     steps:
-      - name: Checkout seL4CP VMM repository
+      - name: Checkout VMM repository
         uses: actions/checkout@v3
-      - name: Download seL4CP SDK
-        run: ./ci/acquire_sdk.sh sel4cp-sdk.zip ${{ secrets.GITHUB_TOKEN }} macos-x86-64
+      - name: Download Microkit SDK
+        run: ./ci/acquire_sdk.sh microkit-sdk.zip ${{ secrets.GITHUB_TOKEN }} macos-x86-64
         shell: bash
-      - name: Extract seL4CP SDK
-        run: unzip sel4cp-sdk.zip && tar -xf sel4cp-sdk-1.2.6.tar.gz
+      - name: Extract Microkit SDK
+        run: unzip microkit-sdk.zip && tar -xf microkit-sdk-1.2.6.tar.gz
       - name: Install VMM dependencies (via Homebrew)
         # 'expect' is only a dependency for CI testing
         run: |
@@ -76,7 +76,7 @@ jobs:
       - name: Install Rust
         run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
       - name: Build and run VMM examples
-        run: ./ci/examples.sh ${PWD}/sel4cp-sdk-1.2.6
+        run: ./ci/examples.sh ${PWD}/microkit-sdk-1.2.6
         shell: bash
       - name: Upload built system images
         uses: actions/upload-artifact@v3
@@ -86,19 +86,19 @@ jobs:
     name: Build and run VMM examples (Linux x86-64 via Nix)
     runs-on: ubuntu-20.04
     steps:
-      - name: Checkout seL4CP VMM repository
+      - name: Checkout VMM repository
         uses: actions/checkout@v3
-      - name: Download seL4CP SDK
-        run: ./ci/acquire_sdk.sh sel4cp-sdk.zip ${{ secrets.GITHUB_TOKEN }} linux-x86-64
+      - name: Download Microkit SDK
+        run: ./ci/acquire_sdk.sh microkit-sdk.zip ${{ secrets.GITHUB_TOKEN }} linux-x86-64
         shell: bash
-      - name: Extract seL4CP SDK
-        run: unzip sel4cp-sdk.zip && tar -xf sel4cp-sdk-1.2.6.tar.gz
+      - name: Extract Microkit SDK
+        run: unzip microkit-sdk.zip && tar -xf microkit-sdk-1.2.6.tar.gz
       - name: Install Nix
         uses: cachix/install-nix-action@v22
         with:
           nix_path: nixpkgs=channel:nixos-unstable
       - name: Build and run VMM examples
-        run: nix-shell --pure --run "./ci/examples.sh ${PWD}/sel4cp-sdk-1.2.6"
+        run: nix-shell --pure --run "./ci/examples.sh ${PWD}/microkit-sdk-1.2.6"
       - name: Upload built system images
         uses: actions/upload-artifact@v3
         with:
@@ -107,13 +107,13 @@ jobs:
     name: Build and run VMM examples (macOS x86-64 via Nix)
     runs-on: macos-12
     steps:
-      - name: Checkout seL4CP VMM repository
+      - name: Checkout VMM repository
         uses: actions/checkout@v3
-      - name: Download seL4CP SDK
-        run: ./ci/acquire_sdk.sh sel4cp-sdk.zip ${{ secrets.GITHUB_TOKEN }} macos-x86-64
+      - name: Download Microkit SDK
+        run: ./ci/acquire_sdk.sh microkit-sdk.zip ${{ secrets.GITHUB_TOKEN }} macos-x86-64
         shell: bash
-      - name: Extract seL4CP SDK
-        run: unzip sel4cp-sdk.zip && tar -xf sel4cp-sdk-1.2.6.tar.gz
+      - name: Extract Microkit SDK
+        run: unzip microkit-sdk.zip && tar -xf microkit-sdk-1.2.6.tar.gz
       - name: Install Nix
         uses: cachix/install-nix-action@v22
         with:
@@ -121,7 +121,7 @@ jobs:
       - name: Update Nix channel
         run: nix-channel --update
       - name: Build and run VMM examples
-        run: nix-shell --pure --run "./ci/examples.sh ${PWD}/sel4cp-sdk-1.2.6"
+        run: nix-shell --pure --run "./ci/examples.sh ${PWD}/microkit-sdk-1.2.6"
       - name: Upload built system images
         uses: actions/upload-artifact@v3
         with:
diff --git a/README.md b/README.md
index e5861d75..be11c084 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
-# VMM on the seL4 Core Platform
+# libvmm
 
-This is a Virtual Machine Monitor (VMM) built on the seL4 Core Platform (seL4CP).
+This is a Virtual Machine Monitor (VMM) built on the [seL4 Microkit](https://github.com/seL4/microkit).
 The purpose of the VMM is to make it easy to run virtual machines on top of the seL4 microkernel.
 
 It is (at least initially) a port of the already existing
@@ -51,10 +51,10 @@ Using [Nix](https://nixos.org/):
 nix-shell --pure
 ```
 
-Finally, you will need an experimental seL4 Core Platform SDK.
+Finally, you will need an experimental Microkit SDK.
 
 * Currently virtualisation support and other patches that the VMM requires are
-  not part of mainline seL4 Core Platform. See below for instructions on
+  not part of mainline Microkit. See below for instructions on
   acquiring the SDK.
 * Upstreaming the required changes is in-progress.
 
@@ -96,16 +96,16 @@ tar xf sel4cp-sdk-dev-bf06734-macos-aarch64.tar.gz
 
 ##### Option 2 - Building the SDK
 
-You will need a development version of the seL4CP SDK source code. You can acquire it with the following command:
+You will need a development version of the Microkit SDK source code. You can acquire it with the following command:
 ```sh
-git clone https://github.com/Ivan-Velickovic/sel4cp.git --branch dev
+git clone https://github.com/Ivan-Velickovic/microkit.git --branch dev
 ```
 
 From here, you can follow the instructions
-[here](https://github.com/Ivan-Velickovic/sel4cp/tree/dev) to build the SDK.
+[here](https://github.com/Ivan-Velickovic/microkit/tree/dev) to build the SDK.
 
 If you have built the SDK then the path to the SDK should look something like
-this: `sel4cp/release/sel4cp-sdk-1.2.6`.
+this: `microkit/release/microkit-sdk-1.2.6`.
 
 ## Building the example system
 
@@ -113,7 +113,7 @@ Finally, we can simulate a basic system with a single Linux guest with the
 following command. We want to run the `simple` example system in a `debug`
 configuration for the QEMU ARM virt system.
 ```sh
-make BOARD=qemu_arm_virt SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6 qemu
+make BOARD=qemu_arm_virt MICROKIT_SDK=/path/to/sdk qemu
 ```
 
 You should see Linux booting and be greeted with the buildroot prompt:
diff --git a/ci/acquire_sdk.sh b/ci/acquire_sdk.sh
index edced959..5d65e1c6 100755
--- a/ci/acquire_sdk.sh
+++ b/ci/acquire_sdk.sh
@@ -17,7 +17,7 @@ fi
 SDK_PATH=$1
 GITHUB_TOKEN=$2
 SDK_TARGET=$3
-SEL4CP_REPO="Ivan-Velickovic/sel4cp"
+MICROKIT_REPO="Ivan-Velickovic/microkit"
 # zip is the only available option
 ARCHIVE_FORMAT="zip"
 
@@ -40,7 +40,7 @@ ARTIFACT_ID=`curl \
   -H "Accept: application/vnd.github+json" \
   -H "Authorization: Bearer ${GITHUB_TOKEN}"\
   -H "X-GitHub-Api-Version: 2022-11-28" \
-  https://api.github.com/repos/$SEL4CP_REPO/actions/artifacts | jq ".artifacts[$ARTIFACT_INDEX].id"`
+  https://api.github.com/repos/$MICROKIT_REPO/actions/artifacts | jq ".artifacts[$ARTIFACT_INDEX].id"`
 
 echo "Downloading SDK with artifact ID: ${ARTIFACT_ID}"
 curl \
@@ -49,4 +49,4 @@ curl \
   -o $SDK_PATH \
   -H "Accept: application/vnd.github+json" \
   -H "X-GitHub-Api-Version: 2022-11-28" \
-  https://api.github.com/repos/$SEL4CP_REPO/actions/artifacts/$ARTIFACT_ID/$ARCHIVE_FORMAT
+  https://api.github.com/repos/$MICROKIT_REPO/actions/artifacts/$ARTIFACT_ID/$ARCHIVE_FORMAT
diff --git a/ci/examples.sh b/ci/examples.sh
index 194428d9..c4561948 100755
--- a/ci/examples.sh
+++ b/ci/examples.sh
@@ -17,7 +17,7 @@ build_simple_make() {
         BUILD_DIR=${BUILD_DIR} \
         CONFIG=${CONFIG} \
         BOARD=${BOARD} \
-        SEL4CP_SDK=${SDK_PATH}
+        MICROKIT_SDK=${SDK_PATH}
 }
 
 build_simple_zig() {
@@ -43,7 +43,7 @@ build_rust() {
     make -C examples/rust -B \
         BUILD_DIR=${BUILD_DIR} \
         CONFIG=${CONFIG} \
-        SEL4CP_SDK=${SDK_PATH}
+        MICROKIT_SDK=${SDK_PATH}
 }
 
 simulate_rust() {
@@ -88,7 +88,7 @@ build_simple_make "odroidc4" "release"
 
 build_rust "debug"
 simulate_rust "debug"
-# @ivanv: TODO get Rust in with release version of seL4CP working
+# @ivanv: TODO get Rust in with release version of Microkit working
 # build_rust "release"
 # simulate_rust "release"
 
diff --git a/docs/MANUAL.md b/docs/MANUAL.md
index 3d0d2af3..541c1d12 100644
--- a/docs/MANUAL.md
+++ b/docs/MANUAL.md
@@ -1,8 +1,8 @@
-# seL4CP VMM manual
+# libvmm manual
 
 This document aims to describe the VMM and how to use it. If you feel there is
 something missing from this document or the VMM itself, feel free to let us
-know by [opening an issue on the GitHub repository](https://github.com/au-ts/sel4cp_vmm).
+know by [opening an issue on the GitHub repository](https://github.com/au-ts/libvmm).
 
 ## Supported platforms
 
@@ -109,7 +109,7 @@ driver in the VMM. Like the UART, the address of the GIC is platform specific.
 An example Make command looks something like this:
 ```sh
 make BUILD_DIR=build \
-     SEL4CP_SDK=/path/to/sdk \
+     MICROKIT_SDK=/path/to/sdk \
      CONFIG=debug \
      BOARD=qemu_arm_virt \
      SYSTEM=simple.system \
@@ -121,7 +121,7 @@ make BUILD_DIR=build \
 Before you can port the VMM to your desired platform you must have the following:
 
 * A working platform port of the seL4 kernel in hypervisor mode.
-* A working platform port of the seL4 Core Platform where the kernel is built as a
+* A working platform port of the seL4 Microkit where the kernel is built as a
   hypervisor.
 
 ### Guest setup
diff --git a/examples/ethernet/Makefile b/examples/ethernet/Makefile
index 23f74239..c170d667 100644
--- a/examples/ethernet/Makefile
+++ b/examples/ethernet/Makefile
@@ -5,8 +5,8 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
-ifeq ($(strip $(SEL4CP_SDK)),)
-$(error SEL4CP_SDK must be specified)
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
 endif
 
 ifeq ($(strip $(BOARD)),)
@@ -43,7 +43,7 @@ endif
 
 CC := $(TOOLCHAIN)-gcc
 LD := $(TOOLCHAIN)-ld
-SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
 
 # @ivanv: need to have a step for putting in the initrd node into the DTB,
 # 		  right now it is unfortunately hard-coded.
@@ -54,7 +54,7 @@ SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
 
 # @ivanv: incremental builds don't work with IMAGE_DIR changing
 
-BOARD_DIR := $(SEL4CP_SDK)/board/$(BOARD)/$(CONFIG)
+BOARD_DIR := $(MICROKIT_SDK)/board/$(BOARD)/$(CONFIG)
 VMM := ../../
 VMM_TOOLS := $(VMM)/tools
 VMM_SRC_DIR := $(VMM)/src
@@ -93,7 +93,7 @@ CFLAGS := -mstrict-align \
 		  -DCONFIG_$(CONFIG) \
 
 LDFLAGS := -L$(BOARD_DIR)/lib
-LIBS := -lsel4cp -Tsel4cp.ld
+LIBS := -lmicrokit -Tmicrokit.ld
 
 all: directories $(IMAGE_FILE)
 
@@ -143,4 +143,4 @@ $(BUILD_DIR)/vmm.elf: $(addprefix $(BUILD_DIR)/, $(VMM_OBJS))
 	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
 
 $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(ELFS)) $(SYSTEM_DESCRIPTION) $(IMAGE_DIR)
-	$(SEL4CP_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+	$(MICROKIT_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
diff --git a/examples/ethernet/README.md b/examples/ethernet/README.md
index 385da719..58198385 100644
--- a/examples/ethernet/README.md
+++ b/examples/ethernet/README.md
@@ -9,7 +9,7 @@ The example currently works on the following platforms:
 ## Building with Make
 
 ```sh
-make BOARD=<BOARD> SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6
+make BOARD=<BOARD> MICROKIT_SDK=/path/to/sdk
 ```
 
 Where `<BOARD>` is one of:
@@ -20,7 +20,7 @@ and `BUILD_DIR`, see the Makefile for details.
 
 If you would like to simulate the QEMU board you can run the following command:
 ```sh
-make BOARD=qemu_arm_virt SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6 qemu
+make BOARD=qemu_arm_virt MICROKIT_SDK=/path/to/sdk qemu
 ```
 
 This will build the example code as well as run the QEMU command to simulate a
diff --git a/examples/ethernet/vmm.c b/examples/ethernet/vmm.c
index 691e432a..ad5ff865 100644
--- a/examples/ethernet/vmm.c
+++ b/examples/ethernet/vmm.c
@@ -5,7 +5,7 @@
  */
 #include <stddef.h>
 #include <stdint.h>
-#include <sel4cp.h>
+#include <microkit.h>
 #include "util/util.h"
 #include "arch/aarch64/vgic/vgic.h"
 #include "arch/aarch64/linux.h"
@@ -58,7 +58,7 @@ extern char _guest_dtb_image_end[];
 /* Data for the initial RAM disk to be passed to the kernel. */
 extern char _guest_initrd_image[];
 extern char _guest_initrd_image_end[];
-/* seL4CP will set this variable to the start of the guest RAM memory region. */
+/* Microkit will set this variable to the start of the guest RAM memory region. */
 uintptr_t guest_ram_vaddr;
 
 static void serial_ack(size_t vcpu_id, int irq, void *cookie) {
@@ -66,20 +66,20 @@ static void serial_ack(size_t vcpu_id, int irq, void *cookie) {
      * For now we by default simply ack the serial IRQ, we have not
      * come across a case yet where more than this needs to be done.
      */
-    sel4cp_irq_ack(SERIAL_IRQ_CH);
+    microkit_irq_ack(SERIAL_IRQ_CH);
 }
 
 static void ethernet_ack(size_t vcpu_id, int irq, void *cookie) {
-    sel4cp_irq_ack(ETHERNET_IRQ_CH);
+    microkit_irq_ack(ETHERNET_IRQ_CH);
 }
 
 static void ethernet_phy_ack(size_t vcpu_id, int irq, void *cookie) {
-    sel4cp_irq_ack(ETHERNET_PHY_IRQ_CH);
+    microkit_irq_ack(ETHERNET_PHY_IRQ_CH);
 }
 
 void init(void) {
     /* Initialise the VMM, the VCPU(s), and start the guest */
-    LOG_VMM("starting \"%s\"\n", sel4cp_name);
+    LOG_VMM("starting \"%s\"\n", microkit_name);
     /* Place all the binaries in the right locations before starting the guest */
     size_t kernel_size = _guest_kernel_image_end - _guest_kernel_image;
     size_t dtb_size = _guest_dtb_image_end - _guest_dtb_image;
@@ -112,12 +112,12 @@ void init(void) {
     success = virq_register(GUEST_VCPU_ID, ETHERNET_PHY_IRQ, &ethernet_phy_ack, NULL);
 #endif
     /* Just in case there is already an interrupt available to handle, we ack it here. */
-    sel4cp_irq_ack(SERIAL_IRQ_CH);
+    microkit_irq_ack(SERIAL_IRQ_CH);
     /* Finally start the guest */
     guest_start(GUEST_VCPU_ID, kernel_pc, GUEST_DTB_VADDR, GUEST_INIT_RAM_DISK_VADDR);
 }
 
-void notified(sel4cp_channel ch) {
+void notified(microkit_channel ch) {
     switch (ch) {
         case ETHERNET_IRQ_CH: {
             bool success = virq_inject(GUEST_VCPU_ID, ETHERNET_IRQ);
@@ -152,11 +152,11 @@ void notified(sel4cp_channel ch) {
  * whenever our guest causes an exception, it gets delivered to this entry point for
  * the VMM to handle.
  */
-void fault(sel4cp_id id, sel4cp_msginfo msginfo) {
+void fault(microkit_id id, microkit_msginfo msginfo) {
     bool success = fault_handle(id, msginfo);
     if (success) {
         /* Now that we have handled the fault successfully, we reply to it so
          * that the guest can resume execution. */
-        sel4cp_fault_reply(sel4cp_msginfo_new(0, 0));
+        microkit_fault_reply(microkit_msginfo_new(0, 0));
     }
 }
diff --git a/examples/framebuffer/Makefile b/examples/framebuffer/Makefile
index 545c7314..ec9a12f1 100644
--- a/examples/framebuffer/Makefile
+++ b/examples/framebuffer/Makefile
@@ -5,8 +5,8 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
-ifeq ($(strip $(SEL4CP_SDK)),)
-$(error SEL4CP_SDK must be specified)
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
 endif
 
 ifeq ($(strip $(BOARD)),)
@@ -43,7 +43,7 @@ endif
 
 CC := $(TOOLCHAIN)-gcc
 LD := $(TOOLCHAIN)-ld
-SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
 
 # @ivanv: need to have a step for putting in the initrd node into the DTB,
 # 		  right now it is unfortunately hard-coded.
@@ -54,7 +54,7 @@ SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
 
 # @ivanv: incremental builds don't work with IMAGE_DIR changing
 
-BOARD_DIR := $(SEL4CP_SDK)/board/$(BOARD)/$(CONFIG)
+BOARD_DIR := $(MICROKIT_SDK)/board/$(BOARD)/$(CONFIG)
 VMM := ../../
 VMM_TOOLS := $(VMM)/tools
 VMM_SRC_DIR := $(VMM)/src
@@ -96,7 +96,7 @@ CFLAGS := -mstrict-align \
 		  -DCONFIG_$(CONFIG)
 
 LDFLAGS := -L$(BOARD_DIR)/lib
-LIBS := -lsel4cp -Tsel4cp.ld
+LIBS := -lmicrokit -Tmicrokit.ld
 
 all: directories $(IMAGE_FILE)
 
@@ -152,4 +152,4 @@ $(BUILD_DIR)/send_rectangle.elf: $(addprefix $(BUILD_DIR)/, $(SEND_RECTANGLE_OBJ
 	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
 
 $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(ELFS)) $(SYSTEM_DESCRIPTION) $(IMAGE_DIR)
-	$(SEL4CP_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+	$(MICROKIT_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
diff --git a/examples/framebuffer/send_rectangle.c b/examples/framebuffer/send_rectangle.c
index 520db6f4..0e1c1b8b 100644
--- a/examples/framebuffer/send_rectangle.c
+++ b/examples/framebuffer/send_rectangle.c
@@ -4,7 +4,7 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 
-#include <sel4cp.h>
+#include <microkit.h>
 #include "util/util.h"
 #include <stddef.h>
 #include "uio.h"
@@ -15,7 +15,7 @@ uint8_t *uio_map0;
 
 void init() {
     // Initialising rectangle PD
-    sel4cp_dbg_puts("SEND RECTANGLE|INFO: starting!\n");
+    microkit_dbg_puts("SEND RECTANGLE|INFO: starting!\n");
 }
 
 fb_config_t *config;
@@ -66,7 +66,7 @@ void readconfig() {
     line_len = config->xres * (config->bpp/8);
 }
 
-void notified(sel4cp_channel ch) {
+void notified(microkit_channel ch) {
     switch (ch) {
         case VMM_CH: {
             // Draw triangle
@@ -74,7 +74,7 @@ void notified(sel4cp_channel ch) {
             readconfig();
             printf("RECT|INFO: writing to uio_map0\n");
             fbwrite();
-            sel4cp_notify(VMM_CH);
+            microkit_notify(VMM_CH);
             break;
         }
         default:
diff --git a/examples/framebuffer/vmm.c b/examples/framebuffer/vmm.c
index 9bab5f25..517bfeed 100644
--- a/examples/framebuffer/vmm.c
+++ b/examples/framebuffer/vmm.c
@@ -5,7 +5,7 @@
  */
 #include <stddef.h>
 #include <stdint.h>
-#include <sel4cp.h>
+#include <microkit.h>
 #include "util/util.h"
 #include "arch/aarch64/vgic/vgic.h"
 #include "arch/aarch64/linux.h"
@@ -40,18 +40,18 @@ extern char _guest_dtb_image_end[];
 /* Data for the initial RAM disk to be passed to the kernel. */
 extern char _guest_initrd_image[];
 extern char _guest_initrd_image_end[];
-/* seL4CP will set this variable to the start of the guest RAM memory region. */
+/* Microkit will set this variable to the start of the guest RAM memory region. */
 uintptr_t guest_ram_vaddr;
 
 #define MAX_IRQ_CH 63
 int passthrough_irq_map[MAX_IRQ_CH];
 
 static void passthrough_device_ack(size_t vcpu_id, int irq, void *cookie) {
-    sel4cp_channel irq_ch = (sel4cp_channel)(int64_t)cookie;
-    sel4cp_irq_ack(irq_ch);
+    microkit_channel irq_ch = (microkit_channel)(int64_t)cookie;
+    microkit_irq_ack(irq_ch);
 }
 
-static void register_passthrough_irq(int irq, sel4cp_channel irq_ch) {
+static void register_passthrough_irq(int irq, microkit_channel irq_ch) {
     LOG_VMM("Register passthrough IRQ %d (channel: 0x%lx)\n", irq, irq_ch);
     assert(irq_ch < MAX_IRQ_CH);
     passthrough_irq_map[irq_ch] = irq;
@@ -69,13 +69,13 @@ void uio_gpu_ack(size_t vcpu_id, int irq, void *cookie) {
 
 bool uio_init_handler(size_t vcpu_id, uintptr_t addr) {
     LOG_VMM("sending notification to UIO PD!\n");
-    sel4cp_notify(UIO_PD_CH);
+    microkit_notify(UIO_PD_CH);
     return true;
 }
 
 void init(void) {
     /* Initialise the VMM, the VCPU(s), and start the guest */
-    LOG_VMM("starting \"%s\"\n", sel4cp_name);
+    LOG_VMM("starting \"%s\"\n", microkit_name);
     /* Place all the binaries in the right locations before starting the guest */
     size_t kernel_size = _guest_kernel_image_end - _guest_kernel_image;
     size_t dtb_size = _guest_dtb_image_end - _guest_dtb_image;
@@ -136,7 +136,7 @@ void init(void) {
     guest_start(GUEST_VCPU_ID, kernel_pc, GUEST_DTB_VADDR, GUEST_INIT_RAM_DISK_VADDR);
 }
 
-void notified(sel4cp_channel ch) {
+void notified(microkit_channel ch) {
     switch (ch) {
         case UIO_PD_CH: {
             LOG_VMM("Got message from UIO PD, injecting IRQ\n");
@@ -163,11 +163,11 @@ void notified(sel4cp_channel ch) {
  * whenever our guest causes an exception, it gets delivered to this entry point for
  * the VMM to handle.
  */
-void fault(sel4cp_id id, sel4cp_msginfo msginfo) {
+void fault(microkit_id id, microkit_msginfo msginfo) {
     bool success = fault_handle(id, msginfo);
     if (success) {
         /* Now that we have handled the fault successfully, we reply to it so
          * that the guest can resume execution. */
-        sel4cp_fault_reply(sel4cp_msginfo_new(0, 0));
+        microkit_fault_reply(microkit_msginfo_new(0, 0));
     }
 }
diff --git a/examples/rust/Cargo.lock b/examples/rust/Cargo.lock
index f2ce4c1b..da4f48d4 100644
--- a/examples/rust/Cargo.lock
+++ b/examples/rust/Cargo.lock
@@ -4,18 +4,18 @@ version = 3
 
 [[package]]
 name = "aho-corasick"
-version = "1.0.4"
+version = "1.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6748e8def348ed4d14996fa801f4122cd763fff530258cdc03f64b25f89d3a5a"
+checksum = "ea5d730647d4fadd988536d06fecce94b7b4f2a7efdae548f1cf4b63205518ab"
 dependencies = [
  "memchr",
 ]
 
 [[package]]
 name = "bindgen"
-version = "0.64.0"
+version = "0.68.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c4243e6031260db77ede97ad86c27e501d646a27ab57b59a574f725d98ab1fb4"
+checksum = "726e4313eb6ec35d2730258ad4e15b547ee75d6afaa1361a922e78e59b7d8078"
 dependencies = [
  "bitflags",
  "cexpr",
@@ -24,20 +24,21 @@ dependencies = [
  "lazycell",
  "log",
  "peeking_take_while",
+ "prettyplease",
  "proc-macro2",
  "quote",
  "regex",
  "rustc-hash",
  "shlex",
- "syn 1.0.109",
+ "syn 2.0.37",
  "which",
 ]
 
 [[package]]
 name = "bitflags"
-version = "1.3.2"
+version = "2.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
+checksum = "b4682ae6287fcf752ecaabbfcc7b6f9b72aa33933dc23a554d853aea8eea8635"
 
 [[package]]
 name = "block-buffer"
@@ -49,10 +50,13 @@ dependencies = [
 ]
 
 [[package]]
-name = "byteorder"
-version = "1.4.3"
+name = "cc"
+version = "1.0.83"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "14c189c53d098945499cdfa7ecc63567cf3886b3332b312a5b4585d8d3a6a610"
+checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0"
+dependencies = [
+ "libc",
+]
 
 [[package]]
 name = "cexpr"
@@ -124,6 +128,27 @@ version = "1.9.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07"
 
+[[package]]
+name = "errno"
+version = "0.3.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "136526188508e25c6fef639d7927dfb3e0e3084488bf202267829cf7fc23dbdd"
+dependencies = [
+ "errno-dragonfly",
+ "libc",
+ "windows-sys",
+]
+
+[[package]]
+name = "errno-dragonfly"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "aa68f1b12764fab894d2755d2518754e71b4fd80ecfb822714a1206c2aab39bf"
+dependencies = [
+ "cc",
+ "libc",
+]
+
 [[package]]
 name = "fallible-iterator"
 version = "0.2.0"
@@ -152,6 +177,15 @@ version = "0.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b"
 
+[[package]]
+name = "home"
+version = "0.5.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5444c27eef6923071f7ebcc33e3444508466a76f7a2b93da00ed6e19f30c1ddb"
+dependencies = [
+ "windows-sys",
+]
+
 [[package]]
 name = "itoa"
 version = "1.0.9"
@@ -172,9 +206,9 @@ checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55"
 
 [[package]]
 name = "libc"
-version = "0.2.147"
+version = "0.2.148"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b4668fb0ea861c1df094127ac5f1da3409a82116a4ba74fca2e58ef927159bb3"
+checksum = "9cdc71e17332e86d2e1d38c1f99edcb6288ee11b815fb1a4b049eaa2114d369b"
 
 [[package]]
 name = "libloading"
@@ -186,6 +220,12 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "linux-raw-sys"
+version = "0.4.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1a9bad9f94746442c783ca431b22403b519cd7fbeed0533fdd6328b2f2212128"
+
 [[package]]
 name = "log"
 version = "0.4.20"
@@ -194,9 +234,9 @@ checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f"
 
 [[package]]
 name = "memchr"
-version = "2.5.0"
+version = "2.6.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d"
+checksum = "8f232d6ef707e1956a43342693d2a31e72989554d58299d7a88738cc95b0d35c"
 
 [[package]]
 name = "minimal-lexical"
@@ -214,26 +254,6 @@ dependencies = [
  "minimal-lexical",
 ]
 
-[[package]]
-name = "num_enum"
-version = "0.5.11"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1f646caf906c20226733ed5b1374287eb97e3c2a5c227ce668c1f2ce20ae57c9"
-dependencies = [
- "num_enum_derive",
-]
-
-[[package]]
-name = "num_enum_derive"
-version = "0.5.11"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dcbff9bc912032c62bf65ef1d5aea88983b420f4f839db1e9b0c281a25c9c799"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "once_cell"
 version = "1.18.0"
@@ -248,19 +268,20 @@ checksum = "19b17cddbe7ec3f8bc800887bab5e717348c95ea2ca0b1bf0837fb964dc67099"
 
 [[package]]
 name = "pest"
-version = "2.7.2"
+version = "2.7.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1acb4a4365a13f749a93f1a094a7805e5cfa0955373a9de860d962eaa3a5fe5a"
+checksum = "d7a4d085fd991ac8d5b05a147b437791b4260b76326baf0fc60cf7c9c27ecd33"
 dependencies = [
+ "memchr",
  "thiserror",
  "ucd-trie",
 ]
 
 [[package]]
 name = "pest_derive"
-version = "2.7.2"
+version = "2.7.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "666d00490d4ac815001da55838c500eafb0320019bbaa44444137c48b443a853"
+checksum = "a2bee7be22ce7918f641a33f08e3f43388c7656772244e2bbb2477f44cc9021a"
 dependencies = [
  "pest",
  "pest_generator",
@@ -268,33 +289,43 @@ dependencies = [
 
 [[package]]
 name = "pest_generator"
-version = "2.7.2"
+version = "2.7.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ca01446f50dbda87c1786af8770d535423fa8a53aec03b8f4e3d7eb10e0929"
+checksum = "d1511785c5e98d79a05e8a6bc34b4ac2168a0e3e92161862030ad84daa223141"
 dependencies = [
  "pest",
  "pest_meta",
  "proc-macro2",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.37",
 ]
 
 [[package]]
 name = "pest_meta"
-version = "2.7.2"
+version = "2.7.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "56af0a30af74d0445c0bf6d9d051c979b516a1a5af790d251daee76005420a48"
+checksum = "b42f0394d3123e33353ca5e1e89092e533d2cc490389f2bd6131c43c634ebc5f"
 dependencies = [
  "once_cell",
  "pest",
  "sha2",
 ]
 
+[[package]]
+name = "prettyplease"
+version = "0.2.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ae005bd773ab59b4725093fd7df83fd7892f7d8eafb48dbd7de6e024e4215f9d"
+dependencies = [
+ "proc-macro2",
+ "syn 2.0.37",
+]
+
 [[package]]
 name = "proc-macro2"
-version = "1.0.66"
+version = "1.0.67"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "18fb31db3f9bddb2ea821cde30a9f70117e3f119938b5ee630b7403aa6e2ead9"
+checksum = "3d433d9f1a3e8c1263d9456598b16fec66f4acc9a74dacffd35c7bb09b3a1328"
 dependencies = [
  "unicode-ident",
 ]
@@ -310,9 +341,9 @@ dependencies = [
 
 [[package]]
 name = "regex"
-version = "1.9.3"
+version = "1.9.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "81bc1d4caf89fac26a70747fe603c130093b53c773888797a6329091246d651a"
+checksum = "697061221ea1b4a94a624f67d0ae2bfe4e22b8a17b6a192afb11046542cc8c47"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -322,9 +353,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.3.6"
+version = "0.3.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fed1ceff11a1dddaee50c9dc8e4938bd106e9d89ae372f192311e7da498e3b69"
+checksum = "c2f401f4955220693b56f8ec66ee9c78abffd8d1c4f23dc41a23839eb88f0795"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -333,9 +364,9 @@ dependencies = [
 
 [[package]]
 name = "regex-syntax"
-version = "0.7.4"
+version = "0.7.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e5ea92a5b6195c6ef2a0295ea818b312502c6fc94dde986c5553242e18fd4ce2"
+checksum = "dbb5fb1acd8a1a18b3dd5be62d25485eb770e05afb408a9627d14d451bae12da"
 
 [[package]]
 name = "rustc-hash"
@@ -343,6 +374,19 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2"
 
+[[package]]
+name = "rustix"
+version = "0.38.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "747c788e9ce8e92b12cd485c49ddf90723550b654b32508f979b71a7b1ecda4f"
+dependencies = [
+ "bitflags",
+ "errno",
+ "libc",
+ "linux-raw-sys",
+ "windows-sys",
+]
+
 [[package]]
 name = "ryu"
 version = "1.0.15"
@@ -352,7 +396,7 @@ checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741"
 [[package]]
 name = "sel4"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "cfg-if",
  "sel4-config",
@@ -362,7 +406,7 @@ dependencies = [
 [[package]]
 name = "sel4-bitfield-parser"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "pest",
  "pest_derive",
@@ -372,17 +416,17 @@ dependencies = [
 [[package]]
 name = "sel4-bitfield-types"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 
 [[package]]
 name = "sel4-build-env"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 
 [[package]]
 name = "sel4-config"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "sel4-config-macros",
 ]
@@ -390,7 +434,7 @@ dependencies = [
 [[package]]
 name = "sel4-config-data"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "lazy_static",
  "sel4-build-env",
@@ -401,7 +445,7 @@ dependencies = [
 [[package]]
 name = "sel4-config-generic-macro-impls"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "fallible-iterator",
  "proc-macro2",
@@ -413,7 +457,7 @@ dependencies = [
 [[package]]
 name = "sel4-config-generic-types"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "serde",
 ]
@@ -421,7 +465,7 @@ dependencies = [
 [[package]]
 name = "sel4-config-macros"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "sel4-config-data",
  "sel4-config-generic-macro-impls",
@@ -430,7 +474,7 @@ dependencies = [
 [[package]]
 name = "sel4-dlmalloc"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "dlmalloc",
  "sel4-sync",
@@ -439,17 +483,48 @@ dependencies = [
 [[package]]
 name = "sel4-externally-shared"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 
 [[package]]
 name = "sel4-immediate-sync-once-cell"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
+
+[[package]]
+name = "sel4-immutable-cell"
+version = "0.1.0"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
+
+[[package]]
+name = "sel4-microkit"
+version = "0.1.0"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
+dependencies = [
+ "cfg-if",
+ "sel4",
+ "sel4-externally-shared",
+ "sel4-immediate-sync-once-cell",
+ "sel4-immutable-cell",
+ "sel4-microkit-macros",
+ "sel4-panicking",
+ "sel4-panicking-env",
+ "sel4-runtime-common",
+]
+
+[[package]]
+name = "sel4-microkit-macros"
+version = "0.1.0"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
 
 [[package]]
 name = "sel4-panicking"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "cfg-if",
  "sel4-immediate-sync-once-cell",
@@ -460,12 +535,12 @@ dependencies = [
 [[package]]
 name = "sel4-panicking-env"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 
 [[package]]
 name = "sel4-reserve-tls-on-stack"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "cfg-if",
  "sel4",
@@ -474,7 +549,7 @@ dependencies = [
 [[package]]
 name = "sel4-runtime-common"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "cfg-if",
  "sel4-dlmalloc",
@@ -486,7 +561,7 @@ dependencies = [
 [[package]]
 name = "sel4-rustfmt-helper"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "which",
 ]
@@ -494,7 +569,7 @@ dependencies = [
 [[package]]
 name = "sel4-sync"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "sel4",
  "sel4-immediate-sync-once-cell",
@@ -503,7 +578,7 @@ dependencies = [
 [[package]]
 name = "sel4-sys"
 version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
+source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#e4bde410c4477057a9bdb6db734fbc26d03c24cd"
 dependencies = [
  "bindgen",
  "glob",
@@ -521,58 +596,31 @@ dependencies = [
  "xmltree",
 ]
 
-[[package]]
-name = "sel4cp"
-version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
-dependencies = [
- "cfg-if",
- "num_enum",
- "sel4",
- "sel4-externally-shared",
- "sel4-immediate-sync-once-cell",
- "sel4-panicking",
- "sel4-panicking-env",
- "sel4-runtime-common",
- "sel4cp-macros",
- "zerocopy",
-]
-
-[[package]]
-name = "sel4cp-macros"
-version = "0.1.0"
-source = "git+https://github.com/Ivan-Velickovic/rust-seL4?branch=dev#d423885168cb2839a0e368cf9641336e1b2de214"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "serde"
-version = "1.0.183"
+version = "1.0.188"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "32ac8da02677876d532745a130fc9d8e6edfa81a269b107c5b00829b91d8eb3c"
+checksum = "cf9e0fcba69a370eed61bcf2b728575f726b50b55cba78064753d708ddc7549e"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.183"
+version = "1.0.188"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aafe972d60b0b9bee71a91b92fee2d4fb3c9d7e8f6b179aa99f27203d99a4816"
+checksum = "4eca7ac642d82aa35b60049a6eccb4be6be75e599bd2e9adb5f875a737654af2"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.37",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.105"
+version = "1.0.107"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "693151e1ac27563d6dbcec9dee9fbd5da8539b20fa14ad3752b2e6d363ace360"
+checksum = "6b420ce6e3d8bd882e9b243c6eed35dbc9a6110c9769e74b584e0d68d1f20c65"
 dependencies = [
  "itoa",
  "ryu",
@@ -592,9 +640,9 @@ dependencies = [
 
 [[package]]
 name = "shlex"
-version = "1.1.0"
+version = "1.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "43b2853a4d09f215c24cc5489c992ce46052d359b5109343cbafbf26bc62f8a3"
+checksum = "a7cee0529a6d40f580e7a5e6c495c8fbfe21b7b52795ed4bb5e62cdf92bc6380"
 
 [[package]]
 name = "syn"
@@ -609,9 +657,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.29"
+version = "2.0.37"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c324c494eba9d92503e6f1ef2e6df781e78f6a7705a0202d9801b198807d518a"
+checksum = "7303ef2c05cd654186cb250d29049a24840ca25d2747c25c0381c8d9e2f582e8"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -620,29 +668,29 @@ dependencies = [
 
 [[package]]
 name = "thiserror"
-version = "1.0.47"
+version = "1.0.48"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "97a802ec30afc17eee47b2855fc72e0c4cd62be9b4efe6591edde0ec5bd68d8f"
+checksum = "9d6d7a740b8a666a7e828dd00da9c0dc290dff53154ea77ac109281de90589b7"
 dependencies = [
  "thiserror-impl",
 ]
 
 [[package]]
 name = "thiserror-impl"
-version = "1.0.47"
+version = "1.0.48"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6bb623b56e39ab7dcd4b1b98bb6c8f8d907ed255b18de254088016b27a8ee19b"
+checksum = "49922ecae66cc8a249b77e68d1d0623c1b2c514f0060c27cdc68bd62a1219d35"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.29",
+ "syn 2.0.37",
 ]
 
 [[package]]
 name = "typenum"
-version = "1.16.0"
+version = "1.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "497961ef93d974e23eb6f433eb5fe1b7930b659f06d12dec6fc44a8f554c0bba"
+checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
 
 [[package]]
 name = "ucd-trie"
@@ -652,9 +700,9 @@ checksum = "ed646292ffc8188ef8ea4d1e0e0150fb15a5c2e12ad9b8fc191ae7a8a7f3c4b9"
 
 [[package]]
 name = "unicode-ident"
-version = "1.0.11"
+version = "1.0.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "301abaae475aa91687eb82514b328ab47a211a533026cb25fc3e519b86adfc3c"
+checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
 
 [[package]]
 name = "unwinding"
@@ -675,18 +723,19 @@ checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
 name = "vmm"
 version = "0.1.0"
 dependencies = [
- "sel4cp",
+ "sel4-microkit",
 ]
 
 [[package]]
 name = "which"
-version = "4.4.0"
+version = "4.4.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2441c784c52b289a054b7201fc93253e288f094e2f4be9058343127c4226a269"
+checksum = "87ba24419a2078cd2b0f2ede2691b6c66d8e47836da3b6db8265ebad47afbfc7"
 dependencies = [
  "either",
- "libc",
+ "home",
  "once_cell",
+ "rustix",
 ]
 
 [[package]]
@@ -712,37 +761,82 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
 
 [[package]]
-name = "xml-rs"
-version = "0.8.16"
+name = "windows-sys"
+version = "0.48.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "47430998a7b5d499ccee752b41567bc3afc57e1327dc855b1a2aa44ce29b5fa1"
+checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9"
+dependencies = [
+ "windows-targets",
+]
 
 [[package]]
-name = "xmltree"
-version = "0.10.3"
+name = "windows-targets"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d7d8a75eaf6557bb84a65ace8609883db44a29951042ada9b393151532e41fcb"
+checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c"
 dependencies = [
- "xml-rs",
+ "windows_aarch64_gnullvm",
+ "windows_aarch64_msvc",
+ "windows_i686_gnu",
+ "windows_i686_msvc",
+ "windows_x86_64_gnu",
+ "windows_x86_64_gnullvm",
+ "windows_x86_64_msvc",
 ]
 
 [[package]]
-name = "zerocopy"
-version = "0.6.3"
+name = "windows_aarch64_gnullvm"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f3b9c234616391070b0b173963ebc65a9195068e7ed3731c6edac2ec45ebe106"
-dependencies = [
- "byteorder",
- "zerocopy-derive",
-]
+checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
+
+[[package]]
+name = "windows_aarch64_msvc"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
+
+[[package]]
+name = "windows_i686_gnu"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
+
+[[package]]
+name = "windows_i686_msvc"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
+
+[[package]]
+name = "windows_x86_64_gnu"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
 
 [[package]]
-name = "zerocopy-derive"
-version = "0.6.3"
+name = "windows_x86_64_gnullvm"
+version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8f7f3a471f98d0a61c34322fbbfd10c384b07687f680d4119813713f72308d91"
+checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
+
+[[package]]
+name = "windows_x86_64_msvc"
+version = "0.48.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
+
+[[package]]
+name = "xml-rs"
+version = "0.8.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fcb9cbac069e033553e8bb871be2fbdffcab578eb25bd0f7c508cedc6dcd75a"
+
+[[package]]
+name = "xmltree"
+version = "0.10.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d7d8a75eaf6557bb84a65ace8609883db44a29951042ada9b393151532e41fcb"
 dependencies = [
- "proc-macro2",
- "quote",
- "syn 2.0.29",
+ "xml-rs",
 ]
diff --git a/examples/rust/Cargo.toml b/examples/rust/Cargo.toml
index a96e1130..ea1b6c39 100644
--- a/examples/rust/Cargo.toml
+++ b/examples/rust/Cargo.toml
@@ -9,7 +9,7 @@ license = "BSD-2-Clause"
 name = "vmm"
 path = "src/vmm.rs"
 
-[dependencies.sel4cp]
+[dependencies.sel4-microkit]
 # Temporarily use fork of rust-seL4 until all the changes
 # we need are upstreamed
 git = "https://github.com/Ivan-Velickovic/rust-seL4"
diff --git a/examples/rust/Makefile b/examples/rust/Makefile
index 4aa41e1f..21f8c76d 100644
--- a/examples/rust/Makefile
+++ b/examples/rust/Makefile
@@ -5,8 +5,8 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
-ifeq ($(strip $(SEL4CP_SDK)),)
-$(error SEL4CP_SDK must be specified)
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
 endif
 
 # Default build directory, pass BUILD_DIR=<dir> to override
@@ -24,9 +24,9 @@ DTC := dtc
 CC := clang
 LD := ld.lld
 AR := llvm-ar
-SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
 
-BOARD_DIR := $(SEL4CP_SDK)/board/$(BOARD)/$(CONFIG)
+BOARD_DIR := $(MICROKIT_SDK)/board/$(BOARD)/$(CONFIG)
 LIBVMM := ../../src
 SYSTEM_DESCRIPTION := rust_vmm.system
 
@@ -73,16 +73,16 @@ CFLAGS := -mstrict-align \
 		  -target aarch64-none-elf
 
 LDFLAGS := -L$(BOARD_DIR)/lib
-LIBS := -lsel4cp -Tsel4cp.ld
+LIBS := -lmicrokit -Tmicrokit.ld
 
 RUST_TARGET_PATH := .
-RUST_SEL4CP_TARGET := aarch64-sel4cp-minimal
+RUST_MICROKIT_TARGET := aarch64-microkit-minimal
 TARGET_DIR := $(BUILD_DIR)/target
 
 RUST_ENV := \
 	RUST_TARGET_PATH=$(abspath $(RUST_TARGET_PATH)) \
 	SEL4_INCLUDE_DIRS=$(abspath $(BOARD_DIR)/include) \
-	SEL4CP_BOARD_DIR=$(abspath $(BOARD_DIR)) \
+	MICROKIT_BOARD_DIR=$(abspath $(BOARD_DIR)) \
 	BUILD_DIR=$(abspath $(BUILD_DIR)) \
 	IMAGE_DIR=$(abspath $(IMAGE_DIR)) \
 
@@ -92,7 +92,7 @@ RUST_OPTIONS := \
 	-Z build-std-features=compiler-builtins-mem \
 	-Z bindeps \
 	--release \
-	--target $(RUST_SEL4CP_TARGET) \
+	--target $(RUST_MICROKIT_TARGET) \
 	--target-dir $(abspath $(TARGET_DIR)) \
 	--out-dir $(abspath $(BUILD_DIR)) \
 
@@ -135,4 +135,4 @@ $(BUILD_DIR)/vmm.elf: src/vmm.rs $(BUILD_DIR)/libvmm.a $(LINUX) $(INITRD) $(DTB)
 		cargo build $(RUST_OPTIONS)
 
 $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(ELFS)) $(SYSTEM_DESCRIPTION)
-	$(SEL4CP_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+	$(MICROKIT_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
diff --git a/examples/rust/README.md b/examples/rust/README.md
index cdc75f62..c136a78b 100644
--- a/examples/rust/README.md
+++ b/examples/rust/README.md
@@ -15,7 +15,7 @@ are sufficient.
 
 It should also be noted that this example makes use of the
 [rust-seL4](https://github.com/coliasgroup/rust-seL4/) project's support for
-seL4CP, which is subject to change.
+Microkit, which is subject to change.
 
 ## Building the example
 
@@ -23,12 +23,12 @@ You will first need to have Rust installed, the instructions for this are [here]
 
 From here, you build the example with:
 ```sh
-make SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6
+make MICROKIT_SDK=/path/to/sdk
 ```
 
 ## Running the example
 
 You can build and run the example in a single command with:
 ```sh
-make SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6 qemu
+make MICROKIT_SDK=/path/to/sdk qemu
 ```
diff --git a/examples/rust/aarch64-sel4cp-minimal.json b/examples/rust/aarch64-microkit-minimal.json
similarity index 100%
rename from examples/rust/aarch64-sel4cp-minimal.json
rename to examples/rust/aarch64-microkit-minimal.json
diff --git a/examples/rust/build.rs b/examples/rust/build.rs
index 9b3871c0..f643127f 100644
--- a/examples/rust/build.rs
+++ b/examples/rust/build.rs
@@ -1,6 +1,6 @@
 fn main() {
-    match std::env::var("SEL4CP_BOARD_DIR") {
-        Ok(sel4cp_board_dir) => println!("cargo:rustc-link-search={sel4cp_board_dir}/lib"),
+    match std::env::var("MICROKIT_BOARD_DIR") {
+        Ok(microkit_board_dir) => println!("cargo:rustc-link-search={microkit_board_dir}/lib"),
         Err(e) => println!("Could not get environment variable 'BOARD_DIR': {e}"),
     }
 
diff --git a/examples/rust/src/vmm.rs b/examples/rust/src/vmm.rs
index 27a9e4f9..565169ac 100644
--- a/examples/rust/src/vmm.rs
+++ b/examples/rust/src/vmm.rs
@@ -5,8 +5,7 @@
 use core::{include_bytes};
 use core::ffi::{c_void};
 
-use sel4cp::message::{MessageInfo};
-use sel4cp::{protection_domain, Channel, Child, Handler, debug_println};
+use sel4_microkit::{protection_domain, MessageInfo, Channel, Child, Handler, debug_println};
 
 const guest_ram_vaddr: usize = 0x40000000;
 const GUEST_DTB_VADDR: usize = 0x4f000000;
@@ -29,7 +28,7 @@ const UART_CH: Channel = Channel::new(1);
 // or even creating your own "Rust-like" bindings for the VMM library to make it
 // nicer to use (or closer to feeling like a Rust crate), or both!
 #[link(name = "vmm", kind = "static")]
-#[link(name = "sel4cp", kind = "static")]
+#[link(name = "microkit", kind = "static")]
 extern "C" {
     fn linux_setup_images(ram_start: usize,
                           kernel: usize, kernel_size: usize,
diff --git a/examples/simple/Makefile b/examples/simple/Makefile
index 4395f9f1..7770844c 100644
--- a/examples/simple/Makefile
+++ b/examples/simple/Makefile
@@ -5,8 +5,8 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
-ifeq ($(strip $(SEL4CP_SDK)),)
-$(error SEL4CP_SDK must be specified)
+ifeq ($(strip $(MICROKIT_SDK)),)
+$(error MICROKIT_SDK must be specified)
 endif
 
 ifeq ($(strip $(BOARD)),)
@@ -43,7 +43,7 @@ DTC := dtc
 
 CC := clang
 LD := ld.lld
-SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
+MICROKIT_TOOL ?= $(MICROKIT_SDK)/bin/microkit
 
 # @ivanv: need to have a step for putting in the initrd node into the DTB,
 # 		  right now it is unfortunately hard-coded.
@@ -54,7 +54,7 @@ SEL4CP_TOOL ?= $(SEL4CP_SDK)/bin/sel4cp
 
 # @ivanv: incremental builds don't work with IMAGE_DIR changing
 
-BOARD_DIR := $(SEL4CP_SDK)/board/$(BOARD)/$(CONFIG)
+BOARD_DIR := $(MICROKIT_SDK)/board/$(BOARD)/$(CONFIG)
 VMM := ../../
 VMM_TOOLS := $(VMM)/tools
 VMM_SRC_DIR := $(VMM)/src
@@ -94,7 +94,7 @@ CFLAGS := -mstrict-align \
 		  -target aarch64-none-elf
 
 LDFLAGS := -L$(BOARD_DIR)/lib
-LIBS := -lsel4cp -Tsel4cp.ld
+LIBS := -lmicrokit -Tmicrokit.ld
 
 all: directories $(IMAGE_FILE)
 
@@ -143,4 +143,4 @@ $(BUILD_DIR)/vmm.elf: $(addprefix $(BUILD_DIR)/, $(VMM_OBJS))
 	$(LD) $(LDFLAGS) $^ $(LIBS) -o $@
 
 $(IMAGE_FILE) $(REPORT_FILE): $(addprefix $(BUILD_DIR)/, $(ELFS)) $(SYSTEM_DESCRIPTION) $(IMAGE_DIR)
-	$(SEL4CP_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
+	$(MICROKIT_TOOL) $(SYSTEM_DESCRIPTION) --search-path $(BUILD_DIR) $(IMAGE_DIR) --board $(BOARD) --config $(CONFIG) -o $(IMAGE_FILE) -r $(REPORT_FILE)
diff --git a/examples/simple/README.md b/examples/simple/README.md
index 24b72553..6bc9d579 100644
--- a/examples/simple/README.md
+++ b/examples/simple/README.md
@@ -11,7 +11,7 @@ The example currently works on the following platforms:
 ## Building with Make
 
 ```sh
-make BOARD=<BOARD> SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6
+make BOARD=<BOARD> MICROKIT_SDK=/path/to/sdk
 ```
 
 Where `<BOARD>` is one of:
@@ -23,7 +23,7 @@ and `BUILD_DIR`, see the Makefile for details.
 
 If you would like to simulate the QEMU board you can run the following command:
 ```sh
-make BOARD=qemu_arm_virt SEL4CP_SDK=/path/to/sel4cp-sdk-1.2.6 qemu
+make BOARD=qemu_arm_virt MICROKIT_SDK=/path/to/sdk qemu
 ```
 
 This will build the example code as well as run the QEMU command to simulate a
@@ -38,7 +38,7 @@ You will first need Zig version 0.11.x (e.g 0.11.0 or 0.11.1) which can be
 downloaded from [here](https://ziglang.org/download/).
 
 ```sh
-zig build -Dsdk=/path/to/sel4cp-sdk-1.2.6 -Dboard=<BOARD>
+zig build -Dsdk=/path/to/sdk -Dboard=<BOARD>
 ```
 
 Where `<BOARD>` is one of:
@@ -47,11 +47,11 @@ Where `<BOARD>` is one of:
 
 If you are building for QEMU then you can also run QEMU by doing:
 ```sh
-zig build -Dsdk=/path/to/sel4cp-sdk-1.2.6 -Dboard=<BOARD> qemu
+zig build -Dsdk=/path/to/sdk -Dboard=<BOARD> qemu
 ```
 
 You can view other options by doing:
 ```sh
-zig build -Dsdk=/path/to/sel4cp-sdk-1.2.6 -Dboard=<BOARD> -h
+zig build -Dsdk=/path/to/sdk -Dboard=<BOARD> -h
 ```
 
diff --git a/examples/simple/build.zig b/examples/simple/build.zig
index aa59bdb8..dae93759 100644
--- a/examples/simple/build.zig
+++ b/examples/simple/build.zig
@@ -56,37 +56,37 @@ const ConfigOptions = enum {
 };
 
 pub fn build(b: *std.Build) void {
-    // @ivanv: need to somehow relate sel4cp config with this optimisation level?
+    // @ivanv: need to somehow relate Microkit config with this optimisation level?
     const optimize = b.standardOptimizeOption(.{});
 
-    // Getting the path to the seL4CP SDK before doing anything else
-    const sel4cp_sdk_arg = b.option([]const u8, "sdk", "Path to seL4CP SDK");
-    if (sel4cp_sdk_arg == null) {
+    // Getting the path to the Microkit SDK before doing anything else
+    const microkit_sdk_arg = b.option([]const u8, "sdk", "Path to Microkit SDK");
+    if (microkit_sdk_arg == null) {
         std.log.err("Missing -Dsdk=/path/to/sdk argument being passed\n", .{});
         std.os.exit(1);
     }
-    const sel4cp_sdk = sel4cp_sdk_arg.?;
+    const microkit_sdk = microkit_sdk_arg.?;
 
-    const sel4cp_config_option = b.option(ConfigOptions, "config", "seL4CP config to build for")
+    const microkit_config_option = b.option(ConfigOptions, "config", "Microkit config to build for")
                                  orelse ConfigOptions.debug;
-    const sel4cp_config = @tagName(sel4cp_config_option);
+    const microkit_config = @tagName(microkit_config_option);
 
-    // Get the seL4CP SDK board we want to target
-    const sel4cp_board_option = b.option(CorePlatformBoard, "board", "seL4CP board to target");
+    // Get the Microkit SDK board we want to target
+    const microkit_board_option = b.option(CorePlatformBoard, "board", "Microkit board to target");
 
-    if (sel4cp_board_option == null) {
+    if (microkit_board_option == null) {
         std.log.err("Missing -Dboard=<BOARD> argument being passed\n", .{});
         std.os.exit(1);
     }
-    const target = findTarget(sel4cp_board_option.?);
-    const sel4cp_board = @tagName(sel4cp_board_option.?);
+    const target = findTarget(microkit_board_option.?);
+    const microkit_board = @tagName(microkit_board_option.?);
 
     // Since we are relying on Zig to produce the final ELF, it needs to do the
     // linking step as well.
-    const sdk_board_dir = fmtPrint("{s}/board/{s}/{s}", .{ sel4cp_sdk, sel4cp_board, sel4cp_config });
-    const sdk_tool = fmtPrint("{s}/bin/sel4cp", .{ sel4cp_sdk });
-    const libsel4cp = fmtPrint("{s}/lib/libsel4cp.a", .{ sdk_board_dir });
-    const libsel4cp_linker_script = fmtPrint("{s}/lib/sel4cp.ld", .{ sdk_board_dir });
+    const sdk_board_dir = fmtPrint("{s}/board/{s}/{s}", .{ microkit_sdk, microkit_board, microkit_config });
+    const sdk_tool = fmtPrint("{s}/bin/microkit", .{ microkit_sdk });
+    const libmicrokit = fmtPrint("{s}/lib/libmicrokit.a", .{ sdk_board_dir });
+    const libmicrokit_linker_script = fmtPrint("{s}/lib/microkit.ld", .{ sdk_board_dir });
     const sdk_board_include_dir = fmtPrint("{s}/include", .{ sdk_board_dir });
 
     const libvmm = b.addStaticLibrary(.{
@@ -136,23 +136,23 @@ pub fn build(b: *std.Build) void {
     });
 
     // For actually compiling the DTS into a DTB
-    const dts_path = fmtPrint("board/{s}/linux.dts", .{ sel4cp_board });
+    const dts_path = fmtPrint("board/{s}/linux.dts", .{ microkit_board });
     const dtc_command = b.addSystemCommand(&[_][]const u8{
         "dtc", "-I", "dts", "-O", "dtb", dts_path, "-o"
     });
     const dtb_image_path = dtc_command.addOutputFileArg("linux.dtb");
 
-    // Add sel4cp.h to be used by the API wrapper.
+    // Add microkit.h to be used by the API wrapper.
     exe.addIncludePath(.{ .path = sdk_board_include_dir });
     // The VMM code will include 
     exe.addIncludePath(.{ .path = libvmm_src });
     exe.addIncludePath(.{ .path = libvmm_src_arch });
     // Add the static library that provides each protection domain's entry
     // point (`main()`), which runs the main handler loop.
-    exe.addObjectFile(.{ .path = libsel4cp });
+    exe.addObjectFile(.{ .path = libmicrokit });
     exe.linkLibrary(libvmm);
     // Specify the linker script, this is necessary to set the ELF entry point address.
-    exe.setLinkerScriptPath(.{ .path = libsel4cp_linker_script });
+    exe.setLinkerScriptPath(.{ .path = libmicrokit_linker_script });
 
     exe.addCSourceFiles(&.{"vmm.c"}, &.{
         "-Wall",
@@ -169,10 +169,10 @@ pub fn build(b: *std.Build) void {
     });
     dtb_image_path.addStepDependencies(&guest_images.step);
 
-    const linux_image_path = fmtPrint("board/{s}/linux", .{ sel4cp_board });
+    const linux_image_path = fmtPrint("board/{s}/linux", .{ microkit_board });
     const kernel_image_arg = fmtPrint("-DGUEST_KERNEL_IMAGE_PATH=\"{s}\"", .{ linux_image_path });
 
-    const initrd_image_path = fmtPrint("board/{s}/rootfs.cpio.gz", .{ sel4cp_board });
+    const initrd_image_path = fmtPrint("board/{s}/rootfs.cpio.gz", .{ microkit_board });
     const initrd_image_arg = fmtPrint("-DGUEST_INITRD_IMAGE_PATH=\"{s}\"", .{ initrd_image_path });
     const dtb_image_arg = fmtPrint("-DGUEST_DTB_IMAGE_PATH=\"{s}\"", .{ dtb_image_path.getPath(b) });
     guest_images.addCSourceFiles(&.{ libvmm_tools ++ "package_guest_images.S" }, &.{
@@ -186,33 +186,33 @@ pub fn build(b: *std.Build) void {
     exe.addObject(guest_images);
     b.installArtifact(exe);
 
-    const system_description_path = fmtPrint("board/{s}/simple.system", .{ sel4cp_board });
+    const system_description_path = fmtPrint("board/{s}/simple.system", .{ microkit_board });
     const final_image_dest = b.getInstallPath(.bin, "./loader.img");
-    const sel4cp_tool_cmd = b.addSystemCommand(&[_][]const u8{
+    const microkit_tool_cmd = b.addSystemCommand(&[_][]const u8{
        sdk_tool,
        system_description_path,
        "--search-path",
        b.getInstallPath(.bin, ""),
        "--board",
-       sel4cp_board,
+       microkit_board,
        "--config",
-       sel4cp_config,
+       microkit_config,
        "-o",
        final_image_dest,
        "-r",
        b.getInstallPath(.prefix, "./report.txt")
     });
-    // Running the seL4CP tool depends on 
-    sel4cp_tool_cmd.step.dependOn(b.getInstallStep());
-    // Add the "sel4cp" step, and make it the default step when we execute `zig build`>
-    const sel4cp_step = b.step("sel4cp", "Compile and build the final bootable image");
-    sel4cp_step.dependOn(&sel4cp_tool_cmd.step);
-    b.default_step = sel4cp_step;
+    // Running the Microkit tool depends on 
+    microkit_tool_cmd.step.dependOn(b.getInstallStep());
+    // Add the "microkit" step, and make it the default step when we execute `zig build`>
+    const microkit_step = b.step("microkit", "Compile and build the final bootable image");
+    microkit_step.dependOn(&microkit_tool_cmd.step);
+    b.default_step = microkit_step;
 
     // This is setting up a `qemu` command for running the system via QEMU,
     // which we only want to do when we have a board that we can actually simulate.
     const loader_arg = fmtPrint("loader,file={s},addr=0x70000000,cpu-num=0", .{ final_image_dest });
-    if (std.mem.eql(u8, sel4cp_board, "qemu_arm_virt")) {
+    if (std.mem.eql(u8, microkit_board, "qemu_arm_virt")) {
         const qemu_cmd = b.addSystemCommand(&[_][]const u8{
             "qemu-system-aarch64",
             "-machine",
diff --git a/examples/simple/vmm.c b/examples/simple/vmm.c
index 18eac9de..c891022d 100644
--- a/examples/simple/vmm.c
+++ b/examples/simple/vmm.c
@@ -5,7 +5,7 @@
  */
 #include <stddef.h>
 #include <stdint.h>
-#include <sel4cp.h>
+#include <microkit.h>
 #include "util/util.h"
 #include "arch/aarch64/vgic/vgic.h"
 #include "arch/aarch64/linux.h"
@@ -73,7 +73,7 @@ extern char _guest_dtb_image_end[];
 /* Data for the initial RAM disk to be passed to the kernel. */
 extern char _guest_initrd_image[];
 extern char _guest_initrd_image_end[];
-/* seL4CP will set this variable to the start of the guest RAM memory region. */
+/* Microkit will set this variable to the start of the guest RAM memory region. */
 uintptr_t guest_ram_vaddr;
 
 static void serial_ack(size_t vcpu_id, int irq, void *cookie) {
@@ -81,12 +81,12 @@ static void serial_ack(size_t vcpu_id, int irq, void *cookie) {
      * For now we by default simply ack the serial IRQ, we have not
      * come across a case yet where more than this needs to be done.
      */
-    sel4cp_irq_ack(SERIAL_IRQ_CH);
+    microkit_irq_ack(SERIAL_IRQ_CH);
 }
 
 void init(void) {
     /* Initialise the VMM, the VCPU(s), and start the guest */
-    LOG_VMM("starting \"%s\"\n", sel4cp_name);
+    LOG_VMM("starting \"%s\"\n", microkit_name);
     /* Place all the binaries in the right locations before starting the guest */
     size_t kernel_size = _guest_kernel_image_end - _guest_kernel_image;
     size_t dtb_size = _guest_dtb_image_end - _guest_dtb_image;
@@ -115,12 +115,12 @@ void init(void) {
     // actually get the interrupt. This should be avoided by making the VGIC driver more stable.
     success = virq_register(GUEST_VCPU_ID, SERIAL_IRQ, &serial_ack, NULL);
     /* Just in case there is already an interrupt available to handle, we ack it here. */
-    sel4cp_irq_ack(SERIAL_IRQ_CH);
+    microkit_irq_ack(SERIAL_IRQ_CH);
     /* Finally start the guest */
     guest_start(GUEST_VCPU_ID, kernel_pc, GUEST_DTB_VADDR, GUEST_INIT_RAM_DISK_VADDR);
 }
 
-void notified(sel4cp_channel ch) {
+void notified(microkit_channel ch) {
     switch (ch) {
         case SERIAL_IRQ_CH: {
             bool success = virq_inject(GUEST_VCPU_ID, SERIAL_IRQ);
@@ -139,11 +139,11 @@ void notified(sel4cp_channel ch) {
  * whenever our guest causes an exception, it gets delivered to this entry point for
  * the VMM to handle.
  */
-void fault(sel4cp_id id, sel4cp_msginfo msginfo) {
+void fault(microkit_id id, microkit_msginfo msginfo) {
     bool success = fault_handle(id, msginfo);
     if (success) {
         /* Now that we have handled the fault successfully, we reply to it so
          * that the guest can resume execution. */
-        sel4cp_fault_reply(sel4cp_msginfo_new(0, 0));
+        microkit_fault_reply(microkit_msginfo_new(0, 0));
     }
 }
diff --git a/examples/zig/build.zig b/examples/zig/build.zig
index c94dc5e9..b924c730 100644
--- a/examples/zig/build.zig
+++ b/examples/zig/build.zig
@@ -15,22 +15,22 @@ pub fn build(b: *std.Build) void {
     const optimize = b.standardOptimizeOption(.{});
 
     // @ivanv sort out
-    const sdk_path = "/home/ivanv/ts/sel4cp/release/sel4cp-sdk-1.2.6";
+    const sdk_path = "microkit-sdk-1.2.6";
     const board = "qemu_arm_virt";
     const config = "debug";
-    // const sel4cp_build_dir = "build";
+    // const microkit_build_dir = "build";
     // Since we are relying on Zig to produce the final ELF, it needs to do the
     // linking step as well.
     const sdk_board_dir = sdk_path ++ "/board/" ++ board ++ "/" ++ config;
 
-    const zig_libsel4cp = b.addObject(.{
-        .name = "zig_libsel4cp",
-        .root_source_file = .{ .path = "src/libsel4cp.c" },
+    const zig_libmicrokit = b.addObject(.{
+        .name = "zig_libmicrokit",
+        .root_source_file = .{ .path = "src/libmicrokit.c" },
         .target = target,
         .optimize = optimize,
     });
-    zig_libsel4cp.addIncludePath(.{ .path = "src/" });
-    zig_libsel4cp.addIncludePath(.{ .path = sdk_board_dir ++ "/include" });
+    zig_libmicrokit.addIncludePath(.{ .path = "src/" });
+    zig_libmicrokit.addIncludePath(.{ .path = sdk_board_dir ++ "/include" });
 
     const vmmlib = b.addStaticLibrary(.{
         .name = "vmm",
@@ -77,27 +77,27 @@ pub fn build(b: *std.Build) void {
         .optimize = optimize,
     });
 
-    // Add sel4cp.h to be used by the API wrapper.
+    // Add microkit.h to be used by the API wrapper.
     exe.addIncludePath(.{ .path = sdk_board_dir ++ "/include" });
     exe.addIncludePath(.{ .path = "../../src/" });
     exe.addIncludePath(.{ .path = "../../src/util/" });
     exe.addIncludePath(.{ .path = "../../src/arch/aarch64/" });
     // Add the static library that provides each protection domain's entry
     // point (`main()`), which runs the main handler loop.
-    exe.addObjectFile(.{ .path = sdk_board_dir ++ "/lib/libsel4cp.a" });
+    exe.addObjectFile(.{ .path = sdk_board_dir ++ "/lib/libmicrokit.a" });
     exe.linkLibrary(vmmlib);
-    exe.addObject(zig_libsel4cp);
+    exe.addObject(zig_libmicrokit);
     // exe.linkLibrary(libsel4);
     // Specify the linker script, this is necessary to set the ELF entry point address.
-    exe.setLinkerScriptPath(.{ .path = sdk_board_dir ++ "/lib/sel4cp.ld"});
+    exe.setLinkerScriptPath(.{ .path = sdk_board_dir ++ "/lib/microkit.ld"});
 
     exe.addIncludePath(.{ .path = "src/" });
 
     b.installArtifact(exe);
 
     const system_description_path = "zig_vmm.system";
-    const sel4cp_tool_cmd = b.addSystemCommand(&[_][]const u8{
-       sdk_path ++ "/bin/sel4cp",
+    const microkit_tool_cmd = b.addSystemCommand(&[_][]const u8{
+       sdk_path ++ "/bin/microkit",
        system_description_path,
        "--search-path",
        "zig-out/bin",
@@ -110,11 +110,11 @@ pub fn build(b: *std.Build) void {
        "-r",
        "zig-out/report.txt",
     });
-    sel4cp_tool_cmd.step.dependOn(b.getInstallStep());
-    // Add the "sel4cp" step, and make it the default step when we execute `zig build`>
-    const sel4cp_step = b.step("sel4cp", "Compile and build the final bootable image");
-    sel4cp_step.dependOn(&sel4cp_tool_cmd.step);
-    b.default_step = sel4cp_step;
+    microkit_tool_cmd.step.dependOn(b.getInstallStep());
+    // Add the "microkit" step, and make it the default step when we execute `zig build`>
+    const microkit_step = b.step("microkit", "Compile and build the final bootable image");
+    microkit_step.dependOn(&microkit_tool_cmd.step);
+    b.default_step = microkit_step;
 
     // This is setting up a `qemu` command for running the system via QEMU,
     // which we only want to do when we have a board that we can actually simulate.
diff --git a/examples/zig/src/libsel4cp.c b/examples/zig/src/libmicrokit.c
similarity index 98%
rename from examples/zig/src/libsel4cp.c
rename to examples/zig/src/libmicrokit.c
index b57d7389..bab4e20f 100644
--- a/examples/zig/src/libsel4cp.c
+++ b/examples/zig/src/libmicrokit.c
@@ -1,4 +1,4 @@
-#include "libsel4cp.h";
+#include "libmicrokit.h";
 
 void zig_arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1,
                                 seL4_Word mr2, seL4_Word mr3)
diff --git a/examples/zig/src/libsel4cp.h b/examples/zig/src/libmicrokit.h
similarity index 95%
rename from examples/zig/src/libsel4cp.h
rename to examples/zig/src/libmicrokit.h
index 5bbcd671..c37f6ac4 100644
--- a/examples/zig/src/libsel4cp.h
+++ b/examples/zig/src/libmicrokit.h
@@ -1,4 +1,4 @@
-#include <sel4cp.h>
+#include <microkit.h>
 
 void zig_arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1,
                                 seL4_Word mr2, seL4_Word mr3);
diff --git a/examples/zig/src/libsel4cp.zig b/examples/zig/src/libmicrokit.zig
similarity index 98%
rename from examples/zig/src/libsel4cp.zig
rename to examples/zig/src/libmicrokit.zig
index ed41727d..1ef000bb 100644
--- a/examples/zig/src/libsel4cp.zig
+++ b/examples/zig/src/libmicrokit.zig
@@ -1,5 +1,5 @@
-const libsel4cp = @cImport({
-    @cInclude("libsel4cp.h");
+const libmicrokit = @cImport({
+    @cInclude("libmicrokit.h");
 });
 
 pub const __builtin_bswap16 = @import("std").zig.c_builtins.__builtin_bswap16;
@@ -3869,7 +3869,7 @@ pub fn seL4_SetCapReceivePath(arg_receiveCNode: seL4_CPtr, arg_receiveIndex: seL
 pub fn seL4_Send(arg_dest: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t) callconv(.C) void {
     var dest = arg_dest;
     var msgInfo = arg_msgInfo;
-    libsel4cp.zig_arm_sys_send(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysSend))), dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], seL4_GetMR(@as(c_int, 0)), seL4_GetMR(@as(c_int, 1)), seL4_GetMR(@as(c_int, 2)), seL4_GetMR(@as(c_int, 3)));
+    libmicrokit.zig_arm_sys_send(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysSend))), dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], seL4_GetMR(@as(c_int, 0)), seL4_GetMR(@as(c_int, 1)), seL4_GetMR(@as(c_int, 2)), seL4_GetMR(@as(c_int, 3)));
 }
 pub fn seL4_Recv(arg_src: seL4_CPtr, arg_sender: [*c]seL4_Word, arg_reply: seL4_CPtr) callconv(.C) seL4_MessageInfo_t {
     var src = arg_src;
@@ -3899,7 +3899,7 @@ pub fn seL4_Call(arg_dest: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t) callconv(
     var msg1: seL4_Word = seL4_GetMR(@as(c_int, 1));
     var msg2: seL4_Word = seL4_GetMR(@as(c_int, 2));
     var msg3: seL4_Word = seL4_GetMR(@as(c_int, 3));
-    libsel4cp.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysCall))), dest, &dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], &info.words[@as(c_uint, @intCast(@as(c_int, 0)))], &msg0, &msg1, &msg2, &msg3, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
+    libmicrokit.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysCall))), dest, &dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], &info.words[@as(c_uint, @intCast(@as(c_int, 0)))], &msg0, &msg1, &msg2, &msg3, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
     seL4_SetMR(@as(c_int, 0), msg0);
     seL4_SetMR(@as(c_int, 1), msg1);
     seL4_SetMR(@as(c_int, 2), msg2);
@@ -3909,7 +3909,7 @@ pub fn seL4_Call(arg_dest: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t) callconv(
 pub fn seL4_NBSend(arg_dest: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t) callconv(.C) void {
     var dest = arg_dest;
     var msgInfo = arg_msgInfo;
-    libsel4cp.zig_arm_sys_send(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysNBSend))), dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], seL4_GetMR(@as(c_int, 0)), seL4_GetMR(@as(c_int, 1)), seL4_GetMR(@as(c_int, 2)), seL4_GetMR(@as(c_int, 3)));
+    libmicrokit.zig_arm_sys_send(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysNBSend))), dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], seL4_GetMR(@as(c_int, 0)), seL4_GetMR(@as(c_int, 1)), seL4_GetMR(@as(c_int, 2)), seL4_GetMR(@as(c_int, 3)));
 }
 pub fn seL4_ReplyRecv(arg_src: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t, arg_sender: [*c]seL4_Word, arg_reply: seL4_CPtr) callconv(.C) seL4_MessageInfo_t {
     var src = arg_src;
@@ -3926,7 +3926,7 @@ pub fn seL4_ReplyRecv(arg_src: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t, arg_s
     msg1 = seL4_GetMR(@as(c_int, 1));
     msg2 = seL4_GetMR(@as(c_int, 2));
     msg3 = seL4_GetMR(@as(c_int, 3));
-    libsel4cp.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysReplyRecv))), src, &badge, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], &info.words[@as(c_uint, @intCast(@as(c_int, 0)))], &msg0, &msg1, &msg2, &msg3, reply);
+    libmicrokit.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysReplyRecv))), src, &badge, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], &info.words[@as(c_uint, @intCast(@as(c_int, 0)))], &msg0, &msg1, &msg2, &msg3, reply);
     seL4_SetMR(@as(c_int, 0), msg0);
     seL4_SetMR(@as(c_int, 1), msg1);
     seL4_SetMR(@as(c_int, 2), msg2);
@@ -4064,7 +4064,7 @@ pub fn seL4_DebugPutChar(arg_c: u8) callconv(.C) void {
     var unused3: seL4_Word = 0;
     var unused4: seL4_Word = 0;
     var unused5: seL4_Word = 0;
-    libsel4cp.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugPutChar))), @as(seL4_Word, @bitCast(@as(c_ulong, c))), &unused0, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused1, &unused2, &unused3, &unused4, &unused5, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
+    libmicrokit.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugPutChar))), @as(seL4_Word, @bitCast(@as(c_ulong, c))), &unused0, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused1, &unused2, &unused3, &unused4, &unused5, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
 }
 pub fn seL4_DebugDumpScheduler() callconv(.C) void {
     var unused0: seL4_Word = 0;
@@ -4073,7 +4073,7 @@ pub fn seL4_DebugDumpScheduler() callconv(.C) void {
     var unused3: seL4_Word = 0;
     var unused4: seL4_Word = 0;
     var unused5: seL4_Word = 0;
-    libsel4cp.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugDumpScheduler))), @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused0, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused1, &unused2, &unused3, &unused4, &unused5, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
+    libmicrokit.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugDumpScheduler))), @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused0, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused1, &unused2, &unused3, &unused4, &unused5, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
 }
 pub fn seL4_DebugHalt() callconv(.C) void {
     arm_sys_null(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugHalt))));
@@ -4087,7 +4087,7 @@ pub fn seL4_DebugCapIdentify(arg_cap: seL4_CPtr) callconv(.C) seL4_Uint32 {
     var unused2: seL4_Word = 0;
     var unused3: seL4_Word = 0;
     var unused4: seL4_Word = 0;
-    libsel4cp.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugCapIdentify))), cap, &cap, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused0, &unused1, &unused2, &unused3, &unused4, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
+    libmicrokit.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugCapIdentify))), cap, &cap, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused0, &unused1, &unused2, &unused3, &unused4, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
     return @as(seL4_Uint32, @bitCast(@as(c_uint, @truncate(cap))));
 }
 pub fn seL4_DebugNameThread(arg_tcb: seL4_CPtr, arg_name: [*c]const u8) callconv(.C) void {
@@ -4100,7 +4100,7 @@ pub fn seL4_DebugNameThread(arg_tcb: seL4_CPtr, arg_name: [*c]const u8) callconv
     var unused3: seL4_Word = 0;
     var unused4: seL4_Word = 0;
     var unused5: seL4_Word = 0;
-    libsel4cp.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugNameThread))), tcb, &unused0, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused1, &unused2, &unused3, &unused4, &unused5, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
+    libmicrokit.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysDebugNameThread))), tcb, &unused0, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), &unused1, &unused2, &unused3, &unused4, &unused5, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
 } // ./sel4/sel4_arch/syscalls.h:71:5: warning: TODO implement translation of stmt class GCCAsmStmtClass
 // ./sel4/sel4_arch/syscalls.h:57:20: warning: unable to translate function, demoted to extern
 pub extern fn arm_sys_send(arg_sys: seL4_Word, arg_dest: seL4_Word, arg_info_arg: seL4_Word, arg_mr0: seL4_Word, arg_mr1: seL4_Word, arg_mr2: seL4_Word, arg_mr3: seL4_Word) callconv(.C) void; // ./sel4/sel4_arch/syscalls.h:109:5: warning: TODO implement translation of stmt class GCCAsmStmtClass
@@ -4121,7 +4121,7 @@ pub fn seL4_SendWithMRs(arg_dest: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t, ar
     var mr1 = arg_mr1;
     var mr2 = arg_mr2;
     var mr3 = arg_mr3;
-    libsel4cp.zig_arm_sys_send(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysSend))), dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], if ((mr0 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr0.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr1 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr1.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr2 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr2.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr3 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr3.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
+    libmicrokit.zig_arm_sys_send(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysSend))), dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], if ((mr0 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr0.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr1 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr1.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr2 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr2.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr3 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr3.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
 }
 pub fn seL4_NBSendWithMRs(arg_dest: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t, arg_mr0: [*c]seL4_Word, arg_mr1: [*c]seL4_Word, arg_mr2: [*c]seL4_Word, arg_mr3: [*c]seL4_Word) callconv(.C) void {
     var dest = arg_dest;
@@ -4130,7 +4130,7 @@ pub fn seL4_NBSendWithMRs(arg_dest: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t,
     var mr1 = arg_mr1;
     var mr2 = arg_mr2;
     var mr3 = arg_mr3;
-    libsel4cp.zig_arm_sys_send(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysNBSend))), dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], if ((mr0 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr0.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr1 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr1.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr2 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr2.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr3 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr3.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
+    libmicrokit.zig_arm_sys_send(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysNBSend))), dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], if ((mr0 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr0.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr1 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr1.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr2 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr2.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))), if ((mr3 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))))) mr3.* else @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
 }
 pub fn seL4_RecvWithMRs(arg_src: seL4_CPtr, arg_sender: [*c]seL4_Word, arg_reply: seL4_CPtr, arg_mr0: [*c]seL4_Word, arg_mr1: [*c]seL4_Word, arg_mr2: [*c]seL4_Word, arg_mr3: [*c]seL4_Word) callconv(.C) seL4_MessageInfo_t {
     var src = arg_src;
@@ -4188,7 +4188,7 @@ pub fn seL4_CallWithMRs(arg_dest: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t, ar
     if ((mr3 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 3)))))) {
         msg3 = mr3.*;
     }
-    libsel4cp.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysCall))), dest, &dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], &info.words[@as(c_uint, @intCast(@as(c_int, 0)))], &msg0, &msg1, &msg2, &msg3, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
+    libmicrokit.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysCall))), dest, &dest, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], &info.words[@as(c_uint, @intCast(@as(c_int, 0)))], &msg0, &msg1, &msg2, &msg3, @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 0)))));
     if (mr0 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) {
         mr0.* = msg0;
     }
@@ -4230,7 +4230,7 @@ pub fn seL4_ReplyRecvWithMRs(arg_src: seL4_CPtr, arg_msgInfo: seL4_MessageInfo_t
     if ((mr3 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) and (seL4_MessageInfo_get_length(msgInfo) > @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 3)))))) {
         msg3 = mr3.*;
     }
-    libsel4cp.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysReplyRecv))), src, &badge, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], &info.words[@as(c_uint, @intCast(@as(c_int, 0)))], &msg0, &msg1, &msg2, &msg3, reply);
+    libmicrokit.zig_arm_sys_send_recv(@as(seL4_Word, @bitCast(@as(c_long, seL4_SysReplyRecv))), src, &badge, msgInfo.words[@as(c_uint, @intCast(@as(c_int, 0)))], &info.words[@as(c_uint, @intCast(@as(c_int, 0)))], &msg0, &msg1, &msg2, &msg3, reply);
     if (mr0 != @as([*c]seL4_Word, @ptrCast(@alignCast(@as(?*anyopaque, @ptrFromInt(@as(c_int, 0))))))) {
         mr0.* = msg0;
     }
@@ -6337,19 +6337,19 @@ pub fn seL4_CapData_Guard_new(arg_guard: seL4_Word, arg_bits: seL4_Word) callcon
     var bits = arg_bits;
     return seL4_CNode_CapData_new(guard, bits).words[@as(c_uint, @intCast(@as(c_int, 0)))];
 }
-pub const sel4cp_channel = c_uint;
-pub const sel4cp_id = c_uint;
-pub const sel4cp_msginfo = seL4_MessageInfo_t;
+pub const microkit_channel = c_uint;
+pub const microkit_id = c_uint;
+pub const microkit_msginfo = seL4_MessageInfo_t;
 pub extern fn init() void;
-pub extern fn notified(ch: sel4cp_channel) void;
-pub extern fn protected(ch: sel4cp_channel, msginfo: sel4cp_msginfo) sel4cp_msginfo;
-pub extern fn fault(ch: sel4cp_channel, msginfo: sel4cp_msginfo) void;
-pub extern var sel4cp_name: [16]u8;
+pub extern fn notified(ch: microkit_channel) void;
+pub extern fn protected(ch: microkit_channel, msginfo: microkit_msginfo) microkit_msginfo;
+pub extern fn fault(ch: microkit_channel, msginfo: microkit_msginfo) void;
+pub extern var microkit_name: [16]u8;
 pub extern var have_signal: bool;
 pub extern var signal: seL4_CPtr;
 pub extern var signal_msg: seL4_MessageInfo_t;
-pub extern fn sel4cp_dbg_putc(c: c_int) void;
-pub extern fn sel4cp_dbg_puts(s: [*c]const u8) void;
+pub extern fn microkit_dbg_putc(c: c_int) void;
+pub extern fn microkit_dbg_puts(s: [*c]const u8) void;
 pub fn memzero(arg_s: ?*anyopaque, arg_n: c_ulong) callconv(.C) void {
     var s = arg_s;
     var n = arg_n;
@@ -6369,145 +6369,145 @@ pub fn memzero(arg_s: ?*anyopaque, arg_n: c_ulong) callconv(.C) void {
         }
     }
 }
-pub fn sel4cp_internal_crash(arg_err: seL4_Error) callconv(.C) void {
+pub fn microkit_internal_crash(arg_err: seL4_Error) callconv(.C) void {
     var err = arg_err;
     var x: [*c]c_int = @as([*c]c_int, @ptrFromInt(@as(usize, @bitCast(@as(c_ulong, err)))));
     x.* = 0;
 }
-pub fn sel4cp_notify(arg_ch: sel4cp_channel) callconv(.C) void {
+pub fn microkit_notify(arg_ch: microkit_channel) callconv(.C) void {
     var ch = arg_ch;
-    seL4_Signal(@as(seL4_CPtr, @bitCast(@as(c_ulong, @as(sel4cp_channel, @bitCast(@as(c_int, 10))) +% ch))));
+    seL4_Signal(@as(seL4_CPtr, @bitCast(@as(c_ulong, @as(microkit_channel, @bitCast(@as(c_int, 10))) +% ch))));
 }
-pub fn sel4cp_irq_ack(arg_ch: sel4cp_channel) callconv(.C) void {
+pub fn microkit_irq_ack(arg_ch: microkit_channel) callconv(.C) void {
     var ch = arg_ch;
-    _ = seL4_IRQHandler_Ack(@as(seL4_IRQHandler, @bitCast(@as(c_ulong, @as(sel4cp_channel, @bitCast(@as(c_int, 138))) +% ch))));
+    _ = seL4_IRQHandler_Ack(@as(seL4_IRQHandler, @bitCast(@as(c_ulong, @as(microkit_channel, @bitCast(@as(c_int, 138))) +% ch))));
 }
-pub fn sel4cp_notify_delayed(arg_ch: sel4cp_channel) callconv(.C) void {
+pub fn microkit_notify_delayed(arg_ch: microkit_channel) callconv(.C) void {
     var ch = arg_ch;
     have_signal = @as(c_int, 1) != 0;
     signal_msg = seL4_MessageInfo_new(@as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))), @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))), @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))), @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))));
-    signal = @as(seL4_CPtr, @bitCast(@as(c_ulong, @as(sel4cp_channel, @bitCast(@as(c_int, 10))) +% ch)));
+    signal = @as(seL4_CPtr, @bitCast(@as(c_ulong, @as(microkit_channel, @bitCast(@as(c_int, 10))) +% ch)));
 }
-pub fn sel4cp_irq_ack_delayed(arg_ch: sel4cp_channel) callconv(.C) void {
+pub fn microkit_irq_ack_delayed(arg_ch: microkit_channel) callconv(.C) void {
     var ch = arg_ch;
     have_signal = @as(c_int, 1) != 0;
     signal_msg = seL4_MessageInfo_new(@as(seL4_Uint64, @bitCast(@as(c_long, IRQAckIRQ))), @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))), @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))), @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))));
-    signal = @as(seL4_CPtr, @bitCast(@as(c_ulong, @as(sel4cp_channel, @bitCast(@as(c_int, 138))) +% ch)));
+    signal = @as(seL4_CPtr, @bitCast(@as(c_ulong, @as(microkit_channel, @bitCast(@as(c_int, 138))) +% ch)));
 }
-pub fn sel4cp_pd_restart(arg_pd: sel4cp_id, arg_entry_point: usize) callconv(.C) void {
+pub fn microkit_pd_restart(arg_pd: microkit_id, arg_entry_point: usize) callconv(.C) void {
     var pd = arg_pd;
     var entry_point = arg_entry_point;
     var err: seL4_Error = undefined;
     var ctxt: seL4_UserContext = undefined;
     memzero(@as(?*anyopaque, @ptrCast(&ctxt)), @sizeOf(seL4_UserContext));
     ctxt.pc = entry_point;
-    err = seL4_TCB_WriteRegisters(@as(seL4_TCB, @bitCast(@as(c_ulong, @as(sel4cp_id, @bitCast(@as(c_int, 202))) +% pd))), @as(seL4_Bool, @bitCast(@as(i8, @truncate(@as(c_int, 1))))), @as(seL4_Uint8, @bitCast(@as(i8, @truncate(@as(c_int, 0))))), @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 1)))), &ctxt);
+    err = seL4_TCB_WriteRegisters(@as(seL4_TCB, @bitCast(@as(c_ulong, @as(microkit_id, @bitCast(@as(c_int, 202))) +% pd))), @as(seL4_Bool, @bitCast(@as(i8, @truncate(@as(c_int, 1))))), @as(seL4_Uint8, @bitCast(@as(i8, @truncate(@as(c_int, 0))))), @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 1)))), &ctxt);
     if (err != @as(c_uint, @bitCast(seL4_NoError))) {
-        sel4cp_dbg_puts("sel4cp_pd_restart: error writing TCB registers\n");
-        sel4cp_internal_crash(err);
+        microkit_dbg_puts("microkit_pd_restart: error writing TCB registers\n");
+        microkit_internal_crash(err);
     }
 }
-pub fn sel4cp_pd_stop(arg_pd: sel4cp_id) callconv(.C) void {
+pub fn microkit_pd_stop(arg_pd: microkit_id) callconv(.C) void {
     var pd = arg_pd;
     var err: seL4_Error = undefined;
-    err = seL4_TCB_Suspend(@as(seL4_TCB, @bitCast(@as(c_ulong, @as(sel4cp_id, @bitCast(@as(c_int, 202))) +% pd))));
+    err = seL4_TCB_Suspend(@as(seL4_TCB, @bitCast(@as(c_ulong, @as(microkit_id, @bitCast(@as(c_int, 202))) +% pd))));
     if (err != @as(c_uint, @bitCast(seL4_NoError))) {
-        sel4cp_dbg_puts("sel4cp_pd_stop: error suspending TCB\n");
-        sel4cp_internal_crash(err);
+        microkit_dbg_puts("microkit_pd_stop: error suspending TCB\n");
+        microkit_internal_crash(err);
     }
 }
-pub fn sel4cp_fault_reply(arg_msginfo: sel4cp_msginfo) callconv(.C) void {
+pub fn microkit_fault_reply(arg_msginfo: microkit_msginfo) callconv(.C) void {
     var msginfo = arg_msginfo;
     seL4_Send(@as(seL4_CPtr, @bitCast(@as(c_long, @as(c_int, 4)))), msginfo);
 }
-pub fn sel4cp_ppcall(arg_ch: sel4cp_channel, arg_msginfo: sel4cp_msginfo) callconv(.C) sel4cp_msginfo {
+pub fn microkit_ppcall(arg_ch: microkit_channel, arg_msginfo: microkit_msginfo) callconv(.C) microkit_msginfo {
     var ch = arg_ch;
     var msginfo = arg_msginfo;
-    return seL4_Call(@as(seL4_CPtr, @bitCast(@as(c_ulong, @as(sel4cp_channel, @bitCast(@as(c_int, 74))) +% ch))), msginfo);
+    return seL4_Call(@as(seL4_CPtr, @bitCast(@as(c_ulong, @as(microkit_channel, @bitCast(@as(c_int, 74))) +% ch))), msginfo);
 }
-pub fn sel4cp_msginfo_new(arg_label: u64, arg_count: u16) callconv(.C) sel4cp_msginfo {
+pub fn microkit_msginfo_new(arg_label: u64, arg_count: u16) callconv(.C) microkit_msginfo {
     var label = arg_label;
     var count = arg_count;
     return seL4_MessageInfo_new(label, @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))), @as(seL4_Uint64, @bitCast(@as(c_long, @as(c_int, 0)))), @as(seL4_Uint64, @bitCast(@as(c_ulong, count))));
 }
-pub fn sel4cp_msginfo_get_label(arg_msginfo: sel4cp_msginfo) callconv(.C) u64 {
+pub fn microkit_msginfo_get_label(arg_msginfo: microkit_msginfo) callconv(.C) u64 {
     var msginfo = arg_msginfo;
     return seL4_MessageInfo_get_label(msginfo);
 }
-pub fn sel4cp_mr_set(arg_mr: u8, arg_value: u64) callconv(.C) void {
+pub fn microkit_mr_set(arg_mr: u8, arg_value: u64) callconv(.C) void {
     var mr = arg_mr;
     var value = arg_value;
     seL4_SetMR(@as(c_int, @bitCast(@as(c_uint, mr))), value);
 }
-pub fn sel4cp_mr_get(arg_mr: u8) callconv(.C) u64 {
+pub fn microkit_mr_get(arg_mr: u8) callconv(.C) u64 {
     var mr = arg_mr;
     return seL4_GetMR(@as(c_int, @bitCast(@as(c_uint, mr))));
 }
-pub fn sel4cp_vm_restart(arg_vm: sel4cp_id, arg_entry_point: usize) callconv(.C) void {
+pub fn microkit_vm_restart(arg_vm: microkit_id, arg_entry_point: usize) callconv(.C) void {
     var vm = arg_vm;
     var entry_point = arg_entry_point;
     var err: seL4_Error = undefined;
     var ctxt: seL4_UserContext = undefined;
     memzero(@as(?*anyopaque, @ptrCast(&ctxt)), @sizeOf(seL4_UserContext));
     ctxt.pc = entry_point;
-    err = seL4_TCB_WriteRegisters(@as(seL4_TCB, @bitCast(@as(c_ulong, @as(sel4cp_id, @bitCast(@as(c_int, 266))) +% vm))), @as(seL4_Bool, @bitCast(@as(i8, @truncate(@as(c_int, 1))))), @as(seL4_Uint8, @bitCast(@as(i8, @truncate(@as(c_int, 0))))), @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 1)))), &ctxt);
+    err = seL4_TCB_WriteRegisters(@as(seL4_TCB, @bitCast(@as(c_ulong, @as(microkit_id, @bitCast(@as(c_int, 266))) +% vm))), @as(seL4_Bool, @bitCast(@as(i8, @truncate(@as(c_int, 1))))), @as(seL4_Uint8, @bitCast(@as(i8, @truncate(@as(c_int, 0))))), @as(seL4_Word, @bitCast(@as(c_long, @as(c_int, 1)))), &ctxt);
     if (err != @as(c_uint, @bitCast(seL4_NoError))) {
-        sel4cp_dbg_puts("sel4cp_vm_restart: error writing registers\n");
-        sel4cp_internal_crash(err);
+        microkit_dbg_puts("microkit_vm_restart: error writing registers\n");
+        microkit_internal_crash(err);
     }
 }
-pub fn sel4cp_vm_stop(arg_vm: sel4cp_id) callconv(.C) void {
+pub fn microkit_vm_stop(arg_vm: microkit_id) callconv(.C) void {
     var vm = arg_vm;
     var err: seL4_Error = undefined;
-    err = seL4_TCB_Suspend(@as(seL4_TCB, @bitCast(@as(c_ulong, @as(sel4cp_id, @bitCast(@as(c_int, 266))) +% vm))));
+    err = seL4_TCB_Suspend(@as(seL4_TCB, @bitCast(@as(c_ulong, @as(microkit_id, @bitCast(@as(c_int, 266))) +% vm))));
     if (err != @as(c_uint, @bitCast(seL4_NoError))) {
-        sel4cp_dbg_puts("sel4cp_vm_stop: error suspending TCB\n");
-        sel4cp_internal_crash(err);
+        microkit_dbg_puts("microkit_vm_stop: error suspending TCB\n");
+        microkit_internal_crash(err);
     }
 }
-pub fn sel4cp_arm_vcpu_inject_irq(arg_vm: sel4cp_id, arg_irq: u16, arg_priority: u8, arg_group: u8, arg_index: u8) callconv(.C) void {
+pub fn microkit_arm_vcpu_inject_irq(arg_vm: microkit_id, arg_irq: u16, arg_priority: u8, arg_group: u8, arg_index: u8) callconv(.C) void {
     var vm = arg_vm;
     var irq = arg_irq;
     var priority = arg_priority;
     var group = arg_group;
     var index = arg_index;
     var err: seL4_Error = undefined;
-    err = seL4_ARM_VCPU_InjectIRQ(@as(seL4_ARM_VCPU, @bitCast(@as(c_ulong, @as(sel4cp_id, @bitCast(@as(c_int, 330))) +% vm))), irq, priority, group, index);
+    err = seL4_ARM_VCPU_InjectIRQ(@as(seL4_ARM_VCPU, @bitCast(@as(c_ulong, @as(microkit_id, @bitCast(@as(c_int, 330))) +% vm))), irq, priority, group, index);
     if (err != @as(c_uint, @bitCast(seL4_NoError))) {
-        sel4cp_dbg_puts("sel4cp_arm_vcpu_inject_irq: error injecting IRQ\n");
-        sel4cp_internal_crash(err);
+        microkit_dbg_puts("microkit_arm_vcpu_inject_irq: error injecting IRQ\n");
+        microkit_internal_crash(err);
     }
 }
-pub fn sel4cp_arm_vcpu_ack_vppi(arg_vm: sel4cp_id, arg_irq: u64) callconv(.C) void {
+pub fn microkit_arm_vcpu_ack_vppi(arg_vm: microkit_id, arg_irq: u64) callconv(.C) void {
     var vm = arg_vm;
     var irq = arg_irq;
     var err: seL4_Error = undefined;
-    err = seL4_ARM_VCPU_AckVPPI(@as(seL4_ARM_VCPU, @bitCast(@as(c_ulong, @as(sel4cp_id, @bitCast(@as(c_int, 330))) +% vm))), irq);
+    err = seL4_ARM_VCPU_AckVPPI(@as(seL4_ARM_VCPU, @bitCast(@as(c_ulong, @as(microkit_id, @bitCast(@as(c_int, 330))) +% vm))), irq);
     if (err != @as(c_uint, @bitCast(seL4_NoError))) {
-        sel4cp_dbg_puts("sel4cp_arm_vcpu_ack_vppi: error acking VPPI\n");
-        sel4cp_internal_crash(err);
+        microkit_dbg_puts("microkit_arm_vcpu_ack_vppi: error acking VPPI\n");
+        microkit_internal_crash(err);
     }
 }
-pub fn sel4cp_arm_vcpu_read_reg(arg_vm: sel4cp_id, arg_reg: u64) callconv(.C) seL4_Word {
+pub fn microkit_arm_vcpu_read_reg(arg_vm: microkit_id, arg_reg: u64) callconv(.C) seL4_Word {
     var vm = arg_vm;
     var reg = arg_reg;
     var ret: seL4_ARM_VCPU_ReadRegs_t = undefined;
-    ret = seL4_ARM_VCPU_ReadRegs(@as(seL4_ARM_VCPU, @bitCast(@as(c_ulong, @as(sel4cp_id, @bitCast(@as(c_int, 330))) +% vm))), reg);
+    ret = seL4_ARM_VCPU_ReadRegs(@as(seL4_ARM_VCPU, @bitCast(@as(c_ulong, @as(microkit_id, @bitCast(@as(c_int, 330))) +% vm))), reg);
     if (ret.@"error" != seL4_NoError) {
-        sel4cp_dbg_puts("sel4cp_arm_vcpu_read_reg: error reading VCPU register\n");
-        sel4cp_internal_crash(@as(c_uint, @bitCast(ret.@"error")));
+        microkit_dbg_puts("microkit_arm_vcpu_read_reg: error reading VCPU register\n");
+        microkit_internal_crash(@as(c_uint, @bitCast(ret.@"error")));
     }
     return ret.value;
 }
-pub fn sel4cp_arm_vcpu_write_reg(arg_vm: sel4cp_id, arg_reg: u64, arg_value: u64) callconv(.C) void {
+pub fn microkit_arm_vcpu_write_reg(arg_vm: microkit_id, arg_reg: u64, arg_value: u64) callconv(.C) void {
     var vm = arg_vm;
     var reg = arg_reg;
     var value = arg_value;
     var err: seL4_Error = undefined;
-    err = seL4_ARM_VCPU_WriteRegs(@as(seL4_ARM_VCPU, @bitCast(@as(c_ulong, @as(sel4cp_id, @bitCast(@as(c_int, 330))) +% vm))), reg, value);
+    err = seL4_ARM_VCPU_WriteRegs(@as(seL4_ARM_VCPU, @bitCast(@as(c_ulong, @as(microkit_id, @bitCast(@as(c_int, 330))) +% vm))), reg, value);
     if (err != @as(c_uint, @bitCast(seL4_NoError))) {
-        sel4cp_dbg_puts("sel4cp_arm_vcpu_write_reg: error VPPI\n");
-        sel4cp_internal_crash(err);
+        microkit_dbg_puts("microkit_arm_vcpu_write_reg: error VPPI\n");
+        microkit_internal_crash(err);
     }
 }
 pub const __INTMAX_C_SUFFIX__ = @compileError("unable to translate macro: undefined identifier `L`"); // (no file):80:9
@@ -7203,7 +7203,7 @@ pub const BASE_IRQ_CAP = @as(c_int, 138);
 pub const BASE_TCB_CAP = @as(c_int, 202);
 pub const BASE_VM_TCB_CAP = @as(c_int, 266);
 pub const BASE_VCPU_CAP = @as(c_int, 330);
-pub const SEL4CP_MAX_CHANNELS = @as(c_int, 63);
+pub const MICROKIT_MAX_CHANNELS = @as(c_int, 63);
 pub const seL4_UserContext_ = struct_seL4_UserContext_;
 pub const seL4_Fault = struct_seL4_Fault;
 pub const seL4_Fault_tag = enum_seL4_Fault_tag;
diff --git a/examples/zig/src/vmm.zig b/examples/zig/src/vmm.zig
index a13e65bc..af4aff8d 100644
--- a/examples/zig/src/vmm.zig
+++ b/examples/zig/src/vmm.zig
@@ -9,7 +9,7 @@ const c = @cImport({
     @cInclude("vcpu.h");
     @cInclude("tcb.h");
 });
-const sel4cp = @import("libsel4cp.zig");
+const microkit = @import("libmicrokit.zig");
 
 const GUEST_BOOT_VCPU_ID = 0;
 const GUEST_RAM_VADDR: usize = 0x40000000;
@@ -37,7 +37,7 @@ const LinuxKernelImage = extern struct {
 // ability to provide your own function to ouput the characters. This is
 // extremely useful for us! Without changing the standard library or bringing
 // in a 3rd party library, in a couple of lines of code we can get formatted
-// printing functionality that ends up calling to sel4cp_dbg_puts which then
+// printing functionality that ends up calling to microkit_dbg_puts which then
 // outputs to the platform's serial connection.
 //
 // In a production system you might want to instead hook up the logger to a
@@ -48,7 +48,7 @@ const log = struct {
     const debug_uart = Writer { .context = 0 };
 
     fn debug_uart_put_str(_: u32, str: []const u8) !usize {
-        sel4cp.sel4cp_dbg_puts(@ptrCast(str));
+        microkit.microkit_dbg_puts(@ptrCast(str));
         return str.len;
     }
 
@@ -61,17 +61,17 @@ const log = struct {
     }
 };
 
-const SERIAL_IRQ_CH: sel4cp.sel4cp_channel = 1;
+const SERIAL_IRQ_CH: microkit.microkit_channel = 1;
 const SERIAL_IRQ: i32 = 79;
 
 fn serial_ack(_: usize, irq: c_int, _: ?*anyopaque) callconv(.C) void {
     // Nothing else needs to be done other than acking the IRQ.
-    sel4cp.sel4cp_irq_ack(@intCast(irq));
+    microkit.microkit_irq_ack(@intCast(irq));
 }
 
 export fn init() callconv(.C) void {
     // Initialise the VMM, the VCPU(s), and start the guest
-    log.info("starting \"{s}\"\n", .{ sel4cp.sel4cp_name });
+    log.info("starting \"{s}\"\n", .{ microkit.microkit_name });
     // Place all the binaries in the right locations before starting the guest
     // @ivanv: should all the vmm functions be prefixed with "vmm_"?
     // var linux_kernel_image: *LinuxKernelImage = @alignCast(@constCast(@ptrCast(guest_kernel_image)));
@@ -102,13 +102,13 @@ export fn init() callconv(.C) void {
     // actually get the interrupt. This should be avoided by making the VGIC driver more stable.
     success = c.virq_register(GUEST_BOOT_VCPU_ID, SERIAL_IRQ, &serial_ack, null);
     // Just in case there is already an interrupt available to handle, we ack it here.
-    sel4cp.sel4cp_irq_ack(SERIAL_IRQ_CH);
+    microkit.microkit_irq_ack(SERIAL_IRQ_CH);
     // Finally start the guest
     success = c.guest_start(GUEST_BOOT_VCPU_ID, kernel_pc, GUEST_DTB_VADDR, GUEST_INIT_RAM_DISK_VADDR);
     std.debug.assert(success);
 }
 
-export fn notified(ch: sel4cp.sel4cp_channel) callconv(.C) void {
+export fn notified(ch: microkit.microkit_channel) callconv(.C) void {
     switch (ch) {
         SERIAL_IRQ_CH => {
             const success = c.virq_inject(GUEST_BOOT_VCPU_ID, SERIAL_IRQ);
@@ -129,26 +129,26 @@ extern fn fault_handle_vcpu_exception(vcpu_id: usize) callconv(.C) bool;
 extern fn fault_handle_vppi_event(vcpu_id: usize) callconv(.C) bool;
 extern fn fault_to_string(fault_label: usize) callconv(.C) [*c]u8;
 
-export fn fault(id: sel4cp.sel4cp_id, msginfo: sel4cp.sel4cp_msginfo) callconv(.C) void {
+export fn fault(id: microkit.microkit_id, msginfo: microkit.microkit_msginfo) callconv(.C) void {
     if (id != GUEST_BOOT_VCPU_ID) {
         log.err("Unexpected faulting PD/VM with ID {}\n", .{ id });
         return;
     }
     // This is the primary fault handler for the guest, all faults that come
     // from seL4 regarding the guest will need to be handled here.
-    const label = sel4cp.sel4cp_msginfo_get_label(msginfo);
+    const label = microkit.microkit_msginfo_get_label(msginfo);
     log.info("fault label: {}", .{ label });
     const success = switch (label) {
-        sel4cp.seL4_Fault_VMFault => fault_handle_vm_exception(id),
-        sel4cp.seL4_Fault_UnknownSyscall => fault_handle_unknown_syscall(id),
-        sel4cp.seL4_Fault_UserException => fault_handle_user_exception(id),
-        sel4cp.seL4_Fault_VGICMaintenance => fault_handle_vgic_maintenance(id),
-        sel4cp.seL4_Fault_VCPUFault => fault_handle_vcpu_exception(id),
-        sel4cp.seL4_Fault_VPPIEvent => fault_handle_vppi_event(id),
+        microkit.seL4_Fault_VMFault => fault_handle_vm_exception(id),
+        microkit.seL4_Fault_UnknownSyscall => fault_handle_unknown_syscall(id),
+        microkit.seL4_Fault_UserException => fault_handle_user_exception(id),
+        microkit.seL4_Fault_VGICMaintenance => fault_handle_vgic_maintenance(id),
+        microkit.seL4_Fault_VCPUFault => fault_handle_vcpu_exception(id),
+        microkit.seL4_Fault_VPPIEvent => fault_handle_vppi_event(id),
         else => {
             // We have reached a genuinely unexpected case, stop the guest.
             log.err("unknown fault label {x}, stopping guest with ID {x}", .{ label, id });
-            sel4cp.sel4cp_vm_stop(id);
+            microkit.microkit_vm_stop(id);
             // Dump the TCB and vCPU registers to hopefully get information as
             // to what has gone wrong.
             c.tcb_print_regs(id);
@@ -159,7 +159,7 @@ export fn fault(id: sel4cp.sel4cp_id, msginfo: sel4cp.sel4cp_msginfo) callconv(.
 
     if (success) {
         // Now that we have handled the fault, we reply to it so that the guest can resume execution.
-        sel4cp.sel4cp_fault_reply(sel4cp.sel4cp_msginfo_new(0, 0));
+        microkit.microkit_fault_reply(microkit.microkit_msginfo_new(0, 0));
     } else {
         log.err("Failed to handle {s} fault\n", .{ fault_to_string(label) });
     }
diff --git a/src/arch/aarch64/fault.c b/src/arch/aarch64/fault.c
index 92c001a2..582e4e20 100644
--- a/src/arch/aarch64/fault.c
+++ b/src/arch/aarch64/fault.c
@@ -212,7 +212,7 @@ bool fault_advance(size_t vcpu_id, seL4_UserContext *regs, uint64_t addr, uint64
 
 bool fault_handle_vcpu_exception(size_t vcpu_id)
 {
-    uint32_t hsr = sel4cp_mr_get(seL4_VCPUFault_HSR);
+    uint32_t hsr = microkit_mr_get(seL4_VCPUFault_HSR);
     uint64_t hsr_ec_class = HSR_EXCEPTION_CLASS(hsr);
     switch (hsr_ec_class) {
         case HSR_SMC_64_EXCEPTION:
@@ -228,7 +228,7 @@ bool fault_handle_vcpu_exception(size_t vcpu_id)
 
 bool fault_handle_vppi_event(size_t vcpu_id)
 {
-    uint64_t ppi_irq = sel4cp_mr_get(seL4_VPPIEvent_IRQ);
+    uint64_t ppi_irq = microkit_mr_get(seL4_VPPIEvent_IRQ);
     // We directly inject the interrupt assuming it has been previously registered.
     // If not the interrupt will dropped by the VM.
     bool success = vgic_inject_irq(vcpu_id, ppi_irq);
@@ -236,7 +236,7 @@ bool fault_handle_vppi_event(size_t vcpu_id)
         // @ivanv, make a note that when having a lot of printing on it can cause this error
         LOG_VMM_ERR("VPPI IRQ %lu dropped on vCPU %d\n", ppi_irq, vcpu_id);
         // Acknowledge to unmask it as our guest will not use the interrupt
-        sel4cp_arm_vcpu_ack_vppi(vcpu_id, ppi_irq);
+        microkit_arm_vcpu_ack_vppi(vcpu_id, ppi_irq);
     }
 
     return true;
@@ -245,8 +245,8 @@ bool fault_handle_vppi_event(size_t vcpu_id)
 bool fault_handle_user_exception(size_t vcpu_id)
 {
     // @ivanv: print out VM name/vCPU id when we have multiple VMs
-    size_t fault_ip = sel4cp_mr_get(seL4_UserException_FaultIP);
-    size_t number = sel4cp_mr_get(seL4_UserException_Number);
+    size_t fault_ip = microkit_mr_get(seL4_UserException_FaultIP);
+    size_t number = microkit_mr_get(seL4_UserException_Number);
     LOG_VMM_ERR("Invalid instruction fault at IP: 0x%lx, number: 0x%lx", fault_ip, number);
     /* All we do is dump the TCB registers. */
     tcb_print_regs(vcpu_id);
@@ -261,8 +261,8 @@ bool fault_handle_user_exception(size_t vcpu_id)
 bool fault_handle_unknown_syscall(size_t vcpu_id)
 {
     // @ivanv: should print out the name of the VM the fault came from.
-    size_t syscall = sel4cp_mr_get(seL4_UnknownSyscall_Syscall);
-    size_t fault_ip = sel4cp_mr_get(seL4_UnknownSyscall_FaultIP);
+    size_t syscall = microkit_mr_get(seL4_UnknownSyscall_Syscall);
+    size_t fault_ip = microkit_mr_get(seL4_UnknownSyscall_FaultIP);
 
     LOG_VMM("Received syscall 0x%lx\n", syscall);
     switch (syscall) {
@@ -345,8 +345,8 @@ static bool fault_handle_registered_vm_exceptions(size_t vcpu_id, uintptr_t addr
 
 bool fault_handle_vm_exception(size_t vcpu_id)
 {
-    uintptr_t addr = sel4cp_mr_get(seL4_VMFault_Addr);
-    size_t fsr = sel4cp_mr_get(seL4_VMFault_FSR);
+    uintptr_t addr = microkit_mr_get(seL4_VMFault_Addr);
+    size_t fsr = microkit_mr_get(seL4_VMFault_FSR);
 
     seL4_UserContext regs;
     int err = seL4_TCB_ReadRegisters(BASE_VM_TCB_CAP + vcpu_id, false, 0, SEL4_USER_CONTEXT_SIZE, &regs);
@@ -370,7 +370,7 @@ bool fault_handle_vm_exception(size_t vcpu_id)
                  * Now we print out as much information relating to the fault as we can, hopefully
                  * the programmer can figure out what went wrong.
                  */
-                size_t ip = sel4cp_mr_get(seL4_VMFault_IP);
+                size_t ip = microkit_mr_get(seL4_VMFault_IP);
                 size_t is_prefetch = seL4_GetMR(seL4_VMFault_PrefetchFault);
                 bool is_write = fault_is_write(fsr);
                 LOG_VMM_ERR("unexpected memory fault on address: 0x%lx, FSR: 0x%lx, IP: 0x%lx, is_prefetch: %s, is_write: %s\n",
@@ -387,8 +387,8 @@ bool fault_handle_vm_exception(size_t vcpu_id)
     }
 }
 
-bool fault_handle(size_t vcpu_id, sel4cp_msginfo msginfo) {
-    size_t label = sel4cp_msginfo_get_label(msginfo);
+bool fault_handle(size_t vcpu_id, microkit_msginfo msginfo) {
+    size_t label = microkit_msginfo_get_label(msginfo);
     bool success = false;
     switch (label) {
         case seL4_Fault_VMFault:
@@ -412,7 +412,7 @@ bool fault_handle(size_t vcpu_id, sel4cp_msginfo msginfo) {
         default:
             /* We have reached a genuinely unexpected case, stop the guest. */
             LOG_VMM_ERR("unknown fault label 0x%lx, stopping guest with ID 0x%lx\n", label, vcpu_id);
-            sel4cp_vm_stop(vcpu_id);
+            microkit_vm_stop(vcpu_id);
             /* Dump the TCB and vCPU registers to hopefully get information as
              * to what has gone wrong. */
             tcb_print_regs(vcpu_id);
diff --git a/src/arch/aarch64/fault.h b/src/arch/aarch64/fault.h
index e956bf43..0c977587 100644
--- a/src/arch/aarch64/fault.h
+++ b/src/arch/aarch64/fault.h
@@ -8,10 +8,10 @@
 
 #include <stdbool.h>
 #include <stdint.h>
-#include <sel4cp.h>
+#include <microkit.h>
 
 /* Fault-handling functions */
-bool fault_handle(size_t vcpu_id, sel4cp_msginfo msginfo);
+bool fault_handle(size_t vcpu_id, microkit_msginfo msginfo);
 
 bool fault_handle_vcpu_exception(size_t vcpu_id);
 bool fault_handle_vppi_event(size_t vcpu_id);
diff --git a/src/arch/aarch64/psci.h b/src/arch/aarch64/psci.h
index dc12fe83..1f2cd805 100644
--- a/src/arch/aarch64/psci.h
+++ b/src/arch/aarch64/psci.h
@@ -8,7 +8,7 @@
 #pragma once
 
 #include <stddef.h>
-#include <sel4cp.h>
+#include <microkit.h>
 
 /* PSCI function IDs */
 typedef enum psci {
diff --git a/src/arch/aarch64/smc.h b/src/arch/aarch64/smc.h
index 1ba3c32a..bc5e6abf 100644
--- a/src/arch/aarch64/smc.h
+++ b/src/arch/aarch64/smc.h
@@ -10,7 +10,7 @@
 #include <stdbool.h>
 #include <stddef.h>
 #include <stdint.h>
-#include <sel4cp.h>
+#include <microkit.h>
 
 /* SMC vCPU fault handler */
 bool handle_smc(size_t vcpu_id, uint32_t hsr);
diff --git a/src/arch/aarch64/tcb.c b/src/arch/aarch64/tcb.c
index 477086f7..4ce3d5a4 100644
--- a/src/arch/aarch64/tcb.c
+++ b/src/arch/aarch64/tcb.c
@@ -4,7 +4,7 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 
-#include <sel4cp.h>
+#include <microkit.h>
 #include "util.h"
 #include "tcb.h"
 
diff --git a/src/arch/aarch64/vcpu.c b/src/arch/aarch64/vcpu.c
index bcae9f6e..108ad701 100644
--- a/src/arch/aarch64/vcpu.c
+++ b/src/arch/aarch64/vcpu.c
@@ -4,7 +4,7 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 
-#include <sel4cp.h>
+#include <microkit.h>
 #include "util.h"
 #include "vcpu.h"
 
@@ -29,75 +29,75 @@ void vcpu_reset(size_t vcpu_id) {
     // @ivanv this is an incredible amount of system calls
     // Reset registers
     // @ivanv: double check, shouldn't we be setting sctlr?
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_SCTLR, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_TTBR0, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_TTBR1, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_TCR, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_MAIR, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_AMAIR, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CIDR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_SCTLR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_TTBR0, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_TTBR1, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_TCR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_MAIR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_AMAIR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CIDR, 0);
     /* other system registers EL1 */
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_ACTLR, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CPACR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_ACTLR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CPACR, 0);
     /* exception handling registers EL1 */
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_AFSR0, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_AFSR1, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_ESR, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_FAR, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_ISR, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_VBAR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_AFSR0, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_AFSR1, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_ESR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_FAR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_ISR, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_VBAR, 0);
     /* thread pointer/ID registers EL0/EL1 */
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_TPIDR_EL1, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_TPIDR_EL1, 0);
 #if CONFIG_MAX_NUM_NODES > 1
     /* Virtualisation Multiprocessor ID Register */
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_VMPIDR_EL2, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_VMPIDR_EL2, 0);
 #endif /* CONFIG_MAX_NUM_NODES > 1 */
     /* general registers x0 to x30 have been saved by traps.S */
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_SP_EL1, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_ELR_EL1, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_SPSR_EL1, 0); // 32-bit
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_SP_EL1, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_ELR_EL1, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_SPSR_EL1, 0); // 32-bit
     /* generic timer registers, to be completed */
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CNTV_CTL, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CNTV_CVAL, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CNTVOFF, 0);
-    sel4cp_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CNTKCTL_EL1, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CNTV_CTL, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CNTV_CVAL, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CNTVOFF, 0);
+    microkit_arm_vcpu_write_reg(vcpu_id, seL4_VCPUReg_CNTKCTL_EL1, 0);
 }
 
 void vcpu_print_regs(size_t vcpu_id) {
     // @ivanv this is an incredible amount of system calls
     LOG_VMM("dumping VCPU (ID 0x%lx) registers:\n", vcpu_id);
     /* VM control registers EL1 */
-    printf("    sctlr: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_SCTLR));
-    printf("    ttbr0: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_TTBR0));
-    printf("    ttbr1: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_TTBR1));
-    printf("    tcr: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_TCR));
-    printf("    mair: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_MAIR));
-    printf("    amair: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_AMAIR));
-    printf("    cidr: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CIDR));
+    printf("    sctlr: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_SCTLR));
+    printf("    ttbr0: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_TTBR0));
+    printf("    ttbr1: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_TTBR1));
+    printf("    tcr: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_TCR));
+    printf("    mair: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_MAIR));
+    printf("    amair: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_AMAIR));
+    printf("    cidr: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CIDR));
     /* other system registers EL1 */
-    printf("    actlr: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_ACTLR));
-    printf("    cpacr: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CPACR));
+    printf("    actlr: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_ACTLR));
+    printf("    cpacr: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CPACR));
     /* exception handling registers EL1 */
-    printf("    afsr0: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_AFSR0));
-    printf("    afsr1: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_AFSR1));
-    printf("    esr: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_ESR));
-    printf("    far: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_FAR));
-    printf("    isr: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_ISR));
-    printf("    vbar: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_VBAR));
+    printf("    afsr0: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_AFSR0));
+    printf("    afsr1: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_AFSR1));
+    printf("    esr: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_ESR));
+    printf("    far: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_FAR));
+    printf("    isr: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_ISR));
+    printf("    vbar: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_VBAR));
     /* thread pointer/ID registers EL0/EL1 */
-    printf("    tpidr_el1: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_TPIDR_EL1));
+    printf("    tpidr_el1: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_TPIDR_EL1));
     // @ivanv: I think thins might not be the correct ifdef
 #if CONFIG_MAX_NUM_NODES > 1
     /* Virtualisation Multiprocessor ID Register */
-    printf("    vmpidr_el2: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_VMPIDR_EL2));
+    printf("    vmpidr_el2: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_VMPIDR_EL2));
 #endif
     /* general registers x0 to x30 have been saved by traps.S */
-    printf("    sp_el1: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_SP_EL1));
-    printf("    elr_el1: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_ELR_EL1));
-    printf("    spsr_el1: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_SPSR_EL1)); // 32-bit // @ivanv what
+    printf("    sp_el1: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_SP_EL1));
+    printf("    elr_el1: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_ELR_EL1));
+    printf("    spsr_el1: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_SPSR_EL1)); // 32-bit // @ivanv what
     /* generic timer registers, to be completed */
-    printf("    cntv_ctl: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CNTV_CTL));
-    printf("    cntv_cval: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CNTV_CVAL));
-    printf("    cntvoff: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CNTVOFF));
-    printf("    cntkctl_el1: 0x%016lx\n", sel4cp_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CNTKCTL_EL1));
+    printf("    cntv_ctl: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CNTV_CTL));
+    printf("    cntv_cval: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CNTV_CVAL));
+    printf("    cntvoff: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CNTVOFF));
+    printf("    cntkctl_el1: 0x%016lx\n", microkit_arm_vcpu_read_reg(vcpu_id, seL4_VCPUReg_CNTKCTL_EL1));
 }
diff --git a/src/arch/aarch64/vgic/vgic.c b/src/arch/aarch64/vgic/vgic.c
index 31d50f3b..50776c98 100644
--- a/src/arch/aarch64/vgic/vgic.c
+++ b/src/arch/aarch64/vgic/vgic.c
@@ -4,7 +4,7 @@
  *
  * SPDX-License-Identifier: BSD-2-Clause
  */
-#include <sel4cp.h>
+#include <microkit.h>
 #include "vgic.h"
 #include "virq.h"
 #include "fault.h"
@@ -27,7 +27,7 @@ bool fault_handle_vgic_maintenance(size_t vcpu_id)
 {
     // @ivanv: reivist, also inconsistency between int and bool
     bool success = true;
-    int idx = sel4cp_mr_get(seL4_VGICMaintenance_IDX);
+    int idx = microkit_mr_get(seL4_VGICMaintenance_IDX);
     /* Currently not handling spurious IRQs */
     // @ivanv: wtf, this comment seems irrelevant to the code.
     assert(idx >= 0);
diff --git a/src/arch/aarch64/vgic/vgic.h b/src/arch/aarch64/vgic/vgic.h
index 68876637..87c5da1a 100644
--- a/src/arch/aarch64/vgic/vgic.h
+++ b/src/arch/aarch64/vgic/vgic.h
@@ -5,7 +5,7 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 
-#include <sel4cp.h>
+#include <microkit.h>
 #include <stdbool.h>
 #include <stdint.h>
 #include "../../../virq.h"
diff --git a/src/arch/aarch64/vgic/vgic_v2.c b/src/arch/aarch64/vgic/vgic_v2.c
index d5cab840..f777e5c1 100644
--- a/src/arch/aarch64/vgic/vgic_v2.c
+++ b/src/arch/aarch64/vgic/vgic_v2.c
@@ -41,7 +41,7 @@
  */
 
 #include <stdint.h>
-#include <sel4cp.h>
+#include <microkit.h>
 
 #include "vgic.h"
 #include "vgic_v2.h"
diff --git a/src/arch/aarch64/vgic/virq.h b/src/arch/aarch64/vgic/virq.h
index 99aa0ed4..3d68df8d 100644
--- a/src/arch/aarch64/vgic/virq.h
+++ b/src/arch/aarch64/vgic/virq.h
@@ -206,7 +206,7 @@ static inline bool vgic_vcpu_load_list_reg(vgic_t *vgic, size_t vcpu_id, int idx
     assert(vgic_vcpu);
     assert((idx >= 0) && (idx < ARRAY_SIZE(vgic_vcpu->lr_shadow)));
     // @ivanv: why is the priority 0?
-    sel4cp_arm_vcpu_inject_irq(vcpu_id, virq->virq, 0, group, idx);
+    microkit_arm_vcpu_inject_irq(vcpu_id, virq->virq, 0, group, idx);
     vgic_vcpu->lr_shadow[idx] = *virq;
 
     return true;
diff --git a/src/arch/aarch64/virq.c b/src/arch/aarch64/virq.c
index 704a3b60..eac507f3 100644
--- a/src/arch/aarch64/virq.c
+++ b/src/arch/aarch64/virq.c
@@ -1,4 +1,4 @@
-#include <sel4cp.h>
+#include <microkit.h>
 #include "vgic/vgic.h"
 #include "../../util/util.h"
 #include "../../virq.h"
@@ -9,7 +9,7 @@
 
 static void vppi_event_ack(size_t vcpu_id, int irq, void *cookie)
 {
-    sel4cp_arm_vcpu_ack_vppi(vcpu_id, irq);
+    microkit_arm_vcpu_ack_vppi(vcpu_id, irq);
 }
 
 static void sgi_ack(size_t vcpu_id, int irq, void *cookie) {}
diff --git a/src/guest.c b/src/guest.c
index b22a1d66..e0d66cc7 100644
--- a/src/guest.c
+++ b/src/guest.c
@@ -1,4 +1,4 @@
-#include <sel4cp.h>
+#include <microkit.h>
 #include "util/util.h"
 #include "vcpu.h"
 #include "guest.h"
@@ -30,21 +30,21 @@ bool guest_start(size_t boot_vcpu_id, uintptr_t kernel_pc, uintptr_t dtb, uintpt
     LOG_VMM("starting guest at 0x%lx, DTB at 0x%lx, initial RAM disk at 0x%lx\n",
         regs.pc, regs.x0, initrd);
     /* Restart the boot vCPU to the program counter of the TCB associated with it */
-    sel4cp_vm_restart(boot_vcpu_id, regs.pc);
+    microkit_vm_restart(boot_vcpu_id, regs.pc);
 
     return true;
 }
 
 void guest_stop(size_t boot_vcpu_id) {
     LOG_VMM("Stopping guest\n");
-    sel4cp_vm_stop(boot_vcpu_id);
+    microkit_vm_stop(boot_vcpu_id);
     LOG_VMM("Stopped guest\n");
 }
 
 bool guest_restart(size_t boot_vcpu_id, uintptr_t guest_ram_vaddr, size_t guest_ram_size) {
     LOG_VMM("Attempting to restart guest\n");
     // First, stop the guest
-    sel4cp_vm_stop(boot_vcpu_id);
+    microkit_vm_stop(boot_vcpu_id);
     LOG_VMM("Stopped guest\n");
     // Then, we need to clear all of RAM
     LOG_VMM("Clearing guest RAM\n");
diff --git a/src/util/util.c b/src/util/util.c
index fc282716..d343ded8 100644
--- a/src/util/util.c
+++ b/src/util/util.c
@@ -11,5 +11,5 @@
    in the VMM. */
 void _putchar(char character)
 {
-    sel4cp_dbg_putc(character);
+    microkit_dbg_putc(character);
 }
diff --git a/src/util/util.h b/src/util/util.h
index 04ff4be8..f473b73e 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -8,7 +8,7 @@
 #pragma once
 
 #include <stdint.h>
-#include <sel4cp.h>
+#include <microkit.h>
 #include "printf.h"
 
 // @ivanv: these are here for convience, should not be here though
@@ -30,8 +30,8 @@
 #define static_assert _Static_assert
 #endif
 
-#define LOG_VMM(...) do{ printf("%s|INFO: ", sel4cp_name); printf(__VA_ARGS__); }while(0)
-#define LOG_VMM_ERR(...) do{ printf("%s|ERROR: ", sel4cp_name); printf(__VA_ARGS__); }while(0)
+#define LOG_VMM(...) do{ printf("%s|INFO: ", microkit_name); printf(__VA_ARGS__); }while(0)
+#define LOG_VMM_ERR(...) do{ printf("%s|ERROR: ", microkit_name); printf(__VA_ARGS__); }while(0)
 
 static void *memcpy(void *restrict dest, const void *restrict src, size_t n)
 {