From 8a97ca85bb5a45cbdc510307d163229608a22b81 Mon Sep 17 00:00:00 2001
From: Jake Ginesin <jakeginesin@gmail.com>
Date: Mon, 8 Dec 2025 17:48:11 -0500
Subject: [PATCH 01/14] first working flake iteration

---
 flake.lock          |  48 ++++++++++++
 flake.nix           | 175 ++++++++++++++++++++++++++++++++++++++++++++
 result              |   1 +
 tools/nix/rustup.py |  27 +++++++
 tools/shell.nix     |  14 ----
 5 files changed, 251 insertions(+), 14 deletions(-)
 create mode 100644 flake.lock
 create mode 100644 flake.nix
 create mode 120000 result
 create mode 100644 tools/nix/rustup.py
 delete mode 100644 tools/shell.nix

diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000000..d19a3cc547
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,48 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1764950072,
+        "narHash": "sha256-BmPWzogsG2GsXZtlT+MTcAWeDK5hkbGRZTeZNW42fwA=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "f61125a668a320878494449750330ca58b78c557",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs",
+        "rust-overlay": "rust-overlay"
+      }
+    },
+    "rust-overlay": {
+      "inputs": {
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
+      "locked": {
+        "lastModified": 1765161692,
+        "narHash": "sha256-XdY9AFzmgRPYIhP4N+WiCHMNxPoifP5/Ld+orMYBD8c=",
+        "owner": "oxalica",
+        "repo": "rust-overlay",
+        "rev": "7ed7e8c74be95906275805db68201e74e9904f07",
+        "type": "github"
+      },
+      "original": {
+        "owner": "oxalica",
+        "repo": "rust-overlay",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000000..7a5ab8e458
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,175 @@
+{
+  description = "Flake for verus";
+  inputs = {
+    nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+    rust-overlay = {
+      url = "github:oxalica/rust-overlay";
+      inputs.nixpkgs.follows = "nixpkgs";
+    };
+  };
+  outputs = { self, nixpkgs, rust-overlay }:
+    let
+      inherit (nixpkgs) lib;
+      systems = [
+        "x86_64-linux"
+        "x86_64-darwin"
+        "aarch64-darwin"
+        "x86_64-windows"
+      ];
+      eachDefaultSystem = f: builtins.foldl' lib.attrsets.recursiveUpdate { }
+        (map f systems);
+    in
+    eachDefaultSystem (system:
+      let
+        overlays = [ (import rust-overlay) ];
+        pkgs = import nixpkgs {
+          inherit system overlays;
+        };
+        formatter = pkgs.nixpkgs-fmt;
+        linters = [ pkgs.statix ];
+        rust-bin = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.toml;
+        
+        # Inline rustup
+        rustup = pkgs.stdenvNoCC.mkDerivation {
+          name = "rustup";
+          src = ./tools/nix;
+          strictDeps = true;
+          buildInputs = [ pkgs.python3 ];
+          preferLocalBuild = true;
+          postPatch = ''
+            substituteInPlace rustup.py \
+              --subst-var-by rustVersion "${rust-bin.version}"
+          '';
+          installPhase = ''
+            runHook preInstall
+            install -Dm755 rustup.py -T $out/bin/rustup
+            runHook postInstall
+          '';
+          meta = {
+            description = "Spoof rustup";
+            mainProgram = "rustup";
+            maintainers = with lib.maintainers; [ stephen-huan jakeginesin ];
+          };
+        };
+        
+        version = "latest";
+        src = ./.;
+        meta = {
+          homepage = "https://github.com/verus-lang/verus";
+          description = "Verified Rust for low-level systems code";
+          license = lib.licenses.mit;
+          maintainers = with lib.maintainers; [ stephen-huan jakeginesin ];
+          platforms = systems;
+        };
+        
+        vargo = pkgs.rustPlatform.buildRustPackage (finalAttrs: {
+          pname = "vargo";
+          inherit version src;
+          buildAndTestSubdir = "tools/vargo";
+          cargoLock = {
+            lockFile = ./tools/vargo/Cargo.lock;
+          };
+          postPatch = ''
+            cp ${./tools/vargo/Cargo.lock} Cargo.lock
+            cp rust-toolchain.toml source/
+          '';
+          cargoHash = "sha256-0WJEW3FtoWxMaedqBoCmaS0HLsLjxtBlBClAXcjf/6s=";
+          meta = meta // { mainProgram = "vargo"; };
+        });
+        
+        verus = pkgs.rustPlatform.buildRustPackage {
+          pname = "verus";
+          inherit version src;
+          buildAndTestSubdir = "source";
+          cargoLock = {
+            lockFile = ./source/Cargo.lock;
+            outputHashes = {
+              "getopts-0.2.21" = "sha256-N/QJvyOmLoU5TabrXi8i0a5s23ldeupmBUzP8waVOiU=";
+              "smt2parser-0.6.1" = "sha256-AKBq8Ph8D2ucyaBpmDtOypwYie12xVl4gLRxttv5Ods=";
+            };
+          };
+          postPatch = ''
+            cp ${./source/Cargo.lock} Cargo.lock
+          '';
+          cargoHash = "sha256-y3SmOo6pCfJfPNN+9yUN7FeFcrmJ8xL4rQrjqtSe96M=";
+          nativeBuildInputs = [ pkgs.makeBinaryWrapper rust-bin rustup vargo z3 ];
+          buildInputs = [ rustup z3 ];
+          buildPhase = ''
+            runHook preBuild
+            cd source
+            ln -s ${lib.getExe z3} ./z3
+            ln -sf ../rust-toolchain.toml rust-toolchain.toml
+            vargo build --release
+            runHook postBuild
+          '';
+          installPhase = ''
+            runHook preInstall
+            mkdir -p $out
+            cp -r target-verus/release -T $out
+            mkdir -p $out/bin
+            ln -s $out/verus $out/bin/verus
+            ln -s $out/rust_verify $out/bin/rust_verify
+            ln -s $out/cargo-verus $out/bin/cargo-verus
+            ln -s $out/z3 $out/bin/z3
+            wrapProgram $out/bin/verus --prefix PATH : ${lib.makeBinPath [ rustup rust-bin z3 ]}
+            runHook postInstall
+          '';
+          doCheck = false;
+          passthru = { inherit vargo; };
+          meta = meta // { mainProgram = "verus"; };
+        };
+        
+        z3 = pkgs.z3.overrideAttrs (finalAttrs: previousAttrs: {
+          version = "4.12.5";
+          src = pkgs.fetchFromGitHub {
+            owner = "Z3Prover";
+            repo = "z3";
+            tag = "z3-${finalAttrs.version}";
+            sha256 = "sha256-Qj9w5s02OSMQ2qA7HG7xNqQGaUacA1d4zbOHynq5k+A=";
+          };
+        });
+      in
+      {
+        packages.${system} = rec {
+          default = verus;
+          inherit rust-bin rustup vargo verus;
+        };
+        formatter.${system} = formatter;
+        checks.${system}.lint = pkgs.stdenvNoCC.mkDerivation {
+          name = "lint";
+          src = ./.;
+          doCheck = true;
+          nativeCheckInputs = linters ++ lib.singleton formatter;
+          checkPhase = ''
+            nixpkgs-fmt --check .
+            statix check
+          '';
+          installPhase = "touch $out";
+        };
+        apps.${system} = {
+          update = {
+            type = "app";
+            program = lib.getExe (pkgs.writeShellApplication {
+              name = "update";
+              runtimeInputs = [ pkgs.nix-update ];
+              text = lib.concatMapStringsSep "\n"
+                (package: "nix-update --flake ${package} || true")
+                (builtins.attrNames self.packages.${system});
+            });
+          };
+        };
+        devShells.${system}.default = (pkgs.mkShellNoCC.override {
+          stdenv = pkgs.stdenvNoCC.override {
+            initialPath = [ pkgs.coreutils ];
+          };
+        }) {
+          packages = with self.packages.${system}; [
+            rust-bin
+            rustup
+            vargo
+            verus
+          ];
+        };
+      }
+    );
+}
diff --git a/result b/result
new file mode 120000
index 0000000000..b3fd69363e
--- /dev/null
+++ b/result
@@ -0,0 +1 @@
+/nix/store/5zjy3m5aqnbrcawkd7n92fgmvlfqky63-verus-latest
\ No newline at end of file
diff --git a/tools/nix/rustup.py b/tools/nix/rustup.py
new file mode 100644
index 0000000000..ae22b638b1
--- /dev/null
+++ b/tools/nix/rustup.py
@@ -0,0 +1,27 @@
+#!/usr/bin/env python3
+"""
+Spoof rustup.
+"""
+import argparse
+import subprocess
+
+# everything past @rustVersion@ arbitrary
+triple = "@rustVersion@-x86_64-unknown-linux-gnu"
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser()
+    subparsers = parser.add_subparsers()
+    parser_show = subparsers.add_parser("show")
+    parser_show.add_argument("show")
+    parser_toolchain = subparsers.add_parser("toolchain")
+    parser_toolchain.add_argument("toolchain")
+    parser_run = subparsers.add_parser("run")
+    parser_run.add_argument("run", nargs="*")
+    args = parser.parse_args()
+
+    if "show" in args and args.show == "active-toolchain":
+        print(triple)
+    elif "toolchain" in args and args.toolchain == "list":
+        print(triple)
+    elif "run" in args:
+        subprocess.run(args.run[1:])
diff --git a/tools/shell.nix b/tools/shell.nix
deleted file mode 100644
index 1b731bfe28..0000000000
--- a/tools/shell.nix
+++ /dev/null
@@ -1,14 +0,0 @@
-# Minimal set of build requirements for Verus
-#
-# Open a shell which has access to nothing but these requirements using
-#    nix-shell --pure tools/shell.nix
-# from the root of the repository.
-
-{ pkgs ? import <nixpkgs> {} }:
-  pkgs.mkShell {
-    nativeBuildInputs = with pkgs; [
-      rustup
-      unzip
-      wget
-    ];
-}

From de0ea1522408fb415c93c84009a3de77a61de720 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Sun, 21 Dec 2025 16:39:53 -0500
Subject: [PATCH 02/14] nits

---
 flake.nix | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/flake.nix b/flake.nix
index 7a5ab8e458..0d60ffde9a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -28,7 +28,7 @@
         formatter = pkgs.nixpkgs-fmt;
         linters = [ pkgs.statix ];
         rust-bin = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.toml;
-        
+
         # Inline rustup
         rustup = pkgs.stdenvNoCC.mkDerivation {
           name = "rustup";
@@ -51,7 +51,7 @@
             maintainers = with lib.maintainers; [ stephen-huan jakeginesin ];
           };
         };
-        
+
         version = "latest";
         src = ./.;
         meta = {
@@ -61,7 +61,7 @@
           maintainers = with lib.maintainers; [ stephen-huan jakeginesin ];
           platforms = systems;
         };
-        
+
         vargo = pkgs.rustPlatform.buildRustPackage (finalAttrs: {
           pname = "vargo";
           inherit version src;
@@ -76,7 +76,7 @@
           cargoHash = "sha256-0WJEW3FtoWxMaedqBoCmaS0HLsLjxtBlBClAXcjf/6s=";
           meta = meta // { mainProgram = "vargo"; };
         });
-        
+
         verus = pkgs.rustPlatform.buildRustPackage {
           pname = "verus";
           inherit version src;
@@ -118,7 +118,7 @@
           passthru = { inherit vargo; };
           meta = meta // { mainProgram = "verus"; };
         };
-        
+
         z3 = pkgs.z3.overrideAttrs (finalAttrs: previousAttrs: {
           version = "4.12.5";
           src = pkgs.fetchFromGitHub {
@@ -163,7 +163,7 @@
             initialPath = [ pkgs.coreutils ];
           };
         }) {
-          packages = with self.packages.${system}; [
+          packages = [
             rust-bin
             rustup
             vargo

From 8005395015f10ae5f3f10f8a9f1031e4bac77fac Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Sun, 21 Dec 2025 16:42:13 -0500
Subject: [PATCH 03/14] remove result, update .envrc, .gitignore

---
 .gitignore        | 1 +
 result            | 1 -
 source/.envrc     | 7 ++++++-
 source/.gitignore | 1 +
 4 files changed, 8 insertions(+), 2 deletions(-)
 delete mode 120000 result

diff --git a/.gitignore b/.gitignore
index 92b1212b4e..960f17e219 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,3 +5,4 @@
 /.vscode/settings.json
 /.vscode/launch.json
 /.vscode/tasks.json
+result
diff --git a/result b/result
deleted file mode 120000
index b3fd69363e..0000000000
--- a/result
+++ /dev/null
@@ -1 +0,0 @@
-/nix/store/5zjy3m5aqnbrcawkd7n92fgmvlfqky63-verus-latest
\ No newline at end of file
diff --git a/source/.envrc b/source/.envrc
index 346b1287b8..8d783d3f19 100644
--- a/source/.envrc
+++ b/source/.envrc
@@ -1 +1,6 @@
-source ../tools/activate
+if command -v nix >/dev/null 2>&1
+then
+  use flake ..
+else
+  source ../tools/activate
+fi
diff --git a/source/.gitignore b/source/.gitignore
index 089a94d6ea..db00030316 100644
--- a/source/.gitignore
+++ b/source/.gitignore
@@ -4,3 +4,4 @@ target/
 /.verus-log/
 doc/
 /target-verus/
+.direnv/

From a9e55196ebc856c8b7d4b14bcde19b1b76270c32 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Sun, 21 Dec 2025 16:46:10 -0500
Subject: [PATCH 04/14] simplify derivations

---
 flake.nix | 19 +++----------------
 1 file changed, 3 insertions(+), 16 deletions(-)

diff --git a/flake.nix b/flake.nix
index 0d60ffde9a..1268255ccc 100644
--- a/flake.nix
+++ b/flake.nix
@@ -66,14 +66,10 @@
           pname = "vargo";
           inherit version src;
           buildAndTestSubdir = "tools/vargo";
+          cargoRoot = "tools/vargo";
           cargoLock = {
             lockFile = ./tools/vargo/Cargo.lock;
           };
-          postPatch = ''
-            cp ${./tools/vargo/Cargo.lock} Cargo.lock
-            cp rust-toolchain.toml source/
-          '';
-          cargoHash = "sha256-0WJEW3FtoWxMaedqBoCmaS0HLsLjxtBlBClAXcjf/6s=";
           meta = meta // { mainProgram = "vargo"; };
         });
 
@@ -81,17 +77,8 @@
           pname = "verus";
           inherit version src;
           buildAndTestSubdir = "source";
-          cargoLock = {
-            lockFile = ./source/Cargo.lock;
-            outputHashes = {
-              "getopts-0.2.21" = "sha256-N/QJvyOmLoU5TabrXi8i0a5s23ldeupmBUzP8waVOiU=";
-              "smt2parser-0.6.1" = "sha256-AKBq8Ph8D2ucyaBpmDtOypwYie12xVl4gLRxttv5Ods=";
-            };
-          };
-          postPatch = ''
-            cp ${./source/Cargo.lock} Cargo.lock
-          '';
-          cargoHash = "sha256-y3SmOo6pCfJfPNN+9yUN7FeFcrmJ8xL4rQrjqtSe96M=";
+          cargoRoot = "source";
+          cargoHash = "sha256-hxEH8qurjEDiXX2GGfZF4FTKaMz2e7O1rKHsb+ywnvc=";
           nativeBuildInputs = [ pkgs.makeBinaryWrapper rust-bin rustup vargo z3 ];
           buildInputs = [ rustup z3 ];
           buildPhase = ''

From ba19fc61139a39a43086e0eb0ed4e38ed06c624f Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Sun, 21 Dec 2025 22:55:38 -0500
Subject: [PATCH 05/14] more fine-grain src, set srcRoot

---
 flake.nix | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/flake.nix b/flake.nix
index 1268255ccc..030d85c336 100644
--- a/flake.nix
+++ b/flake.nix
@@ -53,7 +53,6 @@
         };
 
         version = "latest";
-        src = ./.;
         meta = {
           homepage = "https://github.com/verus-lang/verus";
           description = "Verified Rust for low-level systems code";
@@ -64,9 +63,9 @@
 
         vargo = pkgs.rustPlatform.buildRustPackage (finalAttrs: {
           pname = "vargo";
-          inherit version src;
-          buildAndTestSubdir = "tools/vargo";
-          cargoRoot = "tools/vargo";
+          inherit version;
+          src = ./tools;
+          sourceRoot = "tools/vargo";
           cargoLock = {
             lockFile = ./tools/vargo/Cargo.lock;
           };
@@ -75,17 +74,16 @@
 
         verus = pkgs.rustPlatform.buildRustPackage {
           pname = "verus";
-          inherit version src;
-          buildAndTestSubdir = "source";
-          cargoRoot = "source";
+          inherit version;
+          srcs = [ ./source ./tools ./dependencies ];
+          sourceRoot = "source";
           cargoHash = "sha256-hxEH8qurjEDiXX2GGfZF4FTKaMz2e7O1rKHsb+ywnvc=";
           nativeBuildInputs = [ pkgs.makeBinaryWrapper rust-bin rustup vargo z3 ];
           buildInputs = [ rustup z3 ];
           buildPhase = ''
             runHook preBuild
-            cd source
             ln -s ${lib.getExe z3} ./z3
-            ln -sf ../rust-toolchain.toml rust-toolchain.toml
+            ln -sf ${./rust-toolchain.toml} ../rust-toolchain.toml
             vargo build --release
             runHook postBuild
           '';

From 5fff9b7c6001884850db0c96b86b8c7472f9aa1c Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Mon, 22 Dec 2025 02:09:44 -0500
Subject: [PATCH 06/14] use flake ref

---
 flake.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/flake.nix b/flake.nix
index 030d85c336..e9b4aa7e21 100644
--- a/flake.nix
+++ b/flake.nix
@@ -52,7 +52,7 @@
           };
         };
 
-        version = "latest";
+        version = self.rev or "dirty";
         meta = {
           homepage = "https://github.com/verus-lang/verus";
           description = "Verified Rust for low-level systems code";

From c677f7c9849e8cdd599c18264cc2e01bcd3562e4 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Mon, 22 Dec 2025 02:21:03 -0500
Subject: [PATCH 07/14] add z3 comment

---
 flake.nix | 1 +
 1 file changed, 1 insertion(+)

diff --git a/flake.nix b/flake.nix
index e9b4aa7e21..7baf66285a 100644
--- a/flake.nix
+++ b/flake.nix
@@ -104,6 +104,7 @@
           meta = meta // { mainProgram = "verus"; };
         };
 
+        # EXPECTED_Z3_VERSION in tools/common/consts.rs
         z3 = pkgs.z3.overrideAttrs (finalAttrs: previousAttrs: {
           version = "4.12.5";
           src = pkgs.fetchFromGitHub {

From 99b144bb4d25aafe374d59cef4eba6012a259b05 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Mon, 22 Dec 2025 04:49:00 -0500
Subject: [PATCH 08/14] add cvc5

---
 flake.nix | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

diff --git a/flake.nix b/flake.nix
index 7baf66285a..a5e04164c4 100644
--- a/flake.nix
+++ b/flake.nix
@@ -96,7 +96,7 @@
             ln -s $out/rust_verify $out/bin/rust_verify
             ln -s $out/cargo-verus $out/bin/cargo-verus
             ln -s $out/z3 $out/bin/z3
-            wrapProgram $out/bin/verus --prefix PATH : ${lib.makeBinPath [ rustup rust-bin z3 ]}
+            wrapProgram $out/bin/verus --prefix PATH : ${lib.makeBinPath [ rustup rust-bin z3 cvc5 ]}
             runHook postInstall
           '';
           doCheck = false;
@@ -114,11 +114,24 @@
             sha256 = "sha256-Qj9w5s02OSMQ2qA7HG7xNqQGaUacA1d4zbOHynq5k+A=";
           };
         });
+        cvc5' = pkgs.cvc5.override {
+          cadical = pkgs.cadical.override { version = "2.0.0"; };
+        };
+        # EXPECTED_CVC5_VERSION in tools/common/consts.rs
+        cvc5 = cvc5'.overrideAttrs (finalAttrs: previousAttrs: {
+          version = "1.1.2";
+          src = pkgs.fetchFromGitHub {
+            owner = "cvc5";
+            repo = "cvc5";
+            tag = "cvc5-${finalAttrs.version}";
+            hash = "sha256-v+3/2IUslQOySxFDYgTBWJIDnyjbU2RPdpfLcIkEtgQ=";
+          };
+        });
       in
       {
         packages.${system} = rec {
           default = verus;
-          inherit rust-bin rustup vargo verus;
+          inherit rust-bin rustup vargo verus z3 cvc5;
         };
         formatter.${system} = formatter;
         checks.${system}.lint = pkgs.stdenvNoCC.mkDerivation {

From 522803eff3c13fca09ca0a3454e309038a7cf300 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Mon, 22 Dec 2025 05:53:41 -0500
Subject: [PATCH 09/14] expose z3 and cvc5

---
 flake.nix     | 2 ++
 source/.envrc | 1 +
 2 files changed, 3 insertions(+)

diff --git a/flake.nix b/flake.nix
index a5e04164c4..7faf14f2fd 100644
--- a/flake.nix
+++ b/flake.nix
@@ -167,6 +167,8 @@
             rustup
             vargo
             verus
+            z3
+            cvc5
           ];
         };
       }
