diff --git a/Iris/Iris/BI/BIBase.lean b/Iris/Iris/BI/BIBase.lean
index ae7c216dd..91a9753cd 100644
--- a/Iris/Iris/BI/BIBase.lean
+++ b/Iris/Iris/BI/BIBase.lean
@@ -54,6 +54,8 @@ syntax "⌜" term "⌝" : term
 syntax:35 term:36 " ∗ " term:35 : term
 /-- Separating implication. -/
 syntax:25 term:26 " -∗ " term:25 : term
+/-- Separating implication with an optional wand premise. -/
+syntax:25 term:26 " -∗? " term:25 : term
 /-- Persistency modality. `persistently` is a primitive of BI. -/
 syntax:max "<pers> " term:40 : term
 /-- Later modality. `later` is a primitive of BI. -/
@@ -163,6 +165,18 @@ delab_rule iff
 delab_rule wandIff
   | `($_ $P $Q) => do ``(iprop($(← unpackIprop P) ∗-∗ $(← unpackIprop Q)))
 
+@[simp, rocq_alias bi_wandM]
+def wandM [BIBase PROP] (mP : Option PROP) (Q : PROP) : PROP :=
+  match mP with
+  | none => Q
+  | some P => iprop(P -∗ Q)
+
+macro_rules
+  | `(iprop($mP -∗? $Q)) => ``(wandM $mP iprop($Q))
+
+delab_rule wandM
+  | `($_ $mP $Q) => do ``(iprop($mP -∗? $(← unpackIprop Q)))
+
 /-- Affine modality.
 ```
 def affinely (P) := emp ∧ P
diff --git a/Iris/Iris/BI/DerivedLaws.lean b/Iris/Iris/BI/DerivedLaws.lean
index 2e71ef58c..e4efb8eea 100644
--- a/Iris/Iris/BI/DerivedLaws.lean
+++ b/Iris/Iris/BI/DerivedLaws.lean
@@ -1041,6 +1041,12 @@ theorem emp_or [BI PROP] {P : PROP} [Affine P] : emp ∨ P ⊣⊢ emp := ⟨or_e
 theorem emp_wand [BI PROP] {P : PROP} : (emp -∗ P) ⊣⊢ P :=
   ⟨emp_sep.mpr.trans wand_elim_right, wand_intro_left emp_sep.mp⟩
 
+@[rocq_alias bi.wandM_sound]
+theorem wandM_sound [BI PROP] {mP : Option PROP} {Q : PROP} :
+    (mP -∗? Q) ⊣⊢ (mP.getD emp -∗ Q) := by
+  cases mP <;> simp [BIBase.wandM]
+  exact emp_wand.symm
+
 @[rocq_alias bi.or_emp]
 theorem or_emp [BI PROP] {P : PROP} [Affine P] : P ∨ emp ⊣⊢ emp := or_comm.trans emp_or
 
diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean
index 896ca484a..9149fc3ba 100644
--- a/Iris/Iris/ProgramLogic/WeakestPre.lean
+++ b/Iris/Iris/ProgramLogic/WeakestPre.lean
@@ -681,4 +681,11 @@ instance elimModalFupdWpAtomic_wrongMask :
     p false iprop(|={E₁,E₂}=> P) iprop(False) (WP e @ s ; E₁ {{ Φ }}) iprop(False) where
   elim_modal := nofun
 
+@[rocq_alias add_modal_fupd_wp]
+instance addModalFupdWp : AddModal iprop(|={E}=> P) P (WP e @ s ; E {{ Φ }}) where
+  add_modal := by
+    iintro ⟨H1, H2⟩
+    imod H1
+    iapply H2 $$ H1
+
 end ProofModeClasses
