diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml
index f8f0c867..b7767b65 100644
--- a/.github/workflows/nix.yml
+++ b/.github/workflows/nix.yml
@@ -26,7 +26,7 @@ jobs:
           github_access_token: ${{ secrets.GITHUB_TOKEN }}
       # Ix CLI
       - run: nix build --print-build-logs --accept-flake-config
-      - run: nix run .#default -- --help
+      - run: nix run .#ix -- --help
       # Ix benches
       - run: nix build .#bench-aiur --print-build-logs --accept-flake-config
       - run: nix build .#bench-blake3 --print-build-logs --accept-flake-config
diff --git a/Ix/Address.lean b/Ix/Address.lean
index acdd2228..7c9a6f84 100644
--- a/Ix/Address.lean
+++ b/Ix/Address.lean
@@ -60,7 +60,7 @@ def natOfHex : Char -> Option Nat
 def hexOfByte (b : UInt8) : String :=
   let hi := hexOfNat (UInt8.toNat (b >>> 4))
   let lo := hexOfNat (UInt8.toNat (b &&& 0xF))
-  String.mk [hi.get!, lo.get!]
+  String.ofList [hi.get!, lo.get!]
 
 /-- Convert a ByteArray to a big-endian hexadecimal string. -/
 def hexOfBytes (ba : ByteArray) : String :=
diff --git a/Ix/Benchmark/Bench.lean b/Ix/Benchmark/Bench.lean
index 178017ba..30de8e62 100644
--- a/Ix/Benchmark/Bench.lean
+++ b/Ix/Benchmark/Bench.lean
@@ -333,10 +333,10 @@ def padWhitespace (input : String) (width : Nat) : String :=
   let padWidth := width - input.length 
   let leftPad := padWidth / 2
   let rightPad := padWidth - leftPad
-  String.mk (List.replicate leftPad ' ') ++ input ++ (String.mk (List.replicate rightPad ' '))
+  String.ofList (List.replicate leftPad ' ') ++ input ++ (String.ofList (List.replicate rightPad ' '))
 
 def padDashes (width : Nat) : String :=
-  String.mk (List.replicate width '-')
+  String.ofList (List.replicate width '-')
 
 def mkReportPretty' (columnWidths : ColumnWidths) (reportPretty : String) (row : BenchReport) : String :=
   let functionStr := padWhitespace row.function columnWidths.function
diff --git a/Ix/Common.lean b/Ix/Common.lean
index e5052730..530ec568 100644
--- a/Ix/Common.lean
+++ b/Ix/Common.lean
@@ -38,8 +38,8 @@ deriving instance BEq, Repr, Ord, Hashable for Lean.QuotKind
 deriving instance BEq, Repr, Ord, Hashable for Lean.ReducibilityHints
 deriving instance BEq, Repr, Ord, Hashable for Lean.DefinitionSafety
 deriving instance BEq, Repr, Ord, Hashable for ByteArray
-deriving instance BEq, Repr, Ord, Hashable for String.Pos
-deriving instance BEq, Repr, Ord, Hashable for Substring
+deriving instance BEq, Repr, Ord, Hashable for String.Pos.Raw
+deriving instance BEq, Repr, Ord, Hashable for Substring.Raw
 deriving instance BEq, Repr, Ord, Hashable for Lean.SourceInfo
 deriving instance BEq, Repr, Ord, Hashable for Lean.Syntax.Preresolved
 deriving instance BEq, Repr, Ord, Hashable for Lean.Syntax
diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean
index e21bc3e7..d276bf71 100644
--- a/Ix/CompileM.lean
+++ b/Ix/CompileM.lean
@@ -227,7 +227,7 @@ def compileLevel (lvl: Lean.Level): CompileM MetaAddress := do
       | none   => do throw <| .levelNotFound (<- read).current n lvls s!"compileLevel"
     | l@(.mvar ..) => throw $ .levelMetavariable l
 