diff --git a/source/.envrc b/source/.envrc
index 8d783d3f19..d9b00885d4 100644
--- a/source/.envrc
+++ b/source/.envrc
@@ -1,6 +1,7 @@
 if command -v nix >/dev/null 2>&1
 then
   use flake ..
+  ln -sf "$(nix build .#z3 --print-out-paths --no-link)/bin/z3" z3
 else
   source ../tools/activate
 fi

From ca8a6a884e7d9dc475697ebd355f4ca11aa54ce8 Mon Sep 17 00:00:00 2001
From: Stephen Huan <stephen.huan@cgdct.moe>
Date: Mon, 22 Dec 2025 06:29:06 -0500
Subject: [PATCH 10/14] add verusfmt

---
 flake.nix | 46 +++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 43 insertions(+), 3 deletions(-)

diff --git a/flake.nix b/flake.nix
index 7faf14f2fd..07fb13f0d8 100644
--- a/flake.nix
+++ b/flake.nix
@@ -26,7 +26,7 @@
           inherit system overlays;
         };
         formatter = pkgs.nixpkgs-fmt;
-        linters = [ pkgs.statix ];
+        linters = [ pkgs.statix vargo verusfmt ];
         rust-bin = pkgs.rust-bin.fromRustupToolchainFile ./rust-toolchain.toml;
 
         # Inline rustup
