diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 42e4e4c3109ebe06e22edf31c9e1e66156826f17..7ff16dd1523a0252c962c5547972c16765d0ce51 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -306,7 +306,9 @@ Tactic Notation "iAssumption" :=
   end.
 
 (** * False *)
-Tactic Notation "iExFalso" := apply tac_ex_falso.
+Tactic Notation "iExFalso" :=
+  iStartProof;
+  apply tac_ex_falso.
 
 (** * Making hypotheses intuitionistic or pure *)
 Local Tactic Notation "iIntuitionistic" constr(H) "as" constr(H') :=
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7ebd11da3560c6f616c69d120a05cdbda8ed2b21..9dec1daa99436b5b81803357d6dce5187183eff9 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1420,6 +1420,11 @@ Proof.
   iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
 Qed.
 
+Lemma test_iExfalso_start_proof P : 0 = 1 → ⊢ P.
+Proof.
+  intros. iExFalso. done.
+Qed.
+
 Check "test_iRevert_pure".
 Lemma test_iRevert_pure (φ : Prop) P :
   φ → (<affine> ⌜ φ ⌝ -∗ P) -∗ P.