diff --git a/CHANGELOG.md b/CHANGELOG.md
index 04eb4aeee1d144734d2f0d9841fa9271f540e047..07970642ff5ae7a69aefd5ffd9dae7fa64c68f5d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -51,6 +51,11 @@ Coq 8.11 is no longer supported in this version of Iris.
   value type, instead of a language. This requires extra type annotations or
   explicit coercions in a few cases, in particular `WP v {{ Φ }}` must now be
   written `WP (of_val v) {{ Φ }}`.
+* Improve `make_laterable`:
+  - Adjust definition such that `Laterable P` iff `P ⊢ make_laterable `.
+    As a consequence, `make_laterable_elim` got weaker: elimination now requires
+    an except-0 modality (`make_laterable P -∗ ◇ P`).
+  - Add `iModIntro` support for `make_laterable`.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index d82e531ee7a6a30d2adc33de980cd9960138b07d..6e7ddd53b54e02acdfaab72a1391b03db6c31ada 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -74,7 +74,7 @@ Section definition.
   Proof.
     constructor.
     - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
-      iApply (make_laterable_wand with "[] AU").
+      iApply (make_laterable_intuitionistic_wand with "[] AU").
       iIntros "!> AA". iApply (atomic_acc_wand with "[HP12] AA").
       iSplit; last by eauto. iApply "HP12".
     - intros ??. solve_proper.
@@ -255,7 +255,7 @@ Section lemmas.
     iIntros (Heo) "HAU".
     iApply (greatest_fixpoint_coind _ (λ _, atomic_update_def Eo1 Ei α β Φ)); last done.
     iIntros "!> *". rewrite {1}/atomic_update_def /= greatest_fixpoint_unfold.
-    iApply make_laterable_wand. iIntros "!>".
+    iApply make_laterable_intuitionistic_wand. iIntros "!>".
     iApply atomic_acc_mask_weaken. done.
   Qed.
 
@@ -266,7 +266,7 @@ Section lemmas.
   Proof using Type*.
     rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros "HUpd".
     iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
-    iApply make_laterable_elim. done.
+    iDestruct (make_laterable_elim with "HUpd") as ">?". done.
   Qed.
 
   (* This lets you eliminate atomic updates with iMod. *)
@@ -300,7 +300,7 @@ Section lemmas.
     rewrite atomic_update_eq {1}/atomic_update_def /=.
     iIntros (??? HAU) "[#HP HQ]".
     iApply (greatest_fixpoint_coind _ (λ _, Q)); last done. iIntros "!>" ([]) "HQ".
-    iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> >HQ".
+    iApply (make_laterable_intro Q with "[] HQ"). iIntros "!> HQ".
     iApply HAU. by iFrame.
   Qed.
 
@@ -438,13 +438,44 @@ Section lemmas.
 
 End lemmas.
 
