diff --git a/_CoqProject b/_CoqProject
index 6c703d920a69c7e445ce15a3854fa7f79bd1dd07..e51aa80980c8fddc7478aad6e4e74b03ce3c6a4d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,3 +4,4 @@ theories/prelude/ctx_subst.v
 theories/logic/spec_ra.v
 theories/logic/spec_rules.v
 theories/logic/model.v
+theories/logic/adequacy.v
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
new file mode 100644
index 0000000000000000000000000000000000000000..7266d96fe8fc847714438b20c33ba936afe1d011
--- /dev/null
+++ b/theories/logic/adequacy.v
@@ -0,0 +1,73 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Adequacy statements for the refinement proposition *)
+From iris.algebra Require Import auth frac agree.
+From iris.base_logic.lib Require Import auth.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Export adequacy.
+From reloc.logic Require Export spec_ra model.
+
+Class relocPreG Σ := RelocPreG {
+  reloc_preG_heap :> heapPreG Σ;
+  reloc_preG_cfg  :> inG Σ (authR cfgUR)
+}.
+
+Definition relocΣ : gFunctors := #[heapΣ; authΣ cfgUR].
+Instance subG_relocPreG {Σ} : subG relocΣ Σ → relocPreG Σ.
+Proof. solve_inG. Qed.
+
+Definition pure_lty2 `{relocG Σ} (P : val → val → Prop) :=
+  Lty2 (λ v v', ⌜P v v'⌝)%I.
+
+Lemma refines_adequate Σ `{relocPreG Σ}
+  (A : ∀ `{relocG Σ}, lty2)
+  (P : val → val → Prop) e e' σ :
+  (∀ `{relocG Σ}, ∀ v v', A v v' -∗ pure_lty2 P v v') →
+  (∀ `{relocG Σ}, {⊤;∅} ⊨ e << e' : A) →
+  adequate NotStuck e σ
+    (λ v _, ∃ thp' h v', rtc erased_step ([e'], mkstate ∅ ∅) (of_val v' :: thp', h)
+            ∧ P v v').
+Proof.
+  intros HA Hlog.
+  eapply (heap_adequacy Σ _); iIntros (Hinv).
+  iMod (own_alloc (● (to_tpool [e'], ∅)
+    ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅ : gen_heapUR _ _) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
+  { apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
+  set (Hcfg := RelocG _ _ (CFGSG _ _ γc)).
+  iMod (inv_alloc specN _ (spec_inv ([e'], mkstate ∅ ∅)) with "[Hcfg1]") as "#Hcfg".
+  { iNext. iExists [e'], (mkstate ∅ ∅).
+    rewrite /= /to_gen_heap fin_maps.map_fmap_empty. eauto. }
+  iApply wp_fupd. iApply wp_wand_r.
+  iSplitL.
+  - iPoseProof (Hlog _) as "Hrel".
+    rewrite refines_eq /refines_def /spec_ctx.
+    iSpecialize ("Hrel" $! ∅ with "Hcfg []").
+    { iApply env_ltyped2_empty. }
+    rewrite !fmap_empty !subst_map_empty.
+    iApply fupd_wp.
+    iApply ("Hrel" $! 0%nat []).
+    rewrite tpool_mapsto_eq /tpool_mapsto_def. iFrame.
+  - iIntros (v).
+    iDestruct 1 as (v') "[Hj Hinterp]".
+    rewrite HA.
+    iDestruct "Hinterp" as %Hinterp.
+    iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
+    rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
+    iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
+    move: Hvalid=> /auth_valid_discrete_2
+       [/prod_included [/tpool_singleton_included Hv2 _] _].
+    destruct tp as [|? tp']; simplify_eq/=.
+    iMod ("Hclose" with "[-]") as "_".
+    { iExists (_ :: tp'), σ'. eauto. }
+    iIntros "!> !%"; eauto.
+Qed.
+
+Theorem refines_typesafety Σ `{relocPreG Σ} e e' e1
+        (A : ∀ `{relocG Σ}, lty2) thp σ σ' :
+  (∀ `{relocG Σ}, {⊤;∅} ⊨ e << e' : A) →
+  rtc erased_step ([e], σ) (thp, σ') → e1 ∈ thp →
+  is_Some (to_val e1) ∨ reducible e1 σ'.
+Proof.
+  intros Hlog ??.
+  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], mkstate ∅ ∅) (of_val v' :: thp', h) ∧ True)); first (intros [_ ?]; eauto).
+  eapply (refines_adequate _ A) ; eauto.
+Qed.
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 246579954e69aab65181beba777d25c13bf0669b..6c8e3ee288c9f2a34c1dfab19a788a5e8ea6be25 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -10,7 +10,7 @@ From iris.heap_lang Require Import notation proofmode.
 From reloc Require Import logic.spec_rules prelude.ctx_subst.
 
 (** Semantic intepretation of types *)
-Record lty2 `{relocG Σ} := Lty2 {
+Record lty2 `{invG Σ} := Lty2 {
   lty2_car :> val → val → iProp Σ;
   lty2_persistent v1 v2 : Persistent (lty2_car v1 v2)
 }.