diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 4658f50..52532e8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -25,12 +25,8 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - uses: cachix/install-nix-action@v30
+      - uses: cachix/install-nix-action@v31
         with:
           nix_path: nixpkgs=channel:nixos-unstable
           github_access_token: ${{ secrets.GITHUB_TOKEN }}
-      - uses: cachix/cachix-action@v14
-        with:
-          name: argumentcomputer
-          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-      - run: nix build
+      - run: nix build --accept-flake-config
diff --git a/LSpec/Examples.lean b/Examples/Examples.lean
similarity index 88%
rename from LSpec/Examples.lean
rename to Examples/Examples.lean
index 60db2fe..c656927 100644
--- a/LSpec/Examples.lean
+++ b/Examples/Examples.lean
@@ -25,6 +25,29 @@ This instance is generic enough that tests like `∀ n, n < 10 → n - 5 < 5` ca
 -/
 #lspec test "all lt" $ ∀ n, n < 10 → n - 5 < 5
 
+/-
+It is also possible to run tests inside the `IO` monad. The purpose of these tests is to plug in
+`LSpec` into a testing script for a `lake script`
+-/
+
+def fourIO : IO Nat :=
+  return 4
+
+def fiveIO : IO Nat :=
+  return 5
+
+def main := do
+  let four ← fourIO
+  let five ← fiveIO
+  lspecIO $
+    test "fourIO equals 4" (four = 4) $
+    test "fiveIO equals 5" (five = 5)
+
+#eval main
+-- ✓ fourIO equals 4
+-- ✓ fiveIO equals 5
+-- 0
+
 /-
 There are even more ways to invoke LSpec tests (`lspecEachIO` for example) for more intricate moandic
 testing
diff --git a/LSpec/Testing.lean b/Examples/Testing.lean
similarity index 100%
rename from LSpec/Testing.lean
rename to Examples/Testing.lean
diff --git a/LSpec.lean b/LSpec.lean
index d215c2b..50f1702 100644
--- a/LSpec.lean
+++ b/LSpec.lean
@@ -1,3 +1,3 @@
 import LSpec.LSpec
 import LSpec.Instances
-import LSpec.SlimCheck.Checkable
+import LSpec.SlimCheck
diff --git a/LSpec/LSpec.lean b/LSpec/LSpec.lean
index c98a393..3dab516 100644
--- a/LSpec/LSpec.lean
+++ b/LSpec/LSpec.lean
@@ -183,7 +183,7 @@ def lspecIO (map : HashMap String (List TestSeq)) (args : List String) : IO UInt
   let filteredMap :=
     if args.isEmpty then map
     else Id.run do
-      let mut acc := .empty
+      let mut acc := .emptyWithCapacity args.length
       for arg in args do
         for (key, tSeq) in map do
           if key.startsWith arg then
@@ -191,7 +191,7 @@ def lspecIO (map : HashMap String (List TestSeq)) (args : List String) : IO UInt
       pure acc
 
   -- Accumulate error messages
-  let mut testsWithErrors : HashMap String (Array String) := .empty
+  let mut testsWithErrors : HashMap String (Array String) := .emptyWithCapacity map.size
   for (key, tSeqs) in filteredMap do
     IO.println key
     for tSeq in tSeqs do
diff --git a/LSpec/SlimCheck.lean b/LSpec/SlimCheck.lean
new file mode 100644
index 0000000..111b730
--- /dev/null
+++ b/LSpec/SlimCheck.lean
@@ -0,0 +1,3 @@
+import LSpec.SlimCheck.Gen
+import LSpec.SlimCheck.Checkable
+import LSpec.SlimCheck.Sampleable
diff --git a/LSpec/SlimCheck/Control/Random.lean b/LSpec/SlimCheck/Control/Random.lean
index f19a68a..126e351 100644
--- a/LSpec/SlimCheck/Control/Random.lean
+++ b/LSpec/SlimCheck/Control/Random.lean
@@ -83,8 +83,10 @@ def rand (α : Type u) [Random α] [range : DefaultRange α] [RandomGen g] : Ran
 def randBound (α : Type u) [Random α] (lo hi : α) [RandomGen g] : RandT g α :=
   Random.randomR lo hi
 