-(** ProofMode support for atomic updates *)
+(** ProofMode support for atomic updates. *)
 Section proof_mode.
   Context `{BiFUpd PROP} {TA TB : tele}.
   Implicit Types (α : TA → PROP) (β Φ : TA → TB → PROP) (P : PROP).
 
+  (** We'd like to use the [iModIntro] machinery to transform the context into
+  something all-laterable, but we cannot actually use [iModIntro] on
+  [make_laterable] for that since we need to first make the context laterable,
+  then apply coinduction, and then introduce the modality (the last two steps
+  happen inside [aupd_intro]). We instead we define a dummy modality [make_laterable_id] that also
+  uses [MIEnvTransform IntoLaterable] and use that to pre-process the goal. *)
+  Local Definition make_laterable_id_def (P : PROP) := P.
+  Local Definition make_laterable_id_aux : seal make_laterable_id_def.
+  Proof. by eexists. Qed.
+  Local Definition make_laterable_id := make_laterable_id_aux.(unseal).
+  Local Definition make_laterable_id_eq : make_laterable_id = make_laterable_id_def :=
+    make_laterable_id_aux.(seal_eq).
+
+  Local Lemma modality_make_laterable_id_mixin :
+    modality_mixin make_laterable_id MIEnvId (MIEnvTransform IntoLaterable).
+  Proof.
+    rewrite make_laterable_id_eq. split; simpl; eauto.
+    intros P Q ?. rewrite (into_laterable P). done.
+  Qed.
+
+  Local Definition modality_make_laterable_id :=
+    Modality _ modality_make_laterable_id_mixin.
+
+  Global Instance from_modal_make_laterable P :
+    FromModal True modality_make_laterable_id (make_laterable_id P) (make_laterable_id P) P.
+  Proof. by rewrite /FromModal. Qed.
+
+  Local Lemma make_laterable_id_elim P :
+    make_laterable_id P -∗ P.
+  Proof. rewrite make_laterable_id_eq. done. Qed.
+
   Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
-    Timeless (PROP:=PROP) emp →
+    Laterable (PROP:=PROP) emp →
     TCForall Laterable (env_to_list Γs) →
     P = env_to_prop Γs →
     envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ) →
@@ -458,10 +489,14 @@ End proof_mode.
 
 (** * Now the coq-level tactics *)
 
+(** This tactic makes the context laterable. *)
+Local Ltac iMakeLaterable :=
+  iApply make_laterable_id_elim; iModIntro.
+
 Tactic Notation "iAuIntro" :=
-  iStartProof; eapply tac_aupd_intro; [
-    iSolveTC || fail "iAuIntro: emp is not timeless"
-  | iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
+  iMakeLaterable; notypeclasses refine (tac_aupd_intro _ _ _ _ _ _ _ _ _ _ _ _ _); [
+    iSolveTC || fail "iAuIntro: emp not laterable"
+  | iSolveTC || fail "iAuIntro: context not laterable; this should not happen, please report a bug"
   | (* P = ...: make the P pretty *) pm_reflexivity
   | (* the new proof mode goal *) ].
 
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 92fa677087158ca24554e2a942fd88e64303fdba..797b54a15580e0cbfa3cf3272a1794988d32924f 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -9,6 +9,21 @@ Global Arguments Laterable {_} _%I : simpl never.
 Global Arguments laterable {_} _%I {_}.
 Global Hint Mode Laterable + ! : typeclass_instances.
 
+(** Proofmode class for turning [P] into a laterable [Q].
+    Will be the identity if [P] already is laterable, and add
+    [â–·] otherwise. *)
+Class IntoLaterable {PROP : bi} (P Q : PROP) : Prop := {
+  (** This is non-standard; usually we would just demand
+      [P ⊢ make_laterable Q]. However, we need these stronger properties for
+      the [make_laterable_id] hack in [atomic.v]. *)
+  into_laterable : P ⊢ Q;
+  into_laterable_result_laterable : Laterable Q;
+}.
+Global Arguments IntoLaterable {_} P%I Q%I.
+Global Arguments into_laterable {_} P%I Q%I {_}.
+Global Arguments into_laterable_result_laterable {_} P%I Q%I {_}.
+Global Hint Mode IntoLaterable + ! - : typeclass_instances.
+
 Section instances.
   Context {PROP : bi}.
   Implicit Types P : PROP.
@@ -43,6 +58,16 @@ Section instances.
     iIntros "!> >_". done.
   Qed.
 
+  (** This instance, together with the one below, can lead to massive
+      backtracking, but only when searching for [Laterable]. In the future, it
+      should be rewritten using [Hint Immediate] or [Hint Cut], where the latter
+      is preferred once we figure out how to use it. *)
+  Global Instance persistent_laterable `{!BiAffine PROP} P :
+    Persistent P → Laterable P.
+  Proof.
+    intros ?. apply intuitionistic_laterable; apply _.
+  Qed.
+
   Global Instance sep_laterable P Q :
     Laterable P → Laterable Q → Laterable (P ∗ Q).
   Proof.
@@ -64,14 +89,17 @@ Section instances.
   Qed.
 
   Global Instance big_sepL_laterable Ps :
-    Timeless (PROP:=PROP) emp →
+    Laterable (PROP:=PROP) emp →
     TCForall Laterable Ps →
     Laterable ([∗] Ps).
   Proof. induction 2; simpl; apply _. Qed.
 