-def compileSubstring : Substring -> CompileM Ixon.Substring
+def compileSubstring : Substring.Raw -> CompileM Ixon.Substring
 | ⟨str, startPos, stopPos⟩ => do
     pure ⟨<- storeString str, startPos.byteIdx, stopPos.byteIdx⟩
 
diff --git a/Ix/Store.lean b/Ix/Store.lean
index 9bf05b73..a476a5e3 100644
--- a/Ix/Store.lean
+++ b/Ix/Store.lean
@@ -43,9 +43,11 @@ def storeDir : StoreIO FilePath := do
 def storePath (addr: Address): StoreIO FilePath := do
   let store <- storeDir
   let hex := hexOfBytes addr.hash
-  let dir1 := String.mk [(hex.get ⟨0⟩), (hex.get ⟨1⟩)]
-  let dir2 := String.mk [(hex.get ⟨2⟩), (hex.get ⟨3⟩)]
-  let dir3 := String.mk [(hex.get ⟨4⟩), (hex.get ⟨5⟩)]
+  -- TODO: Use Slice API once it matures
+  let hexChars := hex.toSlice.chars.toList
+  let dir1 := String.ofList [hexChars[0]!, hexChars[1]!]
+  let dir2 := String.ofList [hexChars[2]!, hexChars[3]!]
+  let dir3 := String.ofList [hexChars[4]!, hexChars[5]!]
   let file := hex.drop 6
   let path := store / dir1 / dir2 / dir3
   if !(<- path.pathExists) then
diff --git a/Tests/Ix.lean b/Tests/Ix.lean
index ccef1c14..5db23ab4 100644
--- a/Tests/Ix.lean
+++ b/Tests/Ix.lean
@@ -119,7 +119,7 @@ def parseHex (x : String) : ByteArray :=
   let x :=
     if x.startsWith "0x" || x.startsWith "0X" then x.drop 2 else x
   -- remove underscores
-  let x := String.mk (x.toList.filter (· ≠ '_'))
+  let x := String.ofList (x.toList.filter (· ≠ '_'))
   -- must have an even number of hex digits
   if x.length % 2 = 1 then
     panic! "parseHex: odd number of hex digits"
@@ -128,8 +128,8 @@ def parseHex (x : String) : ByteArray :=
     let rec loop (i : Nat) (acc : ByteArray) : ByteArray :=
       if i < n then
         -- safe since ASCII: `String.get!` indexes by chars
-        let c1 := x.get! ⟨i⟩
-        let c2 := x.get! ⟨i+1⟩
+        let c1 := String.Pos.Raw.get! x ⟨i⟩ 
+        let c2 := String.Pos.Raw.get! x ⟨i+1⟩
         match hexVal? c1, hexVal? c2 with
         | some hi, some lo =>
           let b : UInt8 := (hi <<< 4) ||| lo
@@ -148,8 +148,8 @@ def printHex (ba : ByteArray) : String :=
       let b := ba.get! i
       let hi := (b.toNat / 16)
       let lo := (b.toNat % 16)
-      let acc := acc.push (hexdigits.get! ⟨hi⟩)
-      let acc := acc.push (hexdigits.get! ⟨lo⟩)
+      let acc := acc.push (String.Pos.Raw.get! hexdigits ⟨hi⟩)
+      let acc := acc.push (String.Pos.Raw.get! hexdigits ⟨lo⟩)
       go (i + 1) acc
     else acc
   "0x" ++ go 0 ""
