diff --git a/hacking/nix/scope/default.nix b/hacking/nix/scope/default.nix
index 53dda5e00..f98cc4424 100644
--- a/hacking/nix/scope/default.nix
+++ b/hacking/nix/scope/default.nix
@@ -34,7 +34,6 @@ let
   fenixRev = "9af557bccdfa8fb6a425661c33dbae46afef0afa";
   fenixSource = fetchTarball "https://github.com/nix-community/fenix/archive/${fenixRev}.tar.gz";
   fenix = import fenixSource {};
-
 in
 
 superCallPackage ../rust-utils {} self //
@@ -228,7 +227,11 @@ superCallPackage ../rust-utils {} self //
 
   ### worlds
 
-  mkWorld = unelaboratedWorldConfig: lib.makeScope newScope (callPackage ./world {} unelaboratedWorldConfig);
+  overrideWorldScope = self: super: {};
+
+  mkWorldFrom = newScope: unelaboratedWorldConfig: (lib.makeScope newScope (callPackage ./world {} unelaboratedWorldConfig)).overrideScope' overrideWorldScope;
+
+  mkWorld = mkWorldFrom newScope;
 
   worlds = (callPackage ./worlds.nix {})."${seL4Arch}";
 
diff --git a/hacking/nix/scope/microkit/default.nix b/hacking/nix/scope/microkit/default.nix
index 2f3f9859e..a273b91a0 100644
--- a/hacking/nix/scope/microkit/default.nix
+++ b/hacking/nix/scope/microkit/default.nix
@@ -44,13 +44,6 @@ let
     '';
   };
 
-  vendoredLockfile = vendorLockfile {
-    inherit rustToolchain;
-    lockfile = microkitSource + "/tool/microkit/Cargo.lock";
-  };
-
-  cargoConfigFile = toTOMLFile "config.toml" vendoredLockfile.configFragment;
-
   sdk = stdenv.mkDerivation {
     name = "microkit-sdk-without-tool";
 
@@ -90,100 +83,87 @@ let
     '';
   };
 
