diff --git a/CHANGELOG.md b/CHANGELOG.md
index dc605ae0eef83407c954bf9064a7f22df1f169c9..9e14f5f3e11afe059baa8afa2a96746ae7819d8b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -31,6 +31,9 @@ lemma.
   - `mono_nat_auth_frac_op`, `mono_nat_auth_frac_op_valid`,
     `mono_nat_auth_frac_valid`, `mono_nat_both_frac_valid`: use `dfrac` variant
     instead.
+* Add `mono_list` algebra for monotonically growing lists with an exclusive
+  authoritative element and persistent prefix witnesses. See
+  `iris/algebra/lib/mono_list.v` for details.
 
 **Changes in `bi`:**
 
diff --git a/_CoqProject b/_CoqProject
index 985d186bf819a83e945df5774c0bf0a73f6a299f..0847d523af66f6299728c480015bed726756345c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,6 +55,7 @@ iris/algebra/lib/ufrac_auth.v
 iris/algebra/lib/dfrac_agree.v
 iris/algebra/lib/gmap_view.v
 iris/algebra/lib/mono_nat.v
+iris/algebra/lib/mono_list.v
 iris/algebra/lib/gset_bij.v
 iris/si_logic/siprop.v
 iris/si_logic/bi.v
@@ -174,7 +175,6 @@ iris_heap_lang/lib/arith.v
 iris_heap_lang/lib/array.v
 
 iris_staging/algebra/list.v
-iris_staging/algebra/mono_list.v
 iris_staging/base_logic/algebra.v
 iris_staging/base_logic/mono_list.v
 iris_staging/heap_lang/interpreter.v
diff --git a/iris_staging/algebra/mono_list.v b/iris/algebra/lib/mono_list.v
similarity index 88%
rename from iris_staging/algebra/mono_list.v
rename to iris/algebra/lib/mono_list.v
index ee2468dd707c1e34e056a047d8e832576ac2f7bf..60679ecfe04035c69a1f09b69b082363db5479b8 100644
--- a/iris_staging/algebra/mono_list.v
+++ b/iris/algebra/lib/mono_list.v
@@ -1,13 +1,9 @@
-(* This file is still experimental. See its tracking issue
-https://gitlab.mpi-sws.org/iris/iris/-/issues/439 for details on remaining
-issues before stabilization. *)
-From iris.algebra Require Export auth dfrac max_prefix_list.
-From iris.algebra Require Import updates local_updates proofmode_classes.
-From iris.prelude Require Import options.
-
 (** Authoritative CMRA of append-only lists, where the fragment represents a
   snap-shot of the list, and the authoritative element can only grow by
   appending. *)
+From iris.algebra Require Export auth dfrac max_prefix_list.
+From iris.algebra Require Import updates local_updates proofmode_classes.
+From iris.prelude Require Import options.
 
 Definition mono_listR (A : ofe) : cmra  := authR (max_prefix_listUR A).
 Definition mono_listUR (A : ofe) : ucmra  := authUR (max_prefix_listUR A).
@@ -26,7 +22,7 @@ Notation "â—ML{ dq } l" :=
   (mono_list_auth dq l) (at level 20, format "â—ML{ dq }  l").
 Notation "â—ML{# q } l" :=
   (mono_list_auth (DfracOwn q) l) (at level 20, format "â—ML{# q }  l").
-Notation "â—â–¡ML l" := (mono_list_auth DfracDiscarded l) (at level 20).
+Notation "â—MLâ–¡ l" := (mono_list_auth DfracDiscarded l) (at level 20).
 Notation "â—ML l" := (mono_list_auth (DfracOwn 1) l) (at level 20).
 Notation "â—¯ML l" := (mono_list_lb l) (at level 20).
 
@@ -62,9 +58,6 @@ Section mono_list_props.
     rewrite (comm _ (â—{dq2} _)) -!assoc (assoc _ (â—¯ _)).
     by rewrite -core_id_dup (comm _ (â—¯ _)).
   Qed.