diff --git a/Iris/Iris/ProofMode/Classes.lean b/Iris/Iris/ProofMode/Classes.lean
index ac2ca161b..33ac1c060 100644
--- a/Iris/Iris/ProofMode/Classes.lean
+++ b/Iris/Iris/ProofMode/Classes.lean
@@ -185,6 +185,19 @@ class ElimModal {PROP} [BI PROP] (φ : outParam $ Prop) (p : Bool) (p' : outPara
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q
 export ElimModal (elim_modal)
 
+/--
+`AddModal` is used by `ispecialize` and `iassert` to add a modality to the
+goal corresponding to the premise/asserted proposition.
+-/
+@[ipm_class, rocq_alias AddModal]
+class AddModal {PROP} [BI PROP] (P : outParam $ PROP) (P' Q : PROP) where
+  add_modal : P ∗ (P' -∗ Q) ⊢ Q
+export AddModal (add_modal)
+
+@[rocq_alias add_modal_id]
+theorem addModal_id {PROP} [BI PROP] (P Q : PROP) : AddModal P P Q where
+  add_modal := wand_elim_right
+
 @[ipm_class, rocq_alias Frame]
 class Frame {PROP} [BI PROP] (p : Bool) (R P : PROP) (Q : outParam $ PROP) where
   frame : □?p R ∗ Q ⊢ P
diff --git a/Iris/Iris/ProofMode/Instances.lean b/Iris/Iris/ProofMode/Instances.lean
index 8ebc6aa25..0675dbba6 100644
--- a/Iris/Iris/ProofMode/Instances.lean
+++ b/Iris/Iris/ProofMode/Instances.lean
@@ -51,6 +51,12 @@ instance fromImp_imp [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2 :
 @[rocq_alias from_wand_wand]
 instance fromWand_wand [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) io P1 P2 := ⟨.rfl⟩
 
+-- FromWandM
+@[rocq_alias from_wand_wandM]
+instance fromWand_wandM [BI PROP] (mP1 : Option PROP) (P2 : PROP) :
+    FromWand iprop(mP1 -∗? P2) io (mP1.getD emp) P2 where
+  from_wand := wandM_sound.mpr
+
 -- IntoWand
 #rocq_ignore into_wand_wand' "IntoWand' is not used in Lean"
 #rocq_ignore into_wand_impl' "IntoWand' is not used in Lean"
@@ -61,6 +67,13 @@ instance intoWand_wand (p q : Bool) [BI PROP] (P Q P' : PROP) [h : FromAssumptio
     IntoWand p q iprop(P' -∗ Q) ioP P ioQ Q where
   into_wand := (intuitionisticallyIf_mono <| wand_mono_left h.1).trans intuitionisticallyIf_elim
 
+@[rocq_alias into_wand_wandM]
+instance intoWand_wandM (p q : Bool) [BI PROP] (mP' : Option PROP) (P Q : PROP)
+    [h : FromAssumption q ioP P (mP'.getD emp)] :
+    IntoWand p q iprop(mP' -∗? Q) ioP P ioQ Q where
+  into_wand := (intuitionisticallyIf_mono wandM_sound.mp).trans <|
+    (intuitionisticallyIf_mono <| wand_mono_left h.1).trans intuitionisticallyIf_elim
+
 -- TODO: compare this with into_wand_impl_false_false, into_wand_impl_false_true, ... in Rocq
 instance intoWand_imp_false [BI PROP] (P Q P' : PROP) [Absorbing P'] [Absorbing iprop(P' → Q)]
     [h : FromAssumption b ioP P P'] : IntoWand false b iprop(P' → Q) ioP P ioQ Q where
@@ -321,12 +334,12 @@ instance intoAnd_and_affine_r [BI PROP] (P P' Q : PROP) [Affine Q]
   into_and := (and_mono_right (affine_affinely _).2).trans <|
     affinely_and_right.1.trans <| affinely_and.1.trans <| and_mono h.1 (affine_affinely _).1
 
-@[rocq_alias into_and_sep]
+@[ipm_backtrack, rocq_alias into_and_sep]
 instance intoAnd_sep [BI PROP] [BIPositive PROP] (P Q : PROP) :
     IntoAnd true iprop(P ∗ Q) P Q where
   into_and := intuitionistically_sep.1.trans <| and_sep_intuitionistically.2.trans <| intuitionistically_and.2
 
-@[rocq_alias into_and_sep_affine]
+@[ipm_backtrack, rocq_alias into_and_sep_affine]
 instance intoAnd_sep_affine (p : Bool) [BI PROP] (P Q : PROP)
     [TCOr (Affine P) (Absorbing Q)] [TCOr (Affine Q) (Absorbing P)] :
     IntoAnd p iprop(P ∗ Q) P Q where
@@ -573,7 +586,7 @@ instance (priority := default + 30) intoAbsorbingly_true [BI PROP] :
     IntoAbsorbingly (PROP := PROP) iprop(True) emp where
   into_absorbingly := absorbingly_emp.2
 
-@[rocq_alias into_absorbingly_absorbing]
+@[ipm_backtrack, rocq_alias into_absorbingly_absorbing]
 instance (priority := default + 20) intoAbsorbingly_absorbing [BI PROP] (P : PROP) [Absorbing P] :
     IntoAbsorbingly P P where
   into_absorbingly := absorbing_absorbingly.2
@@ -856,6 +869,46 @@ instance elimModal_absorbingly_here [BI PROP] p (P Q : PROP) [Absorbing Q] :
   ElimModal True p false iprop(<absorb> P) P Q Q where
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans $ absorbingly_sep_left.1.trans $ absorbing_absorbingly.1.trans wand_elim_right
 
+theorem addModal_wand_mp [BI PROP] {P P' Q R : PROP} [h : AddModal P P' Q] :
+    P ∗ (P' -∗ R -∗ Q) ⊢ R -∗ Q := by
+  have h1 : (P' -∗ R -∗ Q) ∗ R ⊢ P' -∗ Q := by
+    apply wand_intro
+    calc
+      _ ⊢ (P' -∗ R -∗ Q) ∗ R ∗ P'   := sep_assoc.mp
+      _ ⊢ (P' -∗ R -∗ Q) ∗ P' ∗ R   := sep_mono_right sep_comm.mp
+      _ ⊢ ((P' -∗ R -∗ Q) ∗ P') ∗ R := sep_assoc.mpr
+      _ ⊢ (R -∗ Q) ∗ R              := sep_mono_left wand_elim_left
+      _ ⊢ Q                         := wand_elim_left
+  apply wand_intro
+  calc
+    _ ⊢ P ∗ (P' -∗ R -∗ Q) ∗ R := sep_assoc.mp
+    _ ⊢ P ∗ (P' -∗ Q)          := sep_mono_right h1
+    _ ⊢ Q                      := h.add_modal
+
+-- AddModal
+@[rocq_alias add_modal_wand]
+instance addModal_wand [BI PROP] (P P' Q R : PROP) [h : AddModal P P' Q] :
+    AddModal P P' iprop(R -∗ Q) where
+  add_modal := addModal_wand_mp
+
+@[rocq_alias add_modal_wandM]
+instance addModal_wandM [BI PROP] (P P' Q : PROP) (mR : Option PROP)
+    [h : AddModal P P' Q] : AddModal P P' iprop(mR -∗? Q) where
+  add_modal := by
+    cases mR with
+    | none => exact h.add_modal
+    | some R => exact addModal_wand_mp
+
+@[rocq_alias add_modal_forall]
+instance addModal_forall {A : Type} [BI PROP] (P P' : PROP) (Φ : A → PROP)
+    [h : ∀ x, AddModal P P' (Φ x)] : AddModal P P' iprop(∀ x, Φ x) where
+  add_modal := by
+    apply forall_intro
+    intro a
+    exact (sep_mono_right (wand_mono .rfl (forall_elim a))).trans (h a).add_modal
+
+#rocq_ignore add_modal_tforall "Rocq-specific telescope infrastructure not needed in the Lean metaprogram"
+
 -- CombineSepAs
 @[rocq_alias maybe_combine_sep_as_default]
 instance (priority := default - 20) combineSepAs_default [BI PROP] (P Q : PROP) :
diff --git a/Iris/Iris/ProofMode/InstancesLater.lean b/Iris/Iris/ProofMode/InstancesLater.lean
index e1089e7e4..52ccff4c4 100644
--- a/Iris/Iris/ProofMode/InstancesLater.lean
+++ b/Iris/Iris/ProofMode/InstancesLater.lean
@@ -318,6 +318,42 @@ instance (priority := default - 10) elimModal_timeless [BI PROP] p (P P' Q : PRO
   ElimModal True p p P P' Q Q where
   elim_modal _ := ((sep_mono ((intuitionisticallyIf_mono into_except0).trans except0_intuitionisticallyIf) except0_intro).trans $ except0_sep.2.trans (except0_mono wand_elim_right)).trans is_except0
 
+/-- AddModal -/
+@[rocq_alias add_modal_later_except_0]
+instance (priority := default + 10) addModal_later_except_0 [BI PROP] (P Q : PROP) [h : Timeless P] :
+    AddModal iprop(▷ P) P iprop(◇ Q) where
+  add_modal := calc
+    _ ⊢ ◇ P ∗ (P -∗ ◇ Q)   := sep_mono_left h.timeless
+    _ ⊢ ◇ (P ∗ (P -∗ ◇ Q)) := except0_frame_right
+    _ ⊢ ◇ (◇ Q)            := except0_mono wand_elim_right
+    _ ⊢ ◇ Q                 := except0_idem.mp
+
+@[rocq_alias add_modal_later]
+instance (priority := default + 10) addModal_later [BI PROP] (P Q : PROP) [h : Timeless P] :
+    AddModal iprop(▷ P) P iprop(▷ Q) where
+  add_modal := calc
+    _ ⊢ ◇ P ∗ (P -∗ ▷ Q)   := sep_mono_left h.timeless
+    _ ⊢ ◇ (P ∗ (P -∗ ▷ Q)) := except0_frame_right
+    _ ⊢ ◇ (▷ Q)            := except0_mono wand_elim_right
+    _ ⊢ ▷ Q                 := except0_later
+
+@[rocq_alias add_modal_except_0]
+instance addModal_except_0 [BI PROP] (P Q : PROP) :
+    AddModal iprop(◇ P) P iprop(◇ Q) where
+  add_modal :=
+    calc
+    _ ⊢ ◇ (P ∗ (P -∗ ◇ Q)) := except0_frame_right
+    _ ⊢ ◇ (◇ Q)            := except0_mono wand_elim_right
+    _ ⊢ ◇ Q                 := except0_idem.mp
+
+@[rocq_alias add_modal_except_0_later]
+instance addModal_except_0_later [BI PROP] (P Q : PROP) :
+    AddModal iprop(◇ P) P iprop(▷ Q) where
+  add_modal := calc
+    _ ⊢ ◇ (P ∗ (P -∗ ▷ Q)) := except0_frame_right
+    _ ⊢ ◇ (▷ Q)            := except0_mono wand_elim_right
+    _ ⊢ ▷ Q                 := except0_later
+
 /-- IntoLaterN -/
 @[rocq_alias maybe_into_laterN_default]
 instance (priority := low) intoLaterN_default [BI PROP] only_head n (P : PROP) :
diff --git a/Iris/Iris/ProofMode/InstancesUpdates.lean b/Iris/Iris/ProofMode/InstancesUpdates.lean
index 30edff808..618ae96ac 100644
--- a/Iris/Iris/ProofMode/InstancesUpdates.lean
+++ b/Iris/Iris/ProofMode/InstancesUpdates.lean
@@ -88,6 +88,11 @@ instance elimModal_bupd p (P Q : PROP) :
   elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans <|
     bupd_frame_right.trans <| (BIUpdate.mono wand_elim_right).trans BIUpdate.trans
 
+@[rocq_alias add_modal_bupd]
+instance addModal_bupd (P Q : PROP) :
+    AddModal iprop(|==> P) P iprop(|==> Q) where
+  add_modal := bupd_wand_right.trans bupd_trans
+
 end BIBasicUpdate
 
 section SBIBasicUpdate
@@ -200,6 +205,16 @@ instance (priority := low) elimModal_fupd_fupd_wrongMask p E0 E1 E2 E3 (P Q : PR
       p false iprop(|={E1,E2}=> P) iprop(False) iprop(|={E0,E3}=> Q) iprop(False) where
   elim_modal h := by cases h
 
+@[rocq_alias add_modal_fupd]
+instance addModal_fupd E1 E2 (P Q : PROP) :
+    AddModal iprop(|={E1}=> P) P iprop(|={E1,E2}=> Q) where
+  add_modal := by
+    calc
+      _ ⊢ (P ={E1, E2}=∗ Q) ∗ (|={E1}=> P)    := sep_comm.mp
+      _ ⊢ |={E1}=> ((P -∗ |={E1,E2}=> Q) ∗ P) := fupd_frame_left
+      _ ⊢ |={E1}=> (|={E1,E2}=> Q)            := BIFUpdate.mono wand_elim_left
+      _ ⊢ |={E1, E2}=> Q                      := BIFUpdate.trans
+
 end BIFancyUpdate
 
 section SBIFancyUpdate
diff --git a/Iris/Iris/ProofMode/Patterns.lean b/Iris/Iris/ProofMode/Patterns.lean
index a204abd27..f49a02676 100644
--- a/Iris/Iris/ProofMode/Patterns.lean
+++ b/Iris/Iris/ProofMode/Patterns.lean
@@ -2,6 +2,5 @@ module
 
 public import Iris.ProofMode.Patterns.CasesPattern
 public import Iris.ProofMode.Patterns.IntroPattern
-public import Iris.ProofMode.Patterns.ProofModeTerm
 public import Iris.ProofMode.Patterns.SelPattern
 public import Iris.ProofMode.Patterns.SpecPattern
diff --git a/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean b/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean
deleted file mode 100644
index 73eec6df9..000000000
--- a/Iris/Iris/ProofMode/Patterns/ProofModeTerm.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-/-
-Copyright (c) 2025 Oliver Soeser. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Oliver Soeser, Zongyuan Liu
--/
-module
-
-public import Iris.ProofMode.Patterns.SpecPattern
-meta import Iris.Std.RocqPorting
-
-@[expose] public section
-
-namespace Iris.ProofMode
-open Lean
-
-declare_syntax_cat pmTerm
-
-syntax term : pmTerm
-syntax term colGt " $$ " (colGt specPat)+ : pmTerm
-
-@[rocq_alias iTrm]
-structure PMTerm where
-  term : Term
-  spats : List SpecPat
-  deriving Repr, Inhabited
-
-partial def PMTerm.parse (term : Syntax) : MacroM PMTerm := do
-  match ← expandMacros term with
-  | `(pmTerm| $trm:term) => return ⟨trm, []⟩
-  | `(pmTerm| $trm:term $$ $[$spats:specPat]*) => return ⟨trm, ← parseSpats spats⟩
-  | _ => Macro.throwUnsupported
-where
-  parseSpats (spats : TSyntaxArray `specPat) : MacroM (List SpecPat) :=
-      return (← spats.toList.mapM fun pat => SpecPat.parse pat.raw)
-
-def PMTerm.is_nontrivial (pmt : PMTerm) : Bool := !pmt.spats.isEmpty
diff --git a/Iris/Iris/ProofMode/Patterns/SpecPattern.lean b/Iris/Iris/ProofMode/Patterns/SpecPattern.lean
index 35612ca96..2b5a65ad0 100644
--- a/Iris/Iris/ProofMode/Patterns/SpecPattern.lean
+++ b/Iris/Iris/ProofMode/Patterns/SpecPattern.lean
@@ -1,12 +1,12 @@
 /-
 Copyright (c) 2025 Oliver Soeser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Oliver Soeser, Zongyuan Liu, Yunsong Yang, Michael Sammler
+Authors: Oliver Soeser, Zongyuan Liu, Yunsong Yang, Michael Sammler, Alvin Tang
 -/
 module
 
 public import Lean.Syntax
-meta import Iris.Std.RocqPorting
+public meta import Iris.Std.RocqPorting
 
 @[expose] public section
 
@@ -20,25 +20,61 @@ syntax ident : frameIdent
 -- syntax "$" ident : frameIdent
 
 declare_syntax_cat specPat
+declare_syntax_cat pmTerm
 
 syntax ident : specPat
+/-- Use a proof or a tactic sequence to match a pure hypothesis in the premise. -/
 syntax "%" term:max : specPat
-syntax "[" frameIdent* optional("//") "]" optional(" as " ident) : specPat
-syntax "[" "-" frameIdent* optional("//") "]" optional(" as " ident) : specPat
-syntax "[>" frameIdent* optional("//") "]" optional(" as " ident) : specPat
-syntax "[>" "-" frameIdent* optional("//") "]" optional(" as " ident) : specPat
-syntax "[#" frameIdent* optional("//") "]" optional(" as " ident) : specPat
+/--
+  `[ H₁ … Hₙ ]` generates a subgoal for the premise with `H₁ … Hₙ` as the
+  hypotheses chosen for the context of the subgoal. `[- H₁ … Hₙ ]` is analogous
+  with all but `H₁ … Hₙ` as the chosen hypotheses. `[ H₁ … Hₙ ]` and
+  `[- H₁ … Hₙ // ]` attempt to solve the subgoal using `itrivial`.
+-/
+syntax "[" ("-")? (colGt ppSpace frameIdent)* (" //")? " ]" (" as " colGt ident)? : specPat
+/--
+  `[> H₁ … Hₙ ]` generates a subgoal for the premise with `H₁ … Hₙ` as the
+  hypotheses chosen for the context of the subgoal wrapped in a modality.
+  `[> H₁ … Hₙ ]` is analogous with all but `H₁ … Hₙ` as the chosen hypotheses.
+  `[ H₁ … Hₙ // ]` and `[> H₁ … Hₙ // ]` also attempt to solve the subgoal
+  using `itrivial`.
+-/
+syntax "[>" ("-")? (colGt ppSpace frameIdent)* (" //")? " ]" (" as " colGt ident)? : specPat
+/--
+  `[# $H₁ … $Hₙ ]` generates a subgoal for the persistent premise
+  with all hypotheses in the context available for the subgoal. The hypotheses
+  `$H₁ … $Hₙ` are framed.
+  `[# $H₁ … $Hₙ // ]` further attempts to solve the subgoal using `itrivial`.
+-/
+syntax "[#" (colGt ppSpace frameIdent)* (" //")? " ]" (" as " colGt ident)? : specPat
+/--
+  `[$]` solves the subgoal by framing, first with spatial hypotheses, and
+  then with intuitionistic hypotheses. Spatial hypotheses that are not framed
+  are carried over to the subsequent goal.
+-/
 syntax "[" "$" "]" : specPat
+/-- `[>$]` solves the subgoal by wrapping the premise with the modality and then by framing. -/
 syntax "[>" "$" "]" : specPat
+/-- `[#$]` solves the subgoal for the persistent premise by framing. -/
 syntax "[#" "$" "]" : specPat
+/--
+  `(H $$ spat₁ … spatₙ)` specialises the hypothesis `H` with the specialisation
+  patterns `spat₁ … spatₙ` before the resultant hypothesis is itself used for
+  matching a premise.
+-/
+syntax "(" pmTerm ")" : specPat
+/--
+  The proof mode term `H $$ spat₁ … spatₙ` refers to `H`, a hypothesis or a
+  Lean term whose conclusion is an entailment, with the specialisation patterns
+  `spat₁ … spatₙ` applied to its premises.
+-/
+syntax term (colGt " $$ " (colGt ppSpace specPat)+)? : pmTerm
 
 @[rocq_alias goal_kind]
 inductive SpecGoalKind
   | spatial
-  -- TODO: implement
   | modal
-  -- TODO: implement
-  | intuitionistic
+  | persistent
   deriving Repr, Inhabited, BEq
 
 @[rocq_alias spec_goal]
@@ -50,10 +86,9 @@ structure SpecGoal where
   hyps : List Ident
 deriving Repr, Inhabited
 
--- see https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/spec_patterns.v?ref_type=heads#L15
 @[rocq_alias spec_pat]
 inductive SpecPat
-  | ident (name : Ident)
+  | ident (name : Ident) (recursiveSpecPats : List <| Syntax × SpecPat)
   | pure (t : Term)
   | goal (goal : SpecGoal) (goalName : Name)
   | autoframe (goal : SpecGoalKind)
@@ -78,36 +113,59 @@ def SpecPat.isModal : SpecPat → Bool
 def FrameIdent.parse : TSyntax `frameIdent → (Ident ⊕ Ident)
   | `(frameIdent| $name:ident) => .inl name
   | e =>
-    -- Antiquotations start with $, so if we find one, it is a framing assumption
+    -- Antiquotations start with `$`, so if we find one, it is a framing assumption
     if e.raw.isAntiquot then
       .inr ⟨e.raw.getAntiquotTerm⟩
     else .inl default -- should not happen
 
+@[rocq_alias iTrm]
+structure PMTerm where
+  term : Term
+  spats : List (Syntax × SpecPat)
+  deriving Repr, Inhabited
+
+def PMTerm.is_nontrivial (pmt : PMTerm) : Bool := !pmt.spats.isEmpty
+
+mutual
+
 @[rocq_alias spec_pat.parse]
-def SpecPat.parse (pat : Syntax) : MacroM SpecPat := do
-  match go ⟨← expandMacros pat⟩ with
-  | none => Macro.throwUnsupported
-  | some pat => return pat
+partial def SpecPat.parse (term : Syntax) : MacroM (Syntax × SpecPat) := do
+  let stx ← expandMacros term
+  match stx with
+  -- Recursive parsing for nested specialisation patterns
+  | `(specPat| ( $pmt:pmTerm )) =>
+    let pmt ← PMTerm.parse pmt
+    return ⟨term, .ident ⟨pmt.term⟩ pmt.spats⟩
+  -- No nested specialisation pattern involved
+  | _ =>
+    match go ⟨stx⟩ with
+    | some pat => return ⟨term, pat⟩
+    | none => Macro.throwUnsupported
 where
   go : TSyntax `specPat → Option SpecPat
-  | `(specPat| $name:ident) => some <| .ident name
+  | `(specPat| $name:ident) => some <| .ident name []
   | `(specPat| % $term:term) => some <| .pure term
-  | `(specPat| [$[$names:frameIdent]* $[//%$trivTk]?] $[as $goal:ident]?) =>
-    let (hyps, frame) := names.toList.partitionMap FrameIdent.parse;
-    some <| .goal {kind := .spatial, negate := false, trivial := trivTk.isSome, frame, hyps } <| (TSyntax.getId <*> goal).getD .anonymous
-  | `(specPat| [- $[$names:frameIdent]* $[//%$trivTk]?] $[as $goal:ident]?) =>
-    let (hyps, frame) := names.toList.partitionMap FrameIdent.parse;
-    some <| .goal {kind := .spatial, negate := true, trivial := trivTk.isSome, frame, hyps } <| (TSyntax.getId <*> goal).getD .anonymous
-  | `(specPat| [> $[$names:frameIdent]* $[//%$trivTk]?] $[as $goal:ident]?) =>
+  | `(specPat| [$[-%$negTk]? $[$names:frameIdent]* $[//%$trivTk]?] $[as $goal:ident]?) =>
     let (hyps, frame) := names.toList.partitionMap FrameIdent.parse;
-    some <| .goal {kind := .modal, negate := false, trivial := trivTk.isSome, frame, hyps } <| (TSyntax.getId <*> goal).getD .anonymous
-  | `(specPat| [> - $[$names:frameIdent]* $[//%$trivTk]?] $[as $goal:ident]?) =>
+    some <| .goal {kind := .spatial, negate := negTk.isSome, trivial := trivTk.isSome, frame, hyps } <| (TSyntax.getId <*> goal).getD .anonymous
+  | `(specPat| [> $[-%$negTk]? $[$names:frameIdent]* $[//%$trivTk]?] $[as $goal:ident]?) =>
     let (hyps, frame) := names.toList.partitionMap FrameIdent.parse;
-    some <| .goal {kind := .modal, negate := true, trivial := trivTk.isSome, frame, hyps } <| (TSyntax.getId <*> goal).getD .anonymous
+    some <| .goal {kind := .modal, negate := negTk.isSome, trivial := trivTk.isSome, frame, hyps } <| (TSyntax.getId <*> goal).getD .anonymous
   | `(specPat| [# $[$names:frameIdent]* $[//%$trivTk]?] $[as $goal:ident]?) =>
     let (hyps, frame) := names.toList.partitionMap FrameIdent.parse;
-    some <| .goal {kind := .intuitionistic, negate := false, trivial := trivTk.isSome, frame, hyps } <| (TSyntax.getId <*> goal).getD .anonymous
+    some <| .goal {kind := .persistent, negate := false, trivial := trivTk.isSome, frame, hyps } <| (TSyntax.getId <*> goal).getD .anonymous
   | `(specPat| [$]) => some <| .autoframe .spatial
-  | `(specPat| [# $]) => some <| .autoframe .intuitionistic
+  | `(specPat| [# $]) => some <| .autoframe .persistent
   | `(specPat| [> $]) => some <| .autoframe .modal
   | _ => none
+
+partial def PMTerm.parse (term : Syntax) : MacroM PMTerm := do
+  match ← expandMacros term with
+  | `(pmTerm| $trm:term) => return ⟨trm, []⟩
+  | `(pmTerm| $trm:term $$ $[$spats:specPat]*) => return ⟨trm, ← parseSpats spats⟩
+  | _ => Macro.throwUnsupported
+where
+  parseSpats (spats : TSyntaxArray `specPat) : MacroM (List (Syntax × SpecPat)) :=
+      return (← spats.toList.mapM fun pat => SpecPat.parse pat.raw)
+
+end
diff --git a/Iris/Iris/ProofMode/Porting.lean b/Iris/Iris/ProofMode/Porting.lean
index dad0da8f9..37e87c1e7 100644
--- a/Iris/Iris/ProofMode/Porting.lean
+++ b/Iris/Iris/ProofMode/Porting.lean
@@ -80,17 +80,17 @@ import Iris.Std.RocqPorting
 #rocq_concept proofmode "Intro Patterns" "IClear (pattern: {selpat})" missing ""
 #rocq_concept proofmode "Intro Patterns" "IClearFrame (pattern: {$selpat})" missing ""
 
-#rocq_concept proofmode "Specialization Patterns" missing ""
+#rocq_concept proofmode "Specialization Patterns" ported ""
 #rocq_concept proofmode "Specialization Patterns" "SIdent (pattern: H)" ported "pattern: H"
-#rocq_concept proofmode "Specialization Patterns" "Nested (pattern: (H spat ...))" missing ""
+#rocq_concept proofmode "Specialization Patterns" "Nested (pattern: (H spat ...))" ported "pattern: (H $$ spat₁ ... spatₙ)"
 #rocq_concept proofmode "Specialization Patterns" "SPureGoal (pattern: [%])" ported "pattern: %"
 #rocq_concept proofmode "Specialization Patterns" "SGoal (Kind: Spatial) (pattern: [H1 ...])" ported "pattern: [H1 ...]"
-#rocq_concept proofmode "Specialization Patterns" "SGoal (Kind: Intuitionistic) (pattern: [#H1 ...])" missing "pattern: [#H1 ...]"
-#rocq_concept proofmode "Specialization Patterns" "SGoal (Kind: Modal) (pattern: [>H1 ...])" missing "pattern: [>H1 ...]"
+#rocq_concept proofmode "Specialization Patterns" "SGoal (Kind: Intuitionistic) (pattern: [#H1 ...])" ported "pattern: [#H1 ...]"
+#rocq_concept proofmode "Specialization Patterns" "SGoal (Kind: Modal) (pattern: [>H1 ...])" ported "pattern: [>H1 ...]"
 #rocq_concept proofmode "Specialization Patterns" "SGoal (Negate) (pattern: [-H1 ...])" ported "pattern: [-H1 ...]"
 #rocq_concept proofmode "Specialization Patterns" "SGoal (Frame) (pattern: [$H1])" ported "pattern: [$H1]"
 #rocq_concept proofmode "Specialization Patterns" "SGoal (Hyps) (pattern: [H1 ...])" ported "pattern: [H1 ...]"
 #rocq_concept proofmode "Specialization Patterns" "SGoal (Done) (pattern: [... //])" ported "pattern: [... //]"
 #rocq_concept proofmode "Specialization Patterns" "SAutoFrame (Kind: Spatial) (pattern: [$])" ported "pattern: [$]"
-#rocq_concept proofmode "Specialization Patterns" "SAutoFrame (Kind: Intuitionistic) (pattern: [#$])" missing "pattern: [#$]"
-#rocq_concept proofmode "Specialization Patterns" "SAutoFrame (Kind: Modal) (pattern: [>$])" missing "pattern: [>$]"
+#rocq_concept proofmode "Specialization Patterns" "SAutoFrame (Kind: Intuitionistic) (pattern: [#$])" ported "pattern: [#$]"
+#rocq_concept proofmode "Specialization Patterns" "SAutoFrame (Kind: Modal) (pattern: [>$])" ported "pattern: [>$]"
diff --git a/Iris/Iris/ProofMode/Tactics/Apply.lean b/Iris/Iris/ProofMode/Tactics/Apply.lean
index dfaa859c8..24d1d79ea 100644
--- a/Iris/Iris/ProofMode/Tactics/Apply.lean
+++ b/Iris/Iris/ProofMode/Tactics/Apply.lean
@@ -7,7 +7,7 @@ module
 
 import Iris.BI
 import Iris.ProofMode.Classes
-meta import Iris.ProofMode.Patterns.ProofModeTerm
+meta import Iris.ProofMode.Patterns.SpecPattern
 meta import Iris.ProofMode.Tactics.Assumption
 public meta import Iris.ProofMode.Tactics.HaveCore
 
@@ -19,16 +19,16 @@ open BI
 theorem apply [BI PROP] {p} {P Q Q1 R : PROP}
     (h1 : P ⊢ Q1)
     [h2 : IntoWand p false Q .out Q1 .in R] : P ∗ □?p Q ⊢ R :=
-      (Entails.trans (sep_mono_left h1) (wand_elim_swap h2.1))
+  (Entails.trans (sep_mono_left h1) (wand_elim_swap h2.into_wand))
 
 public meta section
 open Lean Elab Tactic Meta Qq Std
 
 --  Like `ProofMode.assumption`, but specialized for the `iapply` case
-theorem apply_assumption [BI PROP] {p : Bool} {P A Q : PROP} [inst : FromAssumption p .in A Q]
-  [TCOr (Affine P) (Absorbing Q)]
-  (h : e ⊢ P ∗ □?p A) : e ⊢ Q :=
-  h.trans <| (sep_mono_right inst.1).trans sep_elim_right
+theorem apply_assumption [BI PROP] {p : Bool} {P A Q : PROP}
+    [inst : FromAssumption p .in A Q] [TCOr (Affine P) (Absorbing Q)] :
+    P ∗ □?p A ⊢ Q :=
+  (sep_mono_right inst.from_assumption).trans sep_elim_right
 
 /--
 Apply a hypothesis `A` to the `goal` by eliminating the wands recursively
@@ -40,7 +40,9 @@ Apply a hypothesis `A` to the `goal` by eliminating the wands recursively
 ## Returns
 The proof of `hyps ∗ □?p A ⊢ goal`
 -/
-private partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps : Hyps bi e) (p : Q(Bool)) (A : Q($prop)) (goal : Q($prop)) : ProofModeM Q($e ∗ □?$p $A ⊢ $goal) := do
+private partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (p : Q(Bool)) (A : Q($prop)) (goal : Q($prop)) :
+    ProofModeM Q($e ∗ □?$p $A ⊢ $goal) := do
   let B ← mkFreshExprMVarQ q($prop)
   -- if `A := ?B -∗ goal`, add `B` as a new subgoal and conclude `goal`
   if let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $A .out $B .in $goal) then
@@ -48,11 +50,11 @@ private partial def iApplyCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e} (hyps :
      return q(apply $pf)
 
   -- otherwise, if `A` has the form `?P -∗ ?B`, create a subgoal for `P` and continue with ?B
-  let some ⟨_, hyps', pb, B, pf⟩ ← try? <| iSpecializeCore hyps p A
-    [.goal {kind := .spatial, negate := false, trivial := false, frame := [], hyps := []} .anonymous]
+  let some ⟨_, hyps', pb, B, pf, _⟩ ← try? <| iSpecializeCore hyps p A goal
+    [⟨← getRef, .goal {kind := .spatial, negate := false, trivial := false, frame := [], hyps := []} .anonymous⟩]
     | throwError m!"iapply: cannot apply {A} to {goal}"
   let pf' ← iApplyCore hyps' pb B goal
-  return q($(pf).trans $pf')
+  return q($pf $pf')
 
 /--
   `iapply pmt` matches the conclusion of `pmt : pmTerm` against the goal and
@@ -70,14 +72,14 @@ elab "iapply " colGt pmt:pmTerm : tactic => do
   let pmt ← liftMacroM <| PMTerm.parse pmt
   ProofModeM.runTactic λ mvar { hyps, goal, .. } => do
   -- elaborate the proof mode term `pmt` to the hypothesis `out`
-  let ⟨e, hyps', p, out, pf⟩ ← iHave hyps pmt true
+  let ⟨e, hyps', p, out, pf⟩ ← iHave hyps goal pmt true
   -- if `□?p out` directly matches goal, behave like `iexact`
   if let some _ ← ProofModeM.trySynthInstanceQ q(FromAssumption $p .in $out $goal) then
     -- ensure the context can be discarded
     let LOption.some _ ← trySynthInstanceQ q(TCOr (Affine $e) (Absorbing $goal))
       | throwError "iapply: the context {e} is not affine and goal not absorbing"
-    mvar.assign q(apply_assumption (Q := $goal) $pf)
+    mvar.assign q($pf apply_assumption)
     return
   -- otherwise, `out` should be a wand, handled by `iApplyCore`
   let pf' ← iApplyCore hyps' p out goal
-  mvar.assign q($(pf).trans $pf')
+  mvar.assign q($pf $pf')
diff --git a/Iris/Iris/ProofMode/Tactics/Cases.lean b/Iris/Iris/ProofMode/Tactics/Cases.lean
index 9f5ec3854..81029e18a 100644
--- a/Iris/Iris/ProofMode/Tactics/Cases.lean
+++ b/Iris/Iris/ProofMode/Tactics/Cases.lean
@@ -5,7 +5,7 @@ Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang
 -/
 module
 
-meta import Iris.ProofMode.Patterns.ProofModeTerm
+meta import Iris.ProofMode.Patterns.SpecPattern
 meta import Iris.ProofMode.Patterns.CasesPattern
 public meta import Iris.ProofMode.Tactics.Mod
 public meta import Iris.ProofMode.Tactics.Pure
@@ -215,7 +215,7 @@ partial def iCasesCore {P} (hyps : Hyps bi P) (goal : Q($prop)) (pat : iCasesPat
 
   | .frame => do
     let ⟨ivar, hyps'⟩ ← Hyps.addWithInfo bi (← `(binderIdent | _)) p A hyps
-    let res ← iFrame bi _ hyps' goal [⟨.ipm ivar, true⟩]
+    let res ← iFrame bi hyps' goal [⟨.ipm ivar, true⟩]
     res.finish @k
 
   | .conjunction [arg] | .disjunction [arg] => iCasesCore hyps goal arg p A @k
@@ -266,13 +266,13 @@ elab "icases" keep:("+keep ")? colGt pmt:pmTerm " with " colGt pat:icasesPat : t
 
   -- We keep the persistent hypothesis if it is required by the user (+keep is set by ihave)
   -- or if we perform specialization
-  let ⟨_, hyps, p, A, pf⟩ ← iHave hyps pmt (keep.isSome || pmt.is_nontrivial)
+  let ⟨_, hyps, p, A, pf⟩ ← iHave hyps goal pmt (keep.isSome || pmt.is_nontrivial)
     (try_dup_context := pat.should_try_dup_context)
 
   -- process pattern
   let pf2 ← iCasesCore bi hyps goal pat p A
 
-  mvar.assign q(($pf).trans $pf2)
+  mvar.assign q($pf $pf2)
 
 /--
   `imod pmt with pat` eliminates the modality at the top of `pmt : pmTerm` into
diff --git a/Iris/Iris/ProofMode/Tactics/Frame.lean b/Iris/Iris/ProofMode/Tactics/Frame.lean
index af5be77c3..ddd9e2b99 100644
--- a/Iris/Iris/ProofMode/Tactics/Frame.lean
+++ b/Iris/Iris/ProofMode/Tactics/Frame.lean
@@ -86,7 +86,7 @@ private def FrameResult.step {u prop bi origE origGoal} :
     else
       return st
 
-def iFrame {prop : Q(Type u)} (bi : Q(BI $prop)) (e : Q($prop))
+def iFrame {prop : Q(Type u)} (bi : Q(BI $prop)) {e : Q($prop)}
     (hyps : Hyps bi e) (goal : Q($prop)) (sels : List SelTarget) :
     ProofModeM (FrameResult bi e goal) := do
   let mut st : FrameResult bi e goal := { progress := false, e, hyps, goal, pf := q(frame_init) }
@@ -136,10 +136,10 @@ def FrameResult.finishClose {u prop bi origE origGoal} (res : @FrameResult u pro
 elab "iframe " pats:(colGt ppSpace selPat)+ : tactic => do
   let pats ← liftMacroM <| SelPat.parse pats
 
-  ProofModeM.runTactic λ mvar { bi, e, hyps, goal, .. } => do
+  ProofModeM.runTactic λ mvar { bi, hyps, goal, .. } => do
   let pats ← SelPat.resolve hyps pats
 
-  let res ← iFrame bi e hyps goal pats
+  let res ← iFrame bi hyps goal pats
   mvar.assign (← res.finish (addBIGoal · ·))
 
 /--
diff --git a/Iris/Iris/ProofMode/Tactics/Have.lean b/Iris/Iris/ProofMode/Tactics/Have.lean
index 3c97cd888..bd5fd8f0d 100644
--- a/Iris/Iris/ProofMode/Tactics/Have.lean
+++ b/Iris/Iris/ProofMode/Tactics/Have.lean
@@ -39,6 +39,6 @@ elab "ihave " colGt pat:icasesPat " : " P:term " $$ " spat:specPat : tactic => d
   ProofModeM.runTactic λ mvar { prop, bi, hyps, goal, .. } => do
   let P ← elabTermEnsuringTypeQ (← `(iprop($P))) prop
   --  establish `P` with `spat`
-  let ⟨_, hyps', p, A, pf⟩ ← iSpecializeCore hyps q(true) q(iprop($P -∗ $P)) [spat] (try_dup_context := pat.should_try_dup_context)
+  let ⟨_, hyps', p, A, pf, _⟩ ← iSpecializeCore hyps q(true) q(iprop($P -∗ $P)) goal [spat] (try_dup_context := pat.should_try_dup_context)
   let pf2 ← iCasesCore bi hyps' goal pat p A
-  mvar.assign q(ihave_assert (($pf).trans $pf2))
+  mvar.assign q(ihave_assert ($pf $pf2))
diff --git a/Iris/Iris/ProofMode/Tactics/HaveCore.lean b/Iris/Iris/ProofMode/Tactics/HaveCore.lean
index 83e5f6aed..395c77822 100644
--- a/Iris/Iris/ProofMode/Tactics/HaveCore.lean
+++ b/Iris/Iris/ProofMode/Tactics/HaveCore.lean
@@ -7,7 +7,7 @@ module
 
 import Iris.BI
 import Iris.ProofMode.Classes
-public meta import Iris.ProofMode.Patterns.ProofModeTerm
+public meta import Iris.ProofMode.Patterns.SpecPattern
 public meta import Iris.ProofMode.Tactics.Basic
 public meta import Iris.ProofMode.Tactics.Specialize
 
@@ -56,13 +56,13 @@ private def iHaveCore {e} (hyps : @Hyps u prop bi e)
     let ⟨_, hyps, _, out', p, _, pf⟩ := hyps.remove (!keep) ivar
     return ⟨_, hyps, p, out', q($pf.1)⟩
   else
-    -- lean hypothesis
+    -- Lean hypothesis
     let val ← instantiateMVars <| ← elabTerm tm none (mayPostpone := true)
     let ty ← instantiateMVars <| ← inferType val
 
     let ⟨newMVars, _, _⟩ ← forallMetaTelescope ty
     let val := mkAppN val newMVars
-    -- TOOD: should we call postprocessAppMVars?
+    -- TODO: should we call postprocessAppMVars?
     let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
     let otherMVarIds ← getMVarsNoDelayed val
     let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
@@ -88,11 +88,12 @@ private def iHaveCore {e} (hyps : @Hyps u prop bi e)
 
     return ⟨_, hyps, q(true), hyp, q(have_asEmpValid $val)⟩
 
-def iHave {e} (hyps : @Hyps u prop bi e)
-  (pmt : PMTerm) (keep : Bool) (try_dup_context : Bool := false) :
-  ProofModeM ((e' : _) × Hyps bi e' × (p : Q(Bool)) × (out : Q($prop)) × Q($e ⊢ $e' ∗ □?$p $out)) := do
+def iHave {e} (hyps : @Hyps u prop bi e) (goal : Q($prop))
+    (pmt : PMTerm) (keep : Bool) (try_dup_context : Bool := false) :
+    ProofModeM ((e' : _) × Hyps bi e' × (p : Q(Bool)) × (out : Q($prop)) ×
+      Q(($e' ∗ □?$p $out ⊢ $goal) → $e ⊢ $goal)) := do
   -- assert `term` as hypothesis `A`
   let ⟨_, hyps', p, A, pf⟩ ← iHaveCore hyps pmt.term keep
   -- specialize `A` with `spats`
-  let ⟨_, hyps'', pb, B, pf'⟩ ← iSpecializeCore hyps' p A pmt.spats (try_dup_context := try_dup_context)
-  return ⟨_, hyps'', pb, B, q($(pf).trans $pf')⟩
+  let ⟨_, hyps'', pb, B, pf', _⟩ ← iSpecializeCore hyps' p A goal pmt.spats (try_dup_context := try_dup_context)
+  return ⟨_, hyps'', pb, B, q(fun x => $(pf).trans ($pf' x))⟩
diff --git a/Iris/Iris/ProofMode/Tactics/Revert.lean b/Iris/Iris/ProofMode/Tactics/Revert.lean
index 7245dc91f..1feee2188 100644
--- a/Iris/Iris/ProofMode/Tactics/Revert.lean
+++ b/Iris/Iris/ProofMode/Tactics/Revert.lean
@@ -57,7 +57,8 @@ private def RevertState.revertLeanPropHyp
     ProofModeM (@RevertState u prop bi origE origGoal) := do
   let { e, hyps, goal, reverted, pf } := st
   let P ← mkFreshExprMVarQ prop
-  let _hA : Q(MakeAffinely iprop(⌜$φ⌝) $P) ← synthInstanceQ q(MakeAffinely iprop(⌜$φ⌝) $P)
+  let some _ ← ProofModeM.trySynthInstanceQ q(MakeAffinely iprop(⌜$φ⌝) $P)
+  | throwError m!"irevert: MakeAffinely type class synthesis failed with {φ}"
   let hp : Q($φ) := mkFVar f
   let goal' : Q($prop) := q(iprop($P -∗ $goal))
   let pf' : Q(($e ⊢ $goal') → ($origE ⊢ $origGoal)) := q(fun h => $pf (pure_revert h $hp))
diff --git a/Iris/Iris/ProofMode/Tactics/Rewrite.lean b/Iris/Iris/ProofMode/Tactics/Rewrite.lean
index 8e8e2d4f1..d5b61c6b1 100644
--- a/Iris/Iris/ProofMode/Tactics/Rewrite.lean
+++ b/Iris/Iris/ProofMode/Tactics/Rewrite.lean
@@ -9,7 +9,7 @@ public import Iris.BI.InternalEq
 public import Iris.ProofMode.Classes
 public import Iris.Std.TC
 public import Iris.ProofMode.ProofModeM
-public meta import Iris.ProofMode.Patterns.ProofModeTerm
+public meta import Iris.ProofMode.Patterns.SpecPattern
 public meta import Iris.ProofMode.Tactics.HaveCore
 meta import Lean.Parser.Tactic
 
@@ -112,11 +112,16 @@ end rule
 end IRewrite
 
 private def iRewriteCore {prop : Q(Type u)} {bi : Q(BI $prop)}
-    {e} (hyps : Hyps bi e) (rule : IRewrite.Rule)
+    {e} (hyps : Hyps bi e) (_goal : Q($prop)) (rule : IRewrite.Rule)
     (target : Q($prop))
     (occs : Occurrences := Occurrences.all) :
     ProofModeM ((target' : Q($prop)) × Q($e ⊢ <pers> ($target ∗-∗ $target'))) := do
-  let ⟨_, _, _, eq, pf⟩ ← iHave hyps rule.term true
+  let g : Q($prop) ← mkFreshExprMVarQ q($prop)
+  let ⟨e', _, p, eq, pf⟩ ← iHave hyps g rule.term true
+  unless ← isDefEq g q(iprop($e' ∗ □?$p $eq)) do
+    throwError "irewrite: could not pin the equality goal"
+  have : $g =Q iprop($e' ∗ □?$p $eq) := ⟨⟩
+  let pf' : Q($e ⊢ $e' ∗ □?$p $eq) := q($pf .rfl)
 
   let .some sbi ← trySynthInstanceQ q(Sbi $prop)
     | throwError "irewrite: could not synthesize Sbi instance"
@@ -155,16 +160,16 @@ private def iRewriteCore {prop : Q(Type u)} {bi : Q(BI $prop)}
   match rule.direction with
   | .forward =>
     have : $target =Q $Ψ $a := ⟨⟩
-    return ⟨_, q(rewrite_tac $Ψ $pf)⟩
+    return ⟨_, q(rewrite_tac $Ψ $pf')⟩
   | .backward => do
     have : $target =Q $Ψ $b := ⟨⟩
-    return ⟨_, q(rewrite_tac_symm $Ψ $pf)⟩
+    return ⟨_, q(rewrite_tac_symm $Ψ $pf')⟩
 
 def iRewriteGoal {prop : Q(Type u)} {bi : Q(BI $prop)}
     {e} (hyps : Hyps bi e) (rule : IRewrite.Rule) (goal : Q($prop))
     (occs : Occurrences := Occurrences.all) :
     ProofModeM Q($e ⊢ $goal) := do
-  let ⟨goal', pf⟩ ← iRewriteCore hyps rule goal (occs := occs)
+  let ⟨goal', pf⟩ ← iRewriteCore hyps goal rule goal (occs := occs)
   let pf' ← addBIGoal hyps q($goal')
   return q(rewrite_tac_goal $pf $pf')
 
@@ -174,7 +179,7 @@ def iRewriteHyp {prop : Q(Type u)} {bi : Q(BI $prop)}
     (occs : Occurrences := Occurrences.all) :
     ProofModeM ((e' : _) × Hyps bi e' × Q($e ⊢ $e')) := do
   let some r ← hyps.replace ivar λ _ _ ty => do
-    let ⟨ty', pf⟩ ← iRewriteCore hyps rule ty (occs := occs)
+    let ⟨ty', pf⟩ ← iRewriteCore hyps ty rule ty (occs := occs)
     return ⟨ty', q(rewrite_tac_hyp $pf)⟩
     | throwError "irewrite: cannot find hyp" -- should never happen
   return r
diff --git a/Iris/Iris/ProofMode/Tactics/Specialize.lean b/Iris/Iris/ProofMode/Tactics/Specialize.lean
index 88c7c68da..06e40a779 100644
--- a/Iris/Iris/ProofMode/Tactics/Specialize.lean
+++ b/Iris/Iris/ProofMode/Tactics/Specialize.lean
@@ -1,11 +1,11 @@
 /-
 Copyright (c) 2022 Lars König. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König, Mario Carneiro, Michael Sammler
+Authors: Lars König, Mario Carneiro, Michael Sammler, Alvin Tang
 -/
 module
 
-public meta import Iris.ProofMode.Patterns.ProofModeTerm
+public meta import Iris.ProofMode.Patterns.SpecPattern
 public meta import Iris.ProofMode.Patterns.CasesPattern
 public meta import Iris.ProofMode.Tactics.Basic
 public import Iris.ProofMode.Tactics.Trivial
@@ -16,134 +16,308 @@ namespace Iris.ProofMode
 public section
 open BI
 
-theorem specialize_wand [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP}
-    (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ □?p P1)
-    [h3 : IntoWand q p Q .in P1 .out P2] :
-    A1 ⊢ A3 ∗ □?(p && q) P2 := by
-  refine h1.trans <| (sep_mono_left h2.1).trans <| sep_assoc.1.trans (sep_mono_right ?_)
+theorem specialize_wand [BI PROP] {q p : Bool} {A Q P1 P2 : PROP}
+    (inst : IntoWand q p Q .in P1 .out P2) :
+    (A ∗ □?p P1) ∗ □?q Q ⊢ A ∗ □?(p && q) P2 := by
+  refine sep_assoc.mp.trans (sep_mono_right ?_)
   cases p with
-  | false => exact (sep_mono_right h3.1).trans <| wand_elim_right
-  | true => exact
-    (sep_mono intuitionisticallyIf_intutitionistically.2 intuitionisticallyIf_idem.2).trans <|
-    intuitionisticallyIf_sep_mpr.trans <| intuitionisticallyIf_mono <| (wand_elim_swap h3.1)
+  | false => exact (sep_mono_right inst.into_wand).trans wand_elim_right
+  | true => calc
+    _ ⊢ □?q □ P1 ∗ □?q Q     := sep_mono_left intuitionisticallyIf_intutitionistically.mpr
+    _ ⊢ □?q □ P1 ∗ □?q □?q Q := sep_mono_right intuitionisticallyIf_idem.mpr
+    _ ⊢ □?q (□ P1 ∗ □?q Q)   := intuitionisticallyIf_sep_mpr
+    _ ⊢ □?q P2               := intuitionisticallyIf_mono <| wand_elim_swap inst.into_wand
 
 -- TODO: if q is true and A1 is persistent, this proof can guarantee □ P2 instead of P2
 -- see https://gitlab.mpi-sws.org/iris/iris/-/blob/846ed45bed6951035c6204fef365d9a344022ae6/iris/proofmode/coq_tactics.v#L336
-theorem specialize_wand_subgoal [BI PROP] {q : Bool} {A1 A2 A3 A4 Q P1 : PROP} P2
-    (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ A4) (h3 : A4 ⊢ P1)
-    [inst : IntoWand q false Q .out P1 .out P2] : A1 ⊢ A3 ∗ P2 := by
-  refine h1.trans <| (sep_mono_left h2.1).trans <| sep_assoc.1.trans (sep_mono_right ((sep_mono_left h3).trans ?_))
-  exact (sep_mono_right inst.1).trans wand_elim_right
-
-theorem specialize_wand_autoframe [BI PROP] {q : Bool} {A1 A2 A3 Q P1 : PROP} P2
-     (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊢ A3 ∗ P1)
-     [inst : IntoWand q false Q .out P1 .out P2] : A1 ⊢ A3 ∗ P2 :=
-  h1.trans <| (sep_mono_left h2).trans <| sep_assoc.1.trans
-    (sep_mono_right ((sep_mono_right inst.into_wand).trans wand_elim_right))
-
-theorem specialize_forall [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort _} {Φ : α → PROP}
-    [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p (Φ a) := by
-  refine h.trans <| sep_mono_right <| intuitionisticallyIf_mono <| inst.1.trans (forall_elim a)
-
-theorem specialize_dup_context [BI PROP] {P : PROP} {pa A P' pb B}
-  (h : P ∗ □?pa A ⊢ P' ∗ □?pb B)
-  (h2 : pa = true ∨ Affine A)
-  [IntoPersistently pb B B']
-  : P ∗ □?pa A ⊢ P ∗ □ B' := by
-    apply Entails.trans _ persistently_and_intuitionistically_sep_right.1
-    apply and_intro
-    · cases h2 <;> subst_eqs <;> apply sep_elim_left
-    · apply h.trans $ (sep_mono_right (persistentlyIf_of_intuitionisticallyIf.trans into_persistently)).trans sep_elim_right
+theorem specialize_wand_subgoal [BI PROP] {q : Bool} {A2 A3 A4 Q P1 : PROP} P2
+    (inst : IntoWand q false Q .out P1 .out P2)
+    (h2 : A2 ⊣⊢ A3 ∗ A4) (h3 : A4 ⊢ P1) : A2 ∗ □?q Q ⊢ A3 ∗ P2 := by
+  refine (sep_mono_left h2.mp).trans <| sep_assoc.mp.trans
+    (sep_mono_right ((sep_mono_left h3).trans ?_))
+  exact (sep_mono_right inst.into_wand).trans wand_elim_right
+
+theorem specialize_wand_nest [BI PROP] {e e' e'' out out1' Q out2 : PROP}
+    {p p1 q : Bool} (inst : IntoWand p q out .in Q .out out2)
+    (h1 : e ⊣⊢ e' ∗ □?p1 out1') (h2 : e' ∗ □?p1 out1' ⊢ e'' ∗ □?q Q) :
+    e ∗ □?p out ⊢ e'' ∗ □?(q && p) out2 := calc
+  _ ⊢ (e'' ∗ □?q Q) ∗ □?p out := sep_mono_left <| h1.mp.trans h2
+  _ ⊢ e'' ∗ □?(q && p) out2   := specialize_wand inst
+
+theorem specialize_wand_nest_modal [BI PROP]
+    {orig e e' e'' goal out out1' Q out2 : PROP} {p p1 q : Bool}
+    (inst : IntoWand p q out .in Q .out out2)
+    (h1 : (e ∗ □?p out ⊢ goal) → orig ⊢ goal) (h2 : e ⊣⊢ e' ∗ □?p1 out1')
+    (h3 : (e'' ∗ □?q Q ⊢ □?p out -∗ goal) → e' ∗ □?p1 out1' ⊢ □?p out -∗ goal)
+    (h4 : e'' ∗ □?(q && p) out2 ⊢ goal) : orig ⊢ goal := by
+  apply h1
+  apply wand_elim_left_trans
+  calc
+    _ ⊢ e' ∗ □?p1 out1' := h2.mp
+    _ ⊢ □?p out -∗ goal := h3 <| wand_intro <| (specialize_wand inst).trans h4
+
+theorem specialize_wand_autoframe_spatial [BI PROP] {q : Bool} {A2 A3 Q P1 : PROP} P2
+    (inst : IntoWand q false Q .out P1 .out P2)
+    (h2 : A2 ⊢ A3 ∗ P1) : A2 ∗ □?q Q ⊢ A3 ∗ P2 := calc
+  _ ⊢ (A3 ∗ P1) ∗ □?q Q := sep_mono_left h2
+  _ ⊢ A3 ∗ P1 ∗ □?q Q   := sep_assoc.mp
+  _ ⊢ A3 ∗ P2           := sep_mono_right <| (sep_mono_right inst.into_wand).trans wand_elim_right
+
+theorem specialize_wand_persistent [BI PROP] {q : Bool} {A2 Q P1' : PROP} P1 P2
+    (instWand : IntoWand q true Q .out P1 .out P2) (instPers : Persistent P1)
+    (instAbsorb : IntoAbsorbingly P1' P1) (h1 : A2 ⊢ P1') : A2 ∗ □?q Q ⊢ A2 ∗ □?q P2 := by
+  have h2 : □ P1 ∗ □?q Q ⊢ □?q P2 := by cases q with
+  | false => exact (sep_mono_right instWand.into_wand).trans wand_elim_right
+  | true => calc
+    _ ⊢ □ □ P1 ∗ □ □ Q          := sep_mono intuitionistically_idem.mpr intuitionistically_idem.mpr
+    _ ⊢ □ (□ P1 ∗ □ Q)          := intuitionistically_sep_mpr
+    _ ⊢ □ (□ P1 ∗ (□ P1 -∗ P2)) := intuitionistically_mono <| sep_mono_right instWand.into_wand
+    _ ⊢ □?true P2               := intuitionistically_mono wand_elim_right
+  have h3 : A2 ⊢ A2 ∗ □ P1 := calc
+    _ ⊢ (A2 ∧ A2)                 := and_intro .rfl .rfl
+    _ ⊢ (A2 ∧ P1')                := and_mono_right h1
+    _ ⊢ (A2 ∧ <absorb> P1)        := and_mono_right into_absorbingly
+    _ ⊢ (A2 ∧ <absorb> <pers> P1) := and_mono_right <| absorbingly_mono Persistent.persistent
+    _ ⊢ (A2 ∧ <pers> P1)          := and_mono_right absorbingly_persistently.mp
+    _ ⊢ (A2 ∗ □ P1)               := persistently_and_intuitionistically_sep_right.mp
+  calc
+    _ ⊢ (A2 ∗ □ P1) ∗ □?q Q := sep_mono_left h3
+    _ ⊢ A2 ∗ □ P1 ∗ □?q Q   := sep_assoc.mp
+    _ ⊢ A2 ∗ □?q P2         := sep_mono_right h2
+
+theorem specialize_forall [BI PROP] {p : Bool} {A2 P : PROP} {α : Sort _} {Φ : α → PROP}
+    (inst : IntoForall P Φ) (a : α) : A2 ∗ □?p P ⊢ A2 ∗ □?p (Φ a) :=
+  sep_mono_right <| intuitionisticallyIf_mono <| inst.into_forall.trans (forall_elim a)
+
+theorem specialize_dup_context [BI PROP] {P : PROP} {pa A P' pb B B'}
+    (inst : IntoPersistently pb B B') (h1 : P ∗ □?pa A ⊢ P' ∗ □?pb B)
+    (h2 : pa = true ∨ Affine A) : P ∗ □?pa A ⊢ P ∗ □ B' := by
+  apply Entails.trans _ persistently_and_intuitionistically_sep_right.mp
+  apply and_intro
+  · cases h2 <;> subst_eqs <;> apply sep_elim_left
+  · calc
+      _ ⊢ P' ∗ □?pb B    := h1
+      _ ⊢ P' ∗ <pers> B' := sep_mono_right <| persistentlyIf_of_intuitionisticallyIf.trans into_persistently
+      _ ⊢ <pers> B'      := sep_elim_right
+
+theorem specialize_modal [BI PROP] {e e' goal R P1 P1' P2 : PROP} {p : Bool}
+    (h1 : e ⊢ e' ∗ P1') (h2 : e' ∗ P2 ⊢ goal)
+    (instWand : IntoWand p false R .out P1 .out P2)
+    (instModal : AddModal P1' P1 goal) :
+    e ∗ □?p R ⊢ goal := calc
+  _ ⊢ (e' ∗ P1') ∗ □?p R                := sep_mono_left h1
+  _ ⊢ P1' ∗ (e' ∗ □?p R)                := sep_assoc.mp.trans sep_left_comm.mp
+  _ ⊢ P1' ∗ (e' ∗ (P1 -∗ P2))           := sep_mono_right (sep_mono_right instWand.into_wand)
+  _ ⊢ P1' ∗ ((P2 -∗ goal) ∗ (P1 -∗ P2)) := sep_mono_right (sep_mono_left (wand_intro h2))
+  _ ⊢ P1' ∗ (P1 -∗ goal)                := sep_mono_right (sep_comm.mp.trans wand_trans)
+  _ ⊢ goal                              := instModal.add_modal
 
 public meta section
 open Lean Elab Tactic Meta Qq Std
 
-structure SpecializeState {prop : Q(Type u)} (bi : Q(BI $prop)) (orig : Q($prop)) where
-  (e : Q($prop)) (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop))
-  pf : Q($orig ⊢ $e ∗ □?$p $out)
+structure SpecializeState {prop : Q(Type u)} {bi : Q(BI $prop)} (orig goal : Q($prop)) where
+  {e : Q($prop)} (hyps : Hyps bi e) (p : Q(Bool)) (out : Q($prop))
+  -- A weaker proposition than `pf`, applicable even when the `.modal` kind is involved
+  (pfCont : Q(($e ∗ □?$p $out ⊢ $goal) → $orig ⊢ $goal))
+  -- Holds when the `.modal` kind is not involved, cannot duplicate context if `pf = none`
+  pf : Option Q($orig ⊢ $e ∗ □?$p $out)
+
+/--
+  Updates a `SpecializeState` instance by one iteration.
+  Used in all cases in `processWand` except those involving the `.modal` kind.
+-/
+private def SpecializeState.update {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
+    {orig goal : Q($prop)} (st : @SpecializeState u prop bi orig goal)
+    {e' : Q($prop)} (hyps' : Hyps bi e') (p' : Q(Bool)) (out' : Q($prop))
+    (pfStep : Q($(st.e) ∗ □?$(st.p) $(st.out) ⊢ $e' ∗ □?$p' $out')) :
+    @SpecializeState u prop bi orig goal :=
+  { hyps := hyps', p := p', out := out',
+    pfCont := q(fun pf => $(st.pfCont) ($(pfStep).trans pf)),
+    pf := st.pf.map (fun pf => q($(pf).trans $pfStep)) }
+
+/--
+  Returns `IVarId` values of hypotheses to be included in a subgoal and those to be framed.
+  Used by all `.goal` cases in `processWand`.
+-/
+private def findFrameIVars {u}  {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (subgoalIdents frameIdents : List Ident) :
+    ProofModeM <| IVarIdSet × List IVarId := do
+  -- Hypotheses to be included in the subgoal
+  let subgoalIVars ← subgoalIdents.foldlM (return ·.insert <| ← hyps.findWithInfo ·) {}
+  -- Hypotheses to be framed
+  let mut frameIVars : List IVarId := []
+  for i in frameIdents do
+    let ivar ← hyps.findWithInfo i
+    if frameIVars.contains ivar then
+      throwError "ispecialize: {i} used twice for framing"
+    if subgoalIVars.contains ivar then
+      throwError "ispecialize: {i} cannot be used for both the subgoal and framing"
+    frameIVars := ivar :: frameIVars
+  return ⟨subgoalIVars, frameIVars.reverse⟩
+
+/--
+  Split hypotheses into those to be included in a subgoal and those to be framed.
+  Used by the `.goal` cases with the `.spatial` or `.modal` kind.
+-/
+private def splitFrameHyps {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (subgoalIdents frameIdents : List Ident) (negate : Bool) :
+    ProofModeM <| (el : Q($prop)) × (er : Q($prop)) ×
+      Hyps bi el × Hyps bi er × Q($e ⊣⊢ $el ∗ $er) × List IVarId := do
+  let ⟨ivars, frameIVars⟩ ← findFrameIVars hyps subgoalIdents frameIdents
+  let ⟨el, er, hypsl, hypsr, pf⟩ := Hyps.split bi
+    (λ _ ivar => (negate ^^ ivars.contains ivar) || frameIVars.contains ivar) hyps
+  return ⟨el, er, hypsl, hypsr, pf, frameIVars⟩
+
+/--
+  Applying framing and then solve the goal using `itrivial` (when `trivial` is
+  `true`) or add the goal into the proof state (when `trivial` is `false`).
+  Used by all `.goal` cases and the `.autoframe persistent` case in `processWand`.
+-/
+private def finishFrameSubgoal {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (goal : Q($prop)) (trivial : Bool) (g : Option Name)
+    (frameIVars : Option <| List IVarId) : ProofModeM Q($e ⊢ $goal) := do
+  let targets ← do match frameIVars with
+  -- For auto-framing
+  | none => SelPat.resolve hyps [.spatial, .intuitionistic]
+  -- For framing with the specified hypotheses
+  | some frameIVars => pure (frameIVars.map (⟨.ipm ·, true⟩))
+  let res ← iFrame bi hyps goal targets
+  res.finish λ hyps goal => do
+    if trivial then
+      let some r ← iTrivial hyps goal
+      | throwError "ispecialize: itrivial could not solve\
+          {← ppExpr <| IrisGoal.toExpr {hyps, goal ..}}"
+      return r
+    else addBIGoal hyps goal <| g.getD .anonymous
+
+private def synthIntoWand {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (p : Q(Bool)) (out : Q($prop)) (persistent : Bool) :
+    ProofModeM <| (out1 : Q($prop)) × (out2 : Q($prop)) ×
+      Q(IntoWand $p $persistent $out .out $out1 .out $out2) := do
+  let out1 ← mkFreshExprMVarQ prop
+  let out2 ← mkFreshExprMVarQ prop
+  let some inst ← ProofModeM.trySynthInstanceQ q(IntoWand $p $persistent $out .out $out1 .out $out2)
+    | throwError m!"ispecialize: {out} is not a wand"
+  return ⟨out1, out2, inst⟩
+
+/-- Used by the cases `.autoframe` and `.goal` in `processWand` with the `.persistent` kind. -/
+private def synthIntoWandPersistent {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (p : Q(Bool)) (out : Q($prop)) :
+    ProofModeM ((out1 : Q($prop)) × (out2 : Q($prop)) × (out1' : Q($prop)) ×
+      Q(IntoWand $p true $out .out $out1 .out $out2) ×
+      Q(Persistent $out1) × Q(IntoAbsorbingly $out1' $out1)) := do
+  let ⟨out1, out2, instWand⟩ : (out1 : Q($prop)) × (out2 : Q($prop)) ×
+    Q(IntoWand $p true $out .out $out1 .out $out2) ← @synthIntoWand u prop bi p out true
+  let some intoPers ← ProofModeM.trySynthInstanceQ q(Persistent $out1)
+  | throwError m!"ispecialize: {out1} is not persistent"
+  let out1' ← mkFreshExprMVarQ prop
+  let some instAbsorb ← ProofModeM.trySynthInstanceQ q(IntoAbsorbingly $out1' $out1)
+  | throwError m!"ispecialize: IntoAbsorbingly type class synthesis failed with {out1}"
+  return ⟨out1, out2, out1', instWand, intoPers, instAbsorb⟩
+
+/-- Used by the cases `.autoframe` and `.goal` in `processWand` with the `.modal` kind. -/
+private def synthIntoWandModal {u} {prop : Q(Type u)} {bi : Q(BI $prop)}
+    (p : Q(Bool)) (out goal : Q($prop)) :
+    ProofModeM ((out1 : Q($prop)) × (out2 : Q($prop)) × (out1' : Q($prop)) ×
+      Q(IntoWand $p false $out .out $out1 .out $out2) × Q(AddModal $out1' $out1 $goal)) := do
+  let ⟨out1, out2, instWand⟩ : (out1 : Q($prop)) × (out2 : Q($prop)) ×
+    Q(IntoWand $p false $out .out $out1 .out $out2) ← @synthIntoWand u prop bi p out false
+  let out1' ← mkFreshExprMVarQ prop
+  let some instModal ← ProofModeM.trySynthInstanceQ q(AddModal $out1' $out1 $goal)
+    | throwError m!"ispecialize: AddModal type class synthesis failed with {out1} and {goal}"
+  pure ⟨out1, out2, out1', instWand, instModal⟩
+
+mutual
 
-private def processWand :
-    @SpecializeState u prop bi orig → SpecPat → ProofModeM (SpecializeState bi orig)
-  | { hyps, p, out, pf, .. }, .ident i => do
+private def processWand {u} {prop : Q(Type u)} {bi : Q(BI $prop)} {orig goal : Q($prop)}
+    (specState : @SpecializeState u prop bi orig goal) (spat : Syntax × SpecPat) :
+    ProofModeM (@SpecializeState u prop bi orig goal) := do
+  let { e, hyps, p, out, pfCont, pf } := specState
+  let ⟨ref, spat⟩ := spat
+  withRef ref do
+  match spat with
+  -- A hypothesis name, possibly with nested specialisation patterns
+  | .ident i spats =>
     let ivar ← hyps.findWithInfo i
-    let ⟨e', hyps', out₁, out₁', p1, _, pf'⟩ := hyps.remove false ivar
-    let p2 := if p1.constName! == ``true then p else q(false)
-    have : $out₁ =Q iprop(□?$p1 $out₁') := ⟨⟩
-    have : $p2 =Q ($p1 && $p) := ⟨⟩
-
-    let out₂ ← mkFreshExprMVarQ prop
-    let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p $p1 $out .in $out₁' .out $out₂) |
-      throwError m!"ispecialize: cannot instantiate {out} with {out₁'}"
-    let pf := q(specialize_wand $pf $pf')
-    return { e := e', hyps := hyps', p := p2, out := out₂, pf }
-  | { e, hyps, p, out, pf, .. }, .pure t => do
+    let ⟨_, hyps', _, out1', p1, _, pf'⟩ := hyps.remove false ivar
+    let ⟨_, hyps'', pNest, outNest, pfContNest, pfNest⟩ ←
+      if spats.isEmpty then
+        -- No nested specialisation patterns
+        pure ⟨_, hyps', p1, out1', q(id), some q(.rfl)⟩
+      else
+        -- There are nested specialisation patterns, requires recursive calls
+        iSpecializeCore hyps' p1 out1' q(iprop(□?$p $out -∗ $goal)) spats
+    let p2 := if pNest.constName! == ``true then p else q(false)
+    let out2 ← mkFreshExprMVarQ prop
+    let some inst ← ProofModeM.trySynthInstanceQ q(IntoWand $p $pNest $out .in $outNest .out $out2)
+    | throwError m!"ispecialize: IntoWand type class synthesis failed with {out} and {outNest}"
+    match pfNest with
+    -- Nested specialisation pattern involves the `.modal` kind
+    | none =>
+      let pfCont := q(specialize_wand_nest_modal $inst $pfCont $pf' $pfContNest)
+      return { hyps := hyps'', p := p2, out := out2, pfCont, pf := none }
+    -- Nested specialisation pattern does not involve the `.modal` kind, or no nested pattern
+    | some pfNest =>
+      let pfStep := q(specialize_wand_nest $inst $pf' $pfNest)
+      return specState.update hyps'' p2 out2 pfStep
+  -- A pure Lean hypothesis
+  | .pure t => do
     let v ← mkFreshLevelMVar
     let α : Q(Sort v) ← mkFreshExprMVarQ q(Sort v)
     let Φ : Q($α → $prop) ← mkFreshExprMVarQ q($α → $prop)
-    let some _ ← ProofModeM.trySynthInstanceQ q(IntoForall $out $Φ)
-      | throwError "ispecialize: {out} is not a lean premise"
-    let x ← elabTermEnsuringTypeQ (u := .succ .zero) t α
+    let some inst ← ProofModeM.trySynthInstanceQ q(IntoForall $out $Φ)
+    | throwError "ispecialize: {out} is not a Lean premise"
+    let x ← elabTermEnsuringTypeQ t α
     have out' : Q($prop) := Expr.headBeta q($Φ $x)
-    have : $out' =Q $Φ $x := ⟨⟩
     let newMVarIds ← getMVarsNoDelayed x
     for mvar in newMVarIds do addMVarGoal mvar
-    return { e, hyps, p, out := out', pf := q(specialize_forall $pf $x) }
-  | { hyps, p, out, pf, .. }, .goal {kind, negate, trivial, frame := f, hyps := hs} g => do
-    if kind != .spatial then
-      -- TODO
-      throwError "ispecialize: only spatial kind is supported at the moment"
-    let mut ivars : IVarIdSet := {}
-    for name in hs do
-      ivars := ivars.insert (← hyps.findWithInfo name)
-    let mut frameIVars : List IVarId := []
-    for name in f do
-      let ivar ← hyps.findWithInfo name
-      frameIVars := ivar :: frameIVars
-      if ivars.contains ivar then
-        throwError "ispecialize: {name} used twice"
-    frameIVars := frameIVars.reverse
-    let ⟨el', _, hypsl', hypsr', pf'⟩ := Hyps.split bi
-      (λ _ ivar => (negate ^^ ivars.contains ivar) || frameIVars.contains ivar) hyps
-    let out₁ ← mkFreshExprMVarQ prop
-    let out₂ ← mkFreshExprMVarQ prop
-    let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $out .out $out₁ .out $out₂)
-      | throwError m!"ispecialize: {out} is not a wand"
-    let res ← iFrame bi _ hypsr' out₁ (frameIVars.map (⟨.ipm ·, true⟩))
-    let pf'' ← res.finish λ hyps goal => do
-      if trivial then
-        let some r ← iTrivial hyps goal
-          | throwError "ispecialize: itrivial could not solve {← ppExpr <| IrisGoal.toExpr {hyps, goal ..}}"
-        return r
-      else
-        addBIGoal hyps goal g
-    let pf := q(specialize_wand_subgoal $out₂ $pf $pf' $pf'')
-    return { e := el', hyps := hypsl', p := q(false), out := out₂, pf }
-
-  | { hyps, p, out, pf, .. }, .autoframe kind => do
-    if kind != .spatial then
-      -- TODO
-      throwError "ispecialize: only spatial kind is supported at the moment"
-    let out₁ ← mkFreshExprMVarQ prop
-    let out₂ ← mkFreshExprMVarQ prop
-    let some _ ← ProofModeM.trySynthInstanceQ q(IntoWand $p false $out .out $out₁ .out $out₂)
-      | throwError m!"ispecialize: {out} is not a wand"
-    let res ← iFrame bi _ hyps out₁ (← SelPat.resolve hyps [.spatial, .intuitionistic])
+    let pfStep : Q($e ∗ □?$p $out ⊢ $e ∗ □?$p $Φ $x) :=
+      q(specialize_forall (A2 := $e) (p := $p) $inst $x)
+    return specState.update hyps p out' pfStep
+  -- Subgoal with `[ H₁ … Hₙ ]` or `[- H₁ … Hₙ ]`
+  | .goal { kind := .spatial, negate, trivial, frame := f, hyps := hs } g => do
+    let ⟨_, _, hypsl, hypsr, pf', frameIVars⟩ ← splitFrameHyps hyps hs f negate
+    let ⟨out1, out2, inst⟩ ← synthIntoWand p out false
+    let pf'' ← finishFrameSubgoal hypsr out1 trivial g frameIVars
+    let pfStep := q(specialize_wand_subgoal $out2 $inst $pf' $pf'')
+    return specState.update hypsl q(false) out2 pfStep
+  -- Subgoal with `[# H₁ … Hₙ ]` or `[#- H₁ … Hₙ ]`
+  | .goal { kind := .persistent, trivial, frame := f, hyps := hs, .. } g => do
+    if !hs.isEmpty then
+      throwError "ispecialize: the subgoal for the persistent premise should not consume hypotheses"
+    let ⟨out1, out2, out1', instWand, instPers, instAbsorb⟩ ← synthIntoWandPersistent p out
+    let ⟨_, frameIVars⟩ ← findFrameIVars hyps [] f
+    let pf' ← finishFrameSubgoal hyps out1' trivial g frameIVars
+    let pfStep := q(specialize_wand_persistent $out1 $out2 $instWand $instPers $instAbsorb $pf')
+    return specState.update hyps p out2 pfStep
+  -- Subgoal with `[> H₁ … Hₙ ]` or `[>- H₁ … Hₙ ]`
+  | .goal { kind := .modal, negate, trivial, frame := f, hyps := hs, .. } g =>
+    let ⟨_, _, hypsl', hypsr', pf', frameIVars⟩ ← splitFrameHyps hyps hs f negate
+    let ⟨out1, out2, out1', instWand, instModal⟩ ← synthIntoWandModal p out goal
+    let pf'' ← finishFrameSubgoal hypsr' out1' trivial g frameIVars
+    let h := q($(pf').mp.trans (sep_mono_right $pf''))
+    let pfCont := q(fun pf => $pfCont (specialize_modal $h pf $instWand $instModal))
+    return { hyps := hypsl', p := q(false), out := out2, pfCont, pf := none }
+  -- Auto-framing with `[$]`
+  | .autoframe .spatial => do
+    let ⟨out1, out2, inst⟩ ← synthIntoWand p out false
+    let res ← iFrame bi hyps out1 (← SelPat.resolve hyps [.spatial, .intuitionistic])
     let ⟨_, hyps', pf'⟩ ← res.finishClose
-    return { e := _, hyps := hyps', p := q(false), out := out₂, pf := q(specialize_wand_autoframe $out₂ $pf $pf') }
-
-/-- `iCasesPat.should_try_dup_context` determines when iSpecializeCore should try to duplicate the separation context.
-The duplication only works if the conclusion of the specialization is persistent.
-
-TODO: Should this also return true for lists of intuitionistic patterns? (check in Rocq)
-
-TODO: This also needs to check that there are no modality addition patterns in `pat` once they are implemented.
--/
-@[rocq_alias intro_pat_intuitionistic, rocq_alias use_tac_specialize_intuitionistic_helper]
-def iCasesPat.should_try_dup_context (pat : iCasesPat) : Bool :=
-  match pat with
-  | .intuitionistic _ => true
-  | .pure _ => true
-  | _ => false
+    let pfStep := q(specialize_wand_autoframe_spatial $out2 $inst $pf')
+    return specState.update hyps' q(false) out2 pfStep
+  -- Auto-framing with `[#$]`
+  | .autoframe .persistent =>
+    let ⟨out1, out2, out1', instWand, instPers, instAbsorb⟩ ← synthIntoWandPersistent p out
+    let pf' ← finishFrameSubgoal hyps out1' true none none
+    let pfStep := q(specialize_wand_persistent $out1 $out2 $instWand $instPers $instAbsorb $pf')
+    return specState.update hyps p out2 pfStep
+  -- Auto-framing with `[>$]`
+  | .autoframe .modal =>
+    let ⟨out1, out2, out1', instWand, instModal⟩ ← synthIntoWandModal p out goal
+    let res ← iFrame bi hyps out1' (← SelPat.resolve hyps [.spatial, .intuitionistic])
+    let ⟨_, hyps', pf'⟩ ← res.finishClose
+    let pfCont := q(fun pf => $pfCont (specialize_modal $pf' pf $instWand $instModal))
+    return { hyps := hyps', p := q(false), out := out2, pfCont, pf := none }
 
 /-- Specialize a proposition `A` by applying a sequence of specialization patterns.
 
@@ -161,24 +335,49 @@ A tuple containing:
 - `B`: Resulting proposition after applying all patterns
 - `pf`: Proof of `hyps ∗ □?pa A ⊢ hyps' ∗ □?pb B`, =`hyps ∗ □?pa A ⊢ hyps ∗ □ B` if context duplication succeeds
 -/
-def iSpecializeCore {e} (hyps : @Hyps u prop bi e) (pa : Q(Bool)) (A : Q($prop)) (spats : List SpecPat) (try_dup_context : Bool := false) :
-  ProofModeM ((e' : _) × Hyps bi e' × (pb : Q(Bool)) × (B : Q($prop)) × Q($e ∗ □?$pa $A ⊢ $e' ∗ □?$pb $B)) := do
-  let state := { hyps, out := A, p := pa, pf := q(.rfl), .. }
-  let ⟨_, hyps', pb, B, pf⟩ ← spats.foldlM processWand state
-  if try_dup_context then
-    -- context duplication succeeds if `B` is persistent, and `A` is persistent or affine
+def iSpecializeCore {prop : Q(Type u)} {bi : Q(BI $prop)} {e}
+    (hyps : Hyps bi e) (pa : Q(Bool)) (A : Q($prop)) (goal : Q($prop))
+    (spats : List (Syntax × SpecPat)) (try_dup_context : Bool := false) :
+    ProofModeM ((e' : _) × Hyps bi e' × (pb : Q(Bool)) × (B : Q($prop)) ×
+      Q(($e' ∗ □?$pb $B ⊢ $goal) → $e ∗ □?$pa $A ⊢ $goal) ×
+      Option Q($e ∗ □?$pa $A ⊢ $e' ∗ □?$pb $B)) := do
+  let state : SpecializeState _ goal :=
+    { hyps, out := A, p := pa, pfCont := q(id), pf := some q(.rfl) }
+  let ⟨hyps', pb, B, pfCont, pf⟩ ← spats.foldlM processWand state
+  match try_dup_context, pf with
+  | true, some pf =>
+    -- Duplicate context if `B` is persistent and `A` is persistent/affine
     let B' : Q($prop) ← mkFreshExprMVarQ q($prop)
-    let .some _ ← trySynthInstanceQ q(IntoPersistently $pb $B $B')
-      | return ⟨_, hyps', pb, B, pf⟩
-    have af : MetaM (Option Q($pa = true ∨ Affine $A)) :=
-      match matchBool pa with
-      | .inl _ => return some q(.inl (.refl _))
-      | .inr _ => do
-        let .some h ← trySynthInstanceQ q(Affine $A) | return none
-        return some q(.inr $h)
-    let some af ← af | return ⟨_, hyps', pb, B, pf⟩
-    return ⟨_, hyps, q(true), B', q(specialize_dup_context $pf $af)⟩
-  return ⟨_, hyps', pb, B, pf⟩
+    let af ← do match matchBool pa with
+    | .inl _ => pure <| some q(Or.inl (.refl $pa))
+    | .inr _ => do
+      let .some h ← trySynthInstanceQ q(Affine $A) | pure none
+      pure <| some q(Or.inr (a := $pa = true) $h)
+    let inst ← ProofModeM.trySynthInstanceQ q(IntoPersistently $pb $B $B')
+    match inst, af with
+    -- Context duplication does not succeed
+    | none, _ | _, none => return ⟨_, hyps', pb, B, q($(pf).trans), some q($pf)⟩
+    -- Context duplication succeeds
+    | some inst, some af =>
+      let pf := q(specialize_dup_context $inst $pf $af)
+      return ⟨_, hyps, q(true), B', q($(pf).trans), some q($pf)⟩
+  -- No request to duplicate the context, or the `.modal` kind is involved
+  | _, _ => return ⟨_, hyps', pb, B, pfCont, pf⟩
+
+end
+
+/--
+`iCasesPat.should_try_dup_context` determines when iSpecializeCore should try to
+duplicate the separation context.
+The duplication only works if the conclusion of the specialization is persistent.
+-/
+@[rocq_alias intro_pat_intuitionistic, rocq_alias use_tac_specialize_intuitionistic_helper]
+partial def iCasesPat.should_try_dup_context (pat : iCasesPat) : Bool :=
+  match pat with
+  | .conjunction args | .disjunction args => args.all (·.should_try_dup_context)
+  | .intuitionistic _ => true
+  | .pure _ => true
+  | _ => false
 
 /--
   `ispecialize pmt` specialises a hypothesis according to `pmt : pmTerm`.
@@ -186,15 +385,15 @@ def iSpecializeCore {e} (hyps : @Hyps u prop bi e) (pa : Q(Bool)) (A : Q($prop))
 elab "ispecialize " colGt pmt:pmTerm : tactic => do
   let pmt ← liftMacroM <| PMTerm.parse pmt
   ProofModeM.runTactic λ mvar { bi, hyps, goal, .. } => do
-  -- hypothesis must be in the context, otherwise use ihave
+  -- Hypothesis must be in the context, otherwise use `ihave`
   let name := ⟨pmt.term⟩
   let some ivar ← try? <| hyps.findWithInfo name
-    | throwError "{name} should be a hypothesis, use ihave instead"
+    | throwError "ispecialize: {name} should be a hypothesis, use ihave instead"
   let some ⟨name, _, hyps', _, out, p, _, pf⟩ := Id.run <|
     hyps.removeG true λ name ivar' _ _ => if ivar == ivar' then some name else none
-    | throwError "ispecialize: cannot find argument"
+    | throwError "ispecialize: cannot find argument {name}"
 
-  let ⟨_, hyps'', pb, B, pf'⟩ ← iSpecializeCore hyps' p out pmt.spats
+  let ⟨_, hyps'', pb, B, pf', _⟩ ← iSpecializeCore hyps' p out goal pmt.spats
   let hyps''' := Hyps.add bi name ivar pb B hyps''
   let pf'' ← addBIGoal hyps''' goal
-  mvar.assign q(($pf).1.trans <| $(pf').trans <| $pf'')
+  mvar.assign q(($pf).mp.trans <| $pf' $pf'')
diff --git a/Iris/Iris/Tests/Tactics.lean b/Iris/Iris/Tests/Tactics.lean
index fb8509a5f..5bb770d88 100644
--- a/Iris/Iris/Tests/Tactics.lean
+++ b/Iris/Iris/Tests/Tactics.lean
@@ -10,12 +10,14 @@ public import Iris.ProofMode
 public import Iris.Instances.IProp
 public import Iris.Instances.Lib.LaterCredits
 public import Iris.Instances.Lib.Token
+public import Iris.ProgramLogic.Language
+public import Iris.ProgramLogic.WeakestPre
 public import Iris.Algebra.CMRA
 
 @[expose] public section
 
 namespace Iris.Tests
-open BI CMRA DFrac
+open BI CMRA DFrac ProgramLogic
 
 /- This file contains tests with various scenarios for all available tactics. -/
 
@@ -661,7 +663,7 @@ example [BI PROP] (Q : α → PROP) (a b : α) : (∀ x, ∀ y, ⌜x = a⌝ -∗
   iintro H
   iapply H $$ %_ %b %rfl
 
-/-- error: ispecialize: iprop(P a -∗ Q b) is not a lean premise -/
+/-- error: ispecialize: iprop(P a -∗ Q b) is not a Lean premise -/
 #guard_msgs in
 example [BI PROP] (P Q : α → PROP) (a b : α) : (∀ x, ∀ y, P x -∗ Q y) ⊢ P a -∗ Q b := by
   iintro H HP
@@ -855,6 +857,36 @@ example [BI PROP] (P Q : PROP) (h : P ⊢ □ Q) : ⊢ P -∗ P ∗ Q := by
   · iexact HP
   · iexact HQ
 
+/--
+  Tests `ihave` with the specialisation pattern involving modalities.
+  Despite `try_dup_context` being `true`, the context is not duplicated.
+-/
+example [BI PROP] [BIAffine PROP] [BIUpdate PROP] (P : PROP) [Persistent P] :
+    |==> P ⊢ |==> P := by
+  iintro HP
+  ihave #HP : P $$ [> HP //]
+  imodintro
+  iexact HP
+
+/-- Tests `ihave` with the specialisation pattern involving auto-framing with modalities. -/
+example [BI PROP] [BIAffine PROP] [BIUpdate PROP] (P : PROP) [Persistent P] :
+    |==> P ⊢ |==> P := by
+  iintro HP
+  ihave #HP : P $$ [>$]
+  imodintro
+  iexact HP
+
+/--
+  Tests `ihave` with a destruction pattern involving a conjunction of
+  intuitionistic hypotheses.
+-/
+example [BI PROP] (P Q1 Q2 : PROP) [Persistent Q1] [Persistent Q2] :
+    ⊢ P -∗ (P -∗ □ Q1 ∗ □ Q2) -∗ P ∗ (P -∗ □ Q1 ∗ □ Q2) := by
+  iintro HP HPQ
+  ihave ⟨#HQ1, #HQ2⟩ : □ Q1 ∗ □ Q2 $$ [HP HPQ]
+  · iapply HPQ $$ HP
+  · isplitl [HP] <;> iassumption
+
 end ihave
 
 -- ex falso
@@ -1078,7 +1110,7 @@ example [BI PROP] (Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
 
 -- Test `ispecialize` with failing `//`
 /--
-error: ispecialize: itrivial could not solve ⏎
+error: ispecialize: itrivial could not solve
 ⊢ False
 -/
 #guard_msgs in
@@ -1086,7 +1118,6 @@ example [BI PROP] (Q : PROP) : ⊢ (False -∗ Q) -∗ Q := by
   iintro HQ
   ispecialize HQ $$ [//]
 
-
 /-- Tests `ispecialize` with named subgoal -/
 example [BI PROP] (Q : PROP) : P ⊢ (⌜True⌝ -∗ P -∗ ⌜True⌝ -∗ Q) -∗ Q := by
   iintro HP HPQ
@@ -1292,6 +1323,199 @@ example [BI PROP] (P Q : PROP) :
   · rfl
   iexact H
 
+/-- Tests `ispecialize` with subgoals excluding specified hypotheses -/
+example [BI PROP] (P1 P2 P3 Q : PROP) : P1 -∗ P2 -∗ P3 -∗ (P1 -∗ P2 -∗ P3 -∗ Q) -∗ Q := by
+  iintro HP1 HP2 HP3 HPQ
+  ispecialize HPQ $$ [- HP2 HP3] [- HP3] [-]
+  · iexact HP1
+  · iexact HP2
+  · iexact HP3
+  iexact HPQ
+
+/-- Tests `ispecialize` with autoframing for the intuitionistic kind -/
+example [BI PROP] (P1 P2 P3 Q : PROP) :
+    □ P1 -∗ <pers> P2 -∗ □ P3 -∗ (□ P1 -∗ <pers> P2 -∗ <pers> P3 -∗ Q) -∗ Q := by
+  iintro #HP1 HP2 #HP3 HPQ
+  ispecialize HPQ $$ [# $] [$] [# $]
+  iexact HPQ
+
+/--
+  Tests `ispecialize` with autoframing with a persistent hypothesis in the
+  spatial context used twice.
+-/
+example [BI PROP] (φ : Prop) (Q : PROP) :
+    ⌜φ⌝ -∗ (⌜φ⌝ -∗ Q) -∗ (⌜φ⌝ -∗ Q) -∗ ⌜φ⌝ ∗ Q ∗ Q := by
+  iintro HP1 HPQ1 HPQ2
+  ispecialize HPQ1 $$ [# $]
+  ispecialize HPQ2 $$ [# $]
+  iframe
+
+/- Tests `ispecialize` with autoframing, but the premise is not persistent. -/
+/-- error: ispecialize: P is not persistent -/
+#guard_msgs in
+example [BI PROP] (φ : Prop) (P Q : PROP) :
+    P -∗ (P -∗ Q) -∗ True := by
+  iintro HP HPQ
+  ispecialize HPQ $$ [# $]
+
+/-- Tests `ispecialize` for a persistent premise with chosen hypotheses for the subgoal. -/
+example [BI PROP] (P1 P2 P3 Q : PROP) :
+    <pers> P1 -∗ <pers> P2 -∗ <pers> P3 -∗
+    ((<pers> P1 ∗ <pers> P2) -∗ Q) -∗
+    ((<pers> P1 ∗ <pers> P3) -∗ Q) -∗
+    <pers> P1 ∗ <pers> P2 ∗ <pers> P3 ∗ Q ∗ Q := by
+  iintro HP1 HP2 HP3 HPQ12 HPQ13
+  ispecialize HPQ12 $$ [# $HP1]
+  · iexact HP2
+  ispecialize HPQ13 $$ [# $HP1 $HP3]
+  iframe
+
+/-
+  Tests `ispecialize` for handling a persistent premise, except that the
+  premise is not persistent.
+-/
+/-- error: ispecialize: P is not persistent -/
+#guard_msgs in
+example [BI PROP] (φ : Prop) (P Q : PROP) :
+    P -∗ (P -∗ Q) -∗ True := by
+  iintro HP HPQ
+  ispecialize HPQ $$ [# $HP]
+
+/- Tests `ispecialize` with hypotheses chosen to be consumed for a persistent premise. -/
+/-- error: ispecialize: the subgoal for the persistent premise should not consume hypotheses -/
+#guard_msgs in
+example [BI PROP] (φ : Prop) (P Q : PROP) :
+    <pers> P -∗ (<pers> P -∗ Q) -∗ True := by
+  iintro HP HPQ
+  ispecialize HPQ $$ [# HP]
+
+/-- Tests `ispecialize` with nested specialisation patterns. -/
+example [BI PROP] (P Q R S T : PROP) :
+    ⊢ (P -∗ <pers> T -∗ Q) -∗ (Q -∗ <pers> T -∗ R) -∗ (R -∗ S) -∗ P -∗ <pers> T -∗ S := by
+  iintro HPTQ HQTR HRS HP HT
+  ispecialize HRS $$ (HQTR $$ (HPTQ $$ HP [# $HT]) [HT //])
+  iassumption
+
+/--
+  Tests `ispecialize` with `.autoframe .modal` using the type class instance
+  `addModal_bupd` and `addModal_fupd`.
+-/
+example [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] (P Q R S : PROP) (E : CoPset) :
+    ⊢ (P -∗ Q) -∗ (R -∗ S) -∗ (|==> P) -∗ (|={E}=> R) -∗ (|==> Q) ∗ (|={E}=> S) := by
+  iintro HPQ HRS HP HR
+  isplitl [HPQ HP]
+  · ispecialize HPQ $$ [>$]
+    imodintro
+    iassumption
+  · ispecialize HRS $$ [>$]
+    imodintro
+    iassumption
+
+/-- Tests `ispecialize` for its use of the type class instance `add_modal_forall`,
+  `add_modal_bupd` and `add_modal_later`. -/
+example [BI PROP] [BIUpdate PROP]
+    (P : PROP) (Q : Nat → PROP) (R S : PROP) [Timeless R] :
+    ⊢ (P -∗ (∀ x, Q x)) -∗ (|==> P) -∗ (R -∗ S) -∗ (▷ R) -∗
+      (∀ x, |==> Q x) ∗ (▷ S) := by
+  iintro HPQ HP HRS HR
+  isplitl [HPQ HP]
+  · ispecialize HPQ $$ [>$]
+    iintro %x
+    ispecialize HPQ $$ %x
+    imodintro
+    iassumption
+  · ispecialize HRS $$ [> HR]
+    · imod HR
+      iassumption
+    · inext
+      iassumption
+
+/-- Tests `ispecialize` for its use of the type class instance `add_modal_fupd_wp`. -/
+example {hlc : HasLC} {Expr State Obs Val : Type _} [Language Expr State Obs Val]
+    {GF : BundledGFunctors} [IrisGS_gen hlc Expr GF]
+    (s : Stuckness) (E : CoPset) (e : Expr) (P : IProp GF) (Φ : Val → IProp GF) :
+    ⊢ (P -∗ WP e @ s ; E {{ Φ }}) -∗ (|={E}=> P) -∗ WP e @ s ; E {{ Φ }} := by
+  iintro HPQ HP
+  ispecialize HPQ $$ [>$]
+  iassumption
+
+/--
+  Tests `ispecialize` with the handling of the modality using the type class
+  instance `addModal_bupd`. The subgoal is manually solved.
+-/
+example [BI PROP] [BIUpdate PROP] (P Q : PROP) :
+    ⊢ (P -∗ Q) -∗ (|==> P) -∗ (|==> Q) := by
+  iintro HPQ HP
+  ispecialize HPQ $$ [> HP]
+  · iassumption
+  · imodintro
+    iassumption
+
+/--
+  Tests `ispecialize` with the handling of the modality, nested patterns and
+  the use of the type class instance `addModal_wand`.
+-/
+example [BI PROP] [BIUpdate PROP] (P Q R : PROP) :
+    ⊢ (P -∗ R) -∗ (Q -∗ P) -∗ (|==> Q) -∗ (|==> R) := by
+  iintro HPR HQP HQ
+  ispecialize HPR $$ (HQP $$ [> HQ //])
+  imodintro
+  iassumption
+
+/--
+  Tests `ispecialize` with the auto-framing with modality, nested patterns and
+  the use of the type class instance `addModal_wand`.
+-/
+example [BI PROP] [BIUpdate PROP] (P Q R : PROP) :
+    ⊢ (P -∗ R) -∗ (Q -∗ P) -∗ (|==> Q) -∗ (|==> R) := by
+  iintro HPR HQP HQ
+  ispecialize HPR $$ (HQP $$ [> $])
+  imodintro
+  iassumption
+
+/- Tests `ispecialize` with an invalid specialisation pattern (duplicated hypotheses). -/
+/-- error: ispecialize: HP used twice for framing -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
+  iintro HP HPQ
+  ispecialize HPQ $$ [$HP $HP]
+
+/- Tests `ispecialize` with an invalid specialisation pattern (duplicated hypotheses). -/
+/-- error: ispecialize: HP cannot be used for both the subgoal and framing -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ (P -∗ Q) -∗ Q := by
+  iintro HP HPQ
+  ispecialize HPQ $$ [HP $HP]
+
+/- Tests `ispecialize` with an invalid hypothesis choice. -/
+/-- error: ispecialize: P is not a wand -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q := by
+  iintro HP
+  ispecialize HP $$ [$]
+
+/- Tests `ispecialize` with an invalid specialisation pattern. -/
+/-- error: ispecialize: IntoWand type class synthesis failed with P and Q -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q -∗ Q := by
+  iintro HP HQ
+  ispecialize HP $$ HQ
+
+/- Tests `ispecialize` with an invalid specialisation pattern using pure hypotheses. -/
+/-- error: ispecialize: P is not a Lean premise -/
+#guard_msgs in
+example [BI PROP] (P Q : PROP) : P ⊢ Q := by
+  iintro HP
+  ispecialize HP $$ %(0 : Nat)
+
+/-- Tests `ispecialize` with a specialisation pattern naming the subgoal. -/
+example [BI PROP] [BIUpdate PROP] (P Q : PROP) :
+    ⊢ (P -∗ Q) -∗ (|==> P) -∗ (|==> Q) := by
+  iintro HPQ HP
+  ispecialize HPQ $$ [> HP] as subgoal
+  case subgoal => iassumption
+  imodintro; iassumption
+
 end specialize
 
 -- split
diff --git a/Iris/tactics.md b/Iris/tactics.md
index f9e465ec0..85371a7f5 100644
--- a/Iris/tactics.md
+++ b/Iris/tactics.md
@@ -110,9 +110,15 @@ Used in [proof mode terms](#proof-mode-terms) after `$$` to eliminate the premis
 - `%`*t* — Instantiate a universal quantifier with the pure term *t*.
 - `[`*H₁* ... *Hₙ*`]` — Generate a subgoal for the premise with exactly the spatial hypotheses *Hᵢ*. Hypotheses written as `$H` are framed instead of forming the context.
 - `[-` *H₁* ... *Hₙ*`]` — Like above, but use all spatial hypotheses *except* the listed ones.
+- `[>` *H₁* ... *Hₙ*`]` — Given the proof goal involves a modality, solve the premise by wrapping it with the modality and then by generating a subgoal with the spatial hypotheses *Hᵢ*. Hypotheses written as `$H` are framed instead of forming the context.
+- `[>-` *H₁* ... *Hₙ*`]` — Like above, but use all spatial hypotheses *except* the listed ones.
+- `[#` `$`*H₁* ... `$`*Hₙ*`]` — Generate a subgoal for the *persistent* premise with the hypotheses *H₁*, ..., *Hₙ* being framed. The spatial hypotheses used for framing are not consumed.
 - `[`... `//]` — Additionally try to solve the subgoal with `itrivial` and fail if unsuccessful.
 - `[`...`] as` *name* — Name the generated subgoal *name*.
 - `[$]` — Solve the premise entirely by framing spatial and intuitionistic hypotheses.
+- `[# $]` — Solve the *persistent* premise by framing spatial and intutionistic hypotheses. The spatial hypotheses used for framing are not consumed.
+- `[> $]` — Given the proof goal involves a modality, solve the premise by wrapping it with the modality and then by framing.
+- `(` *H* `$$` *spat₁* ... *spatₙ* `)` — specialises the hypothesis *H* with the specialisation patterns *spat₁*, ..., *spatₙ* before the resultant hypothesis is itself used for matching a premise.
 
 If the conclusion of a specialization is persistent, the context can be shared between the subgoal and the main goal (e.g. `ihave #HQ : □ Q $$ [HP]` keeps `HP` usable in the main goal).