diff --git a/_CoqProject b/_CoqProject
index cbad095135a6d494daaeb4ad166a9e289fe900a8..0a078486a5f77b9a6c4f7c5dd000010fdacfe52f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -50,6 +50,7 @@ iris/algebra/ufrac.v
 iris/algebra/reservation_map.v
 iris/algebra/dyn_reservation_map.v
 iris/algebra/max_prefix_list.v
+iris/algebra/mra.v
 iris/algebra/lib/excl_auth.v
 iris/algebra/lib/frac_auth.v
 iris/algebra/lib/ufrac_auth.v
@@ -187,7 +188,6 @@ 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/iris_unstable/algebra/monotone.v b/iris/algebra/mra.v
similarity index 97%
rename from iris_unstable/algebra/monotone.v
rename to iris/algebra/mra.v
index 0439b9fe21667bcfe9675b0e3ed28f67a2b79138..8e67bcd4f72b5e4f3933045140d8cdd8ecd5cf25 100644
--- a/iris_unstable/algebra/monotone.v
+++ b/iris/algebra/mra.v
@@ -1,7 +1,3 @@
-(** This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/iris/-/issues/414 for details on remaining
-issues before stabilization. *)
-
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
 From iris.prelude Require Import options.
diff --git a/tests/monotone.ref b/tests/mra.ref
similarity index 100%
rename from tests/monotone.ref
rename to tests/mra.ref
diff --git a/tests/monotone.v b/tests/mra.v
similarity index 90%
rename from tests/monotone.v
rename to tests/mra.v
index 061f57872ed84a4f6105808c40ec28f76c77d1bb..fff6183618b6d6432305b8079d06b37a483320cc 100644
--- a/tests/monotone.v
+++ b/tests/mra.v
@@ -1,5 +1,5 @@
 From stdpp Require Import propset gmap strings.
-From iris.unstable.algebra Require Import monotone.
+From iris Require Import algebra.mra.
 
 Unset Mangle Names.