diff --git a/coq/ra/_CoqProject b/coq/ra/_CoqProject
index e397433b0669d16d28a5e8d2c7feec46f74f29ea..924f59403f1039579e1e2b9bdd0761386c011aec 100644
--- a/coq/ra/_CoqProject
+++ b/coq/ra/_CoqProject
@@ -62,3 +62,4 @@ examples/message_passing.v
 examples/spin_lock.v
 examples/circ_buffer.v
 examples/ticket_lock.v
+tests/message_passing.v
diff --git a/coq/ra/tests/message_passing.v b/coq/ra/tests/message_passing.v
new file mode 100644
index 0000000000000000000000000000000000000000..dd84ee78b577190902773c2287c8ceb63e965bc5
--- /dev/null
+++ b/coq/ra/tests/message_passing.v
@@ -0,0 +1,40 @@
+From iris.heap_lang Require Import adequacy.
+From ra.examples Require Import message_passing.
+From ra.gps Require Import shared inst_shared.
+From ra Require Import adequacy.
+
+Let Σ : gFunctors := #[ baseΣ;
+                        gpsΣ protocols.boolProtocol _ ;
+                        gps_agreeΣ protocols.boolProtocol _;
+                        absViewΣ;
+                        persistorΣ;
+                        mpΣ ].
+
+Program Definition initial_state :=
+  {| threads := {[ 1%positive := ∅ ]};
+     mem := mkMemory ∅ (_);
+     nats := ∅ |}.
+Next Obligation.
+  rewrite /pairwise_disj. set_solver.
+Qed.
+
+Lemma message_passing :
+  adequate (message_passing, 1%positive) initial_state (λ v, v = (LitV (LitInt 37), 1%positive)).
+Proof.
+  apply (base_adequacy Σ _ ∅); auto.
+  - split; repeat red; rewrite /initial_state /=; try set_solver.
+    intros ? ?. case: (decide (Ï€ = 1%positive)) => [->|?].
+    + rewrite lookup_singleton. move => [<- {V}]. set_solver.
+    + rewrite lookup_singleton_ne //.
+  - iIntros (?) "[#PS Seen]".
+    iApply fupd_wp.
+    iApply fupd_mask_mono;
+    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.
+Qed.
+
+Print Assumptions message_passing.
\ No newline at end of file