diff --git a/.envrc b/.envrc
index 1d953f4..3550a30 100644
--- a/.envrc
+++ b/.envrc
@@ -1 +1 @@
-use nix
+use flake
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..0ee7307
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,27 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1781577229,
+        "narHash": "sha256-lrp67w8AulE9Ks53n27I45ADSzbOCn4H+CNW1Ck8B+8=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "567a49d1913ce81ac6e9582e3553dd90a955875f",
+        "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 0000000..5d7c5ac
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,27 @@
+{
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+
+  outputs = { self, nixpkgs }:
+  let
+    inherit (nixpkgs) lib;
+
+    systems = [
+      "x86_64-linux"
+      "aarch64-linux"
+      "x86_64-darwin"
+      "aarch64-darwin"
+    ];
+
+    forAllSystems = f: lib.genAttrs systems (system: f system nixpkgs.legacyPackages.${system});
+  in {
+    devShells = forAllSystems (_: pkgs: {
+      default = pkgs.mkShell {
+        packages = with pkgs; [
+          rocqPackages.rocq-core
+          rocqPackages.stdlib
+          rocqPackages.vsrocq-language-server
+        ];
+      };
+    });
+  };
+}
diff --git a/shell.nix b/shell.nix
deleted file mode 100644
index d6fcfc1..0000000
--- a/shell.nix
+++ /dev/null
@@ -1,14 +0,0 @@
-{ pkgs ? import <nixpkgs-unstable> {} }:
-pkgs.mkShell {
-  packages = with pkgs; [
-    # coq_8_20
-    coq
-    coqPackages.stdlib
-    # coqPackages.vscoq-language-server
-  ];
-
-  shellHook = ''
-    export ROCQPATH="$COQPATH"
-    unset COQPATH
-  '';
-}