diff --git a/deny.toml b/deny.toml
index 6519dae3..11d7152e 100644
--- a/deny.toml
+++ b/deny.toml
@@ -75,7 +75,6 @@ ignore = [
     "RUSTSEC-2024-0370", # `proc-macro-error` crate is unmaintained
     "RUSTSEC-2023-0089", # `atomic-polyfill` crate is unmaintained
     "RUSTSEC-2025-0141", # `bincode` crate is unmaintained
-
     #{ id = "RUSTSEC-0000-0000", reason = "you can specify a reason the advisory is ignored" },
     #"a-crate-that-is-yanked@0.1.1", # you can also ignore yanked crate versions if you wish
     #{ crate = "a-crate-that-is-yanked@0.1.1", reason = "you can specify why you are ignoring the yanked crate" },
@@ -122,66 +121,12 @@ exceptions = [
 # Some crates don't have (easily) machine readable licensing information,
 # adding a clarification entry for it allows you to manually specify the
 # licensing information
-[[licenses.clarify]]
-crate = "binius_circuits"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_core"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_field"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_hal"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_hash"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_macros"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_math"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_maybe_rayon"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_ntt"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
-[[licenses.clarify]]
-crate = "binius_utils"
-expression = "Apache-2.0"
-license-files = [
-  { path = "../../LICENSE.txt", hash = 0 }
-]
+# [[licenses.clarify]]
+# crate = "binius_circuits"
+# expression = "Apache-2.0"
+# license-files = [
+#   { path = "../../LICENSE.txt", hash = 0 }
+# ]
 # The package spec the clarification applies to
 #crate = "ring"
 # The SPDX expression for the license requirements of the crate
diff --git a/flake.lock b/flake.lock
index d2aa8952..b0c5033f 100644
--- a/flake.lock
+++ b/flake.lock
@@ -21,18 +21,21 @@
       "inputs": {
         "blake3": "blake3",
         "flake-parts": "flake-parts",
-        "lean4-nix": "lean4-nix",
+        "lean4-nix": [
+          "lean4-nix"
+        ],
         "nixpkgs": [
+          "blake3-lean",
           "lean4-nix",
           "nixpkgs"
         ]
       },
       "locked": {
-        "lastModified": 1761919236,
-        "narHash": "sha256-ZF/+uKH+oLwxm5VTXksBS70Bjt5s9gbSKNjjp2JI2hA=",
+        "lastModified": 1768515341,
+        "narHash": "sha256-r98AAunFEidRoXFWTb8kJkjch9nSEcq95w1ZADJm9Dk=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "732daca6c67f3be3ca44837643cfda906503e9ac",
+        "rev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
         "type": "github"
       },
       "original": {
@@ -83,11 +86,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1754487366,
-        "narHash": "sha256-pHYj8gUBapuUzKV/kN/tR3Zvqc7o6gdFB9XKXIp1SQ8=",
+        "lastModified": 1768135262,
+        "narHash": "sha256-PVvu7OqHBGWN16zSi6tEmPwwHQ4rLPU9Plvs8/1TUBY=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "af66ad14b28a127c5c0f3bbb298218fc63528a18",
+        "rev": "80daad04eddbbf5a4d883996a73f3f542fa437ac",
         "type": "github"
       },
       "original": {
@@ -100,24 +103,6 @@
       "inputs": {
         "nixpkgs-lib": "nixpkgs-lib_2"
       },
-      "locked": {
-        "lastModified": 1727826117,
-        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
-        "type": "github"
-      },
-      "original": {
-        "owner": "hercules-ci",
-        "repo": "flake-parts",
-        "type": "github"
-      }
-    },
-    "flake-parts_3": {
-      "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib_3"
-      },
       "locked": {
         "lastModified": 1762980239,
         "narHash": "sha256-8oNVE8TrD19ulHinjaqONf9QWCKK+w4url56cdStMpM=",
@@ -132,16 +117,16 @@
         "type": "github"
       }
     },
-    "flake-parts_4": {
+    "flake-parts_3": {
       "inputs": {
-        "nixpkgs-lib": "nixpkgs-lib_4"
+        "nixpkgs-lib": "nixpkgs-lib_3"
       },
       "locked": {
-        "lastModified": 1727826117,
-        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
+        "lastModified": 1765835352,
+        "narHash": "sha256-XswHlK/Qtjasvhd1nOa1e8MgZ8GS//jBoTqWtrS1Giw=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
+        "rev": "a34fae9c08a15ad73f295041fec82323541400a9",
         "type": "github"
       },
       "original": {
@@ -152,34 +137,15 @@
     },
     "lean4-nix": {
       "inputs": {
-        "flake-parts": "flake-parts_2",
+        "flake-parts": "flake-parts_3",
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1761368467,
-        "narHash": "sha256-eEs2YpE84+d6a8VKXCACNJy5czcu8GQCaeSZwR/mFMk=",
-        "owner": "lenianiva",
-        "repo": "lean4-nix",
-        "rev": "3550873ed1a87d666d633d34921e79abaa4671c1",
-        "type": "github"
-      },
-      "original": {
-        "owner": "lenianiva",
-        "repo": "lean4-nix",
-        "type": "github"
-      }
-    },
-    "lean4-nix_2": {
-      "inputs": {
-        "flake-parts": "flake-parts_4",
-        "nixpkgs": "nixpkgs_2"
-      },
-      "locked": {
-        "lastModified": 1761368467,
-        "narHash": "sha256-eEs2YpE84+d6a8VKXCACNJy5czcu8GQCaeSZwR/mFMk=",
+        "lastModified": 1768025957,
+        "narHash": "sha256-o9AUUOBq1SKEPGiwjBIP628N9fPNwAjqSm9xXhVEDNY=",
         "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "3550873ed1a87d666d633d34921e79abaa4671c1",
+        "rev": "ecaa70749083e6a0e6e0814c6a66b7561754b6db",
         "type": "github"
       },
       "original": {
@@ -190,11 +156,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1743095683,
-        "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=",
+        "lastModified": 1765779637,
+        "narHash": "sha256-KJ2wa/BLSrTqDjbfyNx70ov/HdgNBCBBSQP3BIzKnv4=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6",
+        "rev": "1306659b587dc277866c7b69eb97e5f07864d8c4",
         "type": "github"
       },
       "original": {
@@ -206,11 +172,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1753579242,
-        "narHash": "sha256-zvaMGVn14/Zz8hnp4VWT9xVnhc8vuL3TStRqwk22biA=",
+        "lastModified": 1765674936,
+        "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "0f36c44e01a6129be94e3ade315a5883f0228a6e",
+        "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85",
         "type": "github"
       },
       "original": {
@@ -220,18 +186,6 @@
       }
     },
     "nixpkgs-lib_2": {
-      "locked": {
-        "lastModified": 1727825735,
-        "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
-      },
-      "original": {
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
-      }
-    },
-    "nixpkgs-lib_3": {
       "locked": {
         "lastModified": 1761765539,
         "narHash": "sha256-b0yj6kfvO8ApcSE+QmA6mUfu8IYG6/uU28OFn4PaC8M=",
@@ -246,31 +200,18 @@
         "type": "github"
       }
     },
-    "nixpkgs-lib_4": {
-      "locked": {
-        "lastModified": 1727825735,
-        "narHash": "sha256-0xHYkMkeLVQAMa7gvkddbPqpxph+hDzdu1XdGPJR+Os=",
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
-      },
-      "original": {
-        "type": "tarball",
-        "url": "https://github.com/NixOS/nixpkgs/archive/fb192fec7cc7a4c26d51779e9bab07ce6fa5597a.tar.gz"
-      }
-    },
-    "nixpkgs_2": {
+    "nixpkgs-lib_3": {
       "locked": {
-        "lastModified": 1743095683,
-        "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=",
-        "owner": "nixos",
-        "repo": "nixpkgs",
-        "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6",
+        "lastModified": 1765674936,
+        "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
+        "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85",
         "type": "github"
       },
       "original": {
-        "owner": "nixos",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
+        "owner": "nix-community",
+        "repo": "nixpkgs.lib",
         "type": "github"
       }
     },
@@ -279,8 +220,8 @@
         "blake3-lean": "blake3-lean",
         "crane": "crane",
         "fenix": "fenix",
-        "flake-parts": "flake-parts_3",
-        "lean4-nix": "lean4-nix_2",
+        "flake-parts": "flake-parts_2",
+        "lean4-nix": "lean4-nix",
         "nixpkgs": [
           "lean4-nix",
           "nixpkgs"
diff --git a/flake.nix b/flake.nix
index d3c4344b..f5cb3364 100644
--- a/flake.nix
+++ b/flake.nix
@@ -29,11 +29,11 @@
 
     crane.url = "github:ipetkov/crane";
 
-    # Blake3 C dependency for static linking
+    # Blake3 C bindings for Lean
     blake3-lean = {
       url = "github:argumentcomputer/Blake3.lean";
-      # Follow lean4-nix nixpkgs so we stay in sync
-      inputs.nixpkgs.follows = "lean4-nix/nixpkgs";
+      # System packages, follows lean4-nix so we stay in sync
+      inputs.lean4-nix.follows = "lean4-nix";
     };
   };
 
@@ -60,7 +60,70 @@
         pkgs,
         ...
       }: let
-        lib = (import ./ix.nix {inherit system pkgs fenix crane lean4-nix blake3-lean;}).lib;
+        # Pins the Rust toolchain
+        rustToolchain = fenix.packages.${system}.fromToolchainFile {
+          file = ./rust-toolchain.toml;
+          sha256 = "sha256-sqSWJDUxc+zaz1nBWMAJKTAGBuGWP25GCftIOlCEAtA=";
+        };
+
+        # Rust package
+        craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;
+        src = craneLib.cleanCargoSource ./.;
+        craneArgs = {
+          inherit src;
+          strictDeps = true;
+
+          buildInputs =
+            []
+            ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [
+              # Additional darwin specific inputs can be set here
+              pkgs.libiconv
+            ];
+        };
+        cargoArtifacts = craneLib.buildDepsOnly craneArgs;
+
+        rustPkg = craneLib.buildPackage (craneArgs
+          // {
+            inherit cargoArtifacts;
+          });
+
+        # Lake package
+        lake2nix = pkgs.callPackage lean4-nix.lake {};
+        lakeDeps = lake2nix.buildDeps {
+          src = ./.;
+          depOverrideDeriv = {
+            Blake3 = blake3-lean.packages.${system}.default;
+          };
+        };
+        lakeBuildArgs = {
+          inherit lakeDeps;
+          src = ./.;
+          # Don't build the `ix_rs` static lib with Lake, since we build it with Crane
+          postPatch = ''
+            substituteInPlace lakefile.lean --replace-fail "let args := match (ixNoPar, ixNet)" "let _args := match (ixNoPar, ixNet)"
+            substituteInPlace lakefile.lean --replace-fail 'proc { cmd := "cargo"' '--proc { cmd := "cargo"'
+          '';
+          # Copy the `ix_rs` static lib from Crane to `target/release` so Lake can use it
+          postConfigure = ''
+            mkdir -p target/release
+            ln -s ${rustPkg}/lib/libix_rs.a target/release/
+          '';
+        };
+        ixLib = lake2nix.mkPackage (lakeBuildArgs
+          // {
+            name = "Ix";
+            buildLibrary = true;
+          });
+        lakeBinArgs =
+          lakeBuildArgs
+          // {
+            lakeArtifacts = ixLib;
+            installArtifacts = false;
+          };
+        ixCLI = lake2nix.mkPackage (lakeBinArgs // {name = "ix";});
+        ixTest = lake2nix.mkPackage (lakeBinArgs // {name = "IxTests";});
+        benchAiur = lake2nix.mkPackage (lakeBinArgs // {name = "bench-aiur";});
+        benchBlake3 = lake2nix.mkPackage (lakeBinArgs // {name = "bench-blake3";});
       in {
         # Lean overlay
         _module.args.pkgs = import nixpkgs {
@@ -69,40 +132,12 @@
         };
 
         packages = {
-          # Ix CLI
-          default = lib.leanPkg.executable;
-
-          # Ix tests
-          test =
-            ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-              src = ./.;
-              roots = ["Tests.Main" "Ix"];
-              deps = [lib.leanPkg];
-              staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
-            }).executable;
-
+          default = ixLib;
+          ix = ixCLI;
+          test = ixTest;
           # Ix benches
-          bench-aiur =
-            ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-              src = ./.;
-              roots = ["Benchmarks.Aiur" "Ix"];
-              deps = [lib.leanPkg];
-              staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
-            }).executable;
-
-          bench-blake3 =
-            ((lean4-nix.lake {inherit pkgs;}).mkPackage {
-              src = ./.;
-              roots = ["Benchmarks.Blake3" "Ix"];
-              deps = [lib.leanPkg];
-              staticLibDeps = ["${lib.rustPkg}/lib" "${lib.cPkg}/lib" "${lib.blake3C}/lib"];
-            }).executable;
-
-          # Rust static lib, needed for static linking downstream
-          rustStaticLib = lib.rustPkg;
-
-          # C static lib, needed for static linking downstream
-          cStaticLib = lib.cPkg;
+          bench-aiur = benchAiur;
+          bench-blake3 = benchBlake3;
         };
 
         # Provide a unified dev shell with Lean + Rust
@@ -113,7 +148,7 @@
             ocl-icd
             gcc
             clang
-            lib.rustToolchain
+            rustToolchain
             rust-analyzer
             lean.lean-all # Includes Lean compiler, lake, stdlib, etc.
           ];
