diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 6d9b3e3cf3c49fba5186f41f225a21e2a272f270..b88fe4d52a81fdeb5d7648629766ba9063ad6e1c 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -265,6 +265,80 @@ Tactic Notation "rel_load_r" :=
   |reflexivity
   |rel_finish  (** new goal *)].
 
+(** Store *)
+Lemma tac_rel_store_l_simpl `{relocG Σ} K ℶ1 ℶ2 ℶ3 i1 Γ (l : loc) v e' v' e t eres A :
+  e = fill K (Store (# l) e') →
+  IntoVal e' v' →
+  MaybeIntoLaterNEnvs 1 ℶ1 ℶ2 →
+  envs_lookup i1 ℶ2 = Some (false, l ↦ v)%I →
+  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ v')) ℶ2 = Some ℶ3 →
+  eres = fill K #() →
+  envs_entails ℶ3 (refines ⊤ Γ eres t A) →
+  envs_entails ℶ1 (refines ⊤ Γ e t A).
+Proof.
+  rewrite envs_entails_eq. intros ?????? Hg.
+  subst e eres.
+  rewrite into_laterN_env_sound envs_simple_replace_sound //; simpl.
+  rewrite bi.later_sep.
+  rewrite right_id.
+  rewrite -(refines_store_l K Γ ⊤ l).
+  rewrite -fupd_intro.
+  rewrite -(bi.exist_intro v).
+  by rewrite Hg.
+Qed.
+
+Lemma tac_rel_store_r `{relocG Σ} K ℶ1 ℶ2 i1 Γ E (l : loc) v e' v' e t eres A :
+  e = fill K (Store (# l) e') →
+  IntoVal e' v' →
+  nclose specN ⊆ E →
+  envs_lookup i1 ℶ1 = Some (false, l ↦ₛ v)%I →
+  envs_simple_replace i1 false (Esnoc Enil i1 (l ↦ₛ v')) ℶ1 = Some ℶ2 →
+  eres = fill K #() →
+  envs_entails ℶ2 (refines E Γ t eres A) →
+  envs_entails ℶ1 (refines E Γ t e A).
+Proof.
+  rewrite envs_entails_eq. intros ?????? Hg.
+  subst e eres.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id.
+  rewrite (refines_store_r Γ E K) //.
+  rewrite Hg.
+  apply bi.wand_elim_l.
+Qed.
+
+Tactic Notation "rel_store_l" :=
+  iStartProof;
+  rel_reshape_cont_l ltac:(fun K e' =>
+      (* Try to apply the simple store tactic first. If it doesn't work then apply the atomic store rule *)
+      first
+        [eapply (tac_rel_store_l_simpl K);
+         [reflexivity       (** e = fill K !#l *)
+         |iSolveTC          (** IntoLaters *)
+         |iAssumptionCore   (** find l ↦ - *)
+         |pm_reflexivity   || fail "rel_store_l: this shouldn't happen"
+         |reflexivity       (** eres = fill K v *)
+         |                  (** new goal *)]
+        |iApply (refines_store_l K)];
+        rel_finish)
+  || fail "rel_store_l: cannot find 'Store'".
+
+Tactic Notation "rel_store_r" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦ₛ _)%I) => l end in
+    iAssumptionCore || fail "rel_store_r: cannot find" l "↦ₛ ?" in
+  iStartProof;
+  first
+    [rel_reshape_cont_r ltac:(fun K e' =>
+       eapply (tac_rel_store_r K);
+       [reflexivity|iSolveTC|idtac..])
+    |fail 1 "rel_store_r: cannot find 'Store'"];
+  (* the remaining goals are from tac_rel_store_r (except for the first one, which has already been solved by this point) *)
+  [solve_ndisj || fail "rel_store_r: cannot prove 'nclose specN ⊆ ?'"
+  |solve_mapsto ()
+  |pm_reflexivity || fail "rel_store_r: this should not happen O-:"
+  |reflexivity
+  |rel_finish  (** new goal *)].
+
 (** Fork *)
 Lemma tac_rel_fork_l `{relocG Σ} K ℶ E e' eres Γ e t A :
   e = fill K (Fork e') →
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index b3689499b17a174c38e9586df34496f9f6a3bb9f..920d0c598223c869d37f5657c68ddca7f99a6ce6 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From reloc.logic.proofmode Require Export tactics.
+From reloc.logic.proofmode Require Export spec_tactics tactics.
 From iris.heap_lang Require Import lang notation.
 
 Section test.
@@ -70,24 +70,27 @@ Proof.
   rel_values.
 Qed.
 
-(* testing fork *)
+(* testing fork and store *)
 Lemma test5 l r Γ N :
   inv N (l ↦ #3) -∗
   r ↦ₛ #4 -∗
-  Γ ⊨ (let: "x" := #1 + (Fork !#l;; !#l) in "x")
-  << (Fork (#r <- #0);; !#r) : EqI.
+  Γ ⊨ (let: "x" := #1 + (Fork (#l <- #3);; !#l) in "x")
+  << (#r <- #0;; Fork (#r <- #4);; !#r) : EqI.
 Proof.
   iIntros "#IN Hr".
   rel_fork_l. iModIntro. iSplitR.
   { iNext. iInv N as "Hl" "Hcl".
-    iApply (wp_load with "Hl"). iNext. iIntros "Hl".
+    iApply (wp_store with "Hl"). iNext. iIntros "Hl".
     by iApply "Hcl". }
   iNext. rel_pure_l. rel_pure_l.
   rel_load_l. iInv N as "?" "Hcl". iModIntro. iExists _; iFrame.
   iNext. iIntros "Hl". iMod ("Hcl" with "Hl") as "_".
   repeat rel_pure_l.
+  rel_store_r. rel_pure_r. rel_pure_r.
   rel_fork_r as i "Hi".
   repeat rel_pure_r.
+  iApply refines_spec_ctx. iDestruct 1 as (?) "#?".
+  tp_store i.
   rel_load_r.
   rel_values.
 Qed.