diff --git a/theories/tests/message_passing.v b/theories/tests/message_passing.v
index 648fc9aeea2e91e7cef9d87a21943e69017cecd5..518033fc27019b0065452ee7dc2210f5978cecaf 100644
--- a/theories/tests/message_passing.v
+++ b/theories/tests/message_passing.v
@@ -18,7 +18,7 @@ Next Obligation.
 Qed.
 
 Lemma message_passing :
-  adequate (message_passing, ∅) initial_state (λ v, v.1 = LitV (LitInt 37)).
+  adequate NotStuck (message_passing, ∅) initial_state (λ v, v.1 = LitV (LitInt 37)).
 Proof.
   apply (base_adequacy Σ _ ∅); auto.
   - split; repeat red; rewrite /initial_state /=; try set_solver.
@@ -29,9 +29,13 @@ Proof.
     last iMod (persistor_init with "PS") as (?) "#Pers".
     { by auto. }
     iModIntro.
-    iApply (message_passing_spec ∅ with "[%] PS Seen Pers").
-    { reflexivity. }
-    iNext. iViewUp. iIntros (v) "? %". by subst.
+    iPoseProof (message_passing_spec (fun v => ⌜v = #37⌝)%I with "[$PS $Pers]") as "T".
+    iSpecialize ("T" $! ∅ with "[%]"); [reflexivity|].
+    rewrite WP_Def.wp_eq /WP_Def.wp_def. cbn.
+    iApply wp_mono; cycle 1.
+    + iApply "T"; [|done|done].
+      iNext. iIntros. iPureIntro. intros []. done.
+    + iIntros ([v ?]) "[_ %]". subst v. done.
 Qed.
 
 Print Assumptions message_passing.