diff --git a/_CoqProject b/_CoqProject
index 82f21fa44e3fedec5d7a9f5b7086ecd09c9a7f58..98757ebd8791e4cabbeed831805e024290f4f000 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,6 +5,7 @@ stlc/typing.v
 stlc/rules.v
 stlc/logrel.v
 stlc/fundamental.v
+stlc/soundness.v
 F_mu/lang.v
 F_mu/typing.v
 F_mu/rules.v
diff --git a/stlc/fundamental.v b/stlc/fundamental.v
index c57f5dbef570918ddd58839ae6f9aac33d7a602c..84fb0bc3c772c421d7fd5760070a5e544af1bf7e 100644
--- a/stlc/fundamental.v
+++ b/stlc/fundamental.v
@@ -31,15 +31,14 @@ Section typed_interp.
        --------------------------------------□
        (_ ∧ _)) => iSplit
   end : itauto.
-  
-  
+
   Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) constr(Hv) constr(Hp) :=
     iApply (@wp_bind _ _ _ [ctx]);
     iApply wp_impl_l;
     iSplit; [| iApply Hp; trivial]; cbn;
     eapply (@always_intro _ _ _ _);
     iIntros {v} Hv.
-              
+
   Local Ltac value_case := iApply wp_value; cbn; rewrite ?to_of_val; trivial.
 
   Lemma typed_interp Γ vs e τ :
@@ -97,4 +96,4 @@ Section typed_interp.
       iApply "Hv"; auto with itauto.
   Qed.
 
-End typed_interp.
+End typed_interp.
\ No newline at end of file
diff --git a/stlc/soundness.v b/stlc/soundness.v
new file mode 100644
index 0000000000000000000000000000000000000000..6fcdababb9ae5dd28255cf69ec6a718cb9991080
--- /dev/null
+++ b/stlc/soundness.v
@@ -0,0 +1,37 @@
+Require Import iris.proofmode.tactics.
+Require Import iris.program_logic.hoare.
+Require Import iris.program_logic.lifting.
+Require Import iris.algebra.upred_big_op.
+Require Import stlc.lang stlc.typing stlc.rules stlc.logrel stlc.fundamental.
+Require Import iris.program_logic.adequacy.
+Import uPred.
+
+Section Soundness.
+  Context {Σ : iFunctor}.
+
+  Lemma empty_env_subst e : e.[env_subst []] = e.
+    replace (env_subst []) with (ids) by reflexivity.
+    asimpl; trivial.
+  Qed.
+
+  Lemma wp_soundness e τ : typed [] e τ → True ⊢ WP e {{@interp Σ τ}}.
+  Proof.
+    iIntros {H} "".
+    rewrite -(empty_env_subst e).
+    iApply typed_interp; eauto.
+  Qed.
+
+  Theorem Soundness e τ :
+    typed [] e τ →
+    ∀ e' thp, rtc step ([e], tt) (e' :: thp, tt) →
+              ¬ reducible e' tt → is_Some (to_val e').
+  Proof.
+    intros H1 e' thp Hstp Hnr.
+    apply wp_soundness in H1.
+    edestruct(@wp_adequacy_reducible lang Σ ⊤ (interp τ) e e' (e' :: thp) tt ∅)
+      as [Ha|Ha]; eauto using cmra_unit_valid; try tauto.
+    - iIntros "H". iApply H1.
+    - constructor.
+  Qed.
+
+End Soundness.
\ No newline at end of file