diff --git a/.github/dependabot.yml b/.github/dependabot.yml
index 1a9ee05d..0329b326 100644
--- a/.github/dependabot.yml
+++ b/.github/dependabot.yml
@@ -6,4 +6,4 @@ updates:
       interval: "weekly"
       day: "monday"
     labels:
-      - "dependencies"
+      - "part: dependencies"
diff --git a/.gitignore b/.gitignore
index b74fc852..2fbabdcc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -65,3 +65,6 @@ Makefile.rocq.conf
 docs/
 # Dune
 _build/
+
+# Nix
+result
diff --git a/.nix/config.nix b/.nix/config.nix
index 5f5c7a19..4a61d5b5 100644
--- a/.nix/config.nix
+++ b/.nix/config.nix
@@ -12,7 +12,7 @@
       coq.override.version = "9.0";
       mathcomp.job = false;
       mathcomp.override.version = "2.3.0";
-      mathcomp-analysis.override.version = "1.8.0";
+      mathcomp-analysis.override.version = "1.12.0";
     }; rocqPackages = {
       rocq-core.override.version = "9.0";
     };
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
index a0f1f6eb..f80c2017 100644
--- a/.nix/coq-nix-toolbox.nix
+++ b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"3e11db1b014f5f6bedf9322eed22ef325c868f9b"
+"af97ff6bc64b9ca3c6101bf4c6ad6cdb50236d73"
diff --git a/.nix/coq-overlays/ssprove/default.nix b/.nix/coq-overlays/ssprove/default.nix
index db0144da..24515e2f 100644
--- a/.nix/coq-overlays/ssprove/default.nix
+++ b/.nix/coq-overlays/ssprove/default.nix
@@ -15,6 +15,7 @@
 mkCoqDerivation {
   pname = "ssprove";
   owner = "SSProve";
+  opam-name = "rocq-ssprove";
 
   inherit version;
   defaultVersion =
@@ -57,6 +58,8 @@ mkCoqDerivation {
   release."0.2.0".sha256 = "sha256-GDkWH0LUsW165vAUoYC5of9ndr0MbfBtmrPhsJVXi3o=";
   release."0.1.0".sha256 = "sha256-Yj+k+mBsudi3d6bRVlZLyM4UqQnzAX5tHvxtKoIuNTE=";
 
+  useDune = true;
+
   propagatedBuildInputs = [
     equations
     mathcomp-boot
diff --git a/.nix/nixpkgs.nix b/.nix/nixpkgs.nix
index ca0f4b66..d16de94a 100644
--- a/.nix/nixpkgs.nix
+++ b/.nix/nixpkgs.nix
@@ -1,4 +1,4 @@
 fetchTarball {
-    url = "https://github.com/NixOS/nixpkgs/archive/082f768988f85a3c4bef2afc7add7821c61a0787.tar.gz";
-    sha256 = "0d6641rsisygspzaw4xh95z6b3mhrr8nlkzndsz8ab2rshd7na7g";
+    url = "https://github.com/NixOS/nixpkgs/archive/2cce2415f39a7845cf97c823e7135f44f4eff809.tar.gz";
+    sha256 = "0i4k6mmf4v8h550f7nr0pjvzrmaan331bkyqg9h21df4axc1r0di";
   }
diff --git a/flake.lock b/flake.lock
index 7af6264b..57ab24d2 100644
--- a/flake.lock
+++ b/flake.lock
@@ -20,11 +20,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1773238310,
-        "narHash": "sha256-KM3PLzBoQa/TMVEikUIJep45f9H1CMqc7Nzo5iwaBvU=",
+        "lastModified": 1775235291,
+        "narHash": "sha256-dThV69ONC86DDiBjaAfPixGfbEbI4NQDydsTP4cv/8k=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "8060123d743fcced007b4dc88f4c704e76966d32",
+        "rev": "468894586ca853a5e960b52388a6347084fcce31",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index df222acc..c47cfd66 100644
--- a/flake.nix
+++ b/flake.nix
@@ -7,22 +7,24 @@
     let
       ssprovePkg = { lib, mkCoqDerivation, coq
                   , equations, extructures, deriving
-                  , mathcomp-analysis, mathcomp-ssreflect
+                  , mathcomp-analysis, mathcomp-boot
                   , mathcomp-experimental-reals
                   , mathcomp-word}:
         mkCoqDerivation {
           pname = "ssprove";
           owner = "SSProve";
-          version = "0.2.0";
+          opam-name = "rocq-ssprove";
+          version = "0.3.1";
           src = ./.;
+          useDune = true;
           propagatedBuildInputs = [
             equations
+            mathcomp-boot
             mathcomp-analysis
             mathcomp-experimental-reals
-            mathcomp-ssreflect
-            mathcomp-word
-            deriving
             extructures
+            deriving
+            mathcomp-word
           ];
           meta = {
             description = "A foundational framework for modular cryptographic proofs in Rocq ";
diff --git a/rocq-ssprove.opam b/rocq-ssprove.opam
index 61aa75f3..a42e15eb 100644
--- a/rocq-ssprove.opam
+++ b/rocq-ssprove.opam
@@ -10,6 +10,7 @@ dev-repo: "git+https://github.com/SSProve/ssprove.git"
 doc: "https://SSProve.github.io/ssprove/index.html"
 license: "MIT"
 depends: [
+  "dune" {>= "3.21"}
   "rocq-core" {>= "9.0" & < "9.2~"}
   "rocq-stdlib" {>= "9.0" & < "9.2~"}
   "rocq-equations" {(>= "1.3.1+9.0")}
@@ -21,10 +22,18 @@ depends: [
   "coq-deriving" {(>= "0.2.1" & < "dev")}
 ]
 build: [
-  [make "-j%{jobs}%"]
-]
-install: [
-  [make "install"]
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
 ]
 tags: [
   "keyword:cryptography"
diff --git a/theories/dune b/theories/dune
index 49343152..64505703 100644
--- a/theories/dune
+++ b/theories/dune
@@ -18,6 +18,17 @@
       Stdlib
       Equations
       mathcomp
+      mathcomp.algebra
+      mathcomp.word
+      mathcomp.classical
+      mathcomp.reals
+      mathcomp.experimental_reals
+      mathcomp.fingroup
+      mathcomp.finmap
+      mathcomp.solvable
+      mathcomp.bigenough
+      mathcomp.ssreflect
+      mathcomp.order
       HB
       elpi
       elpi_elpi