-  tool = stdenv.mkDerivation {
-    name = "microkit-sdk-just-tool";
+  tool =
+    let
+      vendoredLockfile = vendorLockfile {
+        inherit rustToolchain;
+        lockfile = microkitSource + "/tool/microkit/Cargo.lock";
+      };
 
-    src = lib.cleanSource (microkitSource + "/tool/microkit");
+      cargoConfigFile = toTOMLFile "config.toml" vendoredLockfile.configFragment;
 
-    nativeBuildInputs = [
-      rustToolchain
-    ];
+    in
+      stdenv.mkDerivation {
+        name = "microkit-sdk-just-tool";
 
-    depsBuildBuild = [
-      buildPackages.stdenv.cc
-    ];
+        src = lib.cleanSource (microkitSource + "/tool/microkit");
 
-    dontInstall = true;
-    dontFixup = true;
+        nativeBuildInputs = [
+          rustToolchain
+        ];
 
-    configurePhase = ''
-      d=.cargo
-      mkdir $d
-      cp ${cargoConfigFile} $d/config.toml
-    '';
+        depsBuildBuild = [
+          buildPackages.stdenv.cc
+        ];
 
-    buildPhase = ''
-      cargo build -Z unstable-options --frozen --out-dir $out/bin
-    '';
-  };
+        dontInstall = true;
+        dontFixup = true;
 
-  mkSystem = { searchPath, systemXML }:
-    lib.fix (self: runCommand "system" {
-      MICROKIT_SDK = sdk;
-      MICROKIT_BOARD = board;
-      MICROKIT_CONFIG = config;
+        configurePhase = ''
+          d=.cargo
+          mkdir $d
+          cp ${cargoConfigFile} $d/config.toml
+        '';
 
-      nativeBuildInputs = [
-        python3Packages.sel4-deps
-      ];
+        buildPhase = ''
+          cargo build -Z unstable-options --frozen --config ${cargoConfigFile} --out-dir $out/bin
+        '';
+      };
 
-      passthru = rec {
+  mkLoader =
+    { systemXML
+    , searchPath
+    }:
+    lib.fix (self: runCommand "system" {
+      passthru = {
         inherit systemXML;
-        loader = "${self}/loader.img";
-        links = [
-          { name = "pds"; path = searchPath; }
-          { name = "loader.elf"; path = loader; }
-          { name = "report.txt"; path = "${self}/report.txt"; }
-          { name = "sdk/monitor.elf"; path = "${sdk}/board/${board}/${config}/elf/monitor.elf"; }
-          { name = "sdk/loader.elf"; path = "${sdk}/board/${board}/${config}/elf/loader.elf"; }
-        ];
+        image = "${self}/loader.img";
       };
     } ''
       mkdir $out
-      ${tool}/bin/microkit ${systemXML} \
-        --search-path ${searchPath} \
-        --board $MICROKIT_BOARD \
-        --config $MICROKIT_CONFIG \
-        -o $out/loader.img \
-        -r $out/report.txt
+      MICROKIT_SDK=${sdk} \
+        ${tool}/bin/microkit ${systemXML} \
+          --search-path ${lib.concatStringsSep " " searchPath} \
+          --board ${board} \
+          --config ${config} \
+          -o $out/loader.img \
+          -r $out/report.txt
     '');
 
-  exampleSource = microkitSource + "/example/${board}/hello";
-
-  examplePDs = stdenv.mkDerivation {
-    name = "example";
-
-    src = exampleSource;
-
-    MICROKIT_SDK = sdk;
-    MICROKIT_BOARD = board;
-    MICROKIT_CONFIG = config;
-
-    MICROKIT_TOOL = "${tool}/bin/microkit";
-
-    dontConfigure = true;
-    dontFixup = true;
-
-    buildPhase = ''
-      mkdir build
-      make BUILD_DIR=build
-    '';
-
-    installPhase = ''
-      mkdir $out
-      mv build/hello.elf $out
-    '';
-  };
-
-  example = assert board == "qemu_virt_aarch64"; mkSystem {
-    searchPath = examplePDs;
-    systemXML = exampleSource + "/hello.system";
-  };
+  mkSystem =
+    { systemXML
+    , searchPath
+    , extraDebuggingLinks ? []
+    , passthru ? {}
+    }:
+    let
+      loader = mkLoader { inherit systemXML searchPath; };
+    in {
+      inherit loader;
+      loaderImage = loader.image;
+      debuggingLinks = [
+        { name = "loader.img"; path = loader; }
+        { name = "report.txt"; path = "${loader}/report.txt"; }
+        { name = "sdk/elf"; path = "${sdk}/board/${board}/${config}/elf"; }
+        { name = "sel4-symbolize-backtrace";
+          path = "${buildPackages.this.sel4-backtrace-cli}/bin/sel4-symbolize-backtrace";
+        }
+      ] ++ extraDebuggingLinks;
+    } // passthru;
 
 in rec {
   inherit
     sdk tool
     mkSystem
-    example
   ;
 }
diff --git a/hacking/nix/scope/plat-utils/default.nix b/hacking/nix/scope/plat-utils/default.nix
index 65d01c6d5..618838992 100644
--- a/hacking/nix/scope/plat-utils/default.nix
+++ b/hacking/nix/scope/plat-utils/default.nix
@@ -10,7 +10,7 @@
   qemu = callPackage ./qemu {};
   rpi4 = callPackage ./rpi4 {};
 
-  composeInstanceForPlatformAttrs = a: b: {
+  composePlatformExtensions = a: b: {
     attrs = a.attrs // b.attrs;
     links = a.links ++ b.links;
   };
diff --git a/hacking/nix/scope/plat-utils/qemu/default.nix b/hacking/nix/scope/plat-utils/qemu/default.nix
index 7d59becce..281c1ca15 100644
--- a/hacking/nix/scope/plat-utils/qemu/default.nix
+++ b/hacking/nix/scope/plat-utils/qemu/default.nix
@@ -22,7 +22,7 @@ let
 
 in rec {
 
-  automateQemuSimple = { simulate, timeout }:
+  automateQEMUSimple = { simulate, timeout }:
     let
       py = buildPackages.python3.withPackages (pkgs: [
         pkgs.pexpect
@@ -35,24 +35,24 @@ in rec {
         ${py}/bin/python3 ${./automate_simple.py} --simulate ${simulate} --timeout ${toString timeout}
       '';
 
-  mkMkInstanceForPlatform =
-    { mkQemuCmd
-    , platformRequiresLoader ? true
+  mkMkPlatformSystemExtension =
+    { mkQEMUCmd
     }:
 
-    { rootTask ? null
-    , loader ? null
+    { worldConfig
+    , rootTaskImage ? null
+    , loaderImage ? null
+    , extraQEMUArgs ? []
     , canAutomateSimply ? false
     , simpleAutomationParams ? if canAutomateSimply then {} else null
-    , extraQemuArgs ? []
     }:
 
     let
-      qemuCmd = mkQemuCmd (if platformRequiresLoader then loader else rootTask);
+      qemuCmd = mkQEMUCmd (if worldConfig.platformRequiresLoader then loaderImage else rootTaskImage);
 
       simulate = writeScript "run.sh" ''
         #!${buildPackages.runtimeShell}
-        exec ${lib.concatStringsSep " " (qemuCmd ++ extraQemuArgs)} "$@"
+        exec ${lib.concatStringsSep " " (qemuCmd ++ extraQEMUArgs)} "$@"
       '';
 
       elaboratedSimpleAutomationParams =
@@ -63,7 +63,7 @@ in rec {
       automate =
         if elaboratedSimpleAutomationParams == null
         then null
-        else automateQemuSimple {
+        else automateQEMUSimple {
           inherit simulate;
           inherit (elaboratedSimpleAutomationParams) timeout;
         };
diff --git a/hacking/nix/scope/plat-utils/rpi4/default.nix b/hacking/nix/scope/plat-utils/rpi4/default.nix
index b7064d690..f92ecf129 100644
--- a/hacking/nix/scope/plat-utils/rpi4/default.nix
+++ b/hacking/nix/scope/plat-utils/rpi4/default.nix
@@ -39,28 +39,32 @@ let
   uBootBin = "${uBoot}/u-boot.bin";
 
   imageAddr = "0x30000000";
+  defaultBootCmd = "load mmc 0:1 ${imageAddr} /image.elf; bootelf -p ${imageAddr}";
 
-  uBootEnvTxt = writeText "uboot.env.txt" ''
+  uBootEnvTxt = { bootCmd }: writeText "uboot.env.txt" ''
     bootdelay=0
-    bootcmd=load mmc 0:1 ${imageAddr} /image.elf; bootelf -p ${imageAddr}"
+    bootcmd=${bootCmd}"
     autostart=1
   '';
 
-  uBootEnv = runCommand "uboot.env" {
-    nativeBuildInputs = [
-      ubootTools
-    ];
-  } ''
-    mkenvimage \
-      -s 0x4000 \
-      -o $out \
-      ${uBootEnvTxt}
-  '';
+  uBootEnv = { bootCmd }:
+    assert lib.stringLength bootCmd < 3 * 4096; # conservative
+    runCommand "uboot.env" {
+      nativeBuildInputs = [
+        ubootTools
+      ];
+    } ''
+      mkenvimage \
+        -s 0x4000 \
+        -o $out \
+        ${uBootEnvTxt { inherit bootCmd; }}
+    '';
 
   kernelFileName = "kernel${if hostPlatform.is32bit then "7l" else "8"}.img";
 
   mkBootLinks =
     { image ? null
+    , bootCmd ? defaultBootCmd
     , extraCommands ? ""
     }:
     runCommand "boot" {} ''
@@ -74,7 +78,7 @@ let
       rm $out/kernel*.img
       ln -s ${uBootBin} $out/${kernelFileName}
 
-      ln -s ${uBootEnv} $out/uboot.env
+      ln -s ${uBootEnv { inherit bootCmd; }} $out/uboot.env
 
       ${lib.optionalString (image != null) ''
         ln -s ${image} $out/image.elf
@@ -89,18 +93,21 @@ let
 
   defaultBootLinks = mkBootLinks {};
 
-  mkInstanceForPlatform =
-    { loader
-    , rootTask
+  mkPlatformSystemExtension =
+    { worldConfig
+    , loaderImage
+    , extraQEMUPlatformArgs ? {}
+    , bootLinksExtraCommands ? ""
     , simpleAutomationParams ? null # TODO
     }:
     let
       boot = mkBootLinks {
-        image = loader;
+        image = loaderImage;
+        extraCommands = bootLinksExtraCommands;
       };
       bootCopied = mkBootCopied boot;
-      qemu = platUtils.qemu.mkMkInstanceForPlatform {
-        mkQemuCmd = loader: [
+      qemu = platUtils.qemu.mkMkPlatformSystemExtension {
+        mkQEMUCmd = loader: [
           "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-${if hostPlatform.is32bit then "arm" else "aarch64"}"
             "-smp" "4"
             "-m" "size=2048"
@@ -110,10 +117,10 @@ let
             "-serial" "mon:stdio"
             "-kernel" loader
         ];
-      } {
-        inherit loader rootTask;
-      };
-    in platUtils.composeInstanceForPlatformAttrs qemu (rec {
+      } ({
+        inherit worldConfig loaderImage;
+      } // extraQEMUPlatformArgs);
+    in platUtils.composePlatformExtensions qemu (rec {
       attrs = {
         inherit boot bootCopied;
       };
@@ -129,6 +136,7 @@ in {
     firmware
     uBoot
     defaultBootLinks
-    mkInstanceForPlatform
+    mkBootLinks
+    mkPlatformSystemExtension
   ;
 }
diff --git a/hacking/nix/scope/world/capdl/dummy-capdl-spec.nix b/hacking/nix/scope/world/capdl/dummy-capdl-spec.nix
index b5f13a731..5ff69d71b 100644
--- a/hacking/nix/scope/world/capdl/dummy-capdl-spec.nix
+++ b/hacking/nix/scope/world/capdl/dummy-capdl-spec.nix
@@ -7,15 +7,13 @@
 { lib, emptyDirectory, linkFarm, writeText }:
 
 {
-  passthru = {
-    spec = writeText "x.cdl" ''
-      arch aarch64
+  cdl = writeText "x.cdl" ''
+    arch aarch64
 
-      objects {
-        foo = notification
-      }
-      caps {}
-    '';
-    fill = emptyDirectory;
-  };
+    objects {
+      foo = notification
+    }
+    caps {}
+  '';
+  fill = emptyDirectory;
 }
diff --git a/hacking/nix/scope/world/capdl/mk-capdl-initializer-with-spec.nix b/hacking/nix/scope/world/capdl/mk-capdl-initializer-with-spec.nix
index 1bd140237..27c6547e0 100644
--- a/hacking/nix/scope/world/capdl/mk-capdl-initializer-with-spec.nix
+++ b/hacking/nix/scope/world/capdl/mk-capdl-initializer-with-spec.nix
@@ -14,11 +14,11 @@
 , sel4-capdl-initializer
 }:
 
-{ spec, fill }:
+{ cdl, fill }:
 
 let
   json = serializeCapDLSpec {
-    inherit spec;
+    inherit cdl;
   };
 
 in lib.fix (self: runCommand "sel4-capdl-initializer-with-spec" {
@@ -28,7 +28,7 @@ in lib.fix (self: runCommand "sel4-capdl-initializer-with-spec" {
   ];
 
   passthru = {
-    inherit spec json fill;
+    inherit cdl json fill;
     elf = self;
     split = {
       full = sel4-capdl-initializer.elf;
diff --git a/hacking/nix/scope/world/capdl/mk-simple-composition-capdl-spec.nix b/hacking/nix/scope/world/capdl/mk-simple-composition-capdl-spec.nix
index b94824948..a98a7e73a 100644
--- a/hacking/nix/scope/world/capdl/mk-simple-composition-capdl-spec.nix
+++ b/hacking/nix/scope/world/capdl/mk-simple-composition-capdl-spec.nix
@@ -21,6 +21,7 @@
 , command ? "python3 ${script}"
 , computeUtCovers ? false
 , extraNativeBuildInputs ? []
+, extraPythonPath ? []
 }:
 
 let
@@ -59,14 +60,14 @@ lib.fix (self: runCommand "manifest" {
     pyyaml pyelftools pyfdt
   ]) ++ extraNativeBuildInputs;
 
-  PYTHONPATH_ = lib.concatStringsSep ":" [ capdlSimpleCompositionSrc capdlSrc ];
+  PYTHONPATH_ = lib.concatStringsSep ":" ([ capdlSimpleCompositionSrc capdlSrc ] ++ extraPythonPath);
 
   CONFIG = augmentedConfigJSON;
 
   passthru = {
     config = augmentedConfig;
-    cdl = {
-      spec = "${self}/spec.cdl";
+    specAttrs = {
+      cdl = "${self}/spec.cdl";
       fill = "${self}/links";
     };
   };
diff --git a/hacking/nix/scope/world/capdl/mk-small-capdl-initializer.nix b/hacking/nix/scope/world/capdl/mk-small-capdl-initializer.nix
index 2a61459be..4d14a1c40 100644
--- a/hacking/nix/scope/world/capdl/mk-small-capdl-initializer.nix
+++ b/hacking/nix/scope/world/capdl/mk-small-capdl-initializer.nix
@@ -14,11 +14,11 @@
 , mkSeL4RustTargetTriple
 }:
 
-{ spec, fill }:
+{ cdl, fill }:
 
 let
   json = serializeCapDLSpec {
-    inherit spec;
+    inherit cdl;
   };
 
 in mkTask {
@@ -48,7 +48,7 @@ in mkTask {
       CAPDL_EMBED_FRAMES = 1;
 
       passthru = (super.passthru or {}) // {
-        inherit spec json fill;
+        inherit cdl json fill;
       };
     });
   });
diff --git a/hacking/nix/scope/world/capdl/serialize-capdl-spec.nix b/hacking/nix/scope/world/capdl/serialize-capdl-spec.nix
index 2ba9c67a5..cca156df9 100644
--- a/hacking/nix/scope/world/capdl/serialize-capdl-spec.nix
+++ b/hacking/nix/scope/world/capdl/serialize-capdl-spec.nix
@@ -10,7 +10,7 @@
 , sources
 }:
 
-{ spec }:
+{ cdl }:
 
 let
   exe = "parse-capDL";
@@ -25,5 +25,5 @@ runCommand "spec.json" {
     # (import <nixpkgs> {}).stack
   ];
 } ''
-  ${exe} --object-sizes=${objectSizes} --json=$out ${spec}
+  ${exe} --object-sizes=${objectSizes} --json=$out ${cdl}
 ''
diff --git a/hacking/nix/scope/world/default.nix b/hacking/nix/scope/world/default.nix
index 2e02c12cc..2ac7008a1 100644
--- a/hacking/nix/scope/world/default.nix
+++ b/hacking/nix/scope/world/default.nix
@@ -6,7 +6,8 @@
 
 { lib
 , hostPlatform
-, runCommand, runCommandCC
+, buildPackages
+, runCommand, runCommandCC, linkFarm, writeScript
 , jq
 , symlinkToRegularFile
 , crateUtils
@@ -23,16 +24,18 @@ let
     , microkitConfig ? null
     , canSimulate ? false
     , platformRequiresLoader ? true
-    , mkInstanceForPlatform ? _: { attrs = {}; links = []; }
-    }:
-    { inherit
+    , mkPlatformSystemExtension ? _: { attrs = {}; links = []; }
+    , ...
+    } @ args:
+    args // {
+      inherit
         isMicrokit
         kernelConfig
         kernelLoaderConfig
         microkitConfig
         canSimulate
         platformRequiresLoader
-        mkInstanceForPlatform
+        mkPlatformSystemExtension
       ;
     };
 in
@@ -123,8 +126,26 @@ self: with self;
   mkSimpleCompositionCapDLSpec = callPackage ./capdl/mk-simple-composition-capdl-spec.nix {};
   mkCapDLInitializerWithSpec = callPackage ./capdl/mk-capdl-initializer-with-spec.nix {};
 
-  # mkCapDLInitializer = mkSmallCapDLInitializer;
-  mkCapDLInitializer = mkCapDLInitializerWithSpec;
+  mkCapDLInitializer =
+    { spec ? null
+    , specAttrs ? spec.specAttrs
+    , small ? false
+    , extraDebuggingLinks ? []
+    }:
+
+    lib.fix (self:
+      (if small then mkSmallCapDLInitializer else mkCapDLInitializerWithSpec) spec.specAttrs // {
+        inherit spec;
+        debuggingLinks = [
+          { name = "spec.cdl"; path = spec.specAttrs.cdl; }
+          { name = "fill"; path = spec.specAttrs.fill; }
+        ] ++ lib.optionals (spec != null) [
+          { name = "spec"; path = spec; }
+        ] ++ lib.optionals (!small) [
+          { name = "initializer.full.elf"; path = self.split.full; }
+        ] ++ extraDebuggingLinks;
+      }
+    );
 
   sel4-kernel-loader = callPackage ./sel4-kernel-loader.nix {
     inherit (worldConfig) kernelLoaderConfig;
@@ -134,9 +155,61 @@ self: with self;
     app = appELF;
   };
 
-  inherit (callPackage ./mk-instance.nix {})
-    mkInstance mkMicrokitInstance mkCapDLRootTask
-  ;
+  mkSystem =
+    { rootTask
+    , extraDebuggingLinks ? []
+    , passthru ? {}
+    }:
+    let
+      loader =
+        assert worldConfig.platformRequiresLoader;
+        mkSeL4KernelLoaderWithPayload {
+          appELF = rootTask.elf;
+        };
+
+      symbolizeRootTaskBacktrace = writeScript "x.sh" ''
+        #!${buildPackages.runtimeShell}
+        exec ${buildPackages.this.sel4-backtrace-cli}/bin/sel4-symbolize-backtrace -f ${rootTask.elf} "$@"
+      '';
+    in {
+      inherit loader rootTask;
+      rootTaskImage = rootTask.elf;
+      loaderImage = loader.elf;
+      debuggingLinks = [
+        { name = "kernel.elf"; path = "${seL4ForBoot}/bin/kernel.elf"; }
+        { name = "root-task.elf"; path = rootTask.elf; }
+        { name = "symbolize-root-task-backtrace"; path = symbolizeRootTaskBacktrace; }
+        { name = "sel4-symbolize-backtrace";
+          path = "${buildPackages.this.sel4-backtrace-cli}/bin/sel4-symbolize-backtrace";
+        }
+      ] ++ lib.optionals worldConfig.platformRequiresLoader [
+        { name = "loader.elf"; path = loader.elf; }
+        { name = "loader.debug.elf"; path = loader.split.full; }
+      ] ++ (rootTask.debuggingLinks or []) ++ extraDebuggingLinks;
+    } // passthru;
+
+  callPlatform =
+    { system
+    , extraPlatformArgs ? {}
+    , extraDebuggingLinks ? []
+    , ...
+    } @ args:
+    let
+      platformSystemExtension = worldConfig.mkPlatformSystemExtension ({
+        inherit worldConfig;
+      } // (
+        if worldConfig.platformRequiresLoader
+        then { inherit (system) loaderImage; }
+        else { inherit (system) rootTaskImage; }
+      ) // extraPlatformArgs);
+    in {
+      links = linkFarm "links" (
+        system.debuggingLinks ++ platformSystemExtension.links
+      );
+    }
+    // platformSystemExtension.attrs
+    // builtins.removeAttrs system [ "debuggingLinks" ]
+    // builtins.removeAttrs args [ "extraPlatformArgs" "extraDebuggingLinks" ];
 
   instances = callPackage ./instances {};
 
diff --git a/hacking/nix/scope/world/instances/default.nix b/hacking/nix/scope/world/instances/default.nix
index 2535d2875..02052531d 100644
--- a/hacking/nix/scope/world/instances/default.nix
+++ b/hacking/nix/scope/world/instances/default.nix
@@ -25,12 +25,10 @@
 , seL4Config
 , seL4RustEnvVars
 
+, callPlatform
+, mkSystem
 , mkCapDLInitializer
-, mkSmallCapDLInitializer
 , mkSimpleCompositionCapDLSpec
-
-, mkInstance
-, mkCapDLRootTask
 }:
 
 let
@@ -66,6 +64,18 @@ let
     say 'all tests passed'
   '';
 
+  mkInstance =
+    { rootTask
+    , ...
+    } @ args:
+    callPlatform (
+      {
+        system = mkSystem {
+          inherit rootTask;
+        };
+      } // builtins.removeAttrs args [ "rootTask" ]
+    );
+
 in rec {
 
   # TODO collect automatically
@@ -150,7 +160,7 @@ in rec {
         extraPlatformArgs = lib.optionalAttrs canSimulate {
           canAutomateSimply = true;
         };
-        extraLinks = [
+        extraDebuggingLinks = [
           { name = "root-task.orig.elf"; path = rootTask.orig.elf; }
         ];
       });
@@ -205,15 +215,15 @@ in rec {
         };
 
       c = maybe haveFullRuntime (callPackage ./c.nix {
-        inherit canSimulate;
+        inherit mkInstance canSimulate;
       });
 
       verus = maybe (haveFullRuntime && hostPlatform.is64bit && buildPlatform.isx86_64) (callPackage ./verus.nix {
-        inherit canSimulate;
+        inherit mkInstance canSimulate;
       });
 
       dafny = maybe haveFullRuntime (callPackage ./dafny.nix {
-        inherit canSimulate;
+        inherit mkInstance canSimulate;
       });
 
       default-test-harness = maybe (haveFullRuntime && haveUnwindingSupport) (mkInstance {
@@ -279,19 +289,19 @@ in rec {
     };
 
     capdl = {
-      threads = maybe (haveFullRuntime && haveCapDLInitializer) (mkInstance {
-        rootTask = mkCapDLRootTask rec {
+      threads = maybe (haveFullRuntime && haveCapDLInitializer) (mkInstance rec {
+        test = mkTask {
+          rootCrate = crates.tests-capdl-threads-components-test;
+          release = true; # test optimizations
+        };
+        rootTask = mkCapDLInitializer {
           small = true;
-          script = sources.srcRoot + "/crates/private/tests/capdl/threads/cdl.py";
-          config = {
-            components = {
-              example_component.image = passthru.test.elf;
-            };
-          };
-          passthru = {
-            test = mkTask {
-              rootCrate = crates.tests-capdl-threads-components-test;
-              release = true; # test optimizations
+          spec = mkSimpleCompositionCapDLSpec {
+            script = sources.srcRoot + "/crates/private/tests/capdl/threads/cdl.py";
+            config = {
+              components = {
+                example_component.image = test.elf;
+              };
             };
           };
         };
@@ -300,19 +310,19 @@ in rec {
         };
       });
 
-      utcover = maybe (haveFullRuntime && haveCapDLInitializer) (mkInstance {
-        rootTask = mkCapDLRootTask rec {
-          # small = true;
-          script = sources.srcRoot + "/crates/private/tests/capdl/utcover/cdl.py";
-          config = {
-            components = {
-              example_component.image = passthru.test.elf;
-            };
-          };
-          passthru = {
-            test = mkTask {
-              rootCrate = crates.tests-capdl-utcover-components-test;
-              release = false;
+      utcover = maybe (haveFullRuntime && haveCapDLInitializer) (mkInstance rec {
+        test = mkTask {
+          rootCrate = crates.tests-capdl-utcover-components-test;
+          release = false;
+        };
+        rootTask = mkCapDLInitializer {
+          small = true;
+          spec = mkSimpleCompositionCapDLSpec {
+            script = sources.srcRoot + "/crates/private/tests/capdl/utcover/cdl.py";
+            config = {
+              components = {
+                example_component.image = test.elf;
+              };
             };
           };
         };
diff --git a/hacking/nix/scope/world/instances/microkit/banscii/default.nix b/hacking/nix/scope/world/instances/microkit/banscii/default.nix
index bbdcf71d5..65816a1b3 100644
--- a/hacking/nix/scope/world/instances/microkit/banscii/default.nix
+++ b/hacking/nix/scope/world/instances/microkit/banscii/default.nix
@@ -14,9 +14,9 @@
 , crates
 , crateUtils
 , mkSeL4RustTargetTriple
-, mkMicrokitInstance
 , worldConfig
 , seL4ConfigJSON
+, callPlatform
 
 , canSimulate
 , mkPD
@@ -50,16 +50,13 @@ let
   srcPath = relativePath: sources.srcRoot + "/crates/examples/microkit/banscii/${relativePath}";
 
 in
-lib.fix (self: mkMicrokitInstance {
+lib.fix (self: callPlatform {
   system = microkit.mkSystem {
-    searchPath = symlinkJoin {
-      name = "x";
-      paths = [
-        "${pds.serial-driver}/bin"
-        "${pds.assistant}/bin"
-        "${pds.artist}/bin"
-      ];
-    };
+    searchPath = [
+      "${pds.serial-driver}/bin"
+      "${pds.assistant}/bin"
+      "${pds.artist}/bin"
+    ];
     systemXML = runCommand "banscii.system" {
       nativeBuildInputs = [
         python3Packages.jinja2
diff --git a/hacking/nix/scope/world/instances/microkit/default.nix b/hacking/nix/scope/world/instances/microkit/default.nix
index eac9b6e1c..f0adaf862 100644
--- a/hacking/nix/scope/world/instances/microkit/default.nix
+++ b/hacking/nix/scope/world/instances/microkit/default.nix
@@ -14,9 +14,9 @@
 , crates
 , crateUtils
 , mkSeL4RustTargetTriple
-, mkMicrokitInstance
 , worldConfig
 , seL4Config
+, callPlatform
 
 , maybe
 , canSimulate
@@ -51,9 +51,9 @@ in {
           };
         };
       in
-        mkMicrokitInstance {
+        callPlatform {
           system = microkit.mkSystem {
-            searchPath = "${pds.hello}/bin";
+            searchPath =  [ "${pds.hello}/bin" ];
             systemXML = sources.srcRoot + "/crates/examples/microkit/hello/hello.system";
           };
         } // {
@@ -89,15 +89,12 @@ in {
           };
         };
       in
-        mkMicrokitInstance {
+        callPlatform {
           system = microkit.mkSystem {
-            searchPath = symlinkJoin {
-              name = "x";
-              paths = [
-                "${pds.client}/bin"
-                "${pds.server}/bin"
-              ];
-            };
+            searchPath = [
+              "${pds.client}/bin"
+              "${pds.server}/bin"
+            ];
             systemXML = sources.srcRoot + "/crates/private/tests/microkit/passive-server-with-deferred-action/x.system";
           };
           extraPlatformArgs = lib.optionalAttrs canSimulate  {
diff --git a/hacking/nix/scope/world/instances/microkit/http-server/default.nix b/hacking/nix/scope/world/instances/microkit/http-server/default.nix
index e6319494a..8fc8cf0b5 100644
--- a/hacking/nix/scope/world/instances/microkit/http-server/default.nix
+++ b/hacking/nix/scope/world/instances/microkit/http-server/default.nix
@@ -19,7 +19,7 @@
 , seL4Modifications
 , seL4Config
 , worldConfig
-, mkMicrokitInstance
+, callPlatform
 , mkSeL4RustTargetTriple
 
 , canSimulate
@@ -178,22 +178,19 @@ let
   };
 
 in
-lib.fix (self: mkMicrokitInstance {
+lib.fix (self: callPlatform {
   system = microkit.mkSystem {
-    searchPath = symlinkJoin {
-      name = "x";
-      paths = [
-        "${pds.http-server}/bin"
-        "${pds.pl031-driver}/bin"
-        "${pds.sp804-driver}/bin"
-        "${pds.virtio-net-driver}/bin"
-        "${pds.virtio-blk-driver}/bin"
-      ];
-    };
+    searchPath = [
+      "${pds.http-server}/bin"
+      "${pds.pl031-driver}/bin"
+      "${pds.sp804-driver}/bin"
+      "${pds.virtio-net-driver}/bin"
+      "${pds.virtio-blk-driver}/bin"
+    ];
     systemXML = sources.srcRoot + "/crates/examples/microkit/http-server/http-server.system";
   };
   extraPlatformArgs = lib.optionalAttrs canSimulate {
-    extraQemuArgs = [
+    extraQEMUArgs = [
       "-device" "virtio-net-device,netdev=netdev0"
       "-netdev" "user,id=netdev0,hostfwd=tcp::8080-:80,hostfwd=tcp::8443-:443"
 
diff --git a/hacking/nix/scope/world/mk-instance.nix b/hacking/nix/scope/world/mk-instance.nix
deleted file mode 100644
index cd1ac646d..000000000
--- a/hacking/nix/scope/world/mk-instance.nix
+++ /dev/null
@@ -1,124 +0,0 @@
-#
-# Copyright 2023, Colias Group, LLC
-#
-# SPDX-License-Identifier: BSD-2-Clause
-#
-
-{ lib, hostPlatform, buildPackages
-, writeScript, linkFarm
-, mkSeL4KernelLoaderWithPayload
-, worldConfig
-, seL4ForBoot
-
-, mkCapDLInitializer
-, mkSmallCapDLInitializer
-, mkSimpleCompositionCapDLSpec
-}:
-
-let
-  defaultTimeout = 30;
-
-  symbolizeBacktraceLinksEntry = {
-    name = "sel4-symbolize-backtrace";
-    path = "${buildPackages.this.sel4-backtrace-cli}/bin/sel4-symbolize-backtrace";
-  };
-
-  mkInstance =
-    { rootTask
-    , extraLinks ? []
-    , extraPlatformArgs ? {}
-    }:
-
-    let
-
-      loader = mkSeL4KernelLoaderWithPayload {
-        appELF = rootTask.elf;
-      };
-
-      instanceForPlatform = worldConfig.mkInstanceForPlatform ({
-        rootTask = rootTask.elf;
-        loader = loader.elf;
-      } // extraPlatformArgs);
-
-    in rec {
-      inherit loader rootTask instanceForPlatform;
-
-      symbolizeRootTaskBacktrace = writeScript "x.sh" ''
-        #!${buildPackages.runtimeShell}
-        exec ${buildPackages.this.sel4-backtrace-cli}/bin/sel4-symbolize-backtrace -f ${rootTask.elf} "$@"
-      '';
-
-      links = linkFarm "links" (lib.concatLists [
-        instanceForPlatform.links
-        (lib.optionals worldConfig.platformRequiresLoader [
-          { name = "loader.elf"; path = loader.elf; }
-          { name = "loader.debug.elf"; path = loader.split.full; }
-        ])
-        [
-          symbolizeBacktraceLinksEntry
-          { name = "kernel.elf"; path = "${seL4ForBoot}/bin/kernel.elf"; }
-          { name = "root-task.elf"; path = rootTask.elf; }
-          { name = "symbolize-root-task-backtrace"; path = symbolizeRootTaskBacktrace; }
-        ]
-        extraLinks
-        (rootTask.extraLinks or [])
-      ]);
-
-    } // instanceForPlatform.attrs;
-
-  mkMicrokitInstance =
-    { system
-    , extraLinks ? []
-    , extraPlatformArgs ? {}
-    }:
-
-    let
-      instanceForPlatform = worldConfig.mkInstanceForPlatform ({
-        inherit (system) loader;
-      } // extraPlatformArgs);
-
-    in rec {
-      inherit system instanceForPlatform;
-
-      links = linkFarm "links" (lib.concatLists [
-        [
-          symbolizeBacktraceLinksEntry
-        ]
-        instanceForPlatform.links
-        extraLinks
-        system.links
-      ]);
-
-    } // instanceForPlatform.attrs;
-
-  mkCapDLRootTask =
-    { script
-    , config
-    , passthru
-    , small ? false
-    }:
-    let
-    in lib.fix (self: with self;
-      {
-        inherit script config;
-        spec = mkSimpleCompositionCapDLSpec {
-          inherit script config;
-        };
-        extraLinks = [
-          { name = "cdl"; path = spec; }
-        ] ++ lib.optionals (!small) [
-          { name = "initializer.full.elf"; path = self.initializer.split.full; }
-        ];
-      }
-      // (if small then {
-        initializer = mkSmallCapDLInitializer spec.cdl;
-        elf = initializer.elf;
-      } else {
-        initializer = mkCapDLInitializer spec.cdl;
-        elf = initializer.elf;
-      })
-      // passthru
-    );
-in {
-  inherit mkInstance mkMicrokitInstance mkCapDLRootTask;
-}
diff --git a/hacking/nix/scope/world/mk-task.nix b/hacking/nix/scope/world/mk-task.nix
index f45de1a5f..2f7b446cd 100644
--- a/hacking/nix/scope/world/mk-task.nix
+++ b/hacking/nix/scope/world/mk-task.nix
@@ -7,7 +7,6 @@
 { lib, buildPackages
 , runCommand, runCommandCC
 , buildCratesInLayers, buildSysroot, crateUtils
-, crates
 , defaultRustEnvironment
 , defaultRustTargetTriple
 , libclangPath
diff --git a/hacking/nix/scope/worlds.nix b/hacking/nix/scope/worlds.nix
index 42cebfa7c..15563d3d0 100644
--- a/hacking/nix/scope/worlds.nix
+++ b/hacking/nix/scope/worlds.nix
@@ -42,7 +42,7 @@ in rec {
             , el2 ? true
             , hypervisor ? false
             , cpu ? "cortex-a57"
-            , mkSeL4KernelLoaderWithPayloadQEMUArgs ? loader: [ "-kernel" loader ]
+            , mkLoaderQEMUArgs ? loader: [ "-kernel" loader ]
 
             , isMicrokit ? false
             , microkitBoard ? null
@@ -84,8 +84,8 @@ in rec {
                   # KernelArmExportPMUUser = on;
                   # KernelSignalFastpath = on;
                 canSimulate = true;
-                mkInstanceForPlatform = platUtils.qemu.mkMkInstanceForPlatform {
-                  mkQemuCmd = loader: [
+                mkPlatformSystemExtension = platUtils.qemu.mkMkPlatformSystemExtension {
+                  mkQEMUCmd = loader: [
                     # NOTE
                     # virtualization=on even when hypervisor to test loader dropping exception level
                     "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-aarch64"
@@ -93,7 +93,7 @@ in rec {
                       "-cpu" cpu "-smp" numCores "-m" "size=1024"
                       "-nographic"
                       "-serial" "mon:stdio"
-                  ] ++ mkSeL4KernelLoaderWithPayloadQEMUArgs loader ++ extraQEMUArgs;
+                  ] ++ mkLoaderQEMUArgs loader ++ extraQEMUArgs;
                 };
               };
         in rec {
@@ -107,7 +107,7 @@ in rec {
             isMicrokit = true;
             microkitBoard = "qemu_virt_aarch64";
             cpu = "cortex-a53";
-            mkSeL4KernelLoaderWithPayloadQEMUArgs = loader: [ "-device" "loader,file=${loader},addr=0x70000000,cpu-num=0" ];
+            mkLoaderQEMUArgs = loader: [ "-device" "loader,file=${loader},addr=0x70000000,cpu-num=0" ];
             extraQEMUArgs = [ "-m" "size=2G" ];
           };
 
@@ -147,7 +147,7 @@ in rec {
           KernelArmHypervisorSupport = on; # seems incompatible with QEMU's model
           KernelMaxNumNodes = mkString "4"; # currently not working with QEMU
         };
-        mkInstanceForPlatform = platUtils.rpi4.mkInstanceForPlatform;
+        mkPlatformSystemExtension = platUtils.rpi4.mkPlatformSystemExtension;
       };
 
       zcu102 =
@@ -168,8 +168,8 @@ in rec {
               };
             }) // {
               canSimulate = true;
-              mkInstanceForPlatform = platUtils.qemu.mkMkInstanceForPlatform {
-                mkQemuCmd = loader: [
+              mkPlatformSystemExtension = platUtils.qemu.mkMkPlatformSystemExtension {
+                mkQEMUCmd = loader: [
                   "${pkgsBuildBuild.this.qemuForSeL4Xilinx}/bin/qemu-system-aarch64"
                   # "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-aarch64"
                     "-machine" "xlnx-zcu102"
@@ -219,8 +219,8 @@ in rec {
                   KernelIsMCS = fromBool mcs;
                 };
                 canSimulate = true;
-                mkInstanceForPlatform = platUtils.qemu.mkMkInstanceForPlatform {
-                  mkQemuCmd = loader: [
+                mkPlatformSystemExtension = platUtils.qemu.mkMkPlatformSystemExtension {
+                  mkQEMUCmd = loader: [
                     "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-arm"
                       "-machine" "virt,highmem=off,secure=off,virtualization=${if bootInHyp then "on" else "off"}"
                       "-cpu" cpu "-smp" numCores "-m" "size=1024"
@@ -247,7 +247,7 @@ in rec {
           KernelArmHypervisorSupport = off;
           KernelMaxNumNodes = mkString "4";
         };
-        mkInstanceForPlatform = platUtils.rpi4.mkInstanceForPlatform;
+        mkPlatformSystemExtension = platUtils.rpi4.mkPlatformSystemExtension;
       };
     };
 
@@ -277,8 +277,8 @@ in rec {
                   KernelIsMCS = fromBool mcs;
                 };
                 canSimulate = true;
-                mkInstanceForPlatform = platUtils.qemu.mkMkInstanceForPlatform {
-                  mkQemuCmd = loader: [
+                mkPlatformSystemExtension = platUtils.qemu.mkMkPlatformSystemExtension {
+                  mkQEMUCmd = loader: [
                     "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-riscv64"
                       "-machine" "virt"
                       "-cpu" "rv64" "-smp" numCores "-m" "size=${qemuMemory}"
@@ -309,8 +309,8 @@ in rec {
           KernelPlatform = mkString "spike";
         };
         canSimulate = true;
-        mkInstanceForPlatform = platUtils.qemu.mkMkInstanceForPlatform {
-          mkQemuCmd = loader: [
+        mkPlatformSystemExtension = platUtils.qemu.mkMkPlatformSystemExtension {
+          mkQEMUCmd = loader: [
             "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-riscv64"
               "-machine" "spike"
               "-cpu" "rv64" "-m" "size=4096M"
@@ -334,8 +334,8 @@ in rec {
           KernelPlatform = mkString "hifive";
         };
         canSimulate = true;
-        mkInstanceForPlatform = platUtils.qemu.mkMkInstanceForPlatform {
-          mkQemuCmd = loader: [
+        mkPlatformSystemExtension = platUtils.qemu.mkMkPlatformSystemExtension {
+          mkQEMUCmd = loader: [
             "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-riscv64"
               "-machine" "sifive_u"
               "-m" "size=8192M"
@@ -368,8 +368,8 @@ in rec {
                   KernelIsMCS = fromBool mcs;
                 };
                 canSimulate = true;
-                mkInstanceForPlatform = platUtils.qemu.mkMkInstanceForPlatform {
-                  mkQemuCmd = loader: [
+                mkPlatformSystemExtension = platUtils.qemu.mkMkPlatformSystemExtension {
+                  mkQEMUCmd = loader: [
                     "${pkgsBuildBuild.this.qemuForSeL4}/bin/qemu-system-riscv32"
                       "-machine" "spike"
                       "-cpu" "rv32" "-m" "size=2000M"
@@ -408,9 +408,8 @@ in rec {
           KernelFPU = mkString "FXSAVE";
         };
         canSimulate = true;
-        mkInstanceForPlatform = platUtils.qemu.mkMkInstanceForPlatform {
-          platformRequiresLoader = false;
-          mkQemuCmd =
+        mkPlatformSystemExtension = platUtils.qemu.mkMkPlatformSystemExtension {
+          mkQEMUCmd =
             let
               enable = opt: "+${opt}";
               disable = opt: "-${opt}";