-  (* A wrapper to obtain a weaker, laterable form of any assertion. *)
+  (** A wrapper to obtain a weaker, laterable form of any assertion.
+     Alternatively: the modality corresponding to [Laterable].
+     The â—‡ is required to make [make_laterable_intro'] hold.
+   TODO: Define [Laterable] in terms of this (see [laterable_alt] below). *)
   Definition make_laterable (Q : PROP) : PROP :=
-    ∃ P, ▷ P ∗ □ (▷ P -∗ Q).
+    ∃ P, ▷ P ∗ □ (▷ P -∗ ◇ Q).
 
   Global Instance make_laterable_ne : NonExpansive make_laterable.
   Proof. solve_proper. Qed.
@@ -86,13 +114,46 @@ Section instances.
     (Q1 ⊢ Q2) → (make_laterable Q1 ⊢ make_laterable Q2).
   Proof. by intros ->. Qed.
 
-  (** A stronger version of [make_laterable_mono] that lets us keep persistent
-  resources. *)
+  Lemma make_laterable_except_0 Q :
+    make_laterable (◇ Q) -∗ make_laterable Q.
+  Proof.
+    iIntros "(%P & HP & #HPQ)". iExists P. iFrame.
+    iIntros "!# HP". iMod ("HPQ" with "HP"). done.
+  Qed.
+
+  Lemma make_laterable_sep Q1 Q2 :
+    make_laterable Q1 ∗ make_laterable Q2 -∗ make_laterable (Q1 ∗ Q2).
+  Proof.
+    iIntros "[HQ1 HQ2]".
+    iDestruct "HQ1" as (P1) "[HP1 #HQ1]".
+    iDestruct "HQ2" as (P2) "[HP2 #HQ2]".
+    iExists (P1 ∗ P2)%I. iFrame. iIntros "!# [HP1 HP2]".
+    iDestruct ("HQ1" with "HP1") as ">$".
+    iDestruct ("HQ2" with "HP2") as ">$".
+    done.
+  Qed.
+
+  (** A stronger version of [make_laterable_mono] that lets us keep laterable
+  resources. We cannot keep arbitrary resources since that would let us "frame
+  in" non-laterable things. *)
   Lemma make_laterable_wand Q1 Q2 :
+    make_laterable (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
+  Proof.
+    iIntros "HQ HQ1".
+    iDestruct (make_laterable_sep with "[$HQ $HQ1 //]") as "HQ".
+    iApply make_laterable_mono; last done.
+    by rewrite bi.wand_elim_l.
+  Qed.
+
+  (** A variant of the above for keeping arbitrary intuitionistic resources.
+      Sadly, this is not implied by the above for non-affine BIs. *)
+  Lemma make_laterable_intuitionistic_wand Q1 Q2 :
     □ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
   Proof.
     iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
-    iExists P. iFrame. iIntros "!> HP". iApply "HQ". iApply "HQ1". done.
+    iExists P. iFrame. iIntros "!> HP".
+    iDestruct ("HQ1" with "HP") as "{HQ1} >HQ1".
+    iModIntro. iApply "HQ". done.
   Qed.
 
   Global Instance make_laterable_laterable Q :
@@ -103,7 +164,7 @@ Section instances.
   Qed.
 
   Lemma make_laterable_elim Q :
-    make_laterable Q -∗ Q.
+    make_laterable Q -∗ ◇ Q.
   Proof.
     iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
   Qed.
@@ -112,13 +173,69 @@ Section instances.
       that persistent assertions can be kept unchanged. *)
   Lemma make_laterable_intro P Q :
     Laterable P →
-    □ (◇ P -∗ Q) -∗ P -∗ make_laterable Q.
+    □ (P -∗ Q) -∗ P -∗ make_laterable Q.
   Proof.
     iIntros (?) "#HQ HP".
     iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'.
-    iFrame. iIntros "!> HP'". iApply "HQ". iApply "HPi". done.
+    iFrame. iIntros "!> HP'".
+    iDestruct ("HPi" with "HP'") as ">HP". iModIntro.
+    iApply "HQ". done.
+  Qed.
+  Lemma make_laterable_intro' Q :
+    Laterable Q →
+    Q -∗ make_laterable Q.
+  Proof.
+    intros ?. iApply make_laterable_intro. iIntros "!# $".
   Qed.
 
+  Lemma make_laterable_idemp Q :
+    make_laterable (make_laterable Q) ⊣⊢ make_laterable Q.
+  Proof.
+    apply (anti_symm (⊢)).
+    - trans (make_laterable (â—‡ Q)).
+      + apply make_laterable_mono, make_laterable_elim.
+      + apply make_laterable_except_0.
+    - apply make_laterable_intro', _.
+  Qed.
+
+  Lemma laterable_alt Q :
+    Laterable Q ↔ (Q -∗ make_laterable Q).
+  Proof.
+    split.
+    - intros ?. apply make_laterable_intro'. done.
+    - intros ?. done.
+  Qed.
+
+  (** * Proofmode integration
+
+      We integrate [make_laterable] with [iModIntro]. All non-laterable
+      hypotheses have a â–· added in front of them to ensure a laterable context.
+  *)
+  Global Instance into_laterable_laterable P :
+    Laterable P →
+    IntoLaterable P P.
+  Proof. intros ?. constructor; done. Qed.
+
+  Global Instance into_laterable_fallback P :
+    IntoLaterable P (â–· P) | 100.
+  Proof. constructor; last by apply _. apply bi.later_intro. Qed.
+
+  Lemma modality_make_laterable_mixin `{!Timeless (PROP:=PROP) emp} :
+    modality_mixin make_laterable MIEnvId (MIEnvTransform IntoLaterable).
+  Proof.
+    split; simpl; eauto using make_laterable_intro', make_laterable_mono,
+      make_laterable_sep, intuitionistic_laterable with typeclass_instances; [].
+    intros P Q ?. rewrite (into_laterable P).
+    apply make_laterable_intro'. eapply (into_laterable_result_laterable P), _.
+  Qed.
+
+  Definition modality_make_laterable `{!Timeless (PROP:=PROP) emp} :=
+    Modality _ modality_make_laterable_mixin.
+
+  Global Instance from_modal_make_laterable `{!Timeless (PROP:=PROP) emp} P :
+    FromModal True modality_make_laterable (make_laterable P) (make_laterable P) P.
+  Proof. by rewrite /FromModal. Qed.
+
 End instances.
 
 Typeclasses Opaque make_laterable.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index bfd12ae7bc357e39e45b771b3d4d6c83c48f6f3c..d9ab16e89b60ad8eaf85a22679e003574e15645e 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -2623,7 +2623,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
      not have this issue. *)
   notypeclasses refine (tac_löb _ IH _ _ _ _);
     [iSolveTC || fail "iLöb: no 'BiLöb' instance found"
-    |reflexivity || fail "iLöb: spatial context not empty, this should not happen"
+    |reflexivity || fail "iLöb: spatial context not empty; this should not happen, please report a bug"
     |pm_reduce;
      lazymatch goal with
      | |- False =>
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 8bf105a88b974cce1d8b3ddbf9551365d7851f48..8a8f1b5adf8d0d99c245294df51712e330cf1edf 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -14,10 +14,32 @@
   
 "non_laterable"
      : string
-The command has indeed failed with message:
-Tactic failure: iAuIntro: not all spatial assumptions are laterable.
-The command has indeed failed with message:
-Tactic failure: iAuIntro: not all spatial assumptions are laterable.
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  aheap : atomic_heap Σ
+  P : iProp Σ
+  l : loc
+  ============================
+  "HP" : â–· P
+  --------------------------------------∗
+  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> @ ⊤, ∅
+       << l ↦{q} v, COMM True >>
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  aheap : atomic_heap Σ
+  P : iProp Σ
+  l : loc
+  ============================
+  "HP" : â–· P
+  --------------------------------------∗
+  AACC << ∀ (v : val) (q : dfrac), l ↦{q} v ABORT ▷ P >> @ ⊤, ∅
+       << l ↦{q} v, COMM True >>
+  
 "printing"
      : string
 1 goal
diff --git a/tests/atomic.v b/tests/atomic.v
index a621a8ce7715c5dbc7184e93d71f04cf7a5e1ade..02f88fa3d0b6537389a5d5ca8092ad0d4e32992a 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -27,9 +27,9 @@ Section error.
   Lemma non_laterable (P : iProp Σ) (l : loc) :
     P -∗ WP !#l {{ _, True }}.
   Proof.
-    iIntros "HP". wp_apply load_spec. Fail iAuIntro.
+    iIntros "HP". wp_apply load_spec. iAuIntro. Show.
   Restart.
-    iIntros "HP". Fail awp_apply load_spec.
+    iIntros "HP". awp_apply load_spec. Show.
   Abort.
 End error.
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 745fd6013a47f59042da695487b48049636f9ec3..ac5e9cf57c10ad06210c29ba7a38745369ee3c2a 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -383,6 +383,18 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   default emp mP
   
+1 goal
+  
+  PROP : bi
+  H : BiAffine PROP
+  P, Q : PROP
+  H0 : Laterable Q
+  ============================
+  "HP" : â–· P
+  "HQ" : Q
+  --------------------------------------∗
+  ▷ P ∗ Q
+  
 "elim_mod_accessor"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 454da8ec78f183803c0c52ad445b845eb3884553..afcfd89f24e1c9f6aa25391448e8fe50fe7e6c51 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,3 +1,4 @@
+From iris.bi Require Import laterable.
 From iris.proofmode Require Import tactics intro_patterns.
 Set Default Proof Using "Type".
 
@@ -1079,6 +1080,13 @@ Proof.
   iIntros "[P _]". done.
 Qed.
 
+Lemma test_iModIntro_make_laterable `{BiAffine PROP} (P Q : PROP) :
+  Laterable Q →
+  P -∗ Q -∗ make_laterable (▷ P ∗ Q).
+Proof.
+  iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
+Qed.
+
 End tests.
 
 Section parsing_tests.