@@ -104,6 +104,38 @@
           meta = meta // { mainProgram = "verus"; };
         };
 
+        verusfmt = pkgs.rustPlatform.buildRustPackage (finalAttrs: {
+          pname = "verusfmt";
+          version = "0.6.1";
+
+          src = pkgs.fetchFromGitHub {
+            owner = "verus-lang";
+            repo = "verusfmt";
+            tag = "v${finalAttrs.version}";
+            hash = "sha256-+NHI2dvCxEGVIUF9zO2aVvVbPSLRtsHFCIHU4cfRzUY=";
+          };
+
+          cargoHash = "sha256-8r8PzBrYZWibeFDh2nENctEEkigUzQeD9uD0Jl/Nv5U=";
+
+          nativeCheckInputs = [ pkgs.cargo pkgs.rustfmt ];
+
+          doCheck = true;
+
+          meta = {
+            homepage = "https://github.com/verus-lang/verusfmt";
+            description = "An Opinionated Formatter for Verus";
+            license = lib.licenses.mit;
+            mainProgram = "verusfmt";
+            maintainers = with lib.maintainers; [ stephen-huan ];
+            platforms = [
+              "x86_64-linux"
+              "x86_64-darwin"
+              "aarch64-darwin"
+              "x86_64-windows"
+            ];
+          };
+        });
+
         # EXPECTED_Z3_VERSION in tools/common/consts.rs
         z3 = pkgs.z3.overrideAttrs (finalAttrs: previousAttrs: {
           version = "4.12.5";
@@ -131,9 +163,16 @@
       {
         packages.${system} = rec {
           default = verus;
-          inherit rust-bin rustup vargo verus z3 cvc5;
+          inherit rust-bin rustup vargo verus verusfmt z3 cvc5;
+        };
+        formatter.${system} = pkgs.writeShellApplication {
+          name = "formatter";
+          runtimeInputs = [ verusfmt ] ++ lib.singleton formatter;
+          text = ''
+            nixpkgs-fmt "$@"
+            find vstd -name \*.rs -print0 | xargs -0 -n1 verusfmt
+          '';
         };
-        formatter.${system} = formatter;
         checks.${system}.lint = pkgs.stdenvNoCC.mkDerivation {
           name = "lint";
           src = ./.;
@@ -167,6 +206,7 @@
             rustup
             vargo
             verus
+            verusfmt
             z3
             cvc5
           ];

From f9d2c63ba9cfd98f50bed877372e1994836d8be5 Mon Sep 17 00:00:00 2001
From: Jake Ginesin <jakeginesin@gmail.com>
Date: Thu, 15 Jan 2026 19:14:30 -0500
Subject: [PATCH 11/14] moar

---
 flake.lock | 12 ++++++------
 flake.nix  |  6 +++++-
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/flake.lock b/flake.lock
index d19a3cc547..2e29f2bb2b 100644
--- a/flake.lock
+++ b/flake.lock
@@ -2,11 +2,11 @@
   "nodes": {
     "nixpkgs": {
       "locked": {
-        "lastModified": 1764950072,
-        "narHash": "sha256-BmPWzogsG2GsXZtlT+MTcAWeDK5hkbGRZTeZNW42fwA=",
+        "lastModified": 1768305791,
+        "narHash": "sha256-AIdl6WAn9aymeaH/NvBj0H9qM+XuAuYbGMZaP0zcXAQ=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "f61125a668a320878494449750330ca58b78c557",
+        "rev": "1412caf7bf9e660f2f962917c14b1ea1c3bc695e",
         "type": "github"
       },
       "original": {
@@ -29,11 +29,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1765161692,
-        "narHash": "sha256-XdY9AFzmgRPYIhP4N+WiCHMNxPoifP5/Ld+orMYBD8c=",
+        "lastModified": 1768445213,
+        "narHash": "sha256-y0BglISgDr61vvdb35m0O4npuqh1pojlBNDILo9j8AI=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "7ed7e8c74be95906275805db68201e74e9904f07",
+        "rev": "1cd63408e71cc0e6a89ff2cb7c4107214e2523cc",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 07fb13f0d8..9e8a7e4e29 100644
--- a/flake.nix
+++ b/flake.nix
@@ -77,7 +77,8 @@
           inherit version;
           srcs = [ ./source ./tools ./dependencies ];
           sourceRoot = "source";
-          cargoHash = "sha256-hxEH8qurjEDiXX2GGfZF4FTKaMz2e7O1rKHsb+ywnvc=";
+          # cargoHash = "sha256-hxEH8qurjEDiXX2GGfZF4FTKaMz2e7O1rKHsb+ywnvc=";
+          cargoHash = "sha256-y3wfW3a8A/bfCYklV0DcOODvzcBuzXh1i8U14quW1xY=";
           nativeBuildInputs = [ pkgs.makeBinaryWrapper rust-bin rustup vargo z3 ];
           buildInputs = [ rustup z3 ];
           buildPhase = ''
@@ -145,6 +146,9 @@
             tag = "z3-${finalAttrs.version}";
             sha256 = "sha256-Qj9w5s02OSMQ2qA7HG7xNqQGaUacA1d4zbOHynq5k+A=";
           };
+          # NIX_CFLAGS_COMPILE = "-Wno-error=maybe-uninitialized -Wno-error=uninitialized";
+          # GCC 14 fixes: suppress template body checks and uninitialized warnings
+          NIX_CFLAGS_COMPILE = "-Wno-template-body -Wno-error=maybe-uninitialized -Wno-error=uninitialized";
         });
         cvc5' = pkgs.cvc5.override {
           cadical = pkgs.cadical.override { version = "2.0.0"; };

From 61a0a4609d5ec39dea671826a67783b3f0bbb589 Mon Sep 17 00:00:00 2001
From: Jake Ginesin <jakeginesin@gmail.com>
Date: Sat, 7 Feb 2026 19:32:41 -0500
Subject: [PATCH 12/14] updated lockfile and flake

---
 flake.lock |  12 ++---
 flake.nix  | 152 ++++++++++++++++++++++++++++++++++++++++++++---------
 2 files changed, 133 insertions(+), 31 deletions(-)

diff --git a/flake.lock b/flake.lock
index 2e29f2bb2b..e21141829d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -2,11 +2,11 @@
   "nodes": {
     "nixpkgs": {
       "locked": {
-        "lastModified": 1768305791,
-        "narHash": "sha256-AIdl6WAn9aymeaH/NvBj0H9qM+XuAuYbGMZaP0zcXAQ=",
+        "lastModified": 1770197578,
+        "narHash": "sha256-AYqlWrX09+HvGs8zM6ebZ1pwUqjkfpnv8mewYwAo+iM=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "1412caf7bf9e660f2f962917c14b1ea1c3bc695e",
+        "rev": "00c21e4c93d963c50d4c0c89bfa84ed6e0694df2",
         "type": "github"
       },
       "original": {
@@ -29,11 +29,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1768445213,
-        "narHash": "sha256-y0BglISgDr61vvdb35m0O4npuqh1pojlBNDILo9j8AI=",
+        "lastModified": 1770433312,
+        "narHash": "sha256-IaiqGwmLBrR0z67t/oaS6GIFxv9V8mDY7dBTuYVTbKY=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "1cd63408e71cc0e6a89ff2cb7c4107214e2523cc",
+        "rev": "9922ff9f99a6436756cbe6f5d11f9c3630e58cf0",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 9e8a7e4e29..c65340e33d 100644
--- a/flake.nix
+++ b/flake.nix
@@ -18,6 +18,11 @@
       ];
       eachDefaultSystem = f: builtins.foldl' lib.attrsets.recursiveUpdate { }
         (map f systems);
+
+      # Set Z3_SOURCE_BUILD=1 or CVC5_SOURCE_BUILD=1 to build from source.
+      # Requires --impure flag: nix build --impure .#verus
+      z3SourceBuild = (builtins.getEnv "Z3_SOURCE_BUILD") == "1";
+      cvc5SourceBuild = (builtins.getEnv "CVC5_SOURCE_BUILD") == "1";
     in
     eachDefaultSystem (system:
       let
@@ -77,8 +82,12 @@
           inherit version;
           srcs = [ ./source ./tools ./dependencies ];
           sourceRoot = "source";
-          # cargoHash = "sha256-hxEH8qurjEDiXX2GGfZF4FTKaMz2e7O1rKHsb+ywnvc=";
-          cargoHash = "sha256-y3wfW3a8A/bfCYklV0DcOODvzcBuzXh1i8U14quW1xY=";
+          cargoLock = {
+            lockFile = ./source/Cargo.lock;
+            outputHashes = {
+              "getopts-0.2.21" = "sha256-N/QJvyOmLoU5TabrXi8i0a5s23ldeupmBUzP8waVOiU=";
+            };
+          };
           nativeBuildInputs = [ pkgs.makeBinaryWrapper rust-bin rustup vargo z3 ];
           buildInputs = [ rustup z3 ];
           buildPhase = ''
@@ -137,25 +146,128 @@
           };
         });
 
-        # EXPECTED_Z3_VERSION in tools/common/consts.rs
-        z3 = pkgs.z3.overrideAttrs (finalAttrs: previousAttrs: {
-          version = "4.12.5";
+        # --- z3 ---
+
+        z3Version = "4.12.5";
+
+        z3Filename = {
+          x86_64-linux = "z3-${z3Version}-x64-glibc-2.31";
+          aarch64-linux = "z3-${z3Version}-arm64-glibc-2.35";
+          x86_64-darwin = "z3-${z3Version}-x64-osx-11.7.10";
+          aarch64-darwin = "z3-${z3Version}-arm64-osx-11.0";
+          # x86_64-windows = "z3-${z3Version}-x64-win";
+        }.${system} or (throw "Unsupported system for prebuilt z3: ${system}");
+
+        z3PrebuiltHash = {
+          x86_64-linux = "sha256-kHWanLxL180OPiDSvrxXjgyd/sKFHVgX5/SFfL+pJJs=";
+          aarch64-linux = "sha256-+kPQBHmKI7HyCp7oSFNAm321hXwyonSSVXTTvo4tVSA=";
+          x86_64-darwin = "sha256-SfDKEz5p75HGM4lkyQUNPBnQZKtU9cTch6KkTeN94+E=";
+          aarch64-darwin = "sha256-Dkrqjn56UIZcNYKDFZkn2QVLWou4Vf0NjKIITSsweeU=";
+        }.${system} or "sha256-kHWanLxL180OPiDSvrxXjgyd/sKFHVgX5/SFfL+pJJs="; # default to x86_64-linux
+
+        z3Prebuilt = pkgs.stdenvNoCC.mkDerivation {
+          pname = "z3";
+          version = z3Version;
+          src = pkgs.fetchzip {
+            url = "https://github.com/Z3Prover/z3/releases/download/z3-${z3Version}/${z3Filename}.zip";
+            hash = z3PrebuiltHash;
+          };
+          dontBuild = true;
+          installPhase = ''
+            runHook preInstall
+            mkdir -p $out/bin
+            cp bin/z3 $out/bin/z3
+            chmod +x $out/bin/z3
+            runHook postInstall
+          '' + lib.optionalString pkgs.stdenvNoCC.isLinux ''
+            patchelf --set-interpreter "$(cat ${pkgs.stdenv.cc}/nix-support/dynamic-linker)" $out/bin/z3 || true
+          '';
+          nativeBuildInputs = lib.optionals pkgs.stdenvNoCC.isLinux [ pkgs.patchelf pkgs.autoPatchelfHook ];
+          buildInputs = lib.optionals pkgs.stdenvNoCC.isLinux [ pkgs.stdenv.cc.cc.lib ];
+          meta = {
+            description = "Z3 theorem prover (prebuilt binary)";
+            mainProgram = "z3";
+            platforms = systems;
+          };
+        };
+
+        z3Source = pkgs.z3.overrideAttrs (finalAttrs: previousAttrs: {
+          version = z3Version;
           src = pkgs.fetchFromGitHub {
             owner = "Z3Prover";
             repo = "z3";
             tag = "z3-${finalAttrs.version}";
             sha256 = "sha256-Qj9w5s02OSMQ2qA7HG7xNqQGaUacA1d4zbOHynq5k+A=";
           };
-          # NIX_CFLAGS_COMPILE = "-Wno-error=maybe-uninitialized -Wno-error=uninitialized";
-          # GCC 14 fixes: suppress template body checks and uninitialized warnings
+          patches = [];
           NIX_CFLAGS_COMPILE = "-Wno-template-body -Wno-error=maybe-uninitialized -Wno-error=uninitialized";
+          # to fix error at InstallCheck time
+          postFixup = (previousAttrs.postFixup or "") + ''
+            if [ -f $dev/lib/pkgconfig/z3.pc ]; then
+              sed -i 's|''${exec_prefix}//|/|g' $dev/lib/pkgconfig/z3.pc
+            fi
+          '';
         });
+
+        z3 = if z3SourceBuild then z3Source else z3Prebuilt;
+
+        # --- cvc5 ---
+
+        cvc5Version = "1.1.2";
+
+        cvc5Filename = {
+          x86_64-linux = "cvc5-Linux-static";
+          aarch64-linux = "cvc5-Linux-static";
+          x86_64-darwin = "cvc5-macOS-static";
+          aarch64-darwin = "cvc5-macOS-arm64-static";
+        }.${system} or (throw "Unsupported system for prebuilt cvc5: ${system}");
+
+        cvc5PrebuiltHash = {
+          x86_64-linux = "sha256-BLJHO87BFnjBctzla/W2VSJtXBHv7WvC7/RsksIxE2Q=";
+          aarch64-linux = "sha256-NR9F9IQK7z6y/NKnshofzxH2V6vMU2glP0KudKw+fTo=";
+          x86_64-darwin = "sha256-Cg/K89SL2c3G/wPco8T5yL0BlLar0gQtpgikcsWewX8=";
+          aarch64-darwin = "sha256-Cg/K89SL2c3G/wPco8T5yL0BlLar0gQtpgikcsWewX8=";
+        }.${system} or "sha256-BLJHO87BFnjBctzla/W2VSJtXBHv7WvC7/RsksIxE2Q="; # default to x86_64-linux
+
+        cvc5Prebuilt = pkgs.stdenvNoCC.mkDerivation {
+          pname = "cvc5";
+          version = cvc5Version;
+          src = pkgs.fetchzip {
+            url = "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5Version}/${cvc5Filename}.zip";
+            hash = cvc5PrebuiltHash;
+          };
+          dontBuild = true;
+          installPhase = ''
+            runHook preInstall
+            mkdir -p $out/bin
+            cp bin/cvc5 $out/bin/cvc5
+            chmod +x $out/bin/cvc5
+            runHook postInstall
+          '' + lib.optionalString pkgs.stdenvNoCC.isLinux ''
+            patchelf --set-interpreter "$(cat ${pkgs.stdenv.cc}/nix-support/dynamic-linker)" $out/bin/cvc5 || true
+          '';
+          nativeBuildInputs = lib.optionals pkgs.stdenvNoCC.isLinux [ pkgs.patchelf pkgs.autoPatchelfHook ];
+          buildInputs = lib.optionals pkgs.stdenvNoCC.isLinux [ pkgs.stdenv.cc.cc.lib ];
+          meta = {
+            description = "cvc5 SMT solver (prebuilt binary)";
+            mainProgram = "cvc5";
+            platforms = systems;
+          };
+        };
+
         cvc5' = pkgs.cvc5.override {
-          cadical = pkgs.cadical.override { version = "2.0.0"; };
+          cadical = pkgs.cadical.overrideAttrs (old: rec {
+            version = "2.0.0";
+            src = pkgs.fetchFromGitHub {
+              owner = "arminbiere";
+              repo = "cadical";
+              tag = "rel-${version}";
+              hash = "sha256-qoeEM9SdpuFuBPeQlCzuhPLcJ+bMQkTUTGiT8QdU8rc=";
+            };
+          });
         };
-        # EXPECTED_CVC5_VERSION in tools/common/consts.rs
-        cvc5 = cvc5'.overrideAttrs (finalAttrs: previousAttrs: {
-          version = "1.1.2";
+        cvc5Source = cvc5'.overrideAttrs (finalAttrs: previousAttrs: {
+          version = cvc5Version;
           src = pkgs.fetchFromGitHub {
             owner = "cvc5";
             repo = "cvc5";
@@ -163,6 +275,8 @@
             hash = "sha256-v+3/2IUslQOySxFDYgTBWJIDnyjbU2RPdpfLcIkEtgQ=";
           };
         });
+
+        cvc5 = if cvc5SourceBuild then cvc5Source else cvc5Prebuilt;
       in
       {
         packages.${system} = rec {
@@ -174,7 +288,7 @@
           runtimeInputs = [ verusfmt ] ++ lib.singleton formatter;
           text = ''
             nixpkgs-fmt "$@"
-            find vstd -name \*.rs -print0 | xargs -0 -n1 verusfmt
+            vargo fmt
           '';
         };
         checks.${system}.lint = pkgs.stdenvNoCC.mkDerivation {
@@ -183,23 +297,11 @@
           doCheck = true;
           nativeCheckInputs = linters ++ lib.singleton formatter;
           checkPhase = ''
-            nixpkgs-fmt --check .
             statix check
+            vargo fmt -- --check
           '';
           installPhase = "touch $out";
         };
-        apps.${system} = {
-          update = {
-            type = "app";
-            program = lib.getExe (pkgs.writeShellApplication {
-              name = "update";
-              runtimeInputs = [ pkgs.nix-update ];
-              text = lib.concatMapStringsSep "\n"
-                (package: "nix-update --flake ${package} || true")
-                (builtins.attrNames self.packages.${system});
-            });
-          };
-        };
         devShells.${system}.default = (pkgs.mkShellNoCC.override {
           stdenv = pkgs.stdenvNoCC.override {
             initialPath = [ pkgs.coreutils ];

From aa09cf497f4c496846b4615d8214b7fffb5dcaa3 Mon Sep 17 00:00:00 2001
From: Jake Ginesin <jakeginesin@gmail.com>
Date: Tue, 10 Feb 2026 13:41:49 -0500
Subject: [PATCH 13/14] add smt2parser

---
 flake.nix | 1 +
 1 file changed, 1 insertion(+)

diff --git a/flake.nix b/flake.nix
index c65340e33d..f8bf9d9439 100644
--- a/flake.nix
+++ b/flake.nix
@@ -85,6 +85,7 @@
           cargoLock = {
             lockFile = ./source/Cargo.lock;
             outputHashes = {
+              "smt2parser-0.6.1" = "";
               "getopts-0.2.21" = "sha256-N/QJvyOmLoU5TabrXi8i0a5s23ldeupmBUzP8waVOiU=";
             };
           };

From ab78a54a9dc4318144369777b85144800ffa32a1 Mon Sep 17 00:00:00 2001
From: Jake Ginesin <jakeginesin@gmail.com>
Date: Tue, 10 Feb 2026 13:43:28 -0500
Subject: [PATCH 14/14] add smt2parser hash

---
 flake.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/flake.nix b/flake.nix
index f8bf9d9439..4fa50a08d8 100644
--- a/flake.nix
+++ b/flake.nix
@@ -85,7 +85,7 @@
           cargoLock = {
             lockFile = ./source/Cargo.lock;
             outputHashes = {
-              "smt2parser-0.6.1" = "";
+              "smt2parser-0.6.1" = "sha256-AKBq8Ph8D2ucyaBpmDtOypwYie12xVl4gLRxttv5Ods=";
               "getopts-0.2.21" = "sha256-N/QJvyOmLoU5TabrXi8i0a5s23ldeupmBUzP8waVOiU=";
             };
           };