diff --git a/_CoqProject b/_CoqProject
index 26c948832c84aef416aa43fc4e017ec07f22c3da..80e5f22d8549d0d8c2cca5c92572011c3b53cea2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,6 +2,7 @@
 # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
 -Q stdpp stdpp
 -Q stdpp_unstable stdpp.unstable
+-Q stdpp_bitvector stdpp.bv
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
 
@@ -55,6 +56,6 @@ stdpp/telescopes.v
 stdpp/binders.v
 stdpp/ssreflect.v
 
-stdpp_unstable/bitblast.v
-stdpp_unstable/bitvector.v
-stdpp_unstable/bitvector_tactics.v
+stdpp_bitvector/bitblast.v
+stdpp_bitvector/bitvector.v
+stdpp_bitvector/bitvector_tactics.v
diff --git a/coq-stdpp-bitvector.opam b/coq-stdpp-bitvector.opam
new file mode 100644
index 0000000000000000000000000000000000000000..6d8d5eb57644e6dda20230437ac6cb390feec44c
--- /dev/null
+++ b/coq-stdpp-bitvector.opam
@@ -0,0 +1,23 @@
+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The std++ team"
+license: "BSD-3-Clause"
+homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
+bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
+version: "dev"
+
+synopsis: "std++ bitvector"
+description: """
+Needs description
+"""
+tags: [
+  "logpath:stdpp.bv"
+]
+
+depends: [
+  "coq-stdpp" {= version}
+]
+
+build: ["./make-package" "stdpp_bitvector" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_bitvector" "install"]
diff --git a/stdpp_unstable/bitblast.v b/stdpp_bitvector/bitblast.v
similarity index 100%
rename from stdpp_unstable/bitblast.v
rename to stdpp_bitvector/bitblast.v
diff --git a/stdpp_unstable/bitvector.v b/stdpp_bitvector/bitvector.v
similarity index 100%
rename from stdpp_unstable/bitvector.v
rename to stdpp_bitvector/bitvector.v
diff --git a/stdpp_unstable/bitvector_tactics.v b/stdpp_bitvector/bitvector_tactics.v
similarity index 99%
rename from stdpp_unstable/bitvector_tactics.v
rename to stdpp_bitvector/bitvector_tactics.v
index 02ab358678bbc1f188825990aec9cbde8de6d2fa..65c8bcd58f0ad42c24dda6f3202c41870286373e 100644
--- a/stdpp_unstable/bitvector_tactics.v
+++ b/stdpp_bitvector/bitvector_tactics.v
@@ -1,8 +1,8 @@
 (** This file is still experimental. See its tracking issue
 https://gitlab.mpi-sws.org/iris/stdpp/-/issues/146 for details on remaining
 issues before stabilization. This file is maintained by Michael Sammler. *)
-From stdpp.unstable Require Export bitvector.
-From stdpp.unstable Require Import bitblast.
+From stdpp.bv Require Export bitvector.
+From stdpp.bv Require Import bitblast.
 From stdpp Require Import options.
 
 (** * bitvector tactics *)
diff --git a/stdpp_unstable/.keep b/stdpp_unstable/.keep
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/bitblast.v b/tests/bitblast.v
index e68bbfc8b5a4c4149e18f735a57eb107e9f7fe41..15bc7e09a2cbc4076cd1cf96831788562e510d66 100644
--- a/tests/bitblast.v
+++ b/tests/bitblast.v
@@ -1,4 +1,4 @@
-From stdpp.unstable Require Import bitblast.
+From stdpp.bv Require Import bitblast.
 
 Local Open Scope Z_scope.
 
diff --git a/tests/bitvector.v b/tests/bitvector.v
index 13309159f6102a0ca1aacc71c22c2a16a5e03208..5ea0529cd9d3018ab18bd5653c7adb7caa944304 100644
--- a/tests/bitvector.v
+++ b/tests/bitvector.v
@@ -1,5 +1,5 @@
 From stdpp Require Import strings.
-From stdpp.unstable Require Import bitvector.
+From stdpp.bv Require Import bitvector.
 
 Check "notation_test".
 Check (BV 10 3 = BV 10 5).
diff --git a/tests/bitvector_tactics.v b/tests/bitvector_tactics.v
index 46fda5c1c7bb38e0d7f05d7d972961d489fb6634..a2ed007e74f2d97f0fedcafd0281d1517692b1c2 100644
--- a/tests/bitvector_tactics.v
+++ b/tests/bitvector_tactics.v
@@ -1,5 +1,5 @@
 From stdpp Require Import strings.
-From stdpp.unstable Require Import bitblast bitvector_tactics.
+From stdpp.bv Require Import bitblast bitvector_tactics.
 Unset Mangle Names.
 
 Local Open Scope Z_scope.