diff --git a/.reuse/dep5 b/.reuse/dep5
index d92aa7466..5e9d01510 100644
--- a/.reuse/dep5
+++ b/.reuse/dep5
@@ -14,6 +14,11 @@ Files:
 Copyright: 2023, Colias Group, LLC
 License: BSD-2-Clause
 
+Files:
+  hacking/nix/scope/dafny/deps.nix
+Copyright: 2024, Colias Group, LLC
+License: BSD-2-Clause
+
 Files:
   crates/examples/microkit/banscii/pds/assistant/core/assets/fonts/rock-salt/*.ttf
 Copyright: 2010 by Font Diner, Inc DBA Sideshow. All rights reserved.
diff --git a/Cargo.lock b/Cargo.lock
index 345d90ba1..9bc9b28cd 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -73,6 +73,12 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "allocator-api2"
+version = "0.2.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c6cb57a04249c6480766f7f7cef5467412af1490f8d1e243141daddada3264f"
+
 [[package]]
 name = "anstream"
 version = "0.6.13"
@@ -127,6 +133,12 @@ version = "1.0.81"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0952808a6c2afd1aa8947271f3a60f1a6763c7b912d210184c5149b5cf147247"
 
+[[package]]
+name = "as-any"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5b8a30a44e99a1c83ccb2a6298c563c888952a1c9134953db26876528f84c93a"
+
 [[package]]
 name = "async-unsync"
 version = "0.2.2"
@@ -457,6 +469,19 @@ dependencies = [
  "typenum",
 ]
 
+[[package]]
+name = "dafny_runtime"
+version = "0.1.0"
+source = "git+https://github.com/coliasgroup/dafny.git?tag=keep/02d0a578fdf594a38c7c72d7ad56e1a6#02d0a578fdf594a38c7c72d7ad56e1a62e464f44"
+dependencies = [
+ "as-any",
+ "hashbrown 0.14.5",
+ "itertools",
+ "num",
+ "once_cell",
+ "paste",
+]
+
 [[package]]
 name = "defmt"
 version = "0.3.6"
@@ -795,11 +820,12 @@ dependencies = [
 
 [[package]]
 name = "hashbrown"
-version = "0.14.3"
+version = "0.14.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604"
+checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1"
 dependencies = [
  "ahash",
+ "allocator-api2",
 ]
 
 [[package]]
@@ -864,7 +890,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7b0b929d511467233429c45a44ac1dcaa21ba0f5ba11e4879e6ed28ddb4f9df4"
 dependencies = [
  "equivalent",
- "hashbrown 0.14.3",
+ "hashbrown 0.14.5",
 ]
 
 [[package]]
@@ -878,6 +904,15 @@ dependencies = [
  "windows-sys",
 ]
 
+[[package]]
+name = "itertools"
+version = "0.11.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57"
+dependencies = [
+ "either",
+]
+
 [[package]]
 name = "itoa"
 version = "1.0.10"
@@ -1371,7 +1406,7 @@ checksum = "a6a622008b6e321afc04970976f62ee297fdbaa6f95318ca343e3eebb9648441"
 dependencies = [
  "crc32fast",
  "flate2",
- "hashbrown 0.14.3",
+ "hashbrown 0.14.5",
  "indexmap",
  "memchr",
  "ruzstd",
@@ -1393,6 +1428,12 @@ dependencies = [
  "ttf-parser",
 ]
 
+[[package]]
+name = "paste"
+version = "1.0.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
+
 [[package]]
 name = "peeking_take_while"
 version = "0.1.2"
@@ -2387,6 +2428,14 @@ dependencies = [
  "zerocopy 0.7.32",
 ]
 
+[[package]]
+name = "sel4-mod-in-out-dir"
+version = "0.1.0"
+dependencies = [
+ "quote",
+ "syn 1.0.109",
+]
+
 [[package]]
 name = "sel4-newlib"
 version = "0.1.0"
@@ -2960,6 +3009,24 @@ dependencies = [
  "sel4-root-task",
 ]
 
+[[package]]
+name = "tests-root-task-dafny-core"
+version = "0.1.0"
+dependencies = [
+ "dafny_runtime",
+ "num",
+ "sel4-mod-in-out-dir",
+]
+
+[[package]]
+name = "tests-root-task-dafny-task"
+version = "0.1.0"
+dependencies = [
+ "sel4",
+ "sel4-root-task",
+ "tests-root-task-dafny-core",
+]
+
 [[package]]
 name = "tests-root-task-default-test-harness"
 version = "0.1.0"
diff --git a/Cargo.toml b/Cargo.toml
index 80dd5a986..afada6897 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -57,6 +57,8 @@ members = [
     "crates/private/tests/root-task/backtrace",
     "crates/private/tests/root-task/c",
     "crates/private/tests/root-task/config",
+    "crates/private/tests/root-task/dafny/core",
+    "crates/private/tests/root-task/dafny/task",
     "crates/private/tests/root-task/default-test-harness",
     "crates/private/tests/root-task/loader",
     "crates/private/tests/root-task/panicking",
@@ -111,6 +113,7 @@ members = [
     "crates/sel4-microkit/macros",
     "crates/sel4-microkit/message",
     "crates/sel4-microkit/message/types",
+    "crates/sel4-mod-in-out-dir",
     "crates/sel4-newlib",
     "crates/sel4-one-ref-cell",
     "crates/sel4-panicking",
diff --git a/crates/private/tests/root-task/dafny/core/Cargo.nix b/crates/private/tests/root-task/dafny/core/Cargo.nix
new file mode 100644
index 000000000..b4c765c25
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/core/Cargo.nix
@@ -0,0 +1,19 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ mk, localCrates, dafnySource }:
+
+mk {
+  package.name = "tests-root-task-dafny-core";
+  dependencies = {
+    inherit (localCrates)
+      sel4-mod-in-out-dir
+      # dafny_runtime
+    ;
+    dafny_runtime = dafnySource;
+    num = { version = "0.4"; default-features = false; features = ["alloc"]; };
+  };
+}
diff --git a/crates/private/tests/root-task/dafny/core/Cargo.toml b/crates/private/tests/root-task/dafny/core/Cargo.toml
new file mode 100644
index 000000000..ee6a9c07b
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/core/Cargo.toml
@@ -0,0 +1,25 @@
+#
+# 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-dafny-core"
+version = "0.1.0"
+authors = ["Nick Spinale <nick.spinale@coliasgroup.com>"]
+edition = "2021"
+license = "BSD-2-Clause"
+
+[dependencies]
+num = { version = "0.4", default-features = false, features = ["alloc"] }
+sel4-mod-in-out-dir = { path = "../../../../../sel4-mod-in-out-dir" }
+
+[dependencies.dafny_runtime]
+git = "https://github.com/coliasgroup/dafny.git"
+tag = "keep/02d0a578fdf594a38c7c72d7ad56e1a6"
diff --git a/crates/private/tests/root-task/dafny/core/build.rs b/crates/private/tests/root-task/dafny/core/build.rs
new file mode 100644
index 000000000..e0cec6fb1
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/core/build.rs
@@ -0,0 +1,21 @@
+//
+// Copyright 2024, Colias Group, LLC
+//
+// SPDX-License-Identifier: BSD-2-Clause
+//
+
+use std::env;
+use std::fs;
+use std::path::PathBuf;
+
+const TRANSLATED_ENV: &str = "TRANSLATED";
+
+fn main() {
+    let translated_src = env::var(TRANSLATED_ENV).unwrap();
+    let out_dir = env::var("OUT_DIR").unwrap();
+    let translated_dst = PathBuf::from(&out_dir).join("translated.rs");
+    fs::copy(&translated_src, &translated_dst).unwrap();
+
+    println!("cargo:rerun-if-env-changed={TRANSLATED_ENV}");
+    println!("cargo:rerun-if-changed={}", translated_src);
+}
diff --git a/crates/private/tests/root-task/dafny/core/src/lib.rs b/crates/private/tests/root-task/dafny/core/src/lib.rs
new file mode 100644
index 000000000..cc12b522c
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/core/src/lib.rs
@@ -0,0 +1,32 @@
+//
+// Copyright 2024, Colias Group, LLC
+//
+// SPDX-License-Identifier: BSD-2-Clause
+//
+
+#![no_std]
+#![feature(proc_macro_hygiene)]
+
+use dafny_runtime::DafnyInt;
+use num::traits::cast::ToPrimitive;
+use sel4_mod_in_out_dir::in_out_dir;
+
+#[rustfmt::skip]
+#[in_out_dir]
+mod translated;
+
+pub fn max(a: usize, b: usize) -> usize {
+    translated::_module::_default::Max(&DafnyInt::from(a), &DafnyInt::from(b))
+        .to_usize()
+        .unwrap()
+}
+
+#[cfg(test)]
+mod tests {
+    use super::max;
+
+    #[test]
+    fn x() {
+        assert_eq!(max(13, 37), 37);
+    }
+}
diff --git a/crates/private/tests/root-task/dafny/hacking/.gitignore b/crates/private/tests/root-task/dafny/hacking/.gitignore
new file mode 100644
index 000000000..c25bec135
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/hacking/.gitignore
@@ -0,0 +1,7 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+/build/
diff --git a/crates/private/tests/root-task/dafny/hacking/Makefile b/crates/private/tests/root-task/dafny/hacking/Makefile
new file mode 100644
index 000000000..2f10c7615
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/hacking/Makefile
@@ -0,0 +1,61 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+top_level_dir := $(TOP_LEVEL_DIR)
+
+build_dir := build
+
+dafny_link := $(build_dir)/dafny
+dafny_bin := $(dafny_link)/bin/dafny
+
+dafny_name := core
+dafny_src := ../verified/$(dafny_name).dfy
+dafny_output_prefix := $(build_dir)/$(dafny_name)
+dafny_output := $(dafny_output_prefix)-rust/src/$(dafny_name).rs
+dafny_dst := $(build_dir)/translated.rs
+
+.PHONY: none
+none:
+
+.PHONY: clean
+clean:
+	rm -rf $(build_dir)
+
+FORCE: ;
+
+$(build_dir):
+	mkdir -p $@
+
+$(dafny_link): FORCE | $(build_dir)
+	nix-build $(top_level_dir) -A pkgs.build.this.dafny -o $@
+
+$(dafny_output): FORCE | $(build_dir)
+	$(dafny_bin) translate rs $(dafny_src) -o $(dafny_output_prefix)
+
+$(dafny_dst): $(dafny_output)
+	cp $< $@
+
+# # #
+
+.PHONY: dafny
+dafny: $(dafny_link)
+
+.PHONY: translate
+translate: $(dafny_dst)
+
+.PHONY: test
+test:
+	cargo test -p tests-root-task-dafny-core
+
+.PHONY: run
+run:
+	set -eu; \
+	script=$$( \
+		nix-build $(top_level_dir) \
+			-A worlds.aarch64.default.instances.tests.root-task.dafny.automate \
+			--no-out-link \
+	); \
+	$$script
diff --git a/crates/private/tests/root-task/dafny/hacking/shell.nix b/crates/private/tests/root-task/dafny/hacking/shell.nix
new file mode 100644
index 000000000..88b9d8155
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/hacking/shell.nix
@@ -0,0 +1,19 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+let
+  topLevelDir = ../../../../../..;
+  topLevel = import topLevelDir {};
+
+in
+topLevel.worlds.default.shell.overrideAttrs (self: super: {
+  nativeBuildInputs = (super.nativeBuildInputs or []) ++ [
+    topLevel.pkgs.build.dafny
+  ];
+
+  TOP_LEVEL_DIR = toString topLevelDir;
+  TRANSLATED = toString ./build/translated.rs;
+})
diff --git a/crates/private/tests/root-task/dafny/task/Cargo.nix b/crates/private/tests/root-task/dafny/task/Cargo.nix
new file mode 100644
index 000000000..0e255f280
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/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-dafny-task";
+  dependencies = {
+    inherit (localCrates)
+      sel4
+      sel4-root-task
+      tests-root-task-dafny-core
+    ;
+  };
+}
diff --git a/crates/private/tests/root-task/dafny/task/Cargo.toml b/crates/private/tests/root-task/dafny/task/Cargo.toml
new file mode 100644
index 000000000..8a76a89ee
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/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-dafny-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-dafny-core = { path = "../core" }
diff --git a/crates/private/tests/root-task/dafny/task/src/main.rs b/crates/private/tests/root-task/dafny/task/src/main.rs
new file mode 100644
index 000000000..ad840b5a9
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/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_dafny_core::max(13, 37), 37);
+
+    debug_println!("TEST_PASS");
+    sel4::init_thread::suspend_self()
+}
diff --git a/crates/private/tests/root-task/dafny/verified/core.dfy b/crates/private/tests/root-task/dafny/verified/core.dfy
new file mode 100644
index 000000000..bb044840c
--- /dev/null
+++ b/crates/private/tests/root-task/dafny/verified/core.dfy
@@ -0,0 +1,17 @@
+//
+// Copyright 2024, Colias Group, LLC
+// Copyright (c) Microsoft Corporation
+//
+// SPDX-License-Identifier: MIT
+//
+
+method Max(a: int, b:int) returns (c: int)
+  ensures a < b  ==> c == b
+  ensures b <= a ==> c == a
+{
+  if (a < b) {
+    return b;
+  } else {
+    return a;
+  }
+}
diff --git a/crates/sel4-mod-in-out-dir/Cargo.nix b/crates/sel4-mod-in-out-dir/Cargo.nix
new file mode 100644
index 000000000..2a4d6db6e
--- /dev/null
+++ b/crates/sel4-mod-in-out-dir/Cargo.nix
@@ -0,0 +1,16 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ mk, versions }:
+
+mk {
+  package.name = "sel4-mod-in-out-dir";
+  lib.proc-macro = true;
+  dependencies = {
+    inherit (versions) quote;
+    syn = { version = versions.syn; features = [ "full" ]; };
+  };
+}
diff --git a/crates/sel4-mod-in-out-dir/Cargo.toml b/crates/sel4-mod-in-out-dir/Cargo.toml
new file mode 100644
index 000000000..38711ab0b
--- /dev/null
+++ b/crates/sel4-mod-in-out-dir/Cargo.toml
@@ -0,0 +1,24 @@
+#
+# 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 = "sel4-mod-in-out-dir"
+version = "0.1.0"
+authors = ["Nick Spinale <nick.spinale@coliasgroup.com>"]
+edition = "2021"
+license = "BSD-2-Clause"
+
+[lib]
+proc-macro = true
+
+[dependencies]
+quote = "1.0.23"
+syn = { version = "1.0.107", features = ["full"] }
diff --git a/crates/sel4-mod-in-out-dir/src/lib.rs b/crates/sel4-mod-in-out-dir/src/lib.rs
new file mode 100644
index 000000000..b5043c087
--- /dev/null
+++ b/crates/sel4-mod-in-out-dir/src/lib.rs
@@ -0,0 +1,72 @@
+//
+// Copyright 2024, Colias Group, LLC
+//
+// SPDX-License-Identifier: BSD-2-Clause
+//
+
+use std::env;
+use std::path::Path;
+
+use proc_macro::TokenStream;
+use quote::quote;
+use syn::parse::{Error, Parse, ParseStream};
+use syn::{parse_macro_input, ItemMod, MetaNameValue, Result};
+
+/// Set a module's `#[path]` relative to `$OUT_DIR`.
+///
+/// The following is not supported by rustc:
+/// ```ignore
+/// #[path = concat!(env!("OUT_DIR"), "/foo.rs")]
+/// mod foo;
+/// ```
+
+/// This macro does exactly that:
+/// ```ignore
+/// #[in_out_dir]
+/// mod foo;
+/// ```
+
+/// This works too:
+/// ```ignore
+/// #[in_out_dir(relative_path = "path/to/bar.rs")]
+/// mod foo;
+/// ```
+#[proc_macro_attribute]
+pub fn in_out_dir(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let input = parse_macro_input!(attr as Input);
+    let item_mod = parse_macro_input!(item as ItemMod);
+    let relative_path = input
+        .relative_path
+        .unwrap_or_else(|| format!("{}.rs", item_mod.ident));
+    let path = Path::new(&env::var("OUT_DIR").unwrap()).join(relative_path);
+    let path = path.to_str().unwrap();
+    quote!(
+        #[path = #path]
+        #item_mod
+    )
+    .into()
+}
+
+struct Input {
+    relative_path: Option<String>,
+}
+
+impl Parse for Input {
+    fn parse(input: ParseStream) -> Result<Self> {
+        let relative_path = if input.is_empty() {
+            None
+        } else {
+            let name_value = input.parse::<MetaNameValue>()?;
+            let path = name_value.path;
+            if !path.is_ident("relative_path") {
+                return Err(Error::new_spanned(path, "unrecognized argument"));
+            }
+            let lit = name_value.lit;
+            match lit {
+                syn::Lit::Str(s) => Some(s.value()),
+                _ => return Err(Error::new_spanned(lit, "value must be a string literal")),
+            }
+        };
+        Ok(Self { relative_path })
+    }
+}
diff --git a/hacking/cargo-manifest-management/manifest-scope.nix b/hacking/cargo-manifest-management/manifest-scope.nix
index 82ca0491e..2ee305280 100644
--- a/hacking/cargo-manifest-management/manifest-scope.nix
+++ b/hacking/cargo-manifest-management/manifest-scope.nix
@@ -213,4 +213,9 @@ in rec {
     default-features = false;
     inherit features;
   };
+
+  dafnySource = {
+    git = "https://github.com/coliasgroup/dafny.git";
+    tag = "keep/02d0a578fdf594a38c7c72d7ad56e1a6"; # branch dev
+  };
 }
diff --git a/hacking/cargo-manifest-management/manual-manifests.nix b/hacking/cargo-manifest-management/manual-manifests.nix
index ab12e7b96..b91b5cc71 100644
--- a/hacking/cargo-manifest-management/manual-manifests.nix
+++ b/hacking/cargo-manifest-management/manual-manifests.nix
@@ -15,4 +15,5 @@ in {
   # rustls = relativeToTmpSrc "rustls/rustls";
   # lock_api = relativeToTmpSrc "parking_lot/lock_api";
   # volatile = relativeToTmpSrc "volatile";
+  # dafny_runtime = relativeToTmpSrc "dafny/Source/DafnyRuntime/DafnyRuntimeRust";
 }
diff --git a/hacking/nix/scope/dafny/default.nix b/hacking/nix/scope/dafny/default.nix
new file mode 100644
index 000000000..b46379d09
--- /dev/null
+++ b/hacking/nix/scope/dafny/default.nix
@@ -0,0 +1,77 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ lib
+, buildDotnetModule
+, fetchFromGitHub
+, writeScript
+, jdk11
+, z3
+, sources
+}:
+
+let
+  f = { useLocal ? false }: buildDotnetModule rec {
+    pname = "Dafny";
+    version = "4.6.0";
+
+    src = sources.fetchGit {
+      url = "https://github.com/coliasgroup/dafny.git";
+      rev = "02d0a578fdf594a38c7c72d7ad56e1a62e464f44";
+      local = sources.localRoot + "/dafny";
+      inherit useLocal;
+    };
+
+    postPatch = ''
+      cp ${
+        writeScript "fake-gradlew-for-dafny" ''
+          mkdir -p build/libs/
+          javac $(find -name "*.java" | grep "^./src/main") -d classes
+          jar cf build/libs/DafnyRuntime-${version}.jar -C classes dafny
+        ''} Source/DafnyRuntime/DafnyRuntimeJava/gradlew
+
+      # Needed to fix
+      # "error NETSDK1129: The 'Publish' target is not supported without
+      # specifying a target framework. The current project targets multiple
+      # frameworks, you must specify the framework for the published
+      # application."
+      substituteInPlace Source/DafnyRuntime/DafnyRuntime.csproj \
+        --replace TargetFrameworks TargetFramework \
+        --replace "netstandard2.0;net452" net6.0
+    '';
+
+    nativeBuildInputs = [
+      jdk11
+    ];
+
+    nugetDeps = ./deps.nix;
+
+    # Build just these projects. Building Source/Dafny.sln includes a bunch of
+    # unnecessary components like tests.
+    projectFile = [
+      "Source/Dafny/Dafny.csproj"
+      "Source/DafnyRuntime/DafnyRuntime.csproj"
+      # "Source/DafnyLanguageServer/DafnyLanguageServer.csproj"
+    ];
+
+    executables = [ "Dafny" ];
+
+    # Help Dafny find z3
+    makeWrapperArgs = [ "--prefix PATH : ${lib.makeBinPath [ z3 ]}" ];
+
+    postFixup = ''
+      ln -s "$out/bin/Dafny" "$out/bin/dafny" || true
+    '';
+
+    passthru = {
+      local = f { useLocal = true; };
+      remote = f { useLocal = false; };
+    };
+  };
+
+in f {
+  # useLocal = true;
+}
diff --git a/hacking/nix/scope/dafny/deps.nix b/hacking/nix/scope/dafny/deps.nix
new file mode 100644
index 000000000..0c96fca4e
--- /dev/null
+++ b/hacking/nix/scope/dafny/deps.nix
@@ -0,0 +1,182 @@
+# This file was automatically generated by passthru.fetch-deps.
+# Please dont edit it manually, your changes might get overwritten!
+
+{ fetchNuGet }: [
+  (fetchNuGet { pname = "Boogie"; version = "3.1.3"; sha256 = "0xzc7s0rjb8dhdkdf71g6pdsnyhbl534xpwd8gbx6g16a87iqx6i"; })
+  (fetchNuGet { pname = "Boogie.AbstractInterpretation"; version = "3.1.6"; sha256 = "1c6z13dz0sbkmk4ay64aihy7s7xlfdvhpcknxhw1m1b0yly5qj6b"; })
+  (fetchNuGet { pname = "Boogie.BaseTypes"; version = "3.1.6"; sha256 = "1hxcpc45f32g3jpaw7mg6k9qsppcb3p20wxv4d4dc3nz0r52lrmr"; })
+  (fetchNuGet { pname = "Boogie.CodeContractsExtender"; version = "3.1.6"; sha256 = "1qk7w7c40fpkvvarbgi1bkdcxpn12r0lqngpwwjw8i7nk84ni5gl"; })
+  (fetchNuGet { pname = "Boogie.Concurrency"; version = "3.1.6"; sha256 = "11981gfa0n4s214yilnxqhh1clr4l78iqlws6gv01z1n6rxgbyla"; })
+  (fetchNuGet { pname = "Boogie.Core"; version = "3.1.6"; sha256 = "0sgj6i1hvp90g2zfqs1aly500xnv3fq9d4cfgii5kpza8vgm7w4g"; })
+  (fetchNuGet { pname = "Boogie.ExecutionEngine"; version = "3.1.6"; sha256 = "08vxxwcnkykcngihkp0bvfwkgwxb3nnqjp5f1vz4bnw708xs0ydg"; })
+  (fetchNuGet { pname = "Boogie.Graph"; version = "3.1.6"; sha256 = "0fzj65pnky8i83jj2h9nszij25a46z68fy2sm3pxwlg678nmx2jz"; })
+  (fetchNuGet { pname = "Boogie.Houdini"; version = "3.1.6"; sha256 = "0lfljb9brnr79hp1f0ff6fcy51ml66pjj102jk4pqpmsjwvcjx43"; })
+  (fetchNuGet { pname = "Boogie.Model"; version = "3.1.6"; sha256 = "0546b27mxv97v7qilb1carbwip0q7sz9zz7sxizpww6yc3j8w8if"; })
+  (fetchNuGet { pname = "Boogie.Provers.LeanAuto"; version = "3.1.6"; sha256 = "1x1f35g0kxzhxvw4icmbvkik16py47j6h04gj0ckwbny9qmglaby"; })
+  (fetchNuGet { pname = "Boogie.Provers.SMTLib"; version = "3.1.6"; sha256 = "0mqlpwfxgv9dd773254rrbgbjb5mpa3xkvlq32ml752h36j8m2r9"; })
+  (fetchNuGet { pname = "Boogie.VCExpr"; version = "3.1.6"; sha256 = "0p7axpjn4qg191bs7b33zf9l336bdznvxp3305z2ssnkakjx247h"; })
+  (fetchNuGet { pname = "Boogie.VCGeneration"; version = "3.1.6"; sha256 = "05z2lr92hbllikv65gh7m3i879fnn6pjn2acf133sijx9b1jixdb"; })
+  (fetchNuGet { pname = "CocoR"; version = "2014.12.24"; sha256 = "0ps8h7aawkcc1910qnh13llzb01pvgsjmg862pxp0p4wca2dn7a2"; })
+  (fetchNuGet { pname = "JetBrains.Annotations"; version = "2021.1.0"; sha256 = "07pnhxxlgx8spmwmakz37nmbvgyb6yjrbrhad5rrn6y767z5r1gb"; })
+  (fetchNuGet { pname = "MediatR"; version = "8.1.0"; sha256 = "0cqx7yfh998xhsfk5pr6229lcjcs1jxxyqz7dwskc9jddl6a2akp"; })
+  (fetchNuGet { pname = "Microsoft.Bcl.AsyncInterfaces"; version = "1.1.1"; sha256 = "0a1ahssqds2ympr7s4xcxv5y8jgxs7ahd6ah6fbgglj4rki1f1vw"; })
+  (fetchNuGet { pname = "Microsoft.Bcl.AsyncInterfaces"; version = "6.0.0"; sha256 = "15gqy2m14fdlvy1g59207h5kisznm355kbw010gy19vh47z8gpz3"; })
+  (fetchNuGet { pname = "Microsoft.CodeAnalysis.Analyzers"; version = "3.0.0"; sha256 = "0bbl0jpqywqmzz2gagld1p2gvdfldjfjmm25hil9wj2nq1zc4di8"; })
+  (fetchNuGet { pname = "Microsoft.CodeAnalysis.Common"; version = "3.7.0"; sha256 = "0882492nx6x68b0pkh3q5xaawz0b2l5x35r40722ignyjnvjydph"; })
+  (fetchNuGet { pname = "Microsoft.CodeAnalysis.CSharp"; version = "3.7.0"; sha256 = "0adw6rcag8wxydzyiyhls2mxaqkay5qlz25z1fxrlv5qnchqn0n5"; })
+  (fetchNuGet { pname = "Microsoft.DotNet.PlatformAbstractions"; version = "2.0.4"; sha256 = "1fdzln4im9hb55agzwchbfgm3vmngigmbpci5j89b0gqcxixmv8j"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Configuration"; version = "2.0.0"; sha256 = "0yssxq9di5h6xw2cayp5hj3l9b2p0jw9wcjz73rwk4586spac9s9"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Configuration"; version = "5.0.0"; sha256 = "01m9vzlq0vg0lhckj2dimwq42niwny8g3lm13c9a401hlyg90z1p"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Configuration.Abstractions"; version = "2.0.0"; sha256 = "1ilz2yrgg9rbjyhn6a5zh9pr51nmh11z7sixb4p7vivgydj9gxwf"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Configuration.Abstractions"; version = "5.0.0"; sha256 = "0fqxkc9pjxkqylsdf26s9q21ciyk56h1w33pz3v1v4wcv8yv1v6k"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Configuration.Binder"; version = "2.0.0"; sha256 = "1prvdbma6r18n5agbhhabv6g357p1j70gq4m9g0vs859kf44nrgc"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Configuration.CommandLine"; version = "5.0.0"; sha256 = "084hnz5l0vr15ay23rksqipslqnz3pp30w9hsirpx1iqdm5688mc"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Configuration.FileExtensions"; version = "5.0.0"; sha256 = "1wq229r3xcmm9wh9sqdpvmfv4qpbp2zms9x6xk7g7sbb8h32hnz3"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Configuration.Json"; version = "5.0.0"; sha256 = "0hq5i483bjbvprp1la9l3si82x1ydxbvkpfc7r3s7zgxg957fyp9"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.DependencyInjection"; version = "2.0.0"; sha256 = "018izzgykaqcliwarijapgki9kp2c560qv8qsxdjywr7byws5apq"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.DependencyInjection"; version = "5.0.0"; sha256 = "15sdwcyzz0qlybwbdq854bn3jk6kx7awx28gs864c4shhbqkppj4"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.DependencyInjection.Abstractions"; version = "2.0.0"; sha256 = "1pwrfh9b72k9rq6mb2jab5qhhi225d5rjalzkapiayggmygc8nhz"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.DependencyInjection.Abstractions"; version = "5.0.0"; sha256 = "17cz6s80va0ch0a6nqa1wbbbp3p8sqxb96lj4qcw67ivkp2yxiyj"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.DependencyModel"; version = "2.0.4"; sha256 = "041i1vlcibpzgalxxzdk81g5pgmqvmz2g61k0rqa2sky0wpvijx9"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.FileProviders.Abstractions"; version = "5.0.0"; sha256 = "01ahgd0b2z2zycrr2lcsq2cl59fn04bh51hdwdp9dcsdkpvnasj1"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.FileProviders.Physical"; version = "5.0.0"; sha256 = "00vii8148a6pk12l9jl0rhjp7apil5q5qcy7v1smnv17lj4p8szd"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.FileSystemGlobbing"; version = "5.0.0"; sha256 = "0lm6n9vbyjh0l17qcc2y9qwn1cns3dyjmkvbxjp0g9sll32kjpmb"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Logging"; version = "2.0.0"; sha256 = "1jkwjcq1ld9znz1haazk8ili2g4pzfdp6i7r7rki4hg3jcadn386"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Logging"; version = "5.0.0"; sha256 = "1qa1l18q2jh9azya8gv1p8anzcdirjzd9dxxisb4911i9m1648i3"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Logging.Abstractions"; version = "5.0.0"; sha256 = "1yza38675dbv1qqnnhqm23alv2bbaqxp0pb7zinjmw8j2mr5r6wc"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Options"; version = "2.0.0"; sha256 = "0g4zadlg73f507krilhaaa7h0jdga216syrzjlyf5fdk25gxmjqh"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Options"; version = "5.0.0"; sha256 = "1rdmgpg770x8qwaaa6ryc27zh93p697fcyvn5vkxp0wimlhqkbay"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Options.ConfigurationExtensions"; version = "2.0.0"; sha256 = "1isc3rjbzz60f7wbmgcwslx5d10hm5hisnk7v54vfi2bz7132gll"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Primitives"; version = "2.0.0"; sha256 = "1xppr5jbny04slyjgngxjdm0maxdh47vq481ps944d7jrfs0p3mb"; })
+  (fetchNuGet { pname = "Microsoft.Extensions.Primitives"; version = "5.0.0"; sha256 = "0swqcknyh87ns82w539z1mvy804pfwhgzs97cr3nwqk6g5s42gd6"; })
+  (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "1.0.1"; sha256 = "01al6cfxp68dscl15z7rxfw9zvhm64dncsw09a1vmdkacsa2v6lr"; })
+  (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "1.1.0"; sha256 = "08vh1r12g6ykjygq5d3vq09zylgb84l63k49jc4v8faw9g93iqqm"; })
+  (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "2.1.2"; sha256 = "1507hnpr9my3z4w1r6xk5n0s1j3y6a2c2cnynj76za7cphxi1141"; })
+  (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "3.0.0"; sha256 = "1bk8r4r3ihmi6322jmcag14jmw11mjqys202azqjzglcx59pxh51"; })
+  (fetchNuGet { pname = "Microsoft.NETCore.Targets"; version = "1.0.1"; sha256 = "0ppdkwy6s9p7x9jix3v4402wb171cdiibq7js7i13nxpdky7074p"; })
+  (fetchNuGet { pname = "Microsoft.NETCore.Targets"; version = "1.1.0"; sha256 = "193xwf33fbm0ni3idxzbr5fdq3i2dlfgihsac9jj7whj0gd902nh"; })
+  (fetchNuGet { pname = "Microsoft.TestPlatform.Extensions.TrxLogger"; version = "17.9.0"; sha256 = "0wn38vj9i4gjw5zsl4wcivpqrmp1h5n6m1zxcfwj7yjn9hf45rz9"; })
+  (fetchNuGet { pname = "Microsoft.TestPlatform.ObjectModel"; version = "17.9.0"; sha256 = "1kgsl9w9fganbm9wvlkqgk0ag9hfi58z88rkfybc6kvg78bx89ca"; })
+  (fetchNuGet { pname = "Microsoft.TestPlatform.TestHost"; version = "17.9.0"; sha256 = "19ffh31a1jxzn8j69m1vnk5hyfz3dbxmflq77b8x82zybiilh5nl"; })
+  (fetchNuGet { pname = "Microsoft.VisualStudio.Threading"; version = "16.7.56"; sha256 = "13x0xrsjxd86clf9cjjwmpzlyp8pkrf13riya7igs8zy93zw2qap"; })
+  (fetchNuGet { pname = "Microsoft.VisualStudio.Threading.Analyzers"; version = "16.7.56"; sha256 = "04v9df0k7bsc0rzgkw4mnvi43pdrh42vk6xdcwn9m6im33m0nnz2"; })
+  (fetchNuGet { pname = "Microsoft.VisualStudio.Validation"; version = "15.5.31"; sha256 = "1ah99rn922qa0sd2k3h64m324f2r32pw8cn4cfihgvwx4qdrpmgw"; })
+  (fetchNuGet { pname = "Microsoft.Win32.Primitives"; version = "4.3.0"; sha256 = "0j0c1wj4ndj21zsgivsc24whiya605603kxrbiw6wkfdync464wq"; })
+  (fetchNuGet { pname = "Microsoft.Win32.Registry"; version = "4.6.0"; sha256 = "0i4y782yrqqyx85pg597m20gm0v126w0j9ddk5z7xb3crx4z9f2s"; })
+  (fetchNuGet { pname = "Microsoft.Win32.SystemEvents"; version = "6.0.0"; sha256 = "0c6pcj088g1yd1vs529q3ybgsd2vjlk5y1ic6dkmbhvrp5jibl9p"; })
+  (fetchNuGet { pname = "Nerdbank.Streams"; version = "2.6.81"; sha256 = "06wihcaga8537ibh0mkj28m720m6vzkqk562zkynhca85nd236yi"; })
+  (fetchNuGet { pname = "Newtonsoft.Json"; version = "11.0.2"; sha256 = "1784xi44f4k8v1fr696hsccmwpy94bz7kixxqlri98zhcxn406b2"; })
+  (fetchNuGet { pname = "Newtonsoft.Json"; version = "13.0.1"; sha256 = "0fijg0w6iwap8gvzyjnndds0q4b8anwxxvik7y8vgq97dram4srb"; })
+  (fetchNuGet { pname = "OmniSharp.Extensions.JsonRpc"; version = "0.19.5"; sha256 = "0ilcv3cxcvjkd8ngiydi69pzll07rhqdv5nq9yjnhyj142ynw2cb"; })
+  (fetchNuGet { pname = "OmniSharp.Extensions.JsonRpc.Generators"; version = "0.19.5"; sha256 = "1mac4yx29ld8fyirg7n0vqn81hzdvcrl8w0l9w5xhnnm6bcd42v8"; })
+  (fetchNuGet { pname = "OmniSharp.Extensions.LanguageProtocol"; version = "0.19.5"; sha256 = "1clgrbw6dlh46iiiqhavwh15xqar41az352mb5r4ln8ql3wnmk1i"; })
+  (fetchNuGet { pname = "OmniSharp.Extensions.LanguageServer"; version = "0.19.5"; sha256 = "0cvxmc0r4ajnaah7lsppik61qickq7i0df4jwqaj6c6axiizhqlm"; })
+  (fetchNuGet { pname = "OmniSharp.Extensions.LanguageServer.Shared"; version = "0.19.5"; sha256 = "0cczmmsmn3pj74wpasgfhjay1a817sd0zgzgqvvnckxxzq3n463h"; })
+  (fetchNuGet { pname = "RangeTree"; version = "3.0.1"; sha256 = "19si88v2r0rc7kai1avwhigcvh3x3c916vrvqlyb59sn4f27pbm2"; })
+  (fetchNuGet { pname = "runtime.any.System.Collections"; version = "4.3.0"; sha256 = "0bv5qgm6vr47ynxqbnkc7i797fdi8gbjjxii173syrx14nmrkwg0"; })
+  (fetchNuGet { pname = "runtime.any.System.Diagnostics.Tracing"; version = "4.3.0"; sha256 = "00j6nv2xgmd3bi347k00m7wr542wjlig53rmj28pmw7ddcn97jbn"; })
+  (fetchNuGet { pname = "runtime.any.System.Globalization"; version = "4.3.0"; sha256 = "1daqf33hssad94lamzg01y49xwndy2q97i2lrb7mgn28656qia1x"; })
+  (fetchNuGet { pname = "runtime.any.System.IO"; version = "4.3.0"; sha256 = "0l8xz8zn46w4d10bcn3l4yyn4vhb3lrj2zw8llvz7jk14k4zps5x"; })
+  (fetchNuGet { pname = "runtime.any.System.Reflection"; version = "4.3.0"; sha256 = "02c9h3y35pylc0zfq3wcsvc5nqci95nrkq0mszifc0sjx7xrzkly"; })
+  (fetchNuGet { pname = "runtime.any.System.Reflection.Extensions"; version = "4.3.0"; sha256 = "0zyri97dfc5vyaz9ba65hjj1zbcrzaffhsdlpxc9bh09wy22fq33"; })
+  (fetchNuGet { pname = "runtime.any.System.Reflection.Primitives"; version = "4.3.0"; sha256 = "0x1mm8c6iy8rlxm8w9vqw7gb7s1ljadrn049fmf70cyh42vdfhrf"; })
+  (fetchNuGet { pname = "runtime.any.System.Resources.ResourceManager"; version = "4.3.0"; sha256 = "03kickal0iiby82wa5flar18kyv82s9s6d4xhk5h4bi5kfcyfjzl"; })
+  (fetchNuGet { pname = "runtime.any.System.Runtime"; version = "4.3.0"; sha256 = "1cqh1sv3h5j7ixyb7axxbdkqx6cxy00p4np4j91kpm492rf4s25b"; })
+  (fetchNuGet { pname = "runtime.any.System.Runtime.Handles"; version = "4.3.0"; sha256 = "0bh5bi25nk9w9xi8z23ws45q5yia6k7dg3i4axhfqlnj145l011x"; })
+  (fetchNuGet { pname = "runtime.any.System.Runtime.InteropServices"; version = "4.3.0"; sha256 = "0c3g3g3jmhlhw4klrc86ka9fjbl7i59ds1fadsb2l8nqf8z3kb19"; })
+  (fetchNuGet { pname = "runtime.any.System.Text.Encoding"; version = "4.3.0"; sha256 = "0aqqi1v4wx51h51mk956y783wzags13wa7mgqyclacmsmpv02ps3"; })
+  (fetchNuGet { pname = "runtime.any.System.Text.Encoding.Extensions"; version = "4.3.0"; sha256 = "0lqhgqi0i8194ryqq6v2gqx0fb86db2gqknbm0aq31wb378j7ip8"; })
+  (fetchNuGet { pname = "runtime.any.System.Threading.Tasks"; version = "4.3.0"; sha256 = "03mnvkhskbzxddz4hm113zsch1jyzh2cs450dk3rgfjp8crlw1va"; })
+  (fetchNuGet { pname = "runtime.debian.8-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "16rnxzpk5dpbbl1x354yrlsbvwylrq456xzpsha1n9y3glnhyx9d"; })
+  (fetchNuGet { pname = "runtime.fedora.23-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0hkg03sgm2wyq8nqk6dbm9jh5vcq57ry42lkqdmfklrw89lsmr59"; })
+  (fetchNuGet { pname = "runtime.fedora.24-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0c2p354hjx58xhhz7wv6div8xpi90sc6ibdm40qin21bvi7ymcaa"; })
+  (fetchNuGet { pname = "runtime.native.System"; version = "4.0.0"; sha256 = "1ppk69xk59ggacj9n7g6fyxvzmk1g5p4fkijm0d7xqfkig98qrkf"; })
+  (fetchNuGet { pname = "runtime.native.System"; version = "4.3.0"; sha256 = "15hgf6zaq9b8br2wi1i3x0zvmk410nlmsmva9p0bbg73v6hml5k4"; })
+  (fetchNuGet { pname = "runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "18pzfdlwsg2nb1jjjjzyb5qlgy6xjxzmhnfaijq5s2jw3cm3ab97"; })
+  (fetchNuGet { pname = "runtime.opensuse.13.2-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0qyynf9nz5i7pc26cwhgi8j62ps27sqmf78ijcfgzab50z9g8ay3"; })
+  (fetchNuGet { pname = "runtime.opensuse.42.1-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "1klrs545awhayryma6l7g2pvnp9xy4z0r1i40r80zb45q3i9nbyf"; })
+  (fetchNuGet { pname = "runtime.osx.10.10-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0zcxjv5pckplvkg0r6mw3asggm7aqzbdjimhvsasb0cgm59x09l3"; })
+  (fetchNuGet { pname = "runtime.rhel.7-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0vhynn79ih7hw7cwjazn87rm9z9fj0rvxgzlab36jybgcpcgphsn"; })
+  (fetchNuGet { pname = "runtime.ubuntu.14.04-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "160p68l2c7cqmyqjwxydcvgw7lvl1cr0znkw8fp24d1by9mqc8p3"; })
+  (fetchNuGet { pname = "runtime.ubuntu.16.04-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "15zrc8fgd8zx28hdghcj5f5i34wf3l6bq5177075m2bc2j34jrqy"; })
+  (fetchNuGet { pname = "runtime.ubuntu.16.10-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "1p4dgxax6p7rlgj4q73k73rslcnz4wdcv8q2flg1s8ygwcm58ld5"; })
+  (fetchNuGet { pname = "runtime.unix.Microsoft.Win32.Primitives"; version = "4.3.0"; sha256 = "0y61k9zbxhdi0glg154v30kkq7f8646nif8lnnxbvkjpakggd5id"; })
+  (fetchNuGet { pname = "runtime.unix.System.Diagnostics.Debug"; version = "4.3.0"; sha256 = "1lps7fbnw34bnh3lm31gs5c0g0dh7548wfmb8zz62v0zqz71msj5"; })
+  (fetchNuGet { pname = "runtime.unix.System.IO.FileSystem"; version = "4.3.0"; sha256 = "14nbkhvs7sji5r1saj2x8daz82rnf9kx28d3v2qss34qbr32dzix"; })
+  (fetchNuGet { pname = "runtime.unix.System.Private.Uri"; version = "4.3.0"; sha256 = "1jx02q6kiwlvfksq1q9qr17fj78y5v6mwsszav4qcz9z25d5g6vk"; })
+  (fetchNuGet { pname = "runtime.unix.System.Runtime.Extensions"; version = "4.3.0"; sha256 = "0pnxxmm8whx38dp6yvwgmh22smknxmqs5n513fc7m4wxvs1bvi4p"; })
+  (fetchNuGet { pname = "Serilog"; version = "2.12.0"; sha256 = "0lqxpc96qcjkv9pr1rln7mi4y7n7jdi4vb36c2fv3845w1vswgr4"; })
+  (fetchNuGet { pname = "Serilog.Extensions.Logging"; version = "3.0.1"; sha256 = "069qy7dm5nxb372ij112ppa6m99b4iaimj3sji74m659fwrcrl9a"; })
+  (fetchNuGet { pname = "Serilog.Settings.Configuration"; version = "3.1.0"; sha256 = "1cj5am4n073331gbfm2ylqb9cadl4q3ppzgwmm5c8m1drxpiwkb5"; })
+  (fetchNuGet { pname = "Serilog.Sinks.Debug"; version = "2.0.0"; sha256 = "1i7j870l47gan3gpnnlzkccn5lbm7518cnkp25a3g5gp9l0dbwpw"; })
+  (fetchNuGet { pname = "Serilog.Sinks.File"; version = "5.0.0"; sha256 = "097rngmgcrdfy7jy8j7dq3xaq2qky8ijwg0ws6bfv5lx0f3vvb0q"; })
+  (fetchNuGet { pname = "System.AppContext"; version = "4.1.0"; sha256 = "0fv3cma1jp4vgj7a8hqc9n7hr1f1kjp541s6z0q1r6nazb4iz9mz"; })
+  (fetchNuGet { pname = "System.Buffers"; version = "4.3.0"; sha256 = "0fgns20ispwrfqll4q1zc1waqcmylb3zc50ys9x8zlwxh9pmd9jy"; })
+  (fetchNuGet { pname = "System.Collections"; version = "4.3.0"; sha256 = "19r4y64dqyrq6k4706dnyhhw7fs24kpp3awak7whzss39dakpxk9"; })
+  (fetchNuGet { pname = "System.Collections.Immutable"; version = "1.7.0"; sha256 = "1gik4sn9jsi1wcy1pyyp0r4sn2g17cwrsh24b2d52vif8p2h24zx"; })
+  (fetchNuGet { pname = "System.Collections.Immutable"; version = "1.7.1"; sha256 = "1nh4nlxfc7lbnbl86wwk1a3jwl6myz5j6hvgh5sp4krim9901hsq"; })
+  (fetchNuGet { pname = "System.CommandLine"; version = "2.0.0-beta4.22272.1"; sha256 = "1iy5hwwgvx911g3yq65p4zsgpy08w4qz9j3h0igcf7yci44vw8yd"; })
+  (fetchNuGet { pname = "System.Configuration.ConfigurationManager"; version = "6.0.0"; sha256 = "0sqapr697jbb4ljkq46msg0xx1qpmc31ivva6llyz2wzq3mpmxbw"; })
+  (fetchNuGet { pname = "System.Diagnostics.Debug"; version = "4.3.0"; sha256 = "00yjlf19wjydyr6cfviaph3vsjzg3d5nvnya26i2fvfg53sknh3y"; })
+  (fetchNuGet { pname = "System.Diagnostics.Tracing"; version = "4.3.0"; sha256 = "1m3bx6c2s958qligl67q7grkwfz3w53hpy7nc97mh6f7j5k168c4"; })
+  (fetchNuGet { pname = "System.Drawing.Common"; version = "6.0.0"; sha256 = "02n8rzm58dac2np8b3xw8ychbvylja4nh6938l5k2fhyn40imlgz"; })
+  (fetchNuGet { pname = "System.Dynamic.Runtime"; version = "4.0.11"; sha256 = "1pla2dx8gkidf7xkciig6nifdsb494axjvzvann8g2lp3dbqasm9"; })
+  (fetchNuGet { pname = "System.Globalization"; version = "4.0.11"; sha256 = "070c5jbas2v7smm660zaf1gh0489xanjqymkvafcs4f8cdrs1d5d"; })
+  (fetchNuGet { pname = "System.Globalization"; version = "4.3.0"; sha256 = "1cp68vv683n6ic2zqh2s1fn4c2sd87g5hpp6l4d4nj4536jz98ki"; })
+  (fetchNuGet { pname = "System.IO"; version = "4.1.0"; sha256 = "1g0yb8p11vfd0kbkyzlfsbsp5z44lwsvyc0h3dpw6vqnbi035ajp"; })
+  (fetchNuGet { pname = "System.IO"; version = "4.3.0"; sha256 = "05l9qdrzhm4s5dixmx68kxwif4l99ll5gqmh7rqgw554fx0agv5f"; })
+  (fetchNuGet { pname = "System.IO.FileSystem"; version = "4.0.1"; sha256 = "0kgfpw6w4djqra3w5crrg8xivbanh1w9dh3qapb28q060wb9flp1"; })
+  (fetchNuGet { pname = "System.IO.FileSystem.Primitives"; version = "4.3.0"; sha256 = "0j6ndgglcf4brg2lz4wzsh1av1gh8xrzdsn9f0yznskhqn1xzj9c"; })
+  (fetchNuGet { pname = "System.IO.Pipelines"; version = "4.7.3"; sha256 = "0djp59x56klidi04xx8p5jc1nchv5zvd1d59diphqxwvgny3aawy"; })
+  (fetchNuGet { pname = "System.Linq"; version = "4.1.0"; sha256 = "1ppg83svb39hj4hpp5k7kcryzrf3sfnm08vxd5sm2drrijsla2k5"; })
+  (fetchNuGet { pname = "System.Linq.Async"; version = "6.0.1"; sha256 = "10ira8hmv0i54yp9ggrrdm1c06j538sijfjpn1kmnh9j2xk5yzmq"; })
+  (fetchNuGet { pname = "System.Linq.Expressions"; version = "4.1.0"; sha256 = "1gpdxl6ip06cnab7n3zlcg6mqp7kknf73s8wjinzi4p0apw82fpg"; })
+  (fetchNuGet { pname = "System.Memory"; version = "4.5.4"; sha256 = "14gbbs22mcxwggn0fcfs1b062521azb9fbb7c113x0mq6dzq9h6y"; })
+  (fetchNuGet { pname = "System.Net.WebSockets"; version = "4.3.0"; sha256 = "1gfj800078kggcgl0xyl00a6y5k4wwh2k2qm69rjy22wbmq7fy4p"; })
+  (fetchNuGet { pname = "System.ObjectModel"; version = "4.0.12"; sha256 = "1sybkfi60a4588xn34nd9a58png36i0xr4y4v4kqpg8wlvy5krrj"; })
+  (fetchNuGet { pname = "System.Private.Uri"; version = "4.3.0"; sha256 = "04r1lkdnsznin0fj4ya1zikxiqr0h6r6a1ww2dsm60gqhdrf0mvx"; })
+  (fetchNuGet { pname = "System.Reactive"; version = "4.4.1"; sha256 = "0gx8jh3hny2y5kijz5k9pxiqw481d013787c04zlhps21ygklw4a"; })
+  (fetchNuGet { pname = "System.Reflection"; version = "4.1.0"; sha256 = "1js89429pfw79mxvbzp8p3q93il6rdff332hddhzi5wqglc4gml9"; })
+  (fetchNuGet { pname = "System.Reflection"; version = "4.3.0"; sha256 = "0xl55k0mw8cd8ra6dxzh974nxif58s3k1rjv1vbd7gjbjr39j11m"; })
+  (fetchNuGet { pname = "System.Reflection.Emit"; version = "4.0.1"; sha256 = "0ydqcsvh6smi41gyaakglnv252625hf29f7kywy2c70nhii2ylqp"; })
+  (fetchNuGet { pname = "System.Reflection.Emit.ILGeneration"; version = "4.0.1"; sha256 = "1pcd2ig6bg144y10w7yxgc9d22r7c7ww7qn1frdfwgxr24j9wvv0"; })
+  (fetchNuGet { pname = "System.Reflection.Emit.Lightweight"; version = "4.0.1"; sha256 = "1s4b043zdbx9k39lfhvsk68msv1nxbidhkq6nbm27q7sf8xcsnxr"; })
+  (fetchNuGet { pname = "System.Reflection.Extensions"; version = "4.0.1"; sha256 = "0m7wqwq0zqq9gbpiqvgk3sr92cbrw7cp3xn53xvw7zj6rz6fdirn"; })
+  (fetchNuGet { pname = "System.Reflection.Metadata"; version = "1.6.0"; sha256 = "1wdbavrrkajy7qbdblpbpbalbdl48q3h34cchz24gvdgyrlf15r4"; })
+  (fetchNuGet { pname = "System.Reflection.Primitives"; version = "4.0.1"; sha256 = "1bangaabhsl4k9fg8khn83wm6yial8ik1sza7401621jc6jrym28"; })
+  (fetchNuGet { pname = "System.Reflection.Primitives"; version = "4.3.0"; sha256 = "04xqa33bld78yv5r93a8n76shvc8wwcdgr1qvvjh959g3rc31276"; })
+  (fetchNuGet { pname = "System.Reflection.TypeExtensions"; version = "4.1.0"; sha256 = "1bjli8a7sc7jlxqgcagl9nh8axzfl11f4ld3rjqsyxc516iijij7"; })
+  (fetchNuGet { pname = "System.Resources.ResourceManager"; version = "4.0.1"; sha256 = "0b4i7mncaf8cnai85jv3wnw6hps140cxz8vylv2bik6wyzgvz7bi"; })
+  (fetchNuGet { pname = "System.Resources.ResourceManager"; version = "4.3.0"; sha256 = "0sjqlzsryb0mg4y4xzf35xi523s4is4hz9q4qgdvlvgivl7qxn49"; })
+  (fetchNuGet { pname = "System.Runtime"; version = "4.1.0"; sha256 = "02hdkgk13rvsd6r9yafbwzss8kr55wnj8d5c7xjnp8gqrwc8sn0m"; })
+  (fetchNuGet { pname = "System.Runtime"; version = "4.3.0"; sha256 = "066ixvgbf2c929kgknshcxqj6539ax7b9m570cp8n179cpfkapz7"; })
+  (fetchNuGet { pname = "System.Runtime.Caching"; version = "6.0.0"; sha256 = "0wh98a77cby4i3h2mar241k01105x661kh03vlyd399shxkfk60a"; })
+  (fetchNuGet { pname = "System.Runtime.CompilerServices.Unsafe"; version = "4.4.0"; sha256 = "0a6ahgi5b148sl5qyfpyw383p3cb4yrkm802k29fsi4mxkiwir29"; })
+  (fetchNuGet { pname = "System.Runtime.CompilerServices.Unsafe"; version = "4.7.0"; sha256 = "16r6sn4czfjk8qhnz7bnqlyiaaszr0ihinb7mq9zzr1wba257r54"; })
+  (fetchNuGet { pname = "System.Runtime.CompilerServices.Unsafe"; version = "4.7.1"; sha256 = "119br3pd85lq8zcgh4f60jzmv1g976q1kdgi3hvqdlhfbw6siz2j"; })
+  (fetchNuGet { pname = "System.Runtime.Extensions"; version = "4.1.0"; sha256 = "0rw4rm4vsm3h3szxp9iijc3ksyviwsv6f63dng3vhqyg4vjdkc2z"; })
+  (fetchNuGet { pname = "System.Runtime.Extensions"; version = "4.3.0"; sha256 = "1ykp3dnhwvm48nap8q23893hagf665k0kn3cbgsqpwzbijdcgc60"; })
+  (fetchNuGet { pname = "System.Runtime.Handles"; version = "4.0.1"; sha256 = "1g0zrdi5508v49pfm3iii2hn6nm00bgvfpjq1zxknfjrxxa20r4g"; })
+  (fetchNuGet { pname = "System.Runtime.Handles"; version = "4.3.0"; sha256 = "0sw2gfj2xr7sw9qjn0j3l9yw07x73lcs97p8xfc9w1x9h5g5m7i8"; })
+  (fetchNuGet { pname = "System.Runtime.InteropServices"; version = "4.1.0"; sha256 = "01kxqppx3dr3b6b286xafqilv4s2n0gqvfgzfd4z943ga9i81is1"; })
+  (fetchNuGet { pname = "System.Runtime.InteropServices"; version = "4.3.0"; sha256 = "00hywrn4g7hva1b2qri2s6rabzwgxnbpw9zfxmz28z09cpwwgh7j"; })
+  (fetchNuGet { pname = "System.Runtime.InteropServices.RuntimeInformation"; version = "4.0.0"; sha256 = "0glmvarf3jz5xh22iy3w9v3wyragcm4hfdr17v90vs7vcrm7fgp6"; })
+  (fetchNuGet { pname = "System.Runtime.Numerics"; version = "4.3.0"; sha256 = "19rav39sr5dky7afygh309qamqqmi9kcwvz3i0c5700v0c5cg61z"; })
+  (fetchNuGet { pname = "System.Security.AccessControl"; version = "4.6.0"; sha256 = "1wl1dyghi0qhpap1vgfhg2ybdyyhy9vc2a7dpm1xb30vfgmlkjmf"; })
+  (fetchNuGet { pname = "System.Security.AccessControl"; version = "6.0.0"; sha256 = "0a678bzj8yxxiffyzy60z2w1nczzpi8v97igr4ip3byd2q89dv58"; })
+  (fetchNuGet { pname = "System.Security.Cryptography.ProtectedData"; version = "6.0.0"; sha256 = "05kd3a8w7658hjxq9vvszxip30a479fjmfq4bq1r95nrsvs4hbss"; })
+  (fetchNuGet { pname = "System.Security.Permissions"; version = "6.0.0"; sha256 = "0jsl4xdrkqi11iwmisi1r2f2qn5pbvl79mzq877gndw6ans2zhzw"; })
+  (fetchNuGet { pname = "System.Security.Principal.Windows"; version = "4.6.0"; sha256 = "1jmfzfz1n8hp63s5lja5xxpzkinbp6g59l3km9h8avjiisdrg5wm"; })
+  (fetchNuGet { pname = "System.Text.Encoding"; version = "4.0.11"; sha256 = "1dyqv0hijg265dwxg6l7aiv74102d6xjiwplh2ar1ly6xfaa4iiw"; })
+  (fetchNuGet { pname = "System.Text.Encoding"; version = "4.3.0"; sha256 = "1f04lkir4iladpp51sdgmis9dj4y8v08cka0mbmsy0frc9a4gjqr"; })
+  (fetchNuGet { pname = "System.Text.Encoding.CodePages"; version = "4.5.1"; sha256 = "1z21qyfs6sg76rp68qdx0c9iy57naan89pg7p6i3qpj8kyzn921w"; })
+  (fetchNuGet { pname = "System.Text.Encoding.Extensions"; version = "4.3.0"; sha256 = "11q1y8hh5hrp5a3kw25cb6l00v5l5dvirkz8jr3sq00h1xgcgrxy"; })
+  (fetchNuGet { pname = "System.Threading"; version = "4.0.11"; sha256 = "19x946h926bzvbsgj28csn46gak2crv2skpwsx80hbgazmkgb1ls"; })
+  (fetchNuGet { pname = "System.Threading"; version = "4.3.0"; sha256 = "0rw9wfamvhayp5zh3j7p1yfmx9b5khbf4q50d8k5rk993rskfd34"; })
+  (fetchNuGet { pname = "System.Threading.Channels"; version = "4.7.1"; sha256 = "038fyrriypwzsj5fwgnkw79hm5ya0x63r724yizgahbxf512chr2"; })
+  (fetchNuGet { pname = "System.Threading.Tasks"; version = "4.0.11"; sha256 = "0nr1r41rak82qfa5m0lhk9mp0k93bvfd7bbd9sdzwx9mb36g28p5"; })
+  (fetchNuGet { pname = "System.Threading.Tasks"; version = "4.3.0"; sha256 = "134z3v9abw3a6jsw17xl3f6hqjpak5l682k2vz39spj4kmydg6k7"; })
+  (fetchNuGet { pname = "System.Threading.Tasks.Extensions"; version = "4.5.3"; sha256 = "0g7r6hm572ax8v28axrdxz1gnsblg6kszq17g51pj14a5rn2af7i"; })
+  (fetchNuGet { pname = "System.Windows.Extensions"; version = "6.0.0"; sha256 = "1wy9pq9vn1bqg5qnv53iqrbx04yzdmjw4x5yyi09y3459vaa1sip"; })
+  (fetchNuGet { pname = "Tomlyn"; version = "0.16.2"; sha256 = "1i928q6a7l65mk7wj2vvfclyvxamdjxg4dbj3g6g95inrfgvidah"; })
+]
diff --git a/hacking/nix/scope/default.nix b/hacking/nix/scope/default.nix
index 7d3936a62..53d33d810 100644
--- a/hacking/nix/scope/default.nix
+++ b/hacking/nix/scope/default.nix
@@ -145,6 +145,8 @@ superCallPackage ../rust-utils {} self //
 
   capdl-tool = callBuildBuildPackage ./capdl-tool {};
 
+  dafny = callBuildBuildPackage ./dafny {};
+
   ### local tools
 
   mkTool = rootCrate: buildCrateInLayersHere {
diff --git a/hacking/nix/scope/world/instances/dafny.nix b/hacking/nix/scope/world/instances/dafny.nix
new file mode 100644
index 000000000..a2a824b43
--- /dev/null
+++ b/hacking/nix/scope/world/instances/dafny.nix
@@ -0,0 +1,65 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+{ lib
+, runCommand
+
+, dafny
+
+, sources
+, crates
+, crateUtils
+, seL4Modifications
+, mkTask
+
+, mkInstance
+
+, canSimulate
+}:
+
+let
+  verifiedSrcDir = lib.cleanSource (sources.srcRoot + "/crates/private/tests/root-task/dafny/verified");
+  verifiedName = "core";
+  verifiedSrc = "${verifiedSrcDir}/${verifiedName}.dfy";
+
+  translated = runCommand "translated.rs" {
+    nativeBuildInputs = [ dafny ];
+  } ''
+	  dafny translate rs ${verifiedSrc} -o ${verifiedName}
+    mv ${verifiedName}-rust/src/${verifiedName}.rs $out
+  '';
+      # TODO
+      # --standard-libraries \
+
+in
+mkInstance {
+  rootTask = mkTask rec {
+    rootCrate = crates.tests-root-task-dafny-task;
+    release = false;
+
+    layers = [
+      crateUtils.defaultIntermediateLayer
+      {
+        crates = [ "sel4-root-task" ];
+        modifications = seL4Modifications;
+      }
+    ];
+
+    lastLayerModifications.modifyDerivation = drv: drv.overrideAttrs (attrs: {
+      nativeBuildInputs = (attrs.nativeBuildInputs or []) ++ [
+        dafny
+      ];
+
+      TRANSLATED = translated;
+    });
+  };
+
+  extraPlatformArgs = lib.optionalAttrs canSimulate  {
+    canAutomateSimply = true;
+  };
+} // {
+  inherit translated;
+}
diff --git a/hacking/nix/scope/world/instances/default.nix b/hacking/nix/scope/world/instances/default.nix
index ea5d4cf6f..bcebd3d92 100644
--- a/hacking/nix/scope/world/instances/default.nix
+++ b/hacking/nix/scope/world/instances/default.nix
@@ -206,6 +206,10 @@ in rec {
         inherit canSimulate;
       });
 
+      dafny = maybe haveFullRuntime (callPackage ./dafny.nix {
+        inherit canSimulate;
+      });
+
       default-test-harness = maybe (haveFullRuntime && haveUnwindingSupport) (mkInstance {
         rootTask = mkTask {
           rootCrate = crates.tests-root-task-default-test-harness;