-def randFin {n : Nat} [RandomGen g] : RandT g (Fin n.succ) :=
-  λ ⟨g⟩ => randNat g 0 n.succ |>.map (Fin.ofNat' _) ULift.up
+def randFin {n : Nat} [NeZero n] [RandomGen g] : RandT g (Fin n) :=
+  λ ⟨g⟩ =>
+    let (x, gen) := randNat g 0 n.succ
+    (Fin.ofNat n x, ULift.up gen)
 
 instance : Random Bool where
   randomR := fun lo hi g =>
@@ -99,10 +101,10 @@ instance : Random Nat where
     let (n, g') := randNat g.down lo hi
     (n, .up g')
 
-instance {n : Nat} : Random (Fin n.succ) where
+instance {n : Nat} [NeZero n] : Random (Fin n) where
   randomR := fun lo hi g =>
-    let (n, g') := randNat g.down lo hi
-    (.ofNat' _ n, .up g')
+    let (x, g') := randNat g.down lo hi
+    (Fin.ofNat n x, .up g')
 
 instance : Random Int where
   randomR := fun lo hi g =>
diff --git a/LSpec/SlimCheck/Sampleable.lean b/LSpec/SlimCheck/Sampleable.lean
index 8e84567..999b24c 100644
--- a/LSpec/SlimCheck/Sampleable.lean
+++ b/LSpec/SlimCheck/Sampleable.lean
@@ -126,7 +126,7 @@ instance Nat.shrinkable : Shrinkable Nat where
   shrink := Nat.shrink
 
 /-- `Fin.shrink` works like `Nat.shrink` but instead operates on `Fin`. -/
-partial def Fin.shrink {n : Nat} (m : Fin n.succ) : List (Fin n.succ) :=
+partial def Fin.shrink {n : Nat} [NeZero n] (m : Fin n) : List (Fin n) :=
   if 0 < m then
     let m := m / 2
     let rest := shrink m
@@ -134,7 +134,7 @@ partial def Fin.shrink {n : Nat} (m : Fin n.succ) : List (Fin n.succ) :=
   else
     []
 
-instance Fin.shrinkable {n : Nat} : Shrinkable (Fin n.succ) where
+instance Fin.shrinkable {n : Nat} [NeZero n] : Shrinkable (Fin n) where
   shrink := Fin.shrink
 
 local instance Int_sizeOfAbs : SizeOf Int := ⟨Int.natAbs⟩
@@ -162,8 +162,8 @@ open Gen SampleableExt
 instance Nat.sampleableExt : SampleableExt Nat :=
   mkSelfContained (do choose Nat 0 (← getSize))
 
-instance Fin.sampleableExt {n : Nat} : SampleableExt (Fin (n.succ)) :=
-  mkSelfContained (do choose (Fin n.succ) (Fin.ofNat' _ 0) (Fin.ofNat' _ (← getSize)))
+instance Fin.sampleableExt {n : Nat} [NeZero n] : SampleableExt (Fin n) :=
+  mkSelfContained (do choose (Fin n) (Fin.ofNat n 0) (Fin.ofNat n (← getSize)))
 
 instance Int.sampleableExt : SampleableExt Int :=
   mkSelfContained (do choose Int (-(← getSize)) (← getSize))
diff --git a/flake.lock b/flake.lock
index 91c25fb..3ee6b10 100644
--- a/flake.lock
+++ b/flake.lock
@@ -23,11 +23,11 @@
         "nixpkgs-lib": "nixpkgs-lib_2"
       },
       "locked": {
-        "lastModified": 1743550720,
-        "narHash": "sha256-hIshGgKZCgWh6AYJpJmRgFdR3WUbkY04o82X05xqQiY=",
+        "lastModified": 1727826117,
+        "narHash": "sha256-K5ZLCyfO/Zj9mPFldf3iwS6oZStJcU4tSpiXTMYaaL0=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "c621e8422220273271f52058f618c94e405bb0f5",
+        "rev": "3d04084d54bedc3d6b8b736c70ef449225c361b1",
         "type": "github"
       },
       "original": {
@@ -39,31 +39,29 @@
     "lean4-nix": {
       "inputs": {
         "flake-parts": "flake-parts_2",
-        "nixpkgs": [
-          "nixpkgs"
-        ]
+        "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1744206621,
-        "narHash": "sha256-17kctQIIENhliHEQzzM06OlzrF4uyq6w7KOXSeNbZc4=",
-        "owner": "argumentcomputer",
+        "lastModified": 1754679239,
+        "narHash": "sha256-b/sd16BbXD2O/llObC4EaT4iBFvtLuqOv48XwOmfAtU=",
+        "owner": "lenianiva",
         "repo": "lean4-nix",
-        "rev": "f798c4f818301c3dd3f5ffa1b667f824b72921a4",
+        "rev": "3fda6e88605a229cc9e777e10bb7ac35fc2ed8db",
         "type": "github"
       },
       "original": {
-        "owner": "argumentcomputer",
+        "owner": "lenianiva",
         "repo": "lean4-nix",
         "type": "github"
       }
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1744098102,
-        "narHash": "sha256-tzCdyIJj9AjysC3OuKA+tMD/kDEDAF9mICPDU7ix0JA=",
+        "lastModified": 1743095683,
+        "narHash": "sha256-gWd4urRoLRe8GLVC/3rYRae1h+xfQzt09xOfb0PaHSk=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "c8cd81426f45942bb2906d5ed2fe21d2f19d95b7",
+        "rev": "5e5402ecbcb27af32284d4a62553c019a3a49ea6",
         "type": "github"
       },
       "original": {
@@ -90,16 +88,29 @@
     },
     "nixpkgs-lib_2": {
       "locked": {
-        "lastModified": 1743296961,
-        "narHash": "sha256-b1EdN3cULCqtorQ4QeWgLMrd5ZGOjLSLemfa00heasc=",
-        "owner": "nix-community",
-        "repo": "nixpkgs.lib",
-        "rev": "e4822aea2a6d1cdd36653c134cacfd64c97ff4fa",
+        "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": {
+      "locked": {
+        "lastModified": 1744098102,
+        "narHash": "sha256-tzCdyIJj9AjysC3OuKA+tMD/kDEDAF9mICPDU7ix0JA=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "c8cd81426f45942bb2906d5ed2fe21d2f19d95b7",
         "type": "github"
       },
       "original": {
-        "owner": "nix-community",
-        "repo": "nixpkgs.lib",
+        "owner": "nixos",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
         "type": "github"
       }
     },
@@ -107,7 +118,7 @@
       "inputs": {
         "flake-parts": "flake-parts",
         "lean4-nix": "lean4-nix",
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": "nixpkgs_2"
       }
     }
   },
diff --git a/flake.nix b/flake.nix
index d8edd2b..c689a6b 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,13 +1,19 @@
 {
   description = "LSpec Nix Flake";
 
+  nixConfig = {
+    extra-substituters = [
+      "https://cache.garnix.io"
+    ];
+    extra-trusted-public-keys = [
+      "cache.garnix.io:CTFPyKSLcx5RMJKfLo5EEPUObbA78b0YQ2DTCJXqr9g="
+    ];
+  };
+
   inputs = {
     nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
     flake-parts.url = "github:hercules-ci/flake-parts";
-    lean4-nix = {
-      url = "github:argumentcomputer/lean4-nix";
-      inputs.nixpkgs.follows = "nixpkgs";
-    };
+    lean4-nix.url = "github:lenianiva/lean4-nix";
   };
 
   outputs = inputs @ {
diff --git a/lean-toolchain b/lean-toolchain
index b2153cd..980709b 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.18.0
+leanprover/lean4:v4.21.0