diff --git a/CHANGELOG.md b/CHANGELOG.md
index a5783e424cbb3aa9ea307fd3e765bca3d91f0fd6..7722b8e7ad195b3f115b4407f1c89fca4f980d92 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,8 @@ lemma.
   affects `envs_entails_eq`, which is commonly used in the definition of
   custom proof mode tactics. All other unsealing lemmas should be internal, so
   in principle you should not rely on them.
+- Rename `coq-iris-staging` package to `coq-iris-unstable`, and also change the
+  import path from `iris.staging` to `iris.unstable`.
 
 **Changes in `algebra`:**
 
@@ -141,6 +143,8 @@ sed -i -E -f- $(find theories -name "*.v") <<EOF
 # excl_auth
 s/\bexcl_auth_frag_validN_op_1_l\b/excl_auth_frag_op_validN/g
 s/\bexcl_auth_frag_valid_op_1_l\b/excl_auth_frag_op_valid/g
+# staging → unstable
+s/\biris\.staging\b/iris.unstable/g
 EOF
 ```
 
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 5a8ffd47d259b34adfab66255092bdc0e9b34550..1366331479a5542c51be7c14378a83ea60f2b6da 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -15,7 +15,7 @@ style: $(VFILES) coq-lint.sh
 	  ./coq-lint.sh "$$FILE" || exit 1; \
 	done
 # Make sure main Iris does not import other Iris packages.
-	$(HIDE)if egrep 'iris\.(heap_lang|deprecated|staging)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
+	$(HIDE)if egrep 'iris\.(heap_lang|deprecated|unstable)' --include "*.v" -R iris; then echo "ERROR: Iris may not import modules from other Iris packages (see above for violations)."; echo; exit 1; fi
 .PHONY: style
 
 # the test suite
diff --git a/_CoqProject b/_CoqProject
index 5603abd77a7f407997db75ca81ad1a1627b1a98e..b47c82cf54505c93b5b5c5e1565ff03b5b5e6adf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,7 +8,7 @@
 -Q iris/base_logic iris.base_logic
 -Q iris/program_logic iris.program_logic
 -Q iris_heap_lang iris.heap_lang
--Q iris_staging iris.staging
+-Q iris_unstable iris.unstable
 -Q iris_deprecated iris.deprecated
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
@@ -176,11 +176,11 @@ iris_heap_lang/lib/arith.v
 iris_heap_lang/lib/array.v
 iris_heap_lang/lib/logatom_lock.v
 
-iris_staging/algebra/list.v
-iris_staging/base_logic/algebra.v
-iris_staging/base_logic/mono_list.v
-iris_staging/heap_lang/interpreter.v
-iris_staging/algebra/monotone.v
+iris_unstable/algebra/list.v
+iris_unstable/base_logic/algebra.v
+iris_unstable/base_logic/mono_list.v
+iris_unstable/heap_lang/interpreter.v
+iris_unstable/algebra/monotone.v
 
 iris_deprecated/base_logic/auth.v
 iris_deprecated/base_logic/sts.v
diff --git a/coq-iris-staging.opam b/coq-iris-unstable.opam
similarity index 83%
rename from coq-iris-staging.opam
rename to coq-iris-unstable.opam
index 6be6d4d66f89a09edb3234512a316972f4dba4d4..4d77aa5666c4a737fb55595ff65435dcc6a09a21 100644
--- a/coq-iris-staging.opam
+++ b/coq-iris-unstable.opam
@@ -18,5 +18,5 @@ depends: [
   "coq-iris-heap-lang" {= version}
 ]
 
-build: ["./make-package" "iris_staging" "-j%{jobs}%"]
-install: ["./make-package" "iris_staging" "install"]
+build: ["./make-package" "iris_unstable" "-j%{jobs}%"]
+install: ["./make-package" "iris_unstable" "install"]
diff --git a/iris_staging/.keep b/iris_unstable/.keep
similarity index 100%
rename from iris_staging/.keep
rename to iris_unstable/.keep
diff --git a/iris_staging/algebra/list.v b/iris_unstable/algebra/list.v
similarity index 100%
rename from iris_staging/algebra/list.v
rename to iris_unstable/algebra/list.v
diff --git a/iris_staging/algebra/monotone.v b/iris_unstable/algebra/monotone.v
similarity index 100%
rename from iris_staging/algebra/monotone.v
rename to iris_unstable/algebra/monotone.v
diff --git a/iris_staging/base_logic/algebra.v b/iris_unstable/base_logic/algebra.v
similarity index 94%
rename from iris_staging/base_logic/algebra.v
rename to iris_unstable/base_logic/algebra.v
index ba0d2844e30c41ba504509b94b1245f4bf0ded38..511d95f55e7001dbf29ee793fb633fdbe85a0ecc 100644
--- a/iris_staging/base_logic/algebra.v
+++ b/iris_unstable/base_logic/algebra.v
@@ -1,7 +1,7 @@
 (* This is just an integration file for [iris_staging.algebra.list];
 both should be stabilized together. *)
 From iris.algebra Require Import cmra.
-From iris.staging.algebra Require Import list monotone.
+From iris.unstable.algebra Require Import list monotone.
 From iris.base_logic Require Import bi derived.
 From iris.prelude Require Import options.
 
diff --git a/iris_staging/base_logic/mono_list.v b/iris_unstable/base_logic/mono_list.v
similarity index 100%
rename from iris_staging/base_logic/mono_list.v
rename to iris_unstable/base_logic/mono_list.v
diff --git a/iris_staging/heap_lang/interpreter.v b/iris_unstable/heap_lang/interpreter.v
similarity index 100%
rename from iris_staging/heap_lang/interpreter.v
rename to iris_unstable/heap_lang/interpreter.v
diff --git a/tests/heap_lang_interpreter.v b/tests/heap_lang_interpreter.v
index de12d0ae2e31968fe3ff3750ad1f327e3c343498..bc91eac9d8b02f32889a1fb000d2aa185b9df981 100644
--- a/tests/heap_lang_interpreter.v
+++ b/tests/heap_lang_interpreter.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Import notation.
-From iris.staging.heap_lang Require Import interpreter.
+From iris.unstable.heap_lang Require Import interpreter.
 
 Example test_1 :
   exec 1000 ((λ: "x", "x" + #1) #2) = inl #3.