diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 71cb6ffd07bd5cf7baba339ece79808dfd0eb316..a8bcfdb22ee8d5eece409693f96c2d21e8fedc82 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -91,11 +91,11 @@ Proof.
 Qed.
 
 (** Actual proofs *)
-Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) :
+Lemma newbarrier_spec (P : iProp Σ) :
   heapN ⊥ N →
-  heap_ctx ★ (∀ l, recv l P ★ send l P -★ Φ #l) ⊢ WP newbarrier #() {{ Φ }}.
+  {{{ heap_ctx }}} newbarrier #() {{{ l; #l, recv l P ★ send l P }}}.
 Proof.
-  iIntros (HN) "[#? HΦ]".
+  iIntros (HN Φ) "[#? HΦ]".
   rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with ">[-]").
   iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
@@ -117,14 +117,15 @@ Proof.
   - auto.
 Qed.
 
-Lemma signal_spec l P (Φ : val → iProp Σ) :
-  send l P ★ P ★ Φ #() ⊢ WP signal #l {{ Φ }}.
+Lemma signal_spec l P :
+  {{{ send l P ★ P }}} signal #l {{{; #(), True }}}.
 Proof.
   rewrite /signal /send /barrier_ctx /=.
-  iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
+  iIntros (Φ) "((Hs&HP)&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
-  destruct p; [|done]. wp_store. iFrame "HΦ".
+  destruct p; [|done]. wp_store.
+  iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
   iMod ("Hclose" $! (State High I) (∅ : set token) with "[-]"); last done.
   iSplit; [iPureIntro; by eauto using signal_step|].
   iNext. rewrite {2}/barrier_inv /ress /=; iFrame "Hl".
@@ -132,11 +133,11 @@ Proof.
   iNext. iIntros "_"; by iApply "Hr".
 Qed.
 
-Lemma wait_spec l P (Φ : val → iProp Σ) :
-  recv l P ★ (P -★ Φ #()) ⊢ WP wait #l {{ Φ }}.
+Lemma wait_spec l P:
+  {{{ recv l P }}} wait #l {{{ ; #(), P }}}.
 Proof.
   rename P into R; rewrite /recv /barrier_ctx.
-  iIntros "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
+  iIntros (Φ) "[Hr HΦ]"; iDestruct "Hr" as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
   iLöb as "IH". wp_rec. wp_bind (! _)%E.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
diff --git a/heap_lang/lib/barrier/specification.v b/heap_lang/lib/barrier/specification.v
index 720ae3390df5ef4e7beb72bd78db8bdb1c164765..b9ae66872928c848cd356d8f8391767d59493a6f 100644
--- a/heap_lang/lib/barrier/specification.v
+++ b/heap_lang/lib/barrier/specification.v
@@ -21,7 +21,7 @@ Proof.
   exists (λ l, CofeMor (recv N l)), (λ l, CofeMor (send N l)).
   split_and?; simpl.
   - iIntros (P) "#? !# _". iApply (newbarrier_spec _ P); eauto.
-  - iIntros (l P) "!# [Hl HP]". by iApply signal_spec; iFrame "Hl HP".
+  - iIntros (l P) "!# [Hl HP]". iApply signal_spec; iFrame "Hl HP"; by eauto.
   - iIntros (l P) "!# Hl". iApply wait_spec; iFrame "Hl"; eauto.
   - iIntros (l P Q) "!#". by iApply recv_split.
   - apply recv_weaken.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 791eab9f05e7a97e4de36d0b1aa6c09fdffcb03c..75f47b1c395f30d26caa1ef81b8f25a953e15a3b 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -50,6 +50,17 @@ Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
+Notation "'{{{' pre } } } e {{{ x .. y ; pat , post } } }" :=
+  (∀ (ψ : _ → uPred _),
+      (pre ★ (∀ x, .. (∀ y, post -★ ψ (pat)%V) .. )%I) ⊢ WP e {{ ψ }})
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  pre  } } }  e  {{{ x .. y ;  pat ,  post } } }") : C_scope.
+Notation "'{{{' pre } } } e {{{ ; pat , post } } }" :=
+  (∀ (ψ : _ → uPred _),
+      (pre ★ (post -★ ψ (pat)%V)%I) ⊢ WP e {{ ψ }})
+    (at level 20,
+     format "{{{  pre  } } }  e  {{{ ; pat ,  post } } }") : C_scope.
+
 Section wp.
 Context `{irisG Λ Σ}.
 Implicit Types P : iProp Σ.
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 67a78210009786ad462a1b5f91f026c9492a119e..5f1e50946b67ba78c62db8ff882ec316cf905c04 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -43,7 +43,7 @@ Section client.
     iApply (wp_par (λ _, True%I) (λ _, True%I)). iFrame "Hh".
     iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
-      wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
+      wp_store. iApply signal_spec; iFrame "Hs"; iSplitL "Hy"; [|by eauto].
       iExists _; iSplitL; [done|]. iAlways; iIntros (n). wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros (_ _) "_ !>"].
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 6081ff86439194d8576eb217c2b56fbc4064ec51..3c892714cf1a5340c49ab4b5d023a5a5fa3972ea 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -85,7 +85,7 @@ Proof.
     iIntros (v) "HP"; iDestruct "HP" as (x) "HP". wp_let.
     iMod (own_update with "Hγ") as "Hx".
     { by apply (cmra_update_exclusive (Shot x)). }
-    iApply signal_spec; iFrame "Hs"; iSplit; last done.
+    iApply signal_spec; iFrame "Hs"; iSplitR ""; last auto.
     iExists x; auto.
   - iDestruct (recv_weaken with "[] Hr") as "Hr"; first by iApply P_res_split.
     iMod (recv_split with "Hr") as "[H1 H2]"; first done.