diff --git a/_CoqProject b/_CoqProject
index 861ba66eb382881b916d554b23c6901e150f819c..a26b5ebabdd25fd54f089dcb33e2bff2bd72773f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -87,6 +87,7 @@ heap_lang/spawn.v
 heap_lang/par.v
 heap_lang/tests.v
 heap_lang/substitution.v
+heap_lang/assert.v
 barrier/barrier.v
 barrier/specification.v
 barrier/protocol.v
diff --git a/heap_lang/assert.v b/heap_lang/assert.v
new file mode 100644
index 0000000000000000000000000000000000000000..705282b5d4040c3d87ff4ad061c5f9633909db37
--- /dev/null
+++ b/heap_lang/assert.v
@@ -0,0 +1,23 @@
+From iris.heap_lang Require Export derived.
+From iris.heap_lang Require Import wp_tactics substitution notation.
+
+Definition Assert {X} (e : expr X) : expr X :=
+  if: e then #() else #0 #0. (* #0 #0 is unsafe *)
+
+Instance do_wsubst_assert {X Y} x es (H : X `included` x :: Y) e er :
+  WSubst x es H e er → WSubst x es H (Assert e) (Assert er) | 1.
+Proof. intros; red. by rewrite /Assert /wsubst -/wsubst; f_equal/=. Qed.
+Instance do_wexpr_assert {X Y} (H : X `included` Y) e er :
+  WExpr H e er → WExpr H (Assert e) (Assert er) | 1.
+Proof. intros; red. by rewrite /Assert /wexpr -/wexpr; f_equal/=. Qed.
+
+Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) :
+  ▷ Φ #() ⊢ WP Assert #true {{ Φ }}.
+Proof. by rewrite -wp_if_true -wp_value. Qed.
+
+Lemma wp_assert' {Σ} (Φ : val → iProp heap_lang Σ) e :
+  WP e {{ λ v, v = #true ∧ ▷ Φ #() }} ⊢ WP Assert e {{ Φ }}.
+Proof.
+  rewrite /Assert. wp_focus e; apply wp_mono=>v.
+  apply uPred.const_elim_l=>->. apply wp_assert.
+Qed.