diff --git a/Cargo.lock b/Cargo.lock
index 9bc9b28cd..290dea829 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -302,6 +302,24 @@ dependencies = [
  "generic-array",
 ]
 
+[[package]]
+name = "builtin"
+version = "0.1.0"
+source = "git+https://github.com/coliasgroup/verus.git?tag=keep/fdac1c3c52e639bf3e835802f63b4352#fdac1c3c52e639bf3e835802f63b43520379b1a1"
+
+[[package]]
+name = "builtin_macros"
+version = "0.1.0"
+source = "git+https://github.com/coliasgroup/verus.git?tag=keep/fdac1c3c52e639bf3e835802f63b4352#fdac1c3c52e639bf3e835802f63b43520379b1a1"
+dependencies = [
+ "prettyplease_verus",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+ "syn_verus",
+ "synstructure",
+]
+
 [[package]]
 name = "bumpalo"
 version = "3.15.4"
@@ -1591,6 +1609,15 @@ dependencies = [
  "syn 2.0.52",
 ]
 
+[[package]]
+name = "prettyplease_verus"
+version = "0.1.15"
+source = "git+https://github.com/coliasgroup/verus.git?tag=keep/fdac1c3c52e639bf3e835802f63b4352#fdac1c3c52e639bf3e835802f63b43520379b1a1"
+dependencies = [
+ "proc-macro2",
+ "syn_verus",
+]
+
 [[package]]
 name = "proc-macro-error"
 version = "1.0.4"
@@ -2921,6 +2948,16 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "syn_verus"
+version = "1.0.95"
+source = "git+https://github.com/coliasgroup/verus.git?tag=keep/fdac1c3c52e639bf3e835802f63b4352#fdac1c3c52e639bf3e835802f63b43520379b1a1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
+
 [[package]]
 name = "synstructure"
 version = "0.12.6"
@@ -3074,6 +3111,24 @@ dependencies = [
  "sel4-root-task",
 ]
 
+[[package]]
+name = "tests-root-task-verus-core"
+version = "0.1.0"
+dependencies = [
+ "builtin",
+ "builtin_macros",
+ "vstd",
+]
+
+[[package]]
+name = "tests-root-task-verus-task"
+version = "0.1.0"
+dependencies = [
+ "sel4",
+ "sel4-root-task",
+ "tests-root-task-verus-core",
+]
+
 [[package]]
 name = "thiserror"
 version = "1.0.58"
@@ -3238,6 +3293,15 @@ name = "volatile"
 version = "0.5.1"
 source = "git+https://github.com/coliasgroup/volatile.git?tag=keep/aa7512906e9b76066ed928eb6986b0f9#aa7512906e9b76066ed928eb6986b0f9b1750e91"
 
+[[package]]
+name = "vstd"
+version = "0.1.0"
+source = "git+https://github.com/coliasgroup/verus.git?tag=keep/fdac1c3c52e639bf3e835802f63b4352#fdac1c3c52e639bf3e835802f63b43520379b1a1"
+dependencies = [
+ "builtin",
+ "builtin_macros",
+]
+
 [[package]]
 name = "wasi"
 version = "0.11.0+wasi-snapshot-preview1"
diff --git a/Cargo.toml b/Cargo.toml
index afada6897..243cd1519 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -64,6 +64,8 @@ members = [
     "crates/private/tests/root-task/panicking",
     "crates/private/tests/root-task/ring-test-harness",
     "crates/private/tests/root-task/tls",
+    "crates/private/tests/root-task/verus/core",
+    "crates/private/tests/root-task/verus/task",
     "crates/sel4",
     "crates/sel4-async/block-io",
     "crates/sel4-async/block-io/fat",
diff --git a/crates/private/tests/root-task/verus/core/Cargo.nix b/crates/private/tests/root-task/verus/core/Cargo.nix
new file mode 100644
index 000000000..32bafe709
--- /dev/null
+++ b/crates/private/tests/root-task/verus/core/Cargo.nix
@@ -0,0 +1,19 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ mk, verusSource }:
+
+mk {
+  package.name = "tests-root-task-verus-core";
+  dependencies = {
+    builtin = verusSource;
+    builtin_macros = verusSource;
+    vstd = verusSource // { default-features = false; };
+  };
+  package.metadata.verus = {
+    verify = true;
+  };
+}
diff --git a/crates/private/tests/root-task/verus/core/Cargo.toml b/crates/private/tests/root-task/verus/core/Cargo.toml
new file mode 100644
index 000000000..24f08340e
--- /dev/null
+++ b/crates/private/tests/root-task/verus/core/Cargo.toml
@@ -0,0 +1,31 @@
+#
+# Copyright 2023, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+#
+# This file is generated from './Cargo.nix'. You can edit this file directly
+# if you are not using this project's Cargo manifest management tools.
+# See 'hacking/cargo-manifest-management/README.md' for more information.
+#
+
+[package]
+name = "tests-root-task-verus-core"
+version = "0.1.0"
+authors = ["Nick Spinale <nick.spinale@coliasgroup.com>"]
+edition = "2021"
+license = "BSD-2-Clause"
+metadata = { verus = { verify = true } }
+
+[dependencies.builtin]
+git = "https://github.com/coliasgroup/verus.git"
+tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+
+[dependencies.builtin_macros]
+git = "https://github.com/coliasgroup/verus.git"
+tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+
+[dependencies.vstd]
+git = "https://github.com/coliasgroup/verus.git"
+tag = "keep/fdac1c3c52e639bf3e835802f63b4352"
+default-features = false
diff --git a/crates/private/tests/root-task/verus/core/src/lib.rs b/crates/private/tests/root-task/verus/core/src/lib.rs
new file mode 100644
index 000000000..26856955c
--- /dev/null
+++ b/crates/private/tests/root-task/verus/core/src/lib.rs
@@ -0,0 +1,23 @@
+//
+// Copyright 2024, Colias Group, LLC
+//
+// SPDX-License-Identifier: BSD-2-Clause
+//
+
+#![no_std]
+
+use vstd::prelude::*;
+
+verus! {
+    pub fn max(a: u64, b: u64) -> (ret: u64)
+        ensures
+            ret == a || ret == b,
+            ret >= a && ret >= b,
+    {
+        if a >= b {
+            a
+        } else {
+            b
+        }
+    }
+}
diff --git a/crates/private/tests/root-task/verus/task/Cargo.nix b/crates/private/tests/root-task/verus/task/Cargo.nix
new file mode 100644
index 000000000..1fee0f57f
--- /dev/null
+++ b/crates/private/tests/root-task/verus/task/Cargo.nix
@@ -0,0 +1,18 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ mk, localCrates }:
+
+mk {
+  package.name = "tests-root-task-verus-task";
+  dependencies = {
+    inherit (localCrates)
+      sel4
+      sel4-root-task
+      tests-root-task-verus-core
+    ;
+  };
+}
diff --git a/crates/private/tests/root-task/verus/task/Cargo.toml b/crates/private/tests/root-task/verus/task/Cargo.toml
new file mode 100644
index 000000000..80b470c2d
--- /dev/null
+++ b/crates/private/tests/root-task/verus/task/Cargo.toml
@@ -0,0 +1,22 @@
+#
+# Copyright 2023, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+#
+# This file is generated from './Cargo.nix'. You can edit this file directly
+# if you are not using this project's Cargo manifest management tools.
+# See 'hacking/cargo-manifest-management/README.md' for more information.
+#
+
+[package]
+name = "tests-root-task-verus-task"
+version = "0.1.0"
+authors = ["Nick Spinale <nick.spinale@coliasgroup.com>"]
+edition = "2021"
+license = "BSD-2-Clause"
+
+[dependencies]
+sel4 = { path = "../../../../../sel4" }
+sel4-root-task = { path = "../../../../../sel4-root-task" }
+tests-root-task-verus-core = { path = "../core" }
diff --git a/crates/private/tests/root-task/verus/task/src/main.rs b/crates/private/tests/root-task/verus/task/src/main.rs
new file mode 100644
index 000000000..7ebb5fd74
--- /dev/null
+++ b/crates/private/tests/root-task/verus/task/src/main.rs
@@ -0,0 +1,18 @@
+//
+// Copyright 2024, Colias Group, LLC
+//
+// SPDX-License-Identifier: BSD-2-Clause
+//
+
+#![no_std]
+#![no_main]
+
+use sel4_root_task::{debug_println, root_task};
+
+#[root_task(heap_size = 1024 * 1024)]
+fn main(_: &sel4::BootInfoPtr) -> ! {
+    assert_eq!(tests_root_task_verus_core::max(13, 37), 37);
+
+    debug_println!("TEST_PASS");
+    sel4::init_thread::suspend_self()
+}
diff --git a/crates/sel4-externally-shared/src/lib.rs b/crates/sel4-externally-shared/src/lib.rs
index 8f0f01011..a66bd3e05 100644
--- a/crates/sel4-externally-shared/src/lib.rs
+++ b/crates/sel4-externally-shared/src/lib.rs
@@ -52,7 +52,7 @@ impl<'a, T: ?Sized> ExternallySharedPtrExt<'a, T> for ExternallySharedPtr<'a, T,
         T: Atomic,
     {
         let p = self.as_raw_ptr();
-        assert_eq!(p.as_ptr().align_offset(T::ALIGNMENT), 0);
+        assert_eq!(p.as_ptr().cast::<()>().align_offset(T::ALIGNMENT), 0);
         unsafe { AtomicPtr::new(p) }
     }
 }