-  Lemma mono_list_auth_frac_op q1 q2 l :
-    â—ML{#(q1 + q2)} l â‰¡ â—ML{#q1} l â‹… â—ML{#q2} l.
-  Proof. by rewrite -mono_list_auth_dfrac_op dfrac_op_own. Qed.
 
   Lemma mono_list_lb_op_l l1 l2 : l1 `prefix_of` l2 â†’ â—¯ML l1 â‹… â—¯ML l2 â‰¡ â—¯ML l2.
   Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_l. Qed.
@@ -105,9 +98,6 @@ Section mono_list_props.
     - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op auth_both_dfrac_validN.
       naive_solver apply to_max_prefix_list_validN.
   Qed.
-  Lemma mono_list_auth_frac_op_validN n q1 q2 l1 l2 :
-    âœ“{n} (â—ML{#q1} l1 â‹… â—ML{#q2} l2) â†” (q1 + q2 â‰¤ 1)%Qp âˆ§ l1 â‰¡{n}â‰¡ l2.
-  Proof. by apply mono_list_auth_dfrac_op_validN. Qed.
   Lemma mono_list_auth_op_validN n l1 l2 : âœ“{n} (â—ML l1 â‹… â—ML l2) â†” False.
   Proof. rewrite mono_list_auth_dfrac_op_validN. naive_solver. Qed.
 
@@ -117,18 +107,12 @@ Section mono_list_props.
     rewrite cmra_valid_validN equiv_dist.
     setoid_rewrite mono_list_auth_dfrac_op_validN. naive_solver eauto using O.
   Qed.
-  Lemma mono_list_auth_frac_op_valid q1 q2 l1 l2 :
-    âœ“ (â—ML{#q1} l1 â‹… â—ML{#q2} l2) â†” (q1 + q2 â‰¤ 1)%Qp âˆ§ l1 â‰¡ l2.
-  Proof. by apply mono_list_auth_dfrac_op_valid. Qed.
   Lemma mono_list_auth_op_valid l1 l2 : âœ“ (â—ML l1 â‹… â—ML l2) â†” False.
   Proof. rewrite mono_list_auth_dfrac_op_valid. naive_solver. Qed.
 
   Lemma mono_list_auth_dfrac_op_valid_L `{!LeibnizEquiv A} dq1 dq2 l1 l2 :
     âœ“ (â—ML{dq1} l1 â‹… â—ML{dq2} l2) â†” âœ“ (dq1 â‹… dq2) âˆ§ l1 = l2.
   Proof. unfold_leibniz. apply mono_list_auth_dfrac_op_valid. Qed.
-  Lemma mono_list_auth_frac_op_valid_L `{!LeibnizEquiv A} q1 q2 l1 l2 :
-    âœ“ (â—ML{#q1} l1 â‹… â—ML{#q2} l2) â†” (q1 + q2 â‰¤ 1)%Qp âˆ§ l1 = l2.
-  Proof. unfold_leibniz. apply mono_list_auth_frac_op_valid. Qed.
 
   Lemma mono_list_both_dfrac_validN n dq l1 l2 :
     âœ“{n} (â—ML{dq} l1 â‹… â—¯ML l2) â†” âœ“ dq âˆ§ âˆƒ l, l1 â‰¡{n}â‰¡ l2 ++ l.
@@ -192,7 +176,7 @@ Section mono_list_props.
   (** * Update *)
   Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 â†’ â—ML l1 ~~> â—ML l2.
   Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.
-  Lemma mono_list_update_auth_persist dq l : â—ML{dq} l ~~> â—â–¡ML l.
+  Lemma mono_list_auth_persist dq l : â—ML{dq} l ~~> â—MLâ–¡ l.
   Proof.
     rewrite /mono_list_auth. apply cmra_update_op; [|done].
     by apply auth_update_auth_persist.
diff --git a/iris_staging/base_logic/mono_list.v b/iris_staging/base_logic/mono_list.v
index 642a7a1a7ba080d9bc859df23812adb983f4ad1b..ec4ffa575b8522fe579b3cdd64ba4e406acec336 100644
--- a/iris_staging/base_logic/mono_list.v
+++ b/iris_staging/base_logic/mono_list.v
@@ -16,7 +16,7 @@ which allows one to grow the auth element by appending only. At any time the
 auth list can be "snapshotted" with [mono_list_lb_own_get] to produce a
 persistent lower-bound. *)
 From iris.proofmode Require Import tactics.
-From iris.staging.algebra Require Import mono_list.
+From iris.algebra.lib Require Import mono_list.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export own.
 From iris.prelude Require Import options.
@@ -73,7 +73,7 @@ Section mono_list_own.
 
   Global Instance mono_list_auth_own_fractional Î³ l :
     Fractional (Î» q, mono_list_auth_own Î³ q l).
-  Proof. unseal. intros p q. by rewrite -own_op mono_list_auth_frac_op. Qed.
+  Proof. unseal. intros p q. by rewrite -own_op -mono_list_auth_dfrac_op. Qed.
   Global Instance mono_list_auth_own_as_fractional Î³ q l :
     AsFractional (mono_list_auth_own Î³ q l) (Î» q, mono_list_auth_own Î³ q l) q.
   Proof. split; [auto|apply _]. Qed.
@@ -84,7 +84,7 @@ Section mono_list_own.
     âŒœ(q1 + q2 â‰¤ 1)%Qp âˆ§ l1 = l2âŒ.
   Proof.
     unseal. iIntros "H1 H2".
-    by iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_auth_frac_op_valid_L.
+    by iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_auth_dfrac_op_valid_L.
   Qed.
   Lemma mono_list_auth_own_exclusive Î³ l1 l2 :
     mono_list_auth_own Î³ 1 l1 -âˆ— mono_list_auth_own Î³ 1 l2 -âˆ— False.