diff --git a/ix.nix b/ix.nix
deleted file mode 100644
index d2521413..00000000
--- a/ix.nix
+++ /dev/null
@@ -1,96 +0,0 @@
-{
-  system,
-  pkgs,
-  fenix,
-  crane,
-  lean4-nix,
-  blake3-lean,
-}: let
-  # Pins the Rust toolchain
-  rustToolchain = fenix.packages.${system}.fromToolchainFile {
-    file = ./rust-toolchain.toml;
-    sha256 = "sha256-SDu4snEWjuZU475PERvu+iO50Mi39KVjqCeJeNvpguU=";
-  };
-
-  # Rust package
-  craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain;
-  src = craneLib.cleanCargoSource ./.;
-  commonArgs = {
-    inherit src;
-    strictDeps = true;
-
-    buildInputs =
-      [
-        # Add additional build inputs here
-      ]
-      ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [
-        # Additional darwin specific inputs can be set here
-        pkgs.libiconv
-      ];
-  };
-  craneLibLLvmTools = craneLib.overrideToolchain rustToolchain;
-  cargoArtifacts = craneLib.buildDepsOnly commonArgs;
-
-  rustPkg = craneLib.buildPackage (commonArgs
-    // {
-      inherit cargoArtifacts;
-    });
-
-  # C Package
-  cPkg = let
-    # Function to get all files in `./c` ending with given extension
-    getFiles = ext: builtins.filter (file: builtins.match (".*" + ext) file != null) (builtins.attrNames (builtins.readDir "${toString ./c}"));
-    # Gets all C files in `./c`, without the extension
-    cFiles = let ext = ".c"; in builtins.map (file: builtins.replaceStrings [ext] [""] file) (getFiles ext);
-    # Creates `gcc -c` command for each C file
-    buildCmd = builtins.map (file: "${pkgs.gcc}/bin/gcc -Wall -Werror -Wextra -c ${file}.c -o ${file}.o") cFiles;
-    # Final `buildPhase` instructions
-    buildSteps =
-      buildCmd
-      ++ [
-        "ar rcs libix_c.a ${builtins.concatStringsSep " " (builtins.map (file: "${file}.o") cFiles)}"
-      ];
-    # Gets all header files in `./c`
-    hFiles = getFiles ".h";
-    # Final `installPhase` instructions
-    installSteps = [
-      "mkdir -p $out/lib $out/include"
-      "cp libix_c.a $out/lib/"
-      "cp ${builtins.concatStringsSep " " hFiles} $out/include/"
-    ];
-  in
-    pkgs.stdenv.mkDerivation {
-      pname = "ix_c";
-      version = "0.1.0";
-      src = ./c;
-      buildInputs = [pkgs.gcc pkgs.lean.lean-all rustPkg];
-      # Builds the C files
-      buildPhase = builtins.concatStringsSep "\n" buildSteps;
-      # Installs the library files
-      installPhase = builtins.concatStringsSep "\n" installSteps;
-    };
-
-  # Blake3.lean C FFI dependency, needed for explicit static lib linking
-  blake3C = blake3-lean.packages.${system}.staticLib;
-
-  # Lean package, builds the Ix binary and links to FFI static libs
-  # Note: downstream users of Ix as a library should import it in the lakefile,
-  # only need to include the static libs as below in the final `mkPackage`
-  leanPkg = (lean4-nix.lake {inherit pkgs;}).mkPackage {
-    src = ./.;
-    roots = ["Ix" "Main"];
-    staticLibDeps = ["${rustPkg}/lib" "${cPkg}/lib" "${blake3C}/lib"];
-  };
-
-  lib = {
-    inherit
-      rustToolchain
-      blake3C
-      rustPkg
-      cPkg
-      leanPkg
-      ;
-  };
-in {
-  inherit lib;
-}
diff --git a/lake-manifest.json b/lake-manifest.json
index 2e51562a..74b38ab6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,40 +5,40 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/argumentcomputer/Blake3.lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "732daca6c67f3be3ca44837643cfda906503e9ac",
+   "rev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "732daca6c67f3be3ca44837643cfda906503e9ac",
+   "inputRev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b05e6b83798bce0887eb5001cb10fdcbe675dde3",
+   "rev": "fdf848d6cda9f080a09e49e760e2d6f70878800b",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "b05e6b83798bce0887eb5001cb10fdcbe675dde3",
+   "inputRev": "fdf848d6cda9f080a09e49e760e2d6f70878800b",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "ix",
diff --git a/lakefile.lean b/lakefile.lean
index 88b667dc..567d85f3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,28 +12,29 @@ lean_exe ix where
   supportInterpreter := true
 
 require LSpec from git