diff --git a/crates/sel4-runtime-common/src/ctors.rs b/crates/sel4-runtime-common/src/ctors.rs
index f48914cf6..41c8dffe6 100644
--- a/crates/sel4-runtime-common/src/ctors.rs
+++ b/crates/sel4-runtime-common/src/ctors.rs
@@ -25,7 +25,9 @@ pub unsafe fn run_ctors() {
     // Cast to usize for comparison, otherwise rustc seems to apply an erroneous optimization
     // assuming __init_array_start != __init_array_end.
     if start as usize != end as usize {
-        if !start.is_aligned() || !end.is_aligned() {
+        if start.cast::<()>().align_offset(mem::size_of::<Ctor>()) != 0
+            || end.cast::<()>().align_offset(mem::size_of::<Ctor>()) != 0
+        {
             abort!("'.init_array' section is not properly aligned");
         }
 
diff --git a/crates/sel4/src/invocations.rs b/crates/sel4/src/invocations.rs
index b2412eae2..c969e59d5 100644
--- a/crates/sel4/src/invocations.rs
+++ b/crates/sel4/src/invocations.rs
@@ -11,7 +11,7 @@ use core::mem;
 use sel4_config::{sel4_cfg, sel4_cfg_if};
 
 use crate::{
-    cap::*, ipc_buffer, sys, AbsoluteCPtr, CNodeCapData, CPtr, CapRights, Error, InvocationContext,
+    cap::*, sys, AbsoluteCPtr, CNodeCapData, CPtr, CapRights, Error, InvocationContext,
     ObjectBlueprint, Result, UserContext, Word,
 };
 
diff --git a/hacking/cargo-manifest-management/manifest-scope.nix b/hacking/cargo-manifest-management/manifest-scope.nix
index 2ee305280..2c11b6561 100644
--- a/hacking/cargo-manifest-management/manifest-scope.nix
+++ b/hacking/cargo-manifest-management/manifest-scope.nix
@@ -11,6 +11,8 @@ let
   filterOutEmptyFeatureList = attrs:
     builtins.removeAttrs attrs (lib.optional ((attrs.features or null) == []) "features");
 
+  mkKeepRef = rev: "keep/${builtins.substring 0 32 rev}";
+
 in rec {
   inherit lib;
 
@@ -180,12 +182,12 @@ in rec {
 
   volatileSource = {
     git = "https://github.com/coliasgroup/volatile.git";
-    tag = "keep/aa7512906e9b76066ed928eb6986b0f9"; # branch coliasgroup
+    tag = mkKeepRef "aa7512906e9b76066ed928eb6986b0f9b1750e91"; # branch coliasgroup
   };
 
   fatSource = {
     git = "https://github.com/coliasgroup/rust-embedded-fat.git";
-    tag = "keep/e1465a43c9f550ef58701a275b313310"; # branch sel4
+    tag = mkKeepRef "e1465a43c9f550ef58701a275b3133105deb9183"; # branch sel4
   };
 
   ringWith = features: {
@@ -216,6 +218,11 @@ in rec {
 
   dafnySource = {
     git = "https://github.com/coliasgroup/dafny.git";
-    tag = "keep/02d0a578fdf594a38c7c72d7ad56e1a6"; # branch dev
+    tag = mkKeepRef "02d0a578fdf594a38c7c72d7ad56e1a62e464f44"; # branch dev
+  };
+
+  verusSource = {
+    git = "https://github.com/coliasgroup/verus.git";
+    tag = mkKeepRef "fdac1c3c52e639bf3e835802f63b43520379b1a1"; # branch dev
   };
 }
diff --git a/hacking/nix/rust-utils/build-crate-in-layers.nix b/hacking/nix/rust-utils/build-crate-in-layers.nix
index cb43a227e..531bae09c 100644
--- a/hacking/nix/rust-utils/build-crate-in-layers.nix
+++ b/hacking/nix/rust-utils/build-crate-in-layers.nix
@@ -8,15 +8,12 @@
 , linkFarm, emptyDirectory
 , crateUtils
 , vendorLockfile, pruneLockfile
-, defaultRustToolchain, defaultRustTargetInfo
-} @ outerArgs:
-
-{ superLockfile
+, defaultRustEnvironment, defaultRustTargetTriple
+, verus
 }:
 
 let
-
-  superVendoredLockfile = vendorLockfile { lockfile = superLockfile; };
+  defaultStdenv = stdenv;
 
   # TODO not actually resulting in errors
   denyWarningsDefault =
@@ -31,29 +28,33 @@ let
 
 in
 
-{ rootCrate
+{ stdenv ? defaultStdenv
+, rustEnvironment ? defaultRustEnvironment
+, targetTriple ? defaultRustTargetTriple
+
+, rootCrate
 
 , layers ? [ crateUtils.defaultIntermediateLayer ] # default to two building in two steps (external then local)
 , commonModifications ? {}
 , lastLayerModifications ? {}
 
-, test ? false
-
 , release ? false
 , profile ? if release then "release" else null
 
 , features ? []
 , noDefaultFeatures ? false
 
-, rustToolchain ? defaultRustToolchain
-, rustTargetInfo ? defaultRustTargetInfo
+, test ? false
 
-, stdenv ? outerArgs.stdenv
+, verifyWithVerus ? false
+, extraVerusArgs ? []
 
 , denyWarnings ? denyWarningsDefault
 , runClippy ? runClippyDefault
 }:
 
+assert !(test && verifyWithVerus);
+
 let
   inherit (crateUtils) composeModifications elaborateModifications;
 
@@ -71,15 +72,19 @@ let
     in
       f [] {};
 
-  lockfile = builtins.toFile "Cargo.lock" lockfileContents;
-  lockfileContents = builtins.readFile lockfileDrv;
-  lockfileDrv = pruneLockfile {
-    superLockfile = superLockfile;
-    superLockfileVendoringConfig = superVendoredLockfile.configFragment;
+  prunedLockfile = pruneLockfile {
+    inherit (rustEnvironment) rustToolchain vendoredSuperLockfile;
     rootCrates = [ rootCrate ];
     extraManifest = elaboratedCommonModifications.modifyManifest {}; # TODO
   };
 
+  vendoredLockfile = vendorLockfile {
+    inherit (rustEnvironment) rustToolchain;
+    lockfileContents = builtins.readFile prunedLockfile;
+  };
+
+  inherit (vendoredLockfile) lockfile;
+
   elaboratedCommonModifications = elaborateModifications commonModifications;
 
   closure = crateUtils.getClosureOfCrate rootCrate;
@@ -102,9 +107,11 @@ let
 
   baseArgs = {
     depsBuildBuild = [ buildPackages.stdenv.cc ];
-    nativeBuildInputs = [ rustToolchain ];
-  } // lib.optionalAttrs (rustTargetInfo.path != null) {
-    RUST_TARGET_PATH = rustTargetInfo.path;
+    nativeBuildInputs = [ rustEnvironment.rustToolchain ] ++ lib.optionals verifyWithVerus [ verus ];
+    RUST_TARGET_PATH = rustEnvironment.mkTargetPath targetTriple;
+  } // lib.optionalAttrs (!rustEnvironment.isNightly) {
+    # HACK
+    RUSTC_BOOTSTRAP = 1;
   };
 
   baseManifest = {
@@ -114,13 +121,12 @@ let
 
   baseConfig = denyWarnings: crateUtils.clobber [
     (crateUtils.baseConfig {
-      inherit rustToolchain;
-      rustTargetName = rustTargetInfo.name;
+      inherit rustEnvironment targetTriple;
     })
     {
       unstable.unstable-options = true;
     }
-    (vendorLockfile { inherit lockfileContents; }).configFragment
+    vendoredLockfile.configFragment
     (lib.optionalAttrs denyWarnings {
       target."cfg(all())" = {
         rustflags = [ "-D" "warnings" ];
@@ -139,19 +145,27 @@ let
   ] ++ lib.optionals (profile != null) [
     "--profile" profile
   ] ++ [
-    "--target" rustTargetInfo.name
+    "--target" targetTriple.name
     "-j" "$NIX_BUILD_CORES"
   ];
 
-  cargoSubcommand = if test then "test" else "build";
+  cargoSubcommand =
+    if test
+    then "test"
+    else (
+      if verifyWithVerus
+      then "verus"
+      else "build"
+    );
 
   mkCargoInvocation = runClippy: commonArgs: subcommandArgs:
     let
       joinedCommonArgs = lib.concatStringsSep " " commonArgs;
-      joinedSubcommandArgs = lib.concatStringsSep " "
-        (subcommandArgs ++ lib.optionals test [
-          "--no-run"
-        ]);
+      joinedSubcommandArgs = lib.concatStringsSep " " (
+        subcommandArgs
+          ++ lib.optionals test [ "--no-run" ]
+          ++ lib.optionals verifyWithVerus ([ "--" ] ++ extraVerusArgs)
+      );
     in ''
       ${lib.optionalString runClippy ''
         cargo clippy ${joinedCommonArgs} -- -D warnings
@@ -161,7 +175,7 @@ let
 
   findTestsCommandPrefix = targetDir: [
     "find"
-      "${targetDir}/${rustTargetInfo.name}/*/deps"
+      "${targetDir}/${targetTriple.name}/*/deps"
       "-maxdepth" "1"
       "-executable"
       "-name" "'*.elf'"
diff --git a/hacking/nix/rust-utils/build-sysroot.nix b/hacking/nix/rust-utils/build-sysroot.nix
index ae8772c5a..77beca05d 100644
--- a/hacking/nix/rust-utils/build-sysroot.nix
+++ b/hacking/nix/rust-utils/build-sysroot.nix
@@ -6,29 +6,19 @@
 
 { lib, stdenv, buildPlatform, hostPlatform, buildPackages
 , runCommand, runCommandCC, linkFarm
-, fetchurl
-, vendorLockfile, crateUtils, symlinkToRegularFile
-, defaultRustToolchain, defaultRustTargetInfo
-, rustToolchain ? defaultRustToolchain
+, crateUtils
+, defaultRustEnvironment, defaultRustTargetTriple
 }:
 
-let
-  sysrootLockfile = symlinkToRegularFile "Cargo.lock" "${rustToolchain}/lib/rustlib/src/rust/Cargo.lock";
-
-  # NOTE
-  # There is one thunk per package set.
-  # Consolidating further would improve eval perf.
-  vendoredCrates = vendorLockfile { lockfile = sysrootLockfile; };
-in
-
-{ release ? true
+{ rustEnvironment ? defaultRustEnvironment
+, targetTriple ? defaultRustTargetTriple
+, release ? true
 , profile ? if release then "release" else null
-, extraManifest ? {}
-, extraConfig ? {}
-, rustTargetInfo ? defaultRustTargetInfo
 , alloc ? true
 , compilerBuiltinsMem ? true
-, compilerBuiltinsC ? true
+, compilerBuiltinsC ? rustEnvironment.compilerRTSource != null
+, extraManifest ? {}
+, extraConfig ? {}
 }:
 
 let
@@ -60,16 +50,16 @@ let
     # baseConfig # TODO will trigger rebuild
     {
       target = {
-        "${rustTargetInfo.name}" = {
+        "${targetTriple.name}" = {
           rustflags = [
-            # "-C" "force-unwind-tables=yes" # TODO compare with "requires-uwtable" in target.json
-            "-C" "embed-bitcode=yes"
             "--sysroot" "/dev/null"
+            "-C" "embed-bitcode=yes"
+            # "-C" "force-unwind-tables=yes" # TODO compare with "requires-uwtable" in target.json
           ];
         };
       };
     }
-    vendoredCrates.configFragment
+    rustEnvironment.vendoredSysrootLockfile.configFragment
     extraConfig
   ]);
 
@@ -80,34 +70,22 @@ let
     "alloc"
   ]);
 
-  features = lib.concatStringsSep "," (lib.optionals compilerBuiltinsMem [
-    "compiler-builtins-mem"
-  ] ++ lib.optionals compilerBuiltinsC [
-    "compiler-builtins-c"
+  features = lib.concatStringsSep "," (lib.flatten [
+    (lib.optional compilerBuiltinsMem "compiler-builtins-mem")
+    (lib.optional compilerBuiltinsC "compiler-builtins-c")
   ]);
 
-  compilerRTSource = let
-    v = "18.0-2024-02-13";
-    name = "compiler-rt";
-    llvmSourceTarball = fetchurl {
-      name = "llvm-project.tar.gz";
-      url = "https://github.com/rust-lang/llvm-project/archive/rustc/${v}.tar.gz";
-      sha256 = "sha256-fMc84lCWfNy0Xiq1X7nrT53MQPlfRqGEb4qBAmqehAA=";
-    };
-  in
-    runCommand name {} ''
-      tar xzf ${llvmSourceTarball} --strip-components 1 llvm-project-rustc-${v}/${name}
-      mv ${name} $out
-    '';
-
 in
 (if compilerBuiltinsC then runCommandCC else runCommand) "sysroot" ({
   depsBuildBuild = [ buildPackages.stdenv.cc ];
-  nativeBuildInputs = [ rustToolchain ];
-  RUST_TARGET_PATH = rustTargetInfo.path;
+  nativeBuildInputs = [ rustEnvironment.rustToolchain ];
+  RUST_TARGET_PATH = rustEnvironment.mkTargetPath targetTriple;
+} // lib.optionalAttrs (!rustEnvironment.isNightly) {
+  # HACK
+  RUSTC_BOOTSTRAP = 1;
 } // lib.optionalAttrs compilerBuiltinsC {
-  "CC_${rustTargetInfo.name}" = "${stdenv.cc.targetPrefix}gcc";
-  RUST_COMPILER_RT_ROOT = compilerRTSource;
+  "CC_${targetTriple.name}" = "${stdenv.cc.targetPrefix}gcc";
+  RUST_COMPILER_RT_ROOT = rustEnvironment.compilerRTSource;
 }) ''
   cargo build \
     -Z unstable-options \
@@ -115,15 +93,15 @@ in
     --frozen \
     --config ${config} \
     ${lib.optionalString (profile != null) "--profile ${profile}"} \
-    --target ${rustTargetInfo.name} \
+    --target ${targetTriple.name} \
     -Z build-std=${crates} \
     -Z build-std-features=${features} \
     --manifest-path ${workspace}/Cargo.toml \
     --target-dir $(pwd)/target
 
-  d=$out/lib/rustlib/${rustTargetInfo.name}/lib
+  d=$out/lib/rustlib/${targetTriple.name}/lib
   mkdir -p $d
-  mv target/${rustTargetInfo.name}/*/deps/* $d
+  mv target/${targetTriple.name}/*/deps/* $d
 ''
 
 # TODO
diff --git a/hacking/nix/rust-utils/crate-utils.nix b/hacking/nix/rust-utils/crate-utils.nix
index eb018563a..28f2c636f 100644
--- a/hacking/nix/rust-utils/crate-utils.nix
+++ b/hacking/nix/rust-utils/crate-utils.nix
@@ -7,7 +7,7 @@
 { lib, buildPlatform, hostPlatform
 , writeText, linkFarm, runCommand
 , toTOMLFile
-, chooseLinkerForRustTarget ? throw "chooseLinkerForRustTarget must be set"
+, mkBuiltinRustTargetTriple
 }:
 
 let
@@ -95,26 +95,26 @@ rec {
   ###
 
   # TODO improve this mechanism
-  linkerConfig = { rustToolchain, rustTargetName }@args:
+  linkerConfig = { rustEnvironment, targetTriple }@args:
     let
-      f = { rustTargetName, platform }:
+      f = { targetTriple, platform }:
         let
-          linker = chooseLinkerForRustTarget {
-            inherit rustToolchain rustTargetName platform;
+          linker = rustEnvironment.chooseLinker {
+            inherit targetTriple platform;
           };
         in
           lib.optionalAttrs (linker != null) {
             target = {
-              "${rustTargetName}".linker = linker;
+              "${targetTriple.name}".linker = linker;
             };
           };
     in
       clobber [
-        (f { rustTargetName = buildPlatform.config; platform = buildPlatform; })
-        (f { inherit rustTargetName; platform = hostPlatform; })
+        (f { targetTriple = mkBuiltinRustTargetTriple buildPlatform.config; platform = buildPlatform; })
+        (f { inherit targetTriple; platform = hostPlatform; })
       ];
 
-  baseConfig = { rustToolchain, rustTargetName }@args: clobber [
+  baseConfig = { rustEnvironment, targetTriple }@args: clobber [
     {
       build.incremental = false;
     }
diff --git a/hacking/nix/rust-utils/default.nix b/hacking/nix/rust-utils/default.nix
index 422169c52..0c429d16c 100644
--- a/hacking/nix/rust-utils/default.nix
+++ b/hacking/nix/rust-utils/default.nix
@@ -4,7 +4,11 @@
 # SPDX-License-Identifier: BSD-2-Clause
 #
 
-{ lib }:
+{ lib
+, runCommand
+, emptyDirectory
+, fetchFromGitHub
+}:
 
 self: with self;
 
@@ -27,4 +31,53 @@ in
   toTOMLFile = callBuildBuildPackage ./to-toml-file.nix {};
 
   symlinkToRegularFile = callBuildBuildPackage ./symlink-to-regular-file.nix {};
+
+  mkCompilerRTSource = { version, hash }:
+    let
+      llvmProject = fetchFromGitHub {
+        owner = "rust-lang";
+        repo = "llvm-project";
+        rev = "rustc/${version}";
+        inherit hash;
+      };
+    in
+      runCommand "compiler-rt" {} ''
+        cp -r ${llvmProject}/compiler-rt $out
+      '';
+
+  mkBuiltinRustTargetTriple = name: {
+    inherit name;
+    isBuiltin = true;
+  };
+
+  mkCustomRustTargetTriple = name: {
+    inherit name;
+    isBuiltin = false;
+  };
+
+  elaborateRustEnvironment =
+    { rustToolchain
+    , channel ? null
+    , isNightly ?
+        if channel != null
+        then lib.hasPrefix "nightly" channel
+        else throw "could not determine isNightly automatically"
+    , mkCustomTargetPath ? customTargetTripleTripleName: throw "unimplemented"
+    , chooseLinker ? { targetTriple, platform }: null
+    , compilerRTSource ? null
+    , vendoredSuperLockfile ? null
+    }:
+    {
+      inherit rustToolchain channel isNightly;
+      inherit compilerRTSource;
+      inherit chooseLinker;
+      inherit vendoredSuperLockfile;
+
+      mkTargetPath = targetTriple: if !targetTriple.isBuiltin then mkCustomTargetPath targetTriple.name else emptyDirectory;
+
+      vendoredSysrootLockfile = vendorLockfile {
+        inherit rustToolchain;
+        lockfile = symlinkToRegularFile "Cargo.lock" "${rustToolchain}/lib/rustlib/src/rust/Cargo.lock";
+      };
+    };
 }
diff --git a/hacking/nix/rust-utils/prune-lockfile.nix b/hacking/nix/rust-utils/prune-lockfile.nix
index cfc2b92d2..4ef94f975 100644
--- a/hacking/nix/rust-utils/prune-lockfile.nix
+++ b/hacking/nix/rust-utils/prune-lockfile.nix
@@ -7,11 +7,11 @@
 { lib, runCommand
 , crateUtils
 , defaultRustToolchain
-, rustToolchain ? defaultRustToolchain
 }:
 
-{ rootCrates
-, superLockfile, superLockfileVendoringConfig
+{ rustToolchain ? defaultRustToolchain
+, rootCrates
+, vendoredSuperLockfile
 , extraManifest ? {}, extraConfig ? {}
 }:
 
@@ -32,7 +32,7 @@ let
     {
       unstable.unstable-options = true;
     }
-    superLockfileVendoringConfig
+    vendoredSuperLockfile.configFragment
     extraConfig
   ]);
 
@@ -44,7 +44,7 @@ runCommand "Cargo.lock" {
 } ''
   ln -s ${manifest} Cargo.toml
   ln -s ${src} src
-  cp --no-preserve=owner,mode ${superLockfile} Cargo.lock
+  cp --no-preserve=owner,mode ${vendoredSuperLockfile.lockfile} Cargo.lock
   cargo --config ${config} update -wq
   mv Cargo.lock $out
 ''
diff --git a/hacking/nix/rust-utils/vendor-lockfile.nix b/hacking/nix/rust-utils/vendor-lockfile.nix
index fa359bedf..4719b7f09 100644
--- a/hacking/nix/rust-utils/vendor-lockfile.nix
+++ b/hacking/nix/rust-utils/vendor-lockfile.nix
@@ -5,23 +5,22 @@
 #
 
 { lib, runCommand, linkFarm
+, buildPackages
 , fetchurl
 , jq
 , defaultRustToolchain
-, rustToolchain ? defaultRustToolchain
-, buildPackages
 }:
 
-{ lockfileContents ? null
+{ rustToolchain ? defaultRustToolchain
+, lockfileContents ? null
 , lockfile ? null
 , fetchGitSubmodules ? false
+, extraMkCrateTarballURLFns ? {}
 } @ args:
 
 assert lockfileContents != null || lockfile != null;
 
 let
-  cratesIORegistryURL = "https://github.com/rust-lang/crates.io-index";
-
   lockfileContents =
     if lockfile != null
     then builtins.readFile lockfile
@@ -36,13 +35,39 @@ let
 
   remotePackages = lib.filter (lib.hasAttr "source") packages;
 
-  parseRemotePackage = package:
+  remotePackagesBySource = lib.foldAttrs (x: xs: [x] ++ xs) [] (lib.forEach remotePackages (package: {
+    "${package.source}" = builtins.removeAttrs package [ "source" ];
+  }));
+
+  vendoredSources = lib.fold lib.recursiveUpdate {} (lib.mapAttrsToList vendorSource remotePackagesBySource);
+
+  cratesIORegistryURL = "https://github.com/rust-lang/crates.io-index";
+
+  cratesIOSource = "registry+${cratesIORegistryURL}";
+
+  mkCratesIOCrateTarballURL = { name, version }:
+    "https://crates.io/api/v1/crates/${name}/${version}/download";
+
+  mkCrateTarballURLFns = {
+    "${cratesIORegistryURL}" = mkCratesIOCrateTarballURL;
+  } // extraMkCrateTarballURLFns;
+
+  vendorSource = source: packages:
     let
-      parsedSource = parseSource package.source;
+      parsedSource = parseSource source;
+      vendorSourceFn = {
+        registry = vendorRegistrySource;
+        git = vendorGitSource;
+      }.${parsedSource.type};
+      vendoredSource = vendorSourceFn parsedSource.value packages;
+      vendoredSourceName = "vendored+${source}";
+      isCratesIO = source == cratesIOSource;
+      guardedSource = if isCratesIO then "crates-io" else source;
     in {
-      inherit (package) name version;
-      checksum = package.checksum or null;
-      source = parsedSource;
+      source.${vendoredSourceName}.directory = vendoredSource.directory;
+      source.${guardedSource} = lib.optionalAttrs (!isCratesIO) vendoredSource.attrs // {
+        replace-with = vendoredSourceName;
+      };
     };
 
   parseSource = source:
@@ -64,7 +89,7 @@ let
 
   parseGitSource = gitSource:
     let
-      parts = builtins.match ''([^?]*)(\?(rev|tag|branch)=([^#]*))?#(.*)'' gitSource;
+      parts = builtins.match ''([^?]*)(\?(rev|tag|branch)=([^#&]*))?#(.*)'' gitSource;
       url = builtins.elemAt parts 0;
       refType = builtins.elemAt parts 2;
       refValue = builtins.elemAt parts 3;
@@ -77,146 +102,119 @@ let
       };
     };
 
-  vendorRemotePackage = parsedRemotePackage:
-    let
-    in {
-      git =
-        assert parsedRemotePackage.checksum == null;
-        vendorRemoteGitPackage {
-          inherit (parsedRemotePackage) name version;
-          inherit (parsedRemotePackage.source.value) url rev ref;
-        };
-      registry =
-        assert parsedRemotePackage.checksum != null;
-        assert parsedRemotePackage.source.value.registryURL == cratesIORegistryURL;
-        vendorRemoteCratesIOPackage {
-          inherit (parsedRemotePackage) name version checksum;
+  vendorRegistrySource = { registryURL }: packages: {
+    attrs = {
+        registry = registryURL;
+    };
+    directory = linkFarm "vendored-registry-source" (lib.forEach packages (package:
+      let
+        inherit (package) name version checksum;
+      in {
+        name = "${name}-${version}";
+        path = fetchRegistryPackage {
+          inherit registryURL name version checksum;
         };
-    }.${parsedRemotePackage.source.type};
+      }
+    ));
+  };
 
-  vendorRemoteCratesIOPackage = { name, version, checksum }:
+  fetchRegistryPackage = { registryURL, name, version, checksum }:
     let
       tarball = fetchurl {
         name = "crate-${name}-${version}.tar.gz";
-        url = "https://crates.io/api/v1/crates/${name}/${version}/download";
+        url = mkCrateTarballURLFns.${registryURL} {
+          inherit name version;
+        };
         sha256 = checksum;
       };
-      tree = runCommand "${name}-${version}" {} ''
+    in
+      runCommand "${name}-${version}" {} ''
         mkdir $out
         tar xf "${tarball}" -C $out --strip-components=1
 
         # Cargo is happy with partially empty metadata.
         printf '{"files": {}, "package": "${checksum}"}' > "$out/.cargo-checksum.json"
       '';
-    in {
-      inherit tree;
-      configFragment = {};
-    };
 
-  vendorRemoteGitPackage = { name, version, url, rev, ref }:
+  vendorGitSource = { url, rev, ref ? null }: packages:
     let
       superTree = builtins.fetchGit {
         inherit url rev;
         submodules = fetchGitSubmodules;
         allRefs = true; # HACK
       };
-
       # TODO
       # // (if ref != null then {
       #   ref = ref.value;
       # } else {
-      #   # allRefs = true; # HACK
+      #   allRefs = true; # HACK
       # });
-
-      tree = runCommand "${name}-${version}" {
-        nativeBuildInputs = [ jq rustToolchain ];
-      } ''
-        tree=${superTree}
-
-        # If the target package is in a workspace, or if it's the top-level
-        # crate, we should find the crate path using `cargo metadata`.
-        # Some packages do not have a Cargo.toml at the top-level,
-        # but only in nested directories.
-        # Only check the top-level Cargo.toml, if it actually exists
-        if [[ -f $tree/Cargo.toml ]]; then
-          crateCargoTOML=$(cargo metadata --format-version 1 --no-deps --manifest-path $tree/Cargo.toml | \
-          jq -r '.packages[] | select(.name == "${name}") | .manifest_path')
-        fi
-
-        # If the repository is not a workspace the package might be in a subdirectory.
-        if [[ -z $crateCargoTOML ]]; then
-          for manifest in $(find $tree -name "Cargo.toml"); do
-            echo Looking at $manifest
-            crateCargoTOML=$(cargo metadata --format-version 1 --no-deps --manifest-path "$manifest" | jq -r '.packages[] | select(.name == "${name}") | .manifest_path' || :)
-            if [[ ! -z $crateCargoTOML ]]; then
-              break
-            fi
-          done
-
-          if [[ -z $crateCargoTOML ]]; then
-            >&2 echo "Cannot find path for crate '${name}-${version}' in the tree in: $tree"
-            exit 1
-          fi
-        fi
-
-        echo Found crate ${name} at $crateCargoTOML
-        tree=$(dirname $crateCargoTOML)
-
-        cp -prvd "$tree/" $out
-        chmod u+w $out
-
-        # HACK: Recreate some of .git for crates which try to detect whether they're a git dependency
-        mkdir $out/.git
-        echo "${rev}" > $out/.git/HEAD
-
-        # Cargo is happy with empty metadata.
-        printf '{"files": {}, "package": null}' > "$out/.cargo-checksum.json"
-      '';
     in {
-      inherit tree;
-      configFragment = {
-        source.${url} = {
-          git = url;
-          replace-with = "vendored-sources";
-        } // lib.optionalAttrs (ref != null) {
-          "${ref.type}" = ref.value;
-        };
+      attrs = {
+        git = url;
+      } // lib.optionalAttrs (ref != null) {
+        "${ref.type}" = ref.value;
       };
+      directory = linkFarm "vendored-git-source" (lib.forEach packages (package:
+        let
+          inherit (package) name version;
+        in {
+          name = "${name}-${version}";
+          path = extractGitPackage {
+            inherit superTree rev name version;
+          };
+        }
+      ));
     };
 
-  parseAndVendorRemotePackage = remotePackage: rec {
-    parsed = parseRemotePackage remotePackage;
-    vendored = vendorRemotePackage parsed;
-  };
+  extractGitPackage = { superTree, rev, name, version }:
+    runCommand "${name}-${version}" {
+      nativeBuildInputs = [ jq rustToolchain ];
+    } ''
+      tree=${superTree}
+
+      # If the target package is in a workspace, or if it's the top-level
+      # crate, we should find the crate path using `cargo metadata`.
+      # Some packages do not have a Cargo.toml at the top-level,
+      # but only in nested directories.
+      # Only check the top-level Cargo.toml, if it actually exists
+      if [[ -f $tree/Cargo.toml ]]; then
+        crateCargoTOML=$(cargo metadata --format-version 1 --no-deps --manifest-path $tree/Cargo.toml | \
+        jq -r '.packages[] | select(.name == "${name}") | .manifest_path')
+      fi
+
+      # If the repository is not a workspace the package might be in a subdirectory.
+      if [[ -z $crateCargoTOML ]]; then
+        for manifest in $(find $tree -name "Cargo.toml"); do
+          echo Looking at $manifest
+          crateCargoTOML=$(cargo metadata --format-version 1 --no-deps --manifest-path "$manifest" | jq -r '.packages[] | select(.name == "${name}") | .manifest_path' || :)
+          if [[ ! -z $crateCargoTOML ]]; then
+            break
+          fi
+        done
 
-  parsedAndVendoredRemotePackages = map parseAndVendorRemotePackage remotePackages;
+        if [[ -z $crateCargoTOML ]]; then
+          >&2 echo "Cannot find path for crate '${name}-${version}' in the tree in: $tree"
+          exit 1
+        fi
+      fi
 
-  vendoredSourcesDirectory = linkFarm "vendored-sources" (lib.forEach parsedAndVendoredRemotePackages (p: {
-    name = pathForPackage p.parsed;
-    path = p.vendored.tree;
-  }));
+      echo Found crate ${name} at $crateCargoTOML
+      tree=$(dirname $crateCargoTOML)
 
-  aggregateConfigFragment =
-    let
-      base = {
-        source.crates-io.replace-with = "vendored-sources";
-        source.vendored-sources.directory = vendoredSourcesDirectory;
-      };
-    in
-      lib.fold lib.recursiveUpdate base
-        (map (p: p.vendored.configFragment) parsedAndVendoredRemotePackages);
+      cp -prvd "$tree/" $out
+      chmod u+w $out
 
-  pathForPackage = { name, version, checksum, source }:
-    let
-      suffixLen = 8;
-      suffix = {
-        git = lib.substring 0 suffixLen source.value.rev;
-        registry = lib.substring 0 suffixLen checksum;
-      }.${source.type};
-    in
-      "${name}-${version}-${suffix}";
+      # HACK: Recreate some of .git for crates which try to detect whether they're a git dependency
+      mkdir $out/.git
+      echo "${rev}" > $out/.git/HEAD
+
+      # Cargo is happy with empty metadata.
+      printf '{"files": {}, "package": null}' > "$out/.cargo-checksum.json"
+    '';
 
 in {
-  inherit vendoredSourcesDirectory;
-  configFragment = aggregateConfigFragment;
+  lockfile = if lockfile != null then lockfile else builtins.toFile "Cargo.lock" lockfileContents;
+  inherit lockfileValue;
+  configFragment = vendoredSources;
 }
diff --git a/hacking/nix/scope/dafny/default.nix b/hacking/nix/scope/dafny/default.nix
index b46379d09..758ac54a5 100644
--- a/hacking/nix/scope/dafny/default.nix
+++ b/hacking/nix/scope/dafny/default.nix
@@ -22,7 +22,7 @@ let
       url = "https://github.com/coliasgroup/dafny.git";
       rev = "02d0a578fdf594a38c7c72d7ad56e1a62e464f44";
       local = sources.localRoot + "/dafny";
-      inherit useLocal;
+      # inherit useLocal;
     };
 
     postPatch = ''
diff --git a/hacking/nix/scope/default.nix b/hacking/nix/scope/default.nix
index 53d33d810..8a220d388 100644
--- a/hacking/nix/scope/default.nix
+++ b/hacking/nix/scope/default.nix
@@ -8,9 +8,9 @@
 , buildPlatform, hostPlatform, targetPlatform
 , pkgsBuildBuild
 , callPackage
-, linkFarm
+, runCommand, linkFarm
+, makeWrapper
 , overrideCC, libcCross
-, treeHelpers
 , fetchurl
 , qemu
 }:
@@ -31,27 +31,10 @@ let
 in
 
 let
-  fenixRev = "260b00254fc152885283b0d2aec78547a1f77efd";
+  fenixRev = "9af557bccdfa8fb6a425661c33dbae46afef0afa";
   fenixSource = fetchTarball "https://github.com/nix-community/fenix/archive/${fenixRev}.tar.gz";
   fenix = import fenixSource {};
 
-  rustToolchainParams = {
-    channel = "nightly";
-    date = "2024-05-01";
-    sha256 = "sha256-6lRcCTSUmWOh0GheLMTZkY7JC273pWLp2s98Bb2REJQ=";
-  };
-
-  mkRustToolchain = target: fenix.targets.${target}.toolchainOf rustToolchainParams;
-
-  # TODO
-  # rustToolchain = fenix.combine ([
-  #   (mkRustToolchain hostPlatform.config).completeToolchain
-  # ] ++ lib.optionals (hostPlatform.config != targetPlatform.config && !targetPlatform.isNone) [
-  #   (mkRustToolchain targetPlatform.config).rust-std
-  # ]);
-
-  rustToolchain = (mkRustToolchain buildPlatform.config).completeToolchain;
-
 in
 
 superCallPackage ../rust-utils {} self //
@@ -71,7 +54,46 @@ superCallPackage ../rust-utils {} self //
 
   ### rust
 
-  defaultRustToolchain = rustToolchain;
+  inherit fenix;
+
+  topLevelRustToolchainFile = ../../../rust-toolchain.toml;
+
+  defaultRustToolchain = fenix.fromToolchainFile {
+    file = topLevelRustToolchainFile;
+    sha256 = "sha256-6lRcCTSUmWOh0GheLMTZkY7JC273pWLp2s98Bb2REJQ=";
+  };
+
+  defaultRustEnvironment = elaborateRustEnvironment (mkDefaultElaborateRustEnvironmentArgs {
+    rustToolchain = defaultRustToolchain;
+  } // {
+    channel = (builtins.fromTOML (builtins.readFile topLevelRustToolchainFile)).toolchain.channel;
+    compilerRTSource = mkCompilerRTSource {
+      version = "18.0-2024-02-13";
+      hash = "sha256-fbq8H86WT13KsXJECHbcbFkqFseLvV/EC2kihTL2lgI=";
+    };
+    mkCustomTargetPath = customTargetTripleTripleName:
+      let
+        fname = "${customTargetTripleTripleName}.json";
+      in
+        linkFarm "targets" [
+          { name = fname; path = sources.srcRoot + "/support/targets/${fname}"; }
+        ];
+  });
+
+  mkDefaultElaborateRustEnvironmentArgs = { rustToolchain }: rec {
+    inherit rustToolchain;
+
+    chooseLinker = { targetTriple, platform }:
+      if platform.isNone
+      then "${rustToolchain}/lib/rustlib/${buildPlatform.config}/bin/rust-lld"
+      else null;
+
+    vendoredSuperLockfile = vendoredTopLevelLockfile;
+  };
+
+  topLevelLockfile = sources.srcRoot + "/Cargo.lock";
+
+  vendoredTopLevelLockfile = vendorLockfile { lockfile = topLevelLockfile; };
 
   rustTargetArchName = {
     aarch64 = "aarch64";
@@ -82,14 +104,12 @@ superCallPackage ../rust-utils {} self //
     ia32 = "i686";
   }."${seL4Arch}";
 
-  defaultRustTargetInfo =
-    if !hostPlatform.isNone
-    then mkBuiltinRustTargetInfo hostPlatform.config
-    else seL4RustTargetInfoWithConfig {};
+  mkSeL4CustomRustTargetTripleName = { microkit ? false, minimal ? false }:
+    "${rustTargetArchName}-sel4${lib.optionalString microkit "-microkit"}${lib.optionalString minimal "-minimal"}";
 
-  seL4RustTargetInfoWithConfig = { microkit ? false, minimal ? false }: mkCustomRustTargetInfo "${rustTargetArchName}-sel4${lib.optionalString microkit "-microkit"}${lib.optionalString minimal "-minimal"}";
+  mkSeL4RustTargetTriple = args: mkCustomRustTargetTriple (mkSeL4CustomRustTargetTripleName args);
 
-  bareMetalRustTargetInfo = mkBuiltinRustTargetInfo {
+  bareMetalBuiltinRustTargetTriple = {
     aarch64 = "aarch64-unknown-none";
     aarch32 = "armv7a-none-eabi"; # armv7a-none-eabihf?
     riscv64 = "riscv64${hostPlatform.this.rustTargetRiscVArch}-unknown-none-elf";
@@ -98,44 +118,55 @@ superCallPackage ../rust-utils {} self //
     ia32 = "i686-unknown-linux-gnu"; # HACK
   }."${seL4Arch}";
 
-  mkBuiltinRustTargetInfo = name: {
-    inherit name;
-    path = null;
-  };
+  bareMetalRustTargetTriple = mkBuiltinRustTargetTriple bareMetalBuiltinRustTargetTriple;
 
-  mkCustomRustTargetInfo = name: {
-    inherit name;
-    path =
-      let
-        fname = "${name}.json";
-      in
-        linkFarm "targets" [
-          { name = fname; path = sources.srcRoot + "/support/targets/${fname}"; }
-        ];
-  };
+  defaultRustTargetTriple =
+    if hostPlatform.isNone
+    then mkSeL4RustTargetTriple {}
+    else mkBuiltinRustTargetTriple hostPlatform.config;
 
-  chooseLinkerForRustTarget = { rustToolchain, rustTargetName, platform }:
-    if platform.isNone
-    then "${rustToolchain}/lib/rustlib/${buildPlatform.config}/bin/rust-lld"
-    else null;
+  mkMkCustomTargetPathForEnvironment = { rustEnvironment }:
+    let
+      tool = buildCrateInLayers rec {
+        inherit rustEnvironment;
+        rootCrate = crates.sel4-generate-target-specs;
+        lastLayerModifications = crateUtils.elaborateModifications {
+          # HACK
+          modifyDerivation = drv: drv.overrideAttrs (self: super: {
+            nativeBuildInputs = (super.nativeBuildInputs or []) ++ [ makeWrapper ];
+            postBuild = ''
+              wrapProgram $out/bin/${rootCrate.name} \
+                --prefix LD_LIBRARY_PATH : ${lib.makeLibraryPath [ rustEnvironment.rustToolchain ]} 
+            '';
+          });
+        };
+      };
+
+      dir = runCommand "targest" {
+        nativeBuildInputs = [ tool ];
+      } ''
+        mkdir $out
+        sel4-generate-target-specs write --target-dir $out --all
+      '';
+    in
+      customTargetTripleTripleName:
+        let
+          fname = "${customTargetTripleTripleName}.json";
+        in
+          linkFarm "targets" [
+            { name = fname; path = builtins.toFile fname (builtins.readFile "${dir}/${fname}"); }
+          ];
 
   inherit (callPackage ./crates.nix {}) crates globalPatchSection publicCrates publicCratesTxt;
 
   distribution = callPackage ./distribution.nix {};
 
-  buildCrateInLayersHere = buildCrateInLayers {
-    # TODO pass vendored lockfile instead
-    superLockfile = topLevelLockfile;
-  };
-
-  topLevelLockfile = sources.srcRoot + "/Cargo.lock";
-
-  vendoredTopLevelLockfile = vendorLockfile { lockfile = topLevelLockfile; };
-
   publicCratesCargoLock = pruneLockfile {
-    superLockfile = topLevelLockfile;
-    superLockfileVendoringConfig = vendoredTopLevelLockfile.configFragment;
+    vendoredSuperLockfile = vendoredTopLevelLockfile;
     rootCrates = lib.attrValues publicCrates;
+    extraManifest = {
+      patch = globalPatchSection;
+    };
   };
 
   # HACK: reduce closure size, llvm now depends on targetPackage
@@ -145,11 +176,13 @@ superCallPackage ../rust-utils {} self //
 
   capdl-tool = callBuildBuildPackage ./capdl-tool {};
 
+  verus = callBuildBuildPackage ./verus {};
+
   dafny = callBuildBuildPackage ./dafny {};
 
   ### local tools
 
-  mkTool = rootCrate: buildCrateInLayersHere {
+  mkTool = rootCrate: buildCrateInLayers {
     inherit rootCrate;
   };
 
diff --git a/hacking/nix/scope/shell-for-hacking.nix b/hacking/nix/scope/shell-for-hacking.nix
index bc7c91e5a..a56026f73 100644
--- a/hacking/nix/scope/shell-for-hacking.nix
+++ b/hacking/nix/scope/shell-for-hacking.nix
@@ -21,6 +21,8 @@
 
 , openssl
 
+, verus
+
 , shellForMakefile
 }:
 
@@ -41,9 +43,16 @@ mkShell (shellForMakefile.apply {
     strace
     cntr
     cachix
+    verus
   ];
 
   buildInputs = [
     openssl
   ];
+
+  shellHook = ''
+    vargo() {
+      cargo +${verus.rustEnvironment.channel} "$@"
+    }
+  '';
 })
diff --git a/hacking/nix/scope/verus/default.nix b/hacking/nix/scope/verus/default.nix
new file mode 100644
index 000000000..4f4826e08
--- /dev/null
+++ b/hacking/nix/scope/verus/default.nix
@@ -0,0 +1,97 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ lib, stdenv
+, callPackage
+, makeWrapper
+, singular
+
+, crateUtils
+, vendorLockfile
+, sources
+, fenix
+, elaborateRustEnvironment
+, mkDefaultElaborateRustEnvironmentArgs
+, mkMkCustomTargetPathForEnvironment
+}:
+
+let
+  z3 = callPackage ./z3.nix {};
+
+  rustToolchainAttrs = builtins.fromTOML (builtins.readFile (src + "/rust-toolchain.toml"));
+
+  rustToolchain = fenix.fromToolchainFile {
+    file = crateUtils.toTOMLFile "rust-toolchain.toml" (crateUtils.clobber [
+      rustToolchainAttrs
+      {
+        toolchain.components = rustToolchainAttrs.toolchain.components ++ [ "rust-src" ];
+      }
+    ]);
+    sha256 = "sha256-e4mlaJehWBymYxJGgnbuCObVlqMlQSilZ8FljG9zPHY=";
+  };
+
+  rustEnvironment = lib.fix (self: elaborateRustEnvironment (mkDefaultElaborateRustEnvironmentArgs {
+    inherit rustToolchain;
+  } // {
+    inherit (rustToolchainAttrs.toolchain) channel;
+    mkCustomTargetPath = mkMkCustomTargetPathForEnvironment {
+      rustEnvironment = self;
+    };
+  }));
+
+  src = sources.fetchGit {
+    url = "https://github.com/coliasgroup/verus.git";
+    rev = "fdac1c3c52e639bf3e835802f63b43520379b1a1"; # branch dev
+  };
+
+  lockfile = vendorLockfile {
+    inherit rustToolchain;
+    lockfile = src + "/source/Cargo.lock";
+  };
+
+  config = crateUtils.toTOMLFile "config" lockfile.configFragment;
+
+in
+stdenv.mkDerivation {
+  name = "verus";
+
+  inherit src;
+
+  sourceRoot = "source/source"; # looks funny
+
+  nativeBuildInputs = [
+    rustToolchain
+    makeWrapper
+  ];
+
+  dontConfigure = true;
+
+  buildPhase = ''
+    RUSTC_BOOTSTRAP=1 \
+      cargo build \
+        -Z unstable-options \
+        --config ${config} \
+        -p verus-driver -p cargo-verus \
+        --features=verus-driver/singular \
+        --release \
+        --out-dir $out/bin
+  '';
+
+  installPhase = ''
+    # wrap cargo-verus with these so that it can properly assess whether verus-driver fingerprints are dirty
+    wrapProgram $out/bin/cargo-verus \
+      --set-default VERUS_Z3_PATH ${z3}/bin/z3 \
+      --set-default VERUS_SINGULAR_PATH ${singular}/bin/Singular
+
+    wrapProgram $out/bin/verus-driver \
+      --prefix LD_LIBRARY_PATH : ${lib.makeLibraryPath [ rustToolchain ]} # HACK
+  '';
+
+  passthru = {
+    inherit rustEnvironment;
+    rustToolchainChannel = rustToolchainAttrs.toolchain.channel;
+  };
+}
diff --git a/hacking/nix/scope/verus/z3.nix b/hacking/nix/scope/verus/z3.nix
new file mode 100644
index 000000000..ee36ba914
--- /dev/null
+++ b/hacking/nix/scope/verus/z3.nix
@@ -0,0 +1,47 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ stdenv, hostPlatform
+, fetchurl
+, autoPatchelfHook
+, unzip
+}:
+
+let
+  version = "4.12.5";
+
+  arch = {
+    "x86_64" = "x64";
+    "aarch64" = "arm64";
+  }.${hostPlatform.parsed.cpu.name};
+
+  filename = "z3-${version}-${arch}-glibc-2.35";
+
+in
+stdenv.mkDerivation {
+  pname = "z3";
+  inherit version;
+
+  src = fetchurl {
+    url = "https://github.com/Z3Prover/z3/releases/download/z3-${version}/${filename}.zip";
+    sha256 = "sha256-8DZXTV4gKckgT/81A8/mjd9B+m/euzm+7ZnhvzVbf+4=";
+  };
+
+  nativeBuildInputs = [
+    stdenv.cc.cc.lib
+    autoPatchelfHook
+    unzip
+  ];
+
+  dontConfigure = true;
+  dontBuild = true;
+
+  installPhase = ''
+    here=$(pwd)
+    cd $TMPDIR
+    mv $here $out
+  '';
+}
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 e1ec3cc08..2a61459be 100644
--- a/hacking/nix/scope/world/capdl/mk-small-capdl-initializer.nix
+++ b/hacking/nix/scope/world/capdl/mk-small-capdl-initializer.nix
@@ -11,7 +11,7 @@
 , serializeCapDLSpec
 , crateUtils
 , seL4Modifications
-, seL4RustTargetInfoWithConfig
+, mkSeL4RustTargetTriple
 }:
 
 { spec, fill }:
@@ -25,7 +25,7 @@ in mkTask {
 
   rootCrate = crates.sel4-capdl-initializer-with-embedded-spec;
 
-  rustTargetInfo = seL4RustTargetInfoWithConfig { minimal = true; };
+  targetTriple = mkSeL4RustTargetTriple { minimal = true; };
 
   release = true;
 
diff --git a/hacking/nix/scope/world/capdl/sel4-capdl-initializer.nix b/hacking/nix/scope/world/capdl/sel4-capdl-initializer.nix
index eb131abf6..f3d009694 100644
--- a/hacking/nix/scope/world/capdl/sel4-capdl-initializer.nix
+++ b/hacking/nix/scope/world/capdl/sel4-capdl-initializer.nix
@@ -10,14 +10,14 @@
 , mkTask, crates
 , crateUtils
 , seL4Modifications
-, seL4RustTargetInfoWithConfig
+, mkSeL4RustTargetTriple
 }:
 
 mkTask {
 
   rootCrate = crates.sel4-capdl-initializer;
 
-  rustTargetInfo = seL4RustTargetInfoWithConfig { minimal = true; };
+  targetTriple = mkSeL4RustTargetTriple { minimal = true; };
 
   release = true;
 
diff --git a/hacking/nix/scope/world/docs.nix b/hacking/nix/scope/world/docs.nix
index b30b6ca0e..3a304310b 100644
--- a/hacking/nix/scope/world/docs.nix
+++ b/hacking/nix/scope/world/docs.nix
@@ -9,82 +9,59 @@
 , rsync
 
 , crateUtils
-, defaultRustToolchain
-, defaultRustTargetInfo
+, defaultRustEnvironment
+, pruneLockfile, vendorLockfile
+, buildSysroot
 , libclangPath
-, vendorLockfile, pruneLockfile
 , crates
-, buildSysroot
-, seL4RustTargetInfoWithConfig
-
-, topLevelLockfile
-, vendoredTopLevelLockfile
 
+, mkSeL4RustTargetTriple
 , seL4RustEnvVars
 
 , worldConfig
 
-, seL4ConfigJSON
 , seL4Config
+, seL4ConfigJSON
 }:
 
 let
-  rustToolchain = defaultRustToolchain;
-
-  runtimes =
-    let
-      common = lib.optionals (!worldConfig.isMicrokit) [ "sel4-platform-info" ];
-    in [
-      { name = "none";
-        features = common ++ [];
-        rustTargetInfo = seL4RustTargetInfoWithConfig { minimal = false; };
-      }
-    ] ++ lib.optionals (hostPlatform.isAarch64 || hostPlatform.isx86_64) [
-      { name = "sel4-root-task";
-        features = common ++ [ "sel4-root-task" ];
-        rustTargetInfo = seL4RustTargetInfoWithConfig { minimal = false; };
-      }
-    ] ++ lib.optionals (worldConfig.isMicrokit or false) [
-      { name = "sel4-microkit";
-        features = common ++ [ "sel4-microkit" ];
-        rustTargetInfo = seL4RustTargetInfoWithConfig { microkit = true; minimal = true; };
-      }
-    ];
+  rustEnvironment = defaultRustEnvironment;
+  inherit (rustEnvironment) rustToolchain;
 
   rootCrate = crates.meta;
 
   mkView = { runtime ? null, minimal ? true }:
     let
       commonFeatures = lib.optionals (!worldConfig.isMicrokit) [ "sel4-platform-info" ];
-      rustTargetInfo = seL4RustTargetInfoWithConfig { microkit = runtime == "sel4-microkit"; inherit minimal; };
+      targetTriple = mkSeL4RustTargetTriple { microkit = runtime == "sel4-microkit"; inherit minimal; };
     in {
       inherit seL4ConfigJSON;
       inherit (seL4Config) PLAT SEL4_ARCH KERNEL_MCS;
-      hypervisorSupport = if seL4Config.ARCH_ARM then seL4Config.ARM_HYPERVISOR_SUPPORT else false;
-      targetName = rustTargetInfo.name;
-      targetJSON = "${rustTargetInfo.path}/${rustTargetInfo.name}.json";
+      inherit targetTriple;
+      targetJSON =  "${rustEnvironment.mkTargetPath targetTriple}/${targetTriple.name}.json";
       inherit runtime;
       rustdoc = buildDocs {
+        inherit targetTriple;
         features = commonFeatures ++ lib.optional (runtime != null) runtime;
-        inherit rustTargetInfo;
       };
     };
 
-  buildDocs = { features, rustTargetInfo }:
+  buildDocs = { targetTriple, features }:
     let
-      rustTargetName = rustTargetInfo.name;
-      rustTargetPath = rustTargetInfo.path;
-
-      lockfile = builtins.toFile "Cargo.lock" lockfileContents;
-      lockfileContents = builtins.readFile lockfileDrv;
-      lockfileDrv = pruneLockfile {
-        superLockfile = topLevelLockfile;
-        superLockfileVendoringConfig = vendoredTopLevelLockfile.configFragment;
+      prunedLockfile = pruneLockfile {
+        inherit (rustEnvironment) rustToolchain vendoredSuperLockfile;
         rootCrates = [ rootCrate ];
       };
 
+      vendoredLockfile = vendorLockfile {
+        inherit (rustEnvironment) rustToolchain;
+        lockfileContents = builtins.readFile prunedLockfile;
+      };
+
+      inherit (vendoredLockfile) lockfile;
+
       sysrootHost = buildSysroot {
-        inherit rustTargetInfo;
+        inherit targetTriple;
         release = false;
       };
 
@@ -92,8 +69,7 @@ let
 
       # TODO how does this work without std?
       # sysrootBuild = buildSysroot {
-      #   rustTargetName = buildPlatform.config;
-      #   rustTargetPath = emptyDirectory;
+      #   targetTriple = buildPlatform.config;
       #   release = false;
       # };
 
@@ -119,17 +95,19 @@ let
       src = crateUtils.collectReals (lib.attrValues rootCrate.closure);
 
       config = crateUtils.toTOMLFile "config" (crateUtils.clobber [
-        (crateUtils.baseConfig { inherit rustToolchain rustTargetName; })
-        (vendorLockfile { inherit lockfileContents; }).configFragment
+        (crateUtils.baseConfig {
+          inherit rustEnvironment targetTriple;
+        })
+        vendoredLockfile.configFragment
         {
           unstable.unstable-options = true;
 
-          target.${rustTargetName}.rustflags = [
+          target.${targetTriple.name}.rustflags = [
             "--sysroot" sysroot
           ];
 
           # TODO
-          # target.${rustTargetName}.rustdocflags = [
+          # target.${targetTriple.name}.rustdocflags = [
           build.rustdocflags = [
             "--sysroot" sysroot
           ];
@@ -143,15 +121,14 @@ let
       ] ++ lib.optionals (lib.length features > 0) [
         "--features" (lib.concatStringsSep "," features)
       ] ++ [
-        "--target" rustTargetName
+        "--target" targetTriple.name
       ]);
 
     in
       runCommandCC "rustdoc-view" ({
         depsBuildBuild = [ buildPackages.stdenv.cc ];
         nativeBuildInputs = [ rsync rustToolchain ];
-
-        RUST_TARGET_PATH = rustTargetPath;
+        RUST_TARGET_PATH = rustEnvironment.mkTargetPath targetTriple;
         LIBCLANG_PATH = libclangPath;
       } // seL4RustEnvVars)  ''
         target_dir=$(pwd)/target
diff --git a/hacking/nix/scope/world/instances/c.nix b/hacking/nix/scope/world/instances/c.nix
index a1d0fce92..7f2a99943 100644
--- a/hacking/nix/scope/world/instances/c.nix
+++ b/hacking/nix/scope/world/instances/c.nix
@@ -9,7 +9,7 @@
 
 , crateUtils, crates
 , mkTask, seL4Modifications
-, defaultRustTargetInfo
+, defaultRustTargetTriple
 
 , mkInstance
 
@@ -39,8 +39,8 @@ mkInstance {
 
     commonModifications = {
       modifyConfig = old: lib.recursiveUpdate old {
-        target.${defaultRustTargetInfo.name} = {
-          rustflags = (old.target.${defaultRustTargetInfo.name}.rustflags or []) ++ [
+        target.${defaultRustTargetTriple.name} = {
+          rustflags = (old.target.${defaultRustTargetTriple.name}.rustflags or []) ++ [
             # TODO
             # NOTE: won't work because cross gcc always uses hard-coded --with-ld
 
diff --git a/hacking/nix/scope/world/instances/default.nix b/hacking/nix/scope/world/instances/default.nix
index bcebd3d92..531ecbd1d 100644
--- a/hacking/nix/scope/world/instances/default.nix
+++ b/hacking/nix/scope/world/instances/default.nix
@@ -19,7 +19,7 @@
 
 , mkTask, mkSeL4KernelLoaderWithPayload
 , embedDebugInfo
-, seL4RustTargetInfoWithConfig, defaultRustTargetInfo
+, mkSeL4RustTargetTriple
 , worldConfig
 , seL4ForBoot
 , seL4Config
@@ -79,6 +79,8 @@ in rec {
     tests.root-task.panicking.byConfig.unwind.withAlloc
     tests.root-task.panicking.byConfig.unwind.withoutAlloc
     tests.root-task.c
+    tests.root-task.verus
+    tests.root-task.dafny
     tests.root-task.default-test-harness
     # tests.root-task.ring
     tests.capdl.threads
@@ -202,7 +204,11 @@ in rec {
           inherit byConfig automate simulate;
         };
 
-      c = maybe (haveFullRuntime && hostPlatform.isAarch64) (callPackage ./c.nix {
+      c = maybe haveFullRuntime (callPackage ./c.nix {
+        inherit canSimulate;
+      });
+
+      verus = maybe (haveFullRuntime && hostPlatform.is64bit) (callPackage ./verus.nix {
         inherit canSimulate;
       });
 
@@ -343,7 +349,7 @@ in rec {
         rootTask = mkTask {
           rootCrate = crates.example-root-task-without-runtime;
           release = false;
-          rustTargetInfo = seL4RustTargetInfoWithConfig { minimal = true; };
+          targetTriple = mkSeL4RustTargetTriple { minimal = true; };
         };
         extraPlatformArgs = lib.optionalAttrs canSimulate {
           canAutomateSimply = true;
diff --git a/hacking/nix/scope/world/instances/microkit/banscii/default.nix b/hacking/nix/scope/world/instances/microkit/banscii/default.nix
index 6eab754c4..94e3fb567 100644
--- a/hacking/nix/scope/world/instances/microkit/banscii/default.nix
+++ b/hacking/nix/scope/world/instances/microkit/banscii/default.nix
@@ -13,7 +13,7 @@
 , sources
 , crates
 , crateUtils
-, seL4RustTargetInfoWithConfig
+, mkSeL4RustTargetTriple
 , mkMicrokitInstance
 , worldConfig
 
@@ -30,7 +30,7 @@ let
     assistant = mkPD rec {
       rootCrate = crates.banscii-assistant;
       release = true;
-      rustTargetInfo = seL4RustTargetInfoWithConfig { microkit = true; minimal = false; };
+      targetTriple = mkSeL4RustTargetTriple { microkit = true; minimal = false; };
     };
     artist = mkPD rec {
       rootCrate = crates.banscii-artist;
diff --git a/hacking/nix/scope/world/instances/microkit/default.nix b/hacking/nix/scope/world/instances/microkit/default.nix
index 1df51e81b..eac9b6e1c 100644
--- a/hacking/nix/scope/world/instances/microkit/default.nix
+++ b/hacking/nix/scope/world/instances/microkit/default.nix
@@ -13,7 +13,7 @@
 , sources
 , crates
 , crateUtils
-, seL4RustTargetInfoWithConfig
+, mkSeL4RustTargetTriple
 , mkMicrokitInstance
 , worldConfig
 , seL4Config
@@ -35,7 +35,7 @@ let
     #     };
     #   }
     # ];
-    rustTargetInfo = seL4RustTargetInfoWithConfig { microkit = true; minimal = true; };
+    targetTriple = mkSeL4RustTargetTriple { microkit = true; minimal = true; };
   } // args);
 
   inherit (worldConfig) isMicrokit;
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 9de77791c..e6319494a 100644
--- a/hacking/nix/scope/world/instances/microkit/http-server/default.nix
+++ b/hacking/nix/scope/world/instances/microkit/http-server/default.nix
@@ -20,7 +20,7 @@
 , seL4Config
 , worldConfig
 , mkMicrokitInstance
-, seL4RustTargetInfoWithConfig
+, mkSeL4RustTargetTriple
 
 , canSimulate
 , mkPD
@@ -29,7 +29,7 @@
 let
   inherit (worldConfig) isMicrokit;
 
-  rustTargetInfo = seL4RustTargetInfoWithConfig { microkit = true; };
+  targetTriple = mkSeL4RustTargetTriple { microkit = true; };
 
   content = builtins.fetchGit {
     url = "https://github.com/seL4/website_pr_hosting";
@@ -139,7 +139,7 @@ let
       #     modifications = seL4Modifications;
       #   }
       # ];
-      inherit rustTargetInfo;
+      inherit targetTriple;
       commonModifications = {
         modifyManifest = lib.flip lib.recursiveUpdate {
           patch.crates-io = {
@@ -158,22 +158,22 @@ let
     pl031-driver = mkPD {
       rootCrate = crates.microkit-http-server-example-pl031-driver;
       release = true;
-      inherit rustTargetInfo;
+      inherit targetTriple;
     };
     sp804-driver = mkPD {
       rootCrate = crates.microkit-http-server-example-sp804-driver;
       release = true;
-      inherit rustTargetInfo;
+      inherit targetTriple;
     };
     virtio-net-driver = mkPD {
       rootCrate = crates.microkit-http-server-example-virtio-net-driver;
       release = true;
-      inherit rustTargetInfo;
+      inherit targetTriple;
     };
     virtio-blk-driver = mkPD {
       rootCrate = crates.microkit-http-server-example-virtio-blk-driver;
       release = true;
-      inherit rustTargetInfo;
+      inherit targetTriple;
     };
   };
 
diff --git a/hacking/nix/scope/world/instances/verus.nix b/hacking/nix/scope/world/instances/verus.nix
new file mode 100644
index 000000000..a4a1a74a7
--- /dev/null
+++ b/hacking/nix/scope/world/instances/verus.nix
@@ -0,0 +1,42 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ lib
+
+, crates
+, crateUtils
+, seL4Modifications
+, mkTask
+
+, verus
+
+, mkInstance
+
+, canSimulate
+}:
+
+mkInstance {
+  rootTask = mkTask rec {
+    inherit (verus) rustEnvironment;
+
+    rootCrate = crates.tests-root-task-verus-task;
+    release = false;
+
+    verifyWithVerus = true;
+
+    layers = [
+      crateUtils.defaultIntermediateLayer
+      {
+        crates = [ "sel4-root-task" ];
+        modifications = seL4Modifications;
+      }
+    ];
+  };
+
+  extraPlatformArgs = lib.optionalAttrs canSimulate  {
+    canAutomateSimply = true;
+  };
+}
diff --git a/hacking/nix/scope/world/mk-task.nix b/hacking/nix/scope/world/mk-task.nix
index 4d042209b..680037e59 100644
--- a/hacking/nix/scope/world/mk-task.nix
+++ b/hacking/nix/scope/world/mk-task.nix
@@ -6,9 +6,10 @@
 
 { lib, buildPackages
 , runCommand, runCommandCC
-, buildCrateInLayersHere, buildSysroot, crateUtils
+, buildCrateInLayers, buildSysroot, crateUtils
 , crates
-, defaultRustTargetInfo
+, defaultRustEnvironment
+, defaultRustTargetTriple
 , libclangPath
 , seL4RustEnvVars
 } @ scopeArgs:
@@ -20,15 +21,16 @@ let
   '';
 in
 
-{ commonModifications ? {}
+{ rustEnvironment ? defaultRustEnvironment
+, targetTriple ? defaultRustTargetTriple
+
+, commonModifications ? {}
 , lastLayerModifications ? {}
 
 , extraProfile ? {}
 , replaceSysroot ? null
 , getELF ? if test then getELFDefaultForTest else getELFDefault
 
-, rustTargetInfo ? defaultRustTargetInfo
-
 , test ? false
 , release ? false
 , profile ? if release then "release" else (if test then "test" else "dev")
@@ -59,14 +61,16 @@ let
   ];
 
   sysroot = (if replaceSysroot != null then replaceSysroot else buildSysroot) {
-    inherit profile rustTargetInfo;
+    inherit rustEnvironment;
+    inherit targetTriple;
+    inherit profile;
     extraManifest = profiles;
   };
 
   theseCommonModifications = crateUtils.elaborateModifications {
     modifyManifest = lib.flip lib.recursiveUpdate profiles;
     modifyConfig = lib.flip lib.recursiveUpdate {
-      target.${rustTargetInfo.name}.rustflags = [
+      target.${targetTriple.name}.rustflags = [
         "--sysroot" sysroot
       ];
     };
@@ -103,8 +107,7 @@ let
 
 in
 
-buildCrateInLayersHere (prunedArgs // {
-
+buildCrateInLayers (prunedArgs // {
   commonModifications = crateUtils.composeModifications
     (crateUtils.elaborateModifications commonModifications)
     theseCommonModifications
diff --git a/hacking/nix/scope/world/sel4-kernel-loader.nix b/hacking/nix/scope/world/sel4-kernel-loader.nix
index b7ee1ed0a..1107af5bc 100644
--- a/hacking/nix/scope/world/sel4-kernel-loader.nix
+++ b/hacking/nix/scope/world/sel4-kernel-loader.nix
@@ -5,17 +5,15 @@
 #
 
 { lib, buildPackages, writeText
-, buildCrateInLayersHere, buildSysroot, crateUtils
-, crates, bareMetalRustTargetInfo
+, buildCrateInLayers, buildSysroot, crateUtils
+, crates, bareMetalRustTargetTriple
 , libclangPath
 , seL4RustEnvVars, seL4ForBoot, seL4ForUserspace
 , kernelLoaderConfig
 }:
 
 let
-  rustTargetInfo = bareMetalRustTargetInfo;
-  rustTargetName = rustTargetInfo.name;
-  rustTargetPath = rustTargetInfo.path;
+  targetTriple = bareMetalRustTargetTriple;
 
   rootCrate = crates.sel4-kernel-loader;
 
@@ -39,25 +37,25 @@ let
   ];
 
   sysroot = buildSysroot {
-    inherit profile rustTargetInfo;
+    inherit targetTriple;
+    inherit profile;
     extraManifest = profiles;
     alloc = false;
   };
 
 in
-buildCrateInLayersHere {
+buildCrateInLayers {
 
   inherit rootCrate;
+  inherit targetTriple;
   inherit profile;
 
-  rustTargetInfo = bareMetalRustTargetInfo;
-
   features = [];
 
   commonModifications = {
     modifyManifest = lib.flip lib.recursiveUpdate profiles;
     modifyConfig = lib.flip lib.recursiveUpdate {
-      target.${rustTargetName}.rustflags = [
+      target.${targetTriple.name}.rustflags = [
         "--sysroot" sysroot
       ];
     };
diff --git a/hacking/nix/scope/world/shell.nix b/hacking/nix/scope/world/shell.nix
index 7df6a671d..13f16e3f5 100644
--- a/hacking/nix/scope/world/shell.nix
+++ b/hacking/nix/scope/world/shell.nix
@@ -8,13 +8,13 @@
 , writeText, emptyFile
 , mkShell
 , defaultRustToolchain
-, defaultRustTargetInfo
-, bareMetalRustTargetInfo
+, defaultRustTargetTriple
+, bareMetalRustTargetTriple
 , libclangPath
 , sources
 , dummyCapDLSpec, serializeCapDLSpec
 , seL4RustEnvVars
-, seL4RustTargetInfoWithConfig
+, mkSeL4RustTargetTriple
 , worldConfig
 , seL4ForBoot
 , crateUtils
@@ -42,7 +42,7 @@ let
       targets = lib.flatten (
         lib.forEach [ true false ] (microkit:
           lib.forEach [ true false ] (minimal:
-            seL4RustTargetInfoWithConfig { inherit microkit minimal; })));
+            mkSeL4RustTargetTriple { inherit microkit minimal; })));
     in lib.listToAttrs (lib.forEach targets (target: {
       name = "BINDGEN_EXTRA_CLANG_ARGS_${target.name}";
       value = [ "-I${libcDir}/include" ];
@@ -55,9 +55,9 @@ let
 in
 mkShell (seL4RustEnvVars // kernelLoaderConfigEnvVars // capdlEnvVars // bindgenEnvVars // miscEnvVars // {
   # TODO
-  RUST_SEL4_TARGET = defaultRustTargetInfo.name;
+  RUST_SEL4_TARGET = defaultRustTargetTriple.name;
 
-  RUST_BARE_METAL_TARGET = bareMetalRustTargetInfo.name;
+  RUST_BARE_METAL_TARGET = bareMetalRustTargetTriple.name;
 
   HOST_CARGO_FLAGS = lib.concatStringsSep " " [
     "-Z" "build-std=core,alloc,compiler_builtins"
diff --git a/hacking/nix/top-level/default.nix b/hacking/nix/top-level/default.nix
index b6d99bd84..b344e3f17 100644
--- a/hacking/nix/top-level/default.nix
+++ b/hacking/nix/top-level/default.nix
@@ -44,7 +44,7 @@ in {
   prerequisites = aggregate "prerequisites" [
     pkgs.build.this.qemuForSeL4
     pkgs.build.this.capdl-tool
-    pkgs.build.this.vendoredTopLevelLockfile.vendoredSourcesDirectory
+    (builtins.toJSON (pkgs.build.this.vendoredTopLevelLockfile.configFragment))
 
     (lib.forEach (with pkgs.host; [ aarch64 aarch32 ]) (arch:
       arch.none.this.platUtils.rpi4.defaultBootLinks
diff --git a/hacking/nix/top-level/docs/default.nix b/hacking/nix/top-level/docs/default.nix
index e3bec2cb4..ec049c5ae 100644
--- a/hacking/nix/top-level/docs/default.nix
+++ b/hacking/nix/top-level/docs/default.nix
@@ -144,7 +144,7 @@ let
                   (lib.forEach views (view: ''
                     <tr>
                       <td>
-                        <a href="./views/${view.id}/${view.targetName}/doc/${metaCrateName}/index.html">rustdoc</a>
+                        <a href="./views/${view.id}/${view.targetTriple.name}/doc/${metaCrateName}/index.html">rustdoc</a>
                         <ul class=views>
                           ${lib.concatMapStrings mkEntry [
                             ''
@@ -152,7 +152,7 @@ let
                             ''
                             ''
                               rustc target spec:
-                              <a href="${mkJSONDataURI view.targetJSON}">${view.targetName}.json</a>
+                              <a href="${mkJSONDataURI view.targetJSON}">${view.targetTriple.name}.json</a>
                             ''
                             ''
                               seL4 config:
diff --git a/hacking/unstable-feature-monitoring/wishlist/src/lib.rs b/hacking/unstable-feature-monitoring/wishlist/src/lib.rs
index 4fdaa015c..2ea5e7828 100644
--- a/hacking/unstable-feature-monitoring/wishlist/src/lib.rs
+++ b/hacking/unstable-feature-monitoring/wishlist/src/lib.rs
@@ -31,13 +31,16 @@
     feature(riscv_ext_intrinsics),
 )]
 
-// For pointer::is_aligned_to?
+// For pointer::is_aligned_to. Stabilizes in 1.80.0.
+#![feature(pointer_is_aligned)]
+
+// For pointer::is_aligned_to
 //
 // For now, use:
 // ```
 // assert_eq!(ptr.cast::<()>().align_offset(x), 0)
 // ```
-// (See definitions of pointer::is_aligned_to?)
+// (See definitions of pointer::is_aligned_to)
 #![feature(pointer_is_aligned_to)]
 
 // Without these, the more invasive sel4_cfg_if! and sel4_cfg_wrap_match! must be used instead of