diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000000..47ba68eb30
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,27 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1720418205,
+        "narHash": "sha256-cPJoFPXU44GlhWg4pUk9oUPqurPlCFZ11ZQPk21GTPU=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "655a58a72a6601292512670343087c2d75d859c1",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000000..b11360632f
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,162 @@
+# TODO
+# * [x] deal with hardcoded path
+# * [x] the dependency z3
+# * [ ] remove duplicates
+# * [ ] verus as an app (which checks whether verus was build beforehand, otherwise instructs user to call the vargo app)
+# * [ ] think about command names
+# * [x] vargo as a package (technically doable with a cargo)
+
+# MAYBE LATER
+# * [ ] pick right z3 dependency automagically (not super simple when all we have the url in the script...)
+# * [ ] verus as a package (not doable yet, since verus calls rustup and that means internet access during the build phase, which is not possible in nix)
+
+# How to use (if you have the nix package manager installed. These days, I recommend [Lix](https://lix.systems).)
+# ===============================
+#
+# How to use the devshell (meant for developping on vargo or verus itself)
+# `nix develop` This will drop you in a shell environment where all dependencies are (should be) available
+#
+# How to call vargo:
+# `cd src && nix run .#vargo-br`
+#
+# How to call verus;
+# TODO
+
+{
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+  };
+
+  outputs = {
+    nixpkgs,
+    self,
+    ...
+  }: let
+    supportedSystems = [ "x86_64-linux" "x86_64-darwin" "aarch64-linux" "aarch64-darwin" ];
+    forAllSystems = nixpkgs.lib.genAttrs supportedSystems;
+    nixpkgsFor = forAllSystems (system: import nixpkgs { inherit system; });
+
+    overrides = (builtins.fromTOML (builtins.readFile ./rust-toolchain.toml));
+  in {
+    packages = forAllSystems (system: let
+      pkgs = nixpkgsFor.${system};
+    in {
+      vargo = import ./vargo.nix { inherit pkgs; };
+    });
+
+    # enter a dev shell with `nix develop
+    devShells = forAllSystems (system: let
+      pkgs = nixpkgsFor.${system};
+      libPath = with pkgs; lib.makeLibraryPath [
+        # load external libraries that you need in your rust project here
+      ];
+    in {
+      default = pkgs.mkShell {
+        RUSTC_VERSION = overrides.toolchain.channel;
+        # https://github.com/rust-lang/rust-bindgen#environment-variables
+        LIBCLANG_PATH = pkgs.lib.makeLibraryPath [ pkgs.llvmPackages_latest.libclang.lib ];
+
+        # Add precompiled library to rustc search path
+        RUSTFLAGS = (builtins.map (a: ''-L ${a}/lib'') [
+        # add libraries here (e.g. pkgs.libvmi)
+        ]);
+        LD_LIBRARY_PATH = libPath;
+        # Add glibc, clang, glib, and other headers to bindgen search path
+        BINDGEN_EXTRA_CLANG_ARGS =
+        # Includes normal include path
+          (builtins.map (a: ''-I"${a}/include"'') [
+            # add dev libraries here (e.g. pkgs.libvmi.dev)
+            pkgs.glibc.dev
+          ])
+          # Includes with special directory paths
+          ++ [
+            ''-I"${pkgs.llvmPackages_latest.libclang.lib}/lib/clang/${pkgs.llvmPackages_latest.libclang.version}/include"''
+            ''-I"${pkgs.glib.dev}/include/glib-2.0"''
+            ''-I${pkgs.glib.out}/lib/glib-2.0/include/''
+          ];
+
+        packages = [
+          pkgs.z3_4_12
+          pkgs.cvc5
+          pkgs.singular
+
+          pkgs.clang
+          pkgs.llvmPackages.bintools
+          pkgs.rustup
+          (import ./vargo.nix { inherit pkgs; })
+        ];
+        shellHook = ''
+          export PATH=$PATH:''${CARGO_HOME}/bin
+          export PATH=$PATH:''${RUSTUP_HOME}/toolchains/$RUSTC_VERSION-x86_64-unknown-linux-gnu/bin/
+          export PATH=$(realpath .)/source/target-verus/release:$PATH
+          export VERUS_Z3_PATH=$(which z3)
+          export VERUS_CVC5_PATH=$(which cvc5)
+          export VERUS_SINGULAR_PATH=$(which Singular) # what exactly does it need on the path?
+        '';
+      };
+    });
+
+    # this only works if you have rustup installed system wide
+    # invoke as `nix run .#vargo`
+    apps = forAllSystems (system: let
+      pkgs = nixpkgsFor.${system};
+      libPath = with pkgs; lib.makeLibraryPath [
+        # load external libraries that you need in your rust project here
+      ];
+      # todo put these vars inside
+      RUSTC_VERSION = overrides.toolchain.channel; # TODO das hier wird noch gar nicht genutzt so
+#         https://github.com/rust-lang/rust-bindgen#environment-variables
+      LIBCLANG_PATH = pkgs.lib.makeLibraryPath [ pkgs.llvmPackages_latest.libclang.lib ];
+
+#         Add precompiled library to rustc search path
+      RUSTFLAGS = (builtins.map (a: ''-L ${a}/lib'') [
+#           add libraries here (e.g. pkgs.libvmi)
+      ]);
+      LD_LIBRARY_PATH = libPath;
+#       Add glibc, clang, glib, and other headers to bindgen search path
+      BINDGEN_EXTRA_CLANG_ARGS =
+#         Includes normal include path
+        (builtins.map (a: ''-I"${a}/include"'') [
+#         add dev libraries here (e.g. pkgs.libvmi.dev)
+        pkgs.glibc.dev
+      ])
+#         Includes with special directory paths
+      ++ [
+        ''-I"${pkgs.llvmPackages_latest.libclang.lib}/lib/clang/${pkgs.llvmPackages_latest.libclang.version}/include"''
+        ''-I"${pkgs.glib.dev}/include/glib-2.0"''
+          ''-I${pkgs.glib.out}/lib/glib-2.0/include/''
+      ];
+      vargoWithRustup = pkgs.writeShellApplication {
+        name = "vargo";
+        runtimeInputs = [
+          pkgs.z3_4_12
+          pkgs.cvc5
+          pkgs.singular
+
+          pkgs.clang
+          pkgs.llvmPackages.bintools
+          pkgs.rustup
+          (import ./vargo.nix { inherit pkgs; })
+        ];
+
+
+        text = ''
+          VERUS_Z3_PATH=$(which z3)
+          export VERUS_Z3_PATH
+
+
+          export PATH=$PATH:~/.cargo/bin
+          export PATH=$PATH:~/.rutup/toolchains/${RUSTC_VERSION}-x86_64-unknown-linux-gnu/bin/
+
+
+          vargo build --release
+        '';
+      };
+      in {
+        vargo-br = {
+          type = "app";
+          program = "${vargoWithRustup}/bin/vargo";
+        };
+    });
+  };
+}
diff --git a/vargo.diff b/vargo.diff
new file mode 100644
index 0000000000..b5443fe1d7
--- /dev/null
+++ b/vargo.diff
@@ -0,0 +1,28 @@
+--- vargo/src/main.rs	2024-07-05 20:51:28.181535045 +0200
++++ vargo/src/main.rs	2024-07-05 20:52:04.385986052 +0200
+@@ -5,8 +5,11 @@
+ // `target/debug` or `target/release` when they are the main build target, and
+ // not when they're a dependency of another target.
+ 
+-#[path = "../../common/consts.rs"]
+-mod consts;
++
++mod consts {
++    pub const EXPECTED_Z3_VERSION: &str = "4.12.5";
++    pub const EXPECTED_CVC5_VERSION: &str = "1.1.2";
++}
+ 
+ const MINIMUM_VERUSFMT_VERSION: [u64; 3] = [0, 3, 0];
+ 
+@@ -289,11 +291,6 @@
+         let cur_hash = &crate::util::hash_file_contents(
+             files.iter().map(|(f, n)| (f.as_str(), &n[..])).collect(),
+         );
+-        if build_hash != cur_hash {
+-            return Err(format!(
+-                "vargo sources have changed since it was last built, please re-build vargo"
+-            ));
+-        }
+     }
+ 
+     let rust_toolchain_toml_channel = rust_toolchain_toml.get("toolchain").and_then(|t| t.get("channel"))
diff --git a/vargo.nix b/vargo.nix
new file mode 100644
index 0000000000..5254c28196
--- /dev/null
+++ b/vargo.nix
@@ -0,0 +1,22 @@
+{
+  pkgs
+}:  pkgs.rustPlatform.buildRustPackage {
+  pname = "vargo";
+  version = "0.1.0";
+
+  src = pkgs.lib.cleanSource ./tools/vargo;
+  cargoLock.lockFile = ./tools/vargo/Cargo.lock; # yes, this does not use the rust toolchain
+
+  patches = [ ./vargo.diff ];
+  # it references a file outside the vargo dir which is just a headache... don't forget to update it if needed
+  # oh and maybe just remove the entire "toolchain-check"! (although I'd prefer if that worked with the specified Cargo.lock)
+
+  meta = {
+    description = "Verus is a tool for verifying the correctness of code written in Rust.";
+    homepage = "https://github.com/verus-lang/verus";
+    license = pkgs.lib.licenses.mit;
+  };
+}
+
+# docs for packaging this:
+# https://m7.rs/blog/2022-11-01-package-a-rust-app-with-nix/index.html