-  "https://github.com/argumentcomputer/LSpec" @ "b05e6b83798bce0887eb5001cb10fdcbe675dde3"
+  "https://github.com/argumentcomputer/LSpec" @ "fdf848d6cda9f080a09e49e760e2d6f70878800b"
 
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "732daca6c67f3be3ca44837643cfda906503e9ac"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "f66794edb4612106cd7b04a7fbd04917fb1abb7d"
 
 require Cli from git
-  "https://github.com/leanprover/lean4-cli" @ "91c18fa62838ad0ab7384c03c9684d99d306e1da"
+  "https://github.com/leanprover/lean4-cli" @ "v4.26.0"
 
 require batteries from git
-  "https://github.com/leanprover-community/batteries" @ "8da40b72fece29b7d3fe3d768bac4c8910ce9bee"
+  "https://github.com/leanprover-community/batteries" @ "v4.26.0"
 
 section Tests
 
 lean_lib Tests
 
 @[test_driver]
-lean_exe Tests.Main where
+lean_exe IxTests where
+  root := `Tests.Main
   supportInterpreter := true
 
 end Tests
 
-lean_lib IxTest where
+lean_lib IxTestLib where
   srcDir := "ix_test"
 
 section IxApplications
@@ -142,7 +143,7 @@ script install := do
   return 0
 
 script "check-lean-h-hash" := do
-  let cachedLeanHHash := 1323938820889983873
+  let cachedLeanHHash := 11261383907494897568
 
   let leanIncludeDir ← getLeanIncludeDir
   let includedLeanHPath := leanIncludeDir / "lean" / "lean.h"
@@ -154,6 +155,8 @@ script "check-lean-h-hash" := do
     IO.eprintln   "  1. Double-check changes made to lean/lean.h"
     IO.eprintln s!"  2. Cache {includedLeanHHash} instead"
     return 1
+  else
+    IO.println "lean/lean.h hash matches ✓"
   return 0
 
 script "get-exe-targets" := do
diff --git a/lean-toolchain b/lean-toolchain
index c00a5350..e59446d5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.26.0
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index dccca02c..a5b578d8 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -1,4 +1,4 @@
 [toolchain]
 # The default profile includes rustc, rust-std, cargo, rust-docs, rustfmt and clippy.
 profile = "default"
-channel = "1.91"
+channel = "1.92"