diff --git a/pulse/src/checker/Pulse.Checker.If.fst b/pulse/src/checker/Pulse.Checker.If.fst
index c1337896c91..8a559bb46df 100644
--- a/pulse/src/checker/Pulse.Checker.If.fst
+++ b/pulse/src/checker/Pulse.Checker.If.fst
@@ -24,6 +24,7 @@ open Pulse.Checker.Base
 
 module T = FStar.Tactics.V2
 module J = Pulse.JoinComp
+module RU = Pulse.RuntimeUtils
 #set-options "--z3rlimit 40"
 
 
@@ -66,6 +67,7 @@ let check
   let check_branch (eq_v:term) (br:st_term) (is_then:bool)
   : T.Tac (checker_result_t (g_with_eq eq_v) pre post_hint)
   =
+    let branch_range = br.range in
     let br =
       let t =
         mk_term (Tm_ProofHintWithBinders {
@@ -78,7 +80,8 @@ let check
     in
 
     let ppname = mk_ppname_no_range "_if_br" in
-    let r = check (g_with_eq eq_v) pre post_hint ppname br in
+    let r = RU.with_error_bound branch_range (fun () ->
+      check (g_with_eq eq_v) pre post_hint ppname br) in
     r
   in
 
diff --git a/pulse/src/checker/Pulse.Checker.Prover.fst b/pulse/src/checker/Pulse.Checker.Prover.fst
index 8e0577f7d4e..0f057cb1a2a 100644
--- a/pulse/src/checker/Pulse.Checker.Prover.fst
+++ b/pulse/src/checker/Pulse.Checker.Prover.fst
@@ -377,6 +377,13 @@ let pure_eq_unif (g: env) (p: term) skip_eq_uvar : Dv bool =
     )
   | None -> false
 
+// Restore a previously-captured error_range_bound around a thunk.
+let with_saved_bound (saved_bound: option Range.range) (f: unit -> T.Tac 'a)
+  : T.Tac 'a =
+  match saved_bound with
+  | Some r -> RU.with_error_bound r f
+  | None -> f ()
+
 // skip_eq_uvar to support (assert foo. with pure (foo == ....))
 let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slprop_view) :
     T.Tac (option (prover_result g ctxt [goal])) =
@@ -387,9 +394,13 @@ let prove_pure (g: env) (ctxt: list slprop_view) (skip_eq_uvar: bool) (goal: slp
     if pure_eq_unif g p skip_eq_uvar then None else begin
     debug_prover g (fun _ -> Printf.sprintf "prove_pure p=%s success" (show p));
 
+    let saved_bound = RU.get_error_bound () in
     Some (| g, ctxt, [], [], fun g'' ->
  // implied by t2_typing
-      let pv = check_prop_validity g'' p in
+      // Restore the error bound that was active when this pure goal was matched.
+      // This closure is evaluated lazily (via cont_elab_thunk) after the
+      // original with_error_bound scope has exited.
+      let pv = with_saved_bound saved_bound (fun () -> check_prop_validity g'' p) in
       cont_elab_refl g ctxt ([] @ ctxt),
       (fun frame ->
 
@@ -424,12 +435,16 @@ let prove_with_pure (g: env) (ctxt: list slprop_view) skip_eq_uvar (goal: slprop
   | WithPure p n v ->
     if pure_eq_unif g p skip_eq_uvar then None else
 
+    let saved_bound = RU.get_error_bound () in
     Some (| g, ctxt, [Unknown v], [], fun g'' ->
       cont_elab_refl g ctxt ([] @ ctxt),
       (fun frame ->
 
 
-        k_elab_equiv (elab_slprops (frame @ [Unknown v] @ [])) (elab_slprops (frame @ [goal])) (intro_with_pure g'' (elab_slprops frame) p n v))
+        k_elab_equiv (elab_slprops (frame @ [Unknown v] @ [])) (elab_slprops (frame @ [goal]))
+          (fun post t ->
+            with_saved_bound saved_bound
+              (fun () -> intro_with_pure g'' (elab_slprops frame) p n v post t)))
       <: T.Tac _ |)
   | _ -> None
 
@@ -927,13 +942,18 @@ let prove_atom_result (g: env)
     T.Tac (prover_result g ctxt0 [goal]) =
   let Atom _ dup _ _ = ctxt in
   let goal = elab_slprop goal in
+  let saved_bound = RU.get_error_bound () in
   (| g, (if dup then rest_ctxt@[ctxt] else rest_ctxt), [], [ctxt], fun g' ->
-    let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
-    (if dup then
-      // Check that we can indeed synthesize a duplicable instance
-      ignore (compute_term_type g
-        (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
-          [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit])));
+    // Restore the error bound that was active when this atom was matched.
+    // This closure is evaluated lazily (via cont_elab_thunk) after the
+    // original with_error_bound scope has exited.
+    with_saved_bound saved_bound (fun () ->
+      let _ = check_slprop_equiv_ext (RU.range_of_term goal) g (elab_slprop ctxt) goal in
+      (if dup then
+        // Check that we can indeed synthesize a duplicable instance
+        ignore (compute_term_type g
+          (R.mk_app (R.pack_ln (R.Tv_FVar (R.pack_fv dup_lid)))
+            [elab_slprop ctxt, R.Q_Explicit; unit_const, R.Q_Explicit]))));
     cont_elab_refl _ _ _, cont_elab_refl _ _ _ <: T.Tac _ |)
 
 // this matches atoms when they're the only unifiable pair
diff --git a/pulse/src/checker/Pulse.RuntimeUtils.fsti b/pulse/src/checker/Pulse.RuntimeUtils.fsti
index 239fb7d3510..8fd039d1a69 100644
--- a/pulse/src/checker/Pulse.RuntimeUtils.fsti
+++ b/pulse/src/checker/Pulse.RuntimeUtils.fsti
@@ -23,6 +23,7 @@ type context = FStar.Sealed.Inhabited.sealed #(list (string & option range)) []
 val extend_context (tag:string) (r:option range) (ctx:context) : context
 val with_context (c:context) (f:unit -> T.Tac 'a) : T.Tac 'a
 val with_error_bound (r:Range.range) (f:unit -> T.Tac 'a) : T.Tac 'a
+val get_error_bound (_:unit) : T.Tac (option Range.range)
 val with_extv (k v : string) (f:unit -> T.Tac 'a) : T.Tac 'a
 val print_context (c:context) : T.Tac string
 val debug_at_level_no_module (s:string) : bool
diff --git a/pulse/src/ml/Pulse_RuntimeUtils.ml b/pulse/src/ml/Pulse_RuntimeUtils.ml
index b253121f5cf..33cea324835 100644
--- a/pulse/src/ml/Pulse_RuntimeUtils.ml
+++ b/pulse/src/ml/Pulse_RuntimeUtils.ml
@@ -22,6 +22,9 @@ let rec with_context (c:context) (f: unit -> 'a utac) : 'a utac =
 let with_error_bound (r:FStarC_Range.range) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     FStarC_Errors.with_error_bound r (fun _ -> f () ps)
+let get_error_bound () : FStarC_Range.range option utac =
+  fun _ps ->
+    FStarC_Effect.op_Bang FStarC_Errors.error_range_bound
 let with_extv (k:string) (v:string) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
     let open FStarC_Options_Ext in
diff --git a/pulse/src/ml/pulseparser.mly b/pulse/src/ml/pulseparser.mly
index 2ebd859adc6..3c88a10aae6 100644
--- a/pulse/src/ml/pulseparser.mly
+++ b/pulse/src/ml/pulseparser.mly
@@ -328,17 +328,25 @@ pulseStmtNoSeq:
     { PulseSyntaxExtension_Sugar.mk_while tm inv body }
   | INTRO p=pulseSLProp WITH ws=nonempty_list(indexingTerm)
     { PulseSyntaxExtension_Sugar.mk_intro p ws }
-  | bs=withBindersOpt REWRITE body=rewriteBody
-    {
-        PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body bs
-    }
-  | bs=withBindersOpt ASSERT p=pulseSLProp
+  | REWRITE body=rewriteBody
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body [] }
+  | bs=withBinders REWRITE body=rewriteBody
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders body bs }
+  | ASSERT p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSERT p) [] }
+  | bs=withBinders ASSERT p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSERT p) bs }
-  | bs=withBindersOpt ASSUME p=pulseSLProp
+  | ASSUME p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSUME p) [] }
+  | bs=withBinders ASSUME p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (ASSUME p) bs }
-  | bs=withBindersOpt UNFOLD ns=optionalNames p=pulseSLProp
+  | UNFOLD ns=optionalNames p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (UNFOLD (ns,p)) [] }
+  | bs=withBinders UNFOLD ns=optionalNames p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (UNFOLD (ns,p)) bs }
-  | bs=withBindersOpt FOLD ns=optionalNames p=pulseSLProp
+  | FOLD ns=optionalNames p=pulseSLProp
+    { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (FOLD (ns,p)) [] }
+  | bs=withBinders FOLD ns=optionalNames p=pulseSLProp
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders (FOLD (ns,p)) bs }
   | bs=withBinders UNDERSCORE
     { PulseSyntaxExtension_Sugar.mk_proof_hint_with_binders WILD bs }
@@ -410,11 +418,6 @@ withBinders:
   | WITH bs=nonempty_list(multiBinder) DOT
     { List.flatten bs }
 
-withBindersOpt:
-  | w=withBinders
-    { w }
-  | { [] }
-
 ensuresSLProp:
   | ret=option(RETURNS i=lidentOrUnderscore COLON r=term { (i, r) }) ENSURES s=pulseSLProp maybe_opens=option(OPENS inv=appTermNoRecordExp { inv })
     { ret, s, maybe_opens }
diff --git a/pulse/test/Makefile b/pulse/test/Makefile
index 75801ab213c..7e94564022d 100644
--- a/pulse/test/Makefile
+++ b/pulse/test/Makefile
@@ -1,4 +1,5 @@
 SUBDIRS += bug-reports
+SUBDIRS += error_messages
 SUBDIRS += nolib
 SUBDIRS += pool
 
diff --git a/pulse/test/bug-reports/Bug267.fst.output.expected b/pulse/test/bug-reports/Bug267.fst.output.expected
index da251fb87ba..cadbc3c3233 100644
--- a/pulse/test/bug-reports/Bug267.fst.output.expected
+++ b/pulse/test/bug-reports/Bug267.fst.output.expected
@@ -21,7 +21,7 @@
   - Also see: Prims.fst(165,27-165,38)
   - See also Bug267.fst(58,4-58,8)
 
-* Info at Bug267.fst(62,53-63,17):
+* Info at Bug267.fst(63,2-63,17):
   - Expected failure:
   - Tactic failed
   - Cannot prove:
diff --git a/pulse/test/bug-reports/IntroGhost.fst.output.expected b/pulse/test/bug-reports/IntroGhost.fst.output.expected
index f149f0fa0d8..7c23a672481 100644
--- a/pulse/test/bug-reports/IntroGhost.fst.output.expected
+++ b/pulse/test/bug-reports/IntroGhost.fst.output.expected
@@ -6,7 +6,7 @@
   - In the context:
       my_inv _b5 r
 
-* Info at IntroGhost.fst(84,46-87,24):
+* Info at IntroGhost.fst(87,2-87,24):
   - Expected failure:
   - Tactic failed
   - Cannot prove:
diff --git a/pulse/test/error_messages/AssertExtraContext.fst b/pulse/test/error_messages/AssertExtraContext.fst
new file mode 100644
index 00000000000..9f465bc8345
--- /dev/null
+++ b/pulse/test/error_messages/AssertExtraContext.fst
@@ -0,0 +1,13 @@
+module AssertExtraContext
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Assert with binders where the witness is wrong
+[@@expect_failure [19]]
+fn assert_extra (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0
+{
+  with v. assert (pts_to r v ** pure (v > 0));
+  ()
+}
diff --git a/pulse/test/error_messages/AssertExtraContext.fst.output.expected b/pulse/test/error_messages/AssertExtraContext.fst.output.expected
new file mode 100644
index 00000000000..0a8afa3a419
--- /dev/null
+++ b/pulse/test/error_messages/AssertExtraContext.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at AssertExtraContext.fst(11,7-11,43):
+  - Expected failure:
+  - Failed to prove pure property: 0 > 0
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+
diff --git a/pulse/test/error_messages/AtomicMismatch.fst b/pulse/test/error_messages/AtomicMismatch.fst
new file mode 100644
index 00000000000..180ffba57f8
--- /dev/null
+++ b/pulse/test/error_messages/AtomicMismatch.fst
@@ -0,0 +1,14 @@
+module AtomicMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Using non-atomic operation in atomic context
+[@@expect_failure [228]]
+atomic
+fn atomic_fn (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 1;  // Might error if := is not atomic-compatible
+  ()
+}
diff --git a/pulse/test/error_messages/AtomicMismatch.fst.output.expected b/pulse/test/error_messages/AtomicMismatch.fst.output.expected
new file mode 100644
index 00000000000..5f74508d7a5
--- /dev/null
+++ b/pulse/test/error_messages/AtomicMismatch.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at AtomicMismatch.fst(12,2-12,8):
+  - Expected failure:
+  - Tactic failed
+  - Cannot compose computations in this atomic block:
+  - This computation has effect: stt
+  - The continuation has effect: stt_atomic emp_inames
+
diff --git a/pulse/test/error_messages/BindTypeMismatch.fst b/pulse/test/error_messages/BindTypeMismatch.fst
new file mode 100644
index 00000000000..2f4db729d11
--- /dev/null
+++ b/pulse/test/error_messages/BindTypeMismatch.fst
@@ -0,0 +1,21 @@
+module BindTypeMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Binding with wrong type annotation
+fn helper ()
+  requires emp
+  returns r: int
+  ensures emp
+{
+  42
+}
+
+[@@expect_failure [228]]
+fn bind_type_err ()
+  requires emp
+  ensures emp
+{
+  let x : bool = helper ();  // ERROR: helper returns int, binding expects bool
+  ()
+}
diff --git a/pulse/test/error_messages/BindTypeMismatch.fst.output.expected b/pulse/test/error_messages/BindTypeMismatch.fst.output.expected
new file mode 100644
index 00000000000..53c3982e064
--- /dev/null
+++ b/pulse/test/error_messages/BindTypeMismatch.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at BindTypeMismatch.fst(19,17-19,26):
+  - Expected failure:
+  - Tactic failed
+  - Type mismatch (NB: this is a syntactic check)
+  - Expected: bool
+  - Got: int
+
diff --git a/pulse/test/error_messages/ClosureError.fst b/pulse/test/error_messages/ClosureError.fst
new file mode 100644
index 00000000000..2d9e0515a2f
--- /dev/null
+++ b/pulse/test/error_messages/ClosureError.fst
@@ -0,0 +1,19 @@
+module ClosureError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error in a local function definition
+[@@expect_failure [19]]
+fn closure_error (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0
+{
+  fn helper ()
+    requires pts_to r 1  // ERROR: pre says r==1 but caller has r==0
+    ensures pts_to r 1
+  {
+    ()
+  };
+  helper ();
+  ()
+}
diff --git a/pulse/test/error_messages/ClosureError.fst.output.expected b/pulse/test/error_messages/ClosureError.fst.output.expected
new file mode 100644
index 00000000000..07273a8c66f
--- /dev/null
+++ b/pulse/test/error_messages/ClosureError.fst.output.expected
@@ -0,0 +1,18 @@
+* Info at ClosureError.fst(17,2-17,8):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 0
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int)
+      (helper
+        :
+        _: Prims.unit
+          -> fn
+               requires Pulse.Class.PtsTo.pts_to r 1
+               ensures Pulse.Class.PtsTo.pts_to r 1)
+  - VC = Pulse.Lib.Reference.pts_to r 0 == Pulse.Lib.Reference.pts_to r 1
+  - See also ClosureError.fst(17,2-18,4)
+
diff --git a/pulse/test/error_messages/DuplicateResource.fst b/pulse/test/error_messages/DuplicateResource.fst
new file mode 100644
index 00000000000..2786df4f07e
--- /dev/null
+++ b/pulse/test/error_messages/DuplicateResource.fst
@@ -0,0 +1,12 @@
+module DuplicateResource
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Trying to read a ref twice without proper framing
+[@@expect_failure [228]]
+fn dup_fail (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0 ** pts_to r 0
+{
+  ()
+}
diff --git a/pulse/test/error_messages/DuplicateResource.fst.output.expected b/pulse/test/error_messages/DuplicateResource.fst.output.expected
new file mode 100644
index 00000000000..dcd948ca3c4
--- /dev/null
+++ b/pulse/test/error_messages/DuplicateResource.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at DuplicateResource.fst(11,2-11,4):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      Pulse.Lib.Reference.pts_to r 0
+  - In the context:
+
+
diff --git a/pulse/test/error_messages/ExistsIntro.fst b/pulse/test/error_messages/ExistsIntro.fst
new file mode 100644
index 00000000000..0312943156a
--- /dev/null
+++ b/pulse/test/error_messages/ExistsIntro.fst
@@ -0,0 +1,13 @@
+module ExistsIntro
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Postcondition requires existential that can't be satisfied
+[@@expect_failure [19]]
+fn exists_intro_fail (r: ref int)
+  requires pts_to r 5
+  ensures exists* v. pts_to r v ** pure (v > 10)
+{
+  // ERROR: after body, we have pts_to r 5 but need v > 10
+  ()
+}
diff --git a/pulse/test/error_messages/ExistsIntro.fst.output.expected b/pulse/test/error_messages/ExistsIntro.fst.output.expected
new file mode 100644
index 00000000000..bd00eac2064
--- /dev/null
+++ b/pulse/test/error_messages/ExistsIntro.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at ExistsIntro.fst(12,2-12,4):
+  - Expected failure:
+  - Failed to prove pure property: 5 > 10
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+
diff --git a/pulse/test/error_messages/FailAssertion.fst b/pulse/test/error_messages/FailAssertion.fst
new file mode 100644
index 00000000000..8e2b99667d4
--- /dev/null
+++ b/pulse/test/error_messages/FailAssertion.fst
@@ -0,0 +1,13 @@
+module FailAssertion
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Failing assertion: error should point to the assert line
+[@@expect_failure [228]]
+fn test_fail_assert (x: int)
+  requires emp
+  ensures emp
+{
+  assert (x > 0);
+  ()
+}
diff --git a/pulse/test/error_messages/FailAssertion.fst.output.expected b/pulse/test/error_messages/FailAssertion.fst.output.expected
new file mode 100644
index 00000000000..94eba16a291
--- /dev/null
+++ b/pulse/test/error_messages/FailAssertion.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at FailAssertion.fst(11,2-11,16):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      x > 0
+  - In the context:
+
+
diff --git a/pulse/test/error_messages/FoldError.fst b/pulse/test/error_messages/FoldError.fst
new file mode 100644
index 00000000000..de718f264b5
--- /dev/null
+++ b/pulse/test/error_messages/FoldError.fst
@@ -0,0 +1,15 @@
+module FoldError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+let my_inv (r: ref int) (v: int) : slprop = pts_to r v ** pure (v >= 0)
+
+// Trying to fold with mismatched context
+[@@expect_failure [19]]
+fn fold_fail (r: ref int)
+  requires pts_to r (-1)
+  ensures my_inv r (-1)
+{
+  fold (my_inv r (-1));  // ERROR: pure (v >= 0) not satisfiable with v = -1
+  ()
+}
diff --git a/pulse/test/error_messages/FoldError.fst.output.expected b/pulse/test/error_messages/FoldError.fst.output.expected
new file mode 100644
index 00000000000..13c45e6a690
--- /dev/null
+++ b/pulse/test/error_messages/FoldError.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at FoldError.fst(13,2-13,22):
+  - Expected failure:
+  - Failed to prove pure property: false
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+
diff --git a/pulse/test/error_messages/FramingFailure.fst b/pulse/test/error_messages/FramingFailure.fst
new file mode 100644
index 00000000000..63db1c6fe43
--- /dev/null
+++ b/pulse/test/error_messages/FramingFailure.fst
@@ -0,0 +1,14 @@
+module FramingFailure
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Framing failure: trying to use a resource that isn't in scope
+[@@expect_failure [228]]
+fn framing_fail (r1 r2: ref int)
+  requires pts_to r1 0
+  ensures pts_to r1 1
+{
+  let v = !r2;
+  r1 := 1;
+  ()
+}
diff --git a/pulse/test/error_messages/FramingFailure.fst.output.expected b/pulse/test/error_messages/FramingFailure.fst.output.expected
new file mode 100644
index 00000000000..1b5ec8f2002
--- /dev/null
+++ b/pulse/test/error_messages/FramingFailure.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at FramingFailure.fst(11,10-11,13):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      Pulse.Lib.Reference.pts_to r2 (*?u298*)_
+  - In the context:
+      Pulse.Lib.Reference.pts_to r1 0
+
diff --git a/pulse/test/error_messages/GhostEffect.fst b/pulse/test/error_messages/GhostEffect.fst
new file mode 100644
index 00000000000..ab6c7dd1c7d
--- /dev/null
+++ b/pulse/test/error_messages/GhostEffect.fst
@@ -0,0 +1,23 @@
+module GhostEffect
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Using a ghost value in a total computation
+ghost
+fn ghost_fn ()
+  requires emp
+  returns r: int
+  ensures emp
+{
+  42
+}
+
+[@@expect_failure [228]]
+fn non_ghost_caller ()
+  requires emp
+  returns r: int
+  ensures emp
+{
+  let x = ghost_fn ();  // ERROR: ghost in non-ghost context
+  x
+}
diff --git a/pulse/test/error_messages/GhostEffect.fst.output.expected b/pulse/test/error_messages/GhostEffect.fst.output.expected
new file mode 100644
index 00000000000..0e72edd1110
--- /dev/null
+++ b/pulse/test/error_messages/GhostEffect.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at GhostEffect.fst(21,10-21,18):
+  - Expected failure:
+  - Tactic failed
+  - Expected a term with a non-informative (e.g., erased) type.
+  - Got: int
+  - See also GhostEffect.fst(20,1-22,3)
+
diff --git a/pulse/test/error_messages/IfBranchMismatch.fst b/pulse/test/error_messages/IfBranchMismatch.fst
new file mode 100644
index 00000000000..513441a2e21
--- /dev/null
+++ b/pulse/test/error_messages/IfBranchMismatch.fst
@@ -0,0 +1,32 @@
+module IfBranchMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// If branches produce different resources
+[@@expect_failure [19]]
+fn if_branch_mismatch (r: ref int) (b: bool)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  if b {
+    r := 1;
+  } else {
+    r := 2; // ERROR: this branch gives pts_to r 2, should be 1
+  }
+}
+
+
+
+// If branches produce different resources
+[@@expect_failure [19]]
+fn if_branch_mismatch_localized (r: ref int) (b: bool)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  if b {
+    r := 1;
+  } else {
+    r := 2;
+    () // ERROR: this branch gives pts_to r 2, should be 1
+  }
+}
diff --git a/pulse/test/error_messages/IfBranchMismatch.fst.output.expected b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
new file mode 100644
index 00000000000..31b0b93dd8d
--- /dev/null
+++ b/pulse/test/error_messages/IfBranchMismatch.fst.output.expected
@@ -0,0 +1,27 @@
+* Info at IfBranchMismatch.fst(14,4-14,8):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (b : Prims.bool)
+      (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false))
+      (_if_br : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+  - See also IfBranchMismatch.fst(14,4-14,10)
+
+* Info at IfBranchMismatch.fst(30,4-30,6):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (b : Prims.bool)
+      (_if_hyp : Prims.squash (Pulse.Lib.Core.rewrites_to_p b false))
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+
diff --git a/pulse/test/error_messages/IfCondType.fst b/pulse/test/error_messages/IfCondType.fst
new file mode 100644
index 00000000000..0827bb803db
--- /dev/null
+++ b/pulse/test/error_messages/IfCondType.fst
@@ -0,0 +1,13 @@
+module IfCondType
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// If condition that's not a bool
+[@@expect_failure [189]]
+fn bad_if_cond (x: int)
+  requires emp
+  ensures emp
+{
+  if x { () } else { () };
+  ()
+}
diff --git a/pulse/test/error_messages/IfCondType.fst.output.expected b/pulse/test/error_messages/IfCondType.fst.output.expected
new file mode 100644
index 00000000000..f23551408e3
--- /dev/null
+++ b/pulse/test/error_messages/IfCondType.fst.output.expected
@@ -0,0 +1,4 @@
+* Info at IfCondType.fst(11,5-11,6):
+  - Expected failure:
+  - Expected expression of type Prims.bool got expression x of type Prims.int
+
diff --git a/pulse/test/error_messages/IllTypedInvariant.fst b/pulse/test/error_messages/IllTypedInvariant.fst
new file mode 100644
index 00000000000..e8d6ad66d24
--- /dev/null
+++ b/pulse/test/error_messages/IllTypedInvariant.fst
@@ -0,0 +1,17 @@
+module IllTypedInvariant
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// While loop with invariant that can't be established initially
+[@@expect_failure [19]]
+fn bad_invariant ()
+  requires emp
+  ensures emp
+{
+  let mut i = 0;
+  while (!i < 10)
+  invariant pure (!i >= 0 /\ !i <= 10 /\ 1 = 2)
+  {
+    i := !i + 1;
+  }
+}
diff --git a/pulse/test/error_messages/IllTypedInvariant.fst.output.expected b/pulse/test/error_messages/IllTypedInvariant.fst.output.expected
new file mode 100644
index 00000000000..d8db94a3ccc
--- /dev/null
+++ b/pulse/test/error_messages/IllTypedInvariant.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at IllTypedInvariant.fst(13,43-13,44):
+  - Expected failure:
+  - Failed to prove pure property: true /\ true /\ false
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (uu___0 : Prims.unit) (i : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+
diff --git a/pulse/test/error_messages/IllTypedSpec.fst b/pulse/test/error_messages/IllTypedSpec.fst
new file mode 100644
index 00000000000..8e7343695a7
--- /dev/null
+++ b/pulse/test/error_messages/IllTypedSpec.fst
@@ -0,0 +1,12 @@
+module IllTypedSpec
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Ill-typed precondition: using an int where a vprop is expected
+[@@expect_failure [189]]
+fn bad_precondition (x: int)
+  requires x
+  ensures emp
+{
+  ()
+}
diff --git a/pulse/test/error_messages/IllTypedSpec.fst.output.expected b/pulse/test/error_messages/IllTypedSpec.fst.output.expected
new file mode 100644
index 00000000000..abf5dd155f5
--- /dev/null
+++ b/pulse/test/error_messages/IllTypedSpec.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at IllTypedSpec.fst(8,11-8,12):
+  - Expected failure:
+  - Ill-typed term
+  - Expected expression of type Pulse.Lib.Core.slprop
+    got expression x
+    of type Prims.int
+
diff --git a/pulse/test/error_messages/IntroExistsFail.fst b/pulse/test/error_messages/IntroExistsFail.fst
new file mode 100644
index 00000000000..ec666d16d6a
--- /dev/null
+++ b/pulse/test/error_messages/IntroExistsFail.fst
@@ -0,0 +1,12 @@
+module IntroExistsFail
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Existential introduction with wrong witness
+[@@expect_failure [19]]
+fn intro_exists_fail (r: ref int)
+  requires pts_to r 0
+  ensures (exists* v. pts_to r v ** pure (v > 0))
+{
+  ()  // ERROR: can't prove exists* v. pts_to r v ** pure (v > 0)
+}
diff --git a/pulse/test/error_messages/IntroExistsFail.fst.output.expected b/pulse/test/error_messages/IntroExistsFail.fst.output.expected
new file mode 100644
index 00000000000..b2dd425914b
--- /dev/null
+++ b/pulse/test/error_messages/IntroExistsFail.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at IntroExistsFail.fst(11,2-11,4):
+  - Expected failure:
+  - Failed to prove pure property: 0 > 0
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+
diff --git a/pulse/test/error_messages/InvariantPayload.fst b/pulse/test/error_messages/InvariantPayload.fst
new file mode 100644
index 00000000000..fd969bd5137
--- /dev/null
+++ b/pulse/test/error_messages/InvariantPayload.fst
@@ -0,0 +1,15 @@
+module InvariantPayload
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Fold/unfold invariant with wrong payload
+let my_pred (r: ref int) : slprop = exists* v. pts_to r v ** pure (v > 0)
+
+[@@expect_failure [19]]
+fn inv_payload_fail (r: ref int)
+  requires pts_to r 0
+  ensures my_pred r
+{
+  fold my_pred r;  // ERROR: can't prove v > 0 with v = 0
+  ()
+}
diff --git a/pulse/test/error_messages/InvariantPayload.fst.output.expected b/pulse/test/error_messages/InvariantPayload.fst.output.expected
new file mode 100644
index 00000000000..ebca7a8c6ed
--- /dev/null
+++ b/pulse/test/error_messages/InvariantPayload.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at InvariantPayload.fst(13,2-13,16):
+  - Expected failure:
+  - Failed to prove pure property: 0 > 0
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Prims.l_False
+
diff --git a/pulse/test/error_messages/LambdaArg.fst b/pulse/test/error_messages/LambdaArg.fst
new file mode 100644
index 00000000000..6a11da31b95
--- /dev/null
+++ b/pulse/test/error_messages/LambdaArg.fst
@@ -0,0 +1,20 @@
+module LambdaArg
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Passing wrong number of arguments
+fn takes_two (x y: int)
+  requires emp
+  ensures emp
+{
+  ()
+}
+
+[@@expect_failure [71]]
+fn wrong_args ()
+  requires emp
+  ensures emp
+{
+  takes_two 1 2 3;  // ERROR: too many arguments
+  ()
+}
diff --git a/pulse/test/error_messages/LambdaArg.fst.output.expected b/pulse/test/error_messages/LambdaArg.fst.output.expected
new file mode 100644
index 00000000000..207e48596b7
--- /dev/null
+++ b/pulse/test/error_messages/LambdaArg.fst.output.expected
@@ -0,0 +1,9 @@
+* Info at LambdaArg.fst(18,2-18,11):
+  - Expected failure:
+  - Ill-typed term
+  - Expected a function.
+  - Got an expression of type:
+      fn
+        requires Pulse.Lib.Core.emp
+        ensures Pulse.Lib.Core.emp
+
diff --git a/pulse/test/error_messages/LeftoverResources.fst b/pulse/test/error_messages/LeftoverResources.fst
new file mode 100644
index 00000000000..f0dcb78a8ff
--- /dev/null
+++ b/pulse/test/error_messages/LeftoverResources.fst
@@ -0,0 +1,12 @@
+module LeftoverResources
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Leftover resources: postcondition doesn't consume everything
+[@@expect_failure [228]]
+fn leftover (r s: ref int)
+  requires pts_to r 0 ** pts_to s 0
+  ensures pts_to r 0
+{
+  ()  // ERROR: pts_to s 0 is leftover
+}
diff --git a/pulse/test/error_messages/LeftoverResources.fst.output.expected b/pulse/test/error_messages/LeftoverResources.fst.output.expected
new file mode 100644
index 00000000000..bb81b192c59
--- /dev/null
+++ b/pulse/test/error_messages/LeftoverResources.fst.output.expected
@@ -0,0 +1,6 @@
+* Info at LeftoverResources.fst(11,2-11,4):
+  - Expected failure:
+  - Tactic failed
+  - Leftover resources: Pulse.Lib.Reference.pts_to s 0
+  - Did you forget to free these resources?
+
diff --git a/pulse/test/error_messages/LetBindingType.fst b/pulse/test/error_messages/LetBindingType.fst
new file mode 100644
index 00000000000..38b15cbae16
--- /dev/null
+++ b/pulse/test/error_messages/LetBindingType.fst
@@ -0,0 +1,13 @@
+module LetBindingType
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Let binding with wrong type annotation
+[@@expect_failure [189]]
+fn let_binding_type ()
+  requires emp
+  ensures emp
+{
+  let x : bool = 42;
+  ()
+}
diff --git a/pulse/test/error_messages/LetBindingType.fst.output.expected b/pulse/test/error_messages/LetBindingType.fst.output.expected
new file mode 100644
index 00000000000..b33839f105b
--- /dev/null
+++ b/pulse/test/error_messages/LetBindingType.fst.output.expected
@@ -0,0 +1,4 @@
+* Info at LetBindingType.fst(11,17-11,19):
+  - Expected failure:
+  - Expected expression of type Prims.bool got expression 42 of type Prims.int
+
diff --git a/pulse/test/error_messages/Makefile b/pulse/test/error_messages/Makefile
new file mode 100644
index 00000000000..d66d3cb5549
--- /dev/null
+++ b/pulse/test/error_messages/Makefile
@@ -0,0 +1,15 @@
+PULSE_ROOT ?= ../..
+include $(PULSE_ROOT)/mk/test.mk
+
+# Ensure output directories exist
+$(shell mkdir -p _output _cache)
+
+# Suppress warnings that add noise to expected output
+OTHERFLAGS+=--warn_error -241-247-333-274-152-285
+
+# Remove --query_stats and --hint_info since they output timing info
+OTHERFLAGS := $(filter-out --query_stats, $(OTHERFLAGS))
+OTHERFLAGS := $(filter-out --hint_info, $(OTHERFLAGS))
+
+# Strip absolute paths for reproducibility
+OTHERFLAGS += --ext fstar:no_absolute_paths
diff --git a/pulse/test/error_messages/MatchBranchMismatch.fst b/pulse/test/error_messages/MatchBranchMismatch.fst
new file mode 100644
index 00000000000..f2ad66f6a4e
--- /dev/null
+++ b/pulse/test/error_messages/MatchBranchMismatch.fst
@@ -0,0 +1,16 @@
+module MatchBranchMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Match branch postcondition mismatch - error should point to offending branch
+[@@expect_failure [19]]
+fn match_error (r: ref int) (x: int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  match x {
+    0 -> { r := 1 }
+    1 -> { r := 2 }
+    _ -> { r := 1 }
+  }
+}
diff --git a/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
new file mode 100644
index 00000000000..6398b24e0a4
--- /dev/null
+++ b/pulse/test/error_messages/MatchBranchMismatch.fst.output.expected
@@ -0,0 +1,13 @@
+* Info at MatchBranchMismatch.fst(13,11-13,15):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (x : Prims.int)
+      (branch equality : Prims.squash (x == 1)) (_br : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+  - See also MatchBranchMismatch.fst(13,11-13,17)
+
diff --git a/pulse/test/error_messages/MissingPost.fst b/pulse/test/error_messages/MissingPost.fst
new file mode 100644
index 00000000000..10008290cc4
--- /dev/null
+++ b/pulse/test/error_messages/MissingPost.fst
@@ -0,0 +1,13 @@
+module MissingPost
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Function allocates but doesn't return it in post
+[@@expect_failure [228]]
+fn missing_post (r: ref int)
+  requires pts_to r 0
+  ensures emp
+{
+  r := 1;
+  ()  // ERROR: pts_to r 1 is leftover, post says emp
+}
diff --git a/pulse/test/error_messages/MissingPost.fst.output.expected b/pulse/test/error_messages/MissingPost.fst.output.expected
new file mode 100644
index 00000000000..9064d7f8522
--- /dev/null
+++ b/pulse/test/error_messages/MissingPost.fst.output.expected
@@ -0,0 +1,6 @@
+* Info at MissingPost.fst(12,2-12,4):
+  - Expected failure:
+  - Tactic failed
+  - Leftover resources: Pulse.Lib.Reference.pts_to r 1
+  - Did you forget to free these resources?
+
diff --git a/pulse/test/error_messages/MultiError.fst b/pulse/test/error_messages/MultiError.fst
new file mode 100644
index 00000000000..5414347ec31
--- /dev/null
+++ b/pulse/test/error_messages/MultiError.fst
@@ -0,0 +1,14 @@
+module MultiError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Multiple errors in sequence - check that each one is localized correctly
+[@@expect_failure [19]]
+fn multi_error (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 100
+{
+  r := 1;
+  assert (pure (1 = 2));   // first error here
+  r := 100
+}
diff --git a/pulse/test/error_messages/MultiError.fst.output.expected b/pulse/test/error_messages/MultiError.fst.output.expected
new file mode 100644
index 00000000000..6043a7f8030
--- /dev/null
+++ b/pulse/test/error_messages/MultiError.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at MultiError.fst(12,18-12,19):
+  - Expected failure:
+  - Failed to prove pure property: false
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+  - VC = Prims.l_False
+
diff --git a/pulse/test/error_messages/MutualExcl.fst b/pulse/test/error_messages/MutualExcl.fst
new file mode 100644
index 00000000000..4a4f35a50a1
--- /dev/null
+++ b/pulse/test/error_messages/MutualExcl.fst
@@ -0,0 +1,12 @@
+module MutualExcl
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Postcondition has emp but function body leaves resources behind
+[@@expect_failure [228]]
+fn mutual_excl (r: ref int)
+  requires pts_to r 0
+  ensures emp
+{
+  ()  // ERROR: pts_to r 0 is leftover, postcondition is emp
+}
diff --git a/pulse/test/error_messages/MutualExcl.fst.output.expected b/pulse/test/error_messages/MutualExcl.fst.output.expected
new file mode 100644
index 00000000000..721f5efb1bc
--- /dev/null
+++ b/pulse/test/error_messages/MutualExcl.fst.output.expected
@@ -0,0 +1,6 @@
+* Info at MutualExcl.fst(11,2-11,4):
+  - Expected failure:
+  - Tactic failed
+  - Leftover resources: Pulse.Lib.Reference.pts_to r 0
+  - Did you forget to free these resources?
+
diff --git a/pulse/test/error_messages/NestedBlock.fst b/pulse/test/error_messages/NestedBlock.fst
new file mode 100644
index 00000000000..d2365ae8509
--- /dev/null
+++ b/pulse/test/error_messages/NestedBlock.fst
@@ -0,0 +1,15 @@
+module NestedBlock
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error inside a nested block should point to the inner statement
+[@@expect_failure [19]]
+fn nested_block (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 0
+{
+  // {
+    assert (pts_to r 1);  // ERROR: r is 0, not 1
+  // };
+  ()
+}
diff --git a/pulse/test/error_messages/NestedBlock.fst.output.expected b/pulse/test/error_messages/NestedBlock.fst.output.expected
new file mode 100644
index 00000000000..e00db1523b8
--- /dev/null
+++ b/pulse/test/error_messages/NestedBlock.fst.output.expected
@@ -0,0 +1,10 @@
+* Info at NestedBlock.fst(14,2-14,4):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 1
+  - Pulse.Lib.Reference.pts_to r 0
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Pulse.Lib.Reference.pts_to r 1 == Pulse.Lib.Reference.pts_to r 0
+
diff --git a/pulse/test/error_messages/NestedCall.fst b/pulse/test/error_messages/NestedCall.fst
new file mode 100644
index 00000000000..99f49960d43
--- /dev/null
+++ b/pulse/test/error_messages/NestedCall.fst
@@ -0,0 +1,20 @@
+module NestedCall
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error in nested call should point to the specific call site
+fn inner (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 1
+}
+
+[@@expect_failure [19]]
+fn outer (r: ref int)
+  requires pts_to r 5
+  ensures pts_to r 1
+{
+  inner r;  // ERROR: precondition mismatch (pts_to r 5 vs pts_to r 0)
+  ()
+}
diff --git a/pulse/test/error_messages/NestedCall.fst.output.expected b/pulse/test/error_messages/NestedCall.fst.output.expected
new file mode 100644
index 00000000000..6b40aac9b76
--- /dev/null
+++ b/pulse/test/error_messages/NestedCall.fst.output.expected
@@ -0,0 +1,11 @@
+* Info at NestedCall.fst(18,2-18,9):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 5
+  - Pulse.Lib.Reference.pts_to r 0
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Pulse.Lib.Reference.pts_to r 5 == Pulse.Lib.Reference.pts_to r 0
+  - See also NestedCall.fst(18,2-19,4)
+
diff --git a/pulse/test/error_messages/OpenScopeError.fst b/pulse/test/error_messages/OpenScopeError.fst
new file mode 100644
index 00000000000..376b0cf1459
--- /dev/null
+++ b/pulse/test/error_messages/OpenScopeError.fst
@@ -0,0 +1,13 @@
+module OpenScopeError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Opening a nonexistent module should produce a localized error
+[@@expect_failure [168]]
+fn open_fail ()
+  requires emp
+  ensures emp
+{
+  open NonExistent.Module;
+  ()
+}
diff --git a/pulse/test/error_messages/OpenScopeError.fst.output.expected b/pulse/test/error_messages/OpenScopeError.fst.output.expected
new file mode 100644
index 00000000000..fcd9e7f8893
--- /dev/null
+++ b/pulse/test/error_messages/OpenScopeError.fst.output.expected
@@ -0,0 +1,6 @@
+Could not resolve namespace NonExistent.Module
+ valid namespaces are ["fstar", "fstar.algebra", "fstar.algebra.commmonoid", "fstar.algebra.commmonoid.fold", "fstar.cardinality", "fstar.class", "fstar.class.eq", "fstar.class.ord", "fstar.class.totalorder", "fstar.classical", "fstar.constanttime", "fstar.finitemap", "fstar.finiteset", "fstar.immutablearray", "fstar.int", "fstar.int.cast", "fstar.list", "fstar.list.pure", "fstar.list.tot", "fstar.math", "fstar.monotonic", "fstar.pervasives", "fstar.pure", "fstar.reflection", "fstar.reflection.termeq", "fstar.reflection.typing", "fstar.reflection.v2", "fstar.reflection.v2.derived", "fstar.sealed", "fstar.seq", "fstar.sequence", "fstar.stubs", "fstar.stubs.errors", "fstar.stubs.reflection", "fstar.stubs.reflection.v2", "fstar.stubs.syntax", "fstar.stubs.tactics", "fstar.stubs.tactics.types", "fstar.stubs.tactics.v2", "fstar.stubs.typechecker", "fstar.tactics", "fstar.tactics.bv", "fstar.tactics.canon", "fstar.tactics.canoncommmonoidsimple", "fstar.tactics.logic", "fstar.tactics.v2", "fstar.universe", "fstar.vector", "fstar.wellfounded", "pulse", "pulse.c", "pulse.c.types", "pulse.c.types.array", "pulse.c.types.struct", "pulse.class", "pulse.lib", "pulse.lib.array", "pulse.lib.core", "pulse.lib.forall", "pulse.lib.hashtable", "pulse.lib.linkedlist", "pulse.lib.pcm", "pulse.lib.reference", "pulse.lib.seqmatch", "pulse.lib.slice", "pulse.lib.sort", "pulse.lib.sort.merge", "pulse.lib.spec", "pulse.lib.swap", "pulse.lib.trade", "pulsecore"]
+* Info at OpenScopeError.fst(11,2-11,25):
+  - Expected failure:
+  - Failed to open namespace NonExistent.Module; You may need to bind this namespace outside Pulse for the F* dependency scanner to pick it up, e.g., write ``module _X = NonExistent.Module`` in F*
+
diff --git a/pulse/test/error_messages/PrePostMismatch.fst b/pulse/test/error_messages/PrePostMismatch.fst
new file mode 100644
index 00000000000..88f248c6745
--- /dev/null
+++ b/pulse/test/error_messages/PrePostMismatch.fst
@@ -0,0 +1,13 @@
+module PrePostMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Post-condition doesn't match what the body establishes
+[@@expect_failure [19]]
+fn pre_post_mismatch (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 42
+{
+  r := 1;
+  ()
+}
diff --git a/pulse/test/error_messages/PrePostMismatch.fst.output.expected b/pulse/test/error_messages/PrePostMismatch.fst.output.expected
new file mode 100644
index 00000000000..1061f4c0beb
--- /dev/null
+++ b/pulse/test/error_messages/PrePostMismatch.fst.output.expected
@@ -0,0 +1,10 @@
+* Info at PrePostMismatch.fst(12,2-12,4):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 1
+  - Pulse.Lib.Reference.pts_to r 42
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 1 == Pulse.Lib.Reference.pts_to r 42
+
diff --git a/pulse/test/error_messages/ReturnImplicit.fst b/pulse/test/error_messages/ReturnImplicit.fst
new file mode 100644
index 00000000000..64a876b0965
--- /dev/null
+++ b/pulse/test/error_messages/ReturnImplicit.fst
@@ -0,0 +1,13 @@
+module ReturnImplicit
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Return type annotation mismatch with body
+[@@expect_failure [19]]
+fn return_impl ()
+  requires emp
+  returns r: nat
+  ensures emp
+{
+  -1  // ERROR: -1 is not nat
+}
diff --git a/pulse/test/error_messages/ReturnImplicit.fst.output.expected b/pulse/test/error_messages/ReturnImplicit.fst.output.expected
new file mode 100644
index 00000000000..f9e2fd24e7e
--- /dev/null
+++ b/pulse/test/error_messages/ReturnImplicit.fst.output.expected
@@ -0,0 +1,9 @@
+* Info at ReturnImplicit.fst(12,2-12,4):
+  - Expected failure:
+  - Ill-typed term
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (uu___0 : Prims.unit)
+  - VC = Prims.l_False
+  - Also see: Prims.fst(642,18-642,24)
+
diff --git a/pulse/test/error_messages/ReturnTypeMismatch.fst b/pulse/test/error_messages/ReturnTypeMismatch.fst
new file mode 100644
index 00000000000..fbb48c56adf
--- /dev/null
+++ b/pulse/test/error_messages/ReturnTypeMismatch.fst
@@ -0,0 +1,13 @@
+module ReturnTypeMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Returning wrong type
+[@@expect_failure [189]]
+fn return_wrong_type (x: int)
+  requires emp
+  returns r: bool
+  ensures emp
+{
+  x
+}
diff --git a/pulse/test/error_messages/ReturnTypeMismatch.fst.output.expected b/pulse/test/error_messages/ReturnTypeMismatch.fst.output.expected
new file mode 100644
index 00000000000..64fef0ba1de
--- /dev/null
+++ b/pulse/test/error_messages/ReturnTypeMismatch.fst.output.expected
@@ -0,0 +1,4 @@
+* Info at ReturnTypeMismatch.fst(12,2-12,3):
+  - Expected failure:
+  - Expected expression of type Prims.bool got expression x of type Prims.int
+
diff --git a/pulse/test/error_messages/RewriteFail.fst b/pulse/test/error_messages/RewriteFail.fst
new file mode 100644
index 00000000000..a7d09146ccd
--- /dev/null
+++ b/pulse/test/error_messages/RewriteFail.fst
@@ -0,0 +1,13 @@
+module RewriteFail
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Rewrite with incompatible propositions
+[@@expect_failure [19]]
+fn rewrite_fail (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  rewrite (pts_to r 0) as (pts_to r 1);  // ERROR: can't rewrite, not equivalent
+  ()
+}
diff --git a/pulse/test/error_messages/RewriteFail.fst.output.expected b/pulse/test/error_messages/RewriteFail.fst.output.expected
new file mode 100644
index 00000000000..94833d73aaf
--- /dev/null
+++ b/pulse/test/error_messages/RewriteFail.fst.output.expected
@@ -0,0 +1,10 @@
+* Info at RewriteFail.fst(11,11-11,33):
+  - Expected failure:
+  - rewrite: could not prove equality of
+  - pts_to r 0
+  - pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (r : Pulse.Lib.Reference.ref Prims.int)
+  - VC = Pulse.Class.PtsTo.pts_to r 0 == Pulse.Class.PtsTo.pts_to r 1
+
diff --git a/pulse/test/error_messages/SequenceError.fst b/pulse/test/error_messages/SequenceError.fst
new file mode 100644
index 00000000000..ccf9ba006d0
--- /dev/null
+++ b/pulse/test/error_messages/SequenceError.fst
@@ -0,0 +1,14 @@
+module SequenceError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error after a sequence of operations - check where error is reported
+[@@expect_failure [19]]
+fn seq_error (r1 r2: ref int)
+  requires pts_to r1 0 ** pts_to r2 0
+  ensures pts_to r1 1 ** pts_to r2 1
+{
+  r1 := 1;
+  r2 := 2;
+  ()  // ERROR: postcondition pts_to r2 1 checked here, but context has pts_to r2 2
+}
diff --git a/pulse/test/error_messages/SequenceError.fst.output.expected b/pulse/test/error_messages/SequenceError.fst.output.expected
new file mode 100644
index 00000000000..6f8b8dc5af9
--- /dev/null
+++ b/pulse/test/error_messages/SequenceError.fst.output.expected
@@ -0,0 +1,13 @@
+* Info at SequenceError.fst(13,2-13,4):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r2 2
+  - Pulse.Lib.Reference.pts_to r2 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r1 : Pulse.Lib.Reference.ref Prims.int)
+      (r2 : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r2 2 == Pulse.Lib.Reference.pts_to r2 1
+
diff --git a/pulse/test/error_messages/SubtypingFailure.fst b/pulse/test/error_messages/SubtypingFailure.fst
new file mode 100644
index 00000000000..aaaa769666c
--- /dev/null
+++ b/pulse/test/error_messages/SubtypingFailure.fst
@@ -0,0 +1,20 @@
+module SubtypingFailure
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Subtyping failure in function argument
+fn callee (x: nat)
+  requires emp
+  ensures emp
+{
+  ()
+}
+
+[@@expect_failure [19]]
+fn caller (x: int)
+  requires emp
+  ensures emp
+{
+  callee x;
+  ()
+}
diff --git a/pulse/test/error_messages/SubtypingFailure.fst.output.expected b/pulse/test/error_messages/SubtypingFailure.fst.output.expected
new file mode 100644
index 00000000000..9bc10f32976
--- /dev/null
+++ b/pulse/test/error_messages/SubtypingFailure.fst.output.expected
@@ -0,0 +1,9 @@
+* Info at SubtypingFailure.fst(18,2-18,10):
+  - Expected failure:
+  - Ill-typed term
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env = (x : Prims.int)
+  - VC = x >= 0
+  - Also see: Prims.fst(642,18-642,24)
+
diff --git a/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst
new file mode 100644
index 00000000000..a52a78f36df
--- /dev/null
+++ b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst
@@ -0,0 +1,24 @@
+module TerminalActionPostConditionMismatch
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Terminal action with postcondition that doesn't match the actual state
+[@@expect_failure [19]]
+fn terminal_action_mismatch (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 0;
+  r := 2;
+}
+
+// Same error, with explicit () at end — both should localize to r := 2
+[@@expect_failure [19]]
+fn terminal_action_mismatch_localized (r: ref int)
+  requires pts_to r 0
+  ensures pts_to r 1
+{
+  r := 0;
+  r := 2;
+  ()
+}
\ No newline at end of file
diff --git a/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected
new file mode 100644
index 00000000000..2baeab648ef
--- /dev/null
+++ b/pulse/test/error_messages/TerminalActionPostConditionMismatch.fst.output.expected
@@ -0,0 +1,25 @@
+* Info at TerminalActionPostConditionMismatch.fst(12,2-12,6):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+  - See also TerminalActionPostConditionMismatch.fst(12,2-12,8)
+
+* Info at TerminalActionPostConditionMismatch.fst(23,2-23,4):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to r 2
+  - Pulse.Lib.Reference.pts_to r 1
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (r : Pulse.Lib.Reference.ref Prims.int) (__ : Prims.unit)
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to r 2 == Pulse.Lib.Reference.pts_to r 1
+
diff --git a/pulse/test/error_messages/UnfoldFailure.fst b/pulse/test/error_messages/UnfoldFailure.fst
new file mode 100644
index 00000000000..ba783101628
--- /dev/null
+++ b/pulse/test/error_messages/UnfoldFailure.fst
@@ -0,0 +1,15 @@
+module UnfoldFailure
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Failure when trying to match a predicate that can't be unfolded
+let my_pred (r: ref int) : slprop = pts_to r 0
+
+[@@expect_failure [228]]
+fn unfold_fail (r: ref int)
+  requires my_pred r
+  ensures pts_to r 1
+{
+  r := 1;  // ERROR: can't write to r without unfolding my_pred first
+  ()
+}
diff --git a/pulse/test/error_messages/UnfoldFailure.fst.output.expected b/pulse/test/error_messages/UnfoldFailure.fst.output.expected
new file mode 100644
index 00000000000..b0980b5f4f7
--- /dev/null
+++ b/pulse/test/error_messages/UnfoldFailure.fst.output.expected
@@ -0,0 +1,8 @@
+* Info at UnfoldFailure.fst(13,4-13,6):
+  - Expected failure:
+  - Tactic failed
+  - Cannot prove:
+      pts_to_uninit r
+  - In the context:
+      my_pred r
+
diff --git a/pulse/test/error_messages/WhileInvPreservation.fst b/pulse/test/error_messages/WhileInvPreservation.fst
new file mode 100644
index 00000000000..b33a97161fb
--- /dev/null
+++ b/pulse/test/error_messages/WhileInvPreservation.fst
@@ -0,0 +1,17 @@
+module WhileInvPreservation
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// While loop body fails to preserve invariant
+[@@expect_failure [19]]
+fn while_inv_fail ()
+  requires emp
+  ensures emp
+{
+  let mut i = 0;
+  while (let vi = !i; (vi < 10))
+  invariant pure (!i >= 0 /\ !i <= 10)
+  {
+    i := !i + 2  // ERROR: i + 2 might exceed 10, violating invariant
+  }
+}
diff --git a/pulse/test/error_messages/WhileInvPreservation.fst.output.expected b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected
new file mode 100644
index 00000000000..6a896a2cf21
--- /dev/null
+++ b/pulse/test/error_messages/WhileInvPreservation.fst.output.expected
@@ -0,0 +1,17 @@
+* Info at WhileInvPreservation.fst(15,4-15,8):
+  - Expected failure:
+  - Could not prove equality of:
+  - Pulse.Lib.Reference.pts_to i 2
+  - Pulse.Lib.Reference.pts_to i 0
+  - Assertion failed
+  - The SMT solver could not prove the query.
+  - Env =
+      (uu___0 : Prims.unit) (i : Pulse.Lib.Reference.ref Prims.int)
+      (meas : Prims.unit) (__ : Prims.squash (true /\ true))
+      (__ : Prims.squash (meas == ())) (__ : Prims.squash (true == true))
+      (__anf0 : Prims.int)
+      (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p __anf0 0))
+      (__ : Prims.unit)
+  - VC = Pulse.Lib.Reference.pts_to i 2 == Pulse.Lib.Reference.pts_to i 0
+  - See also WhileInvPreservation.fst(15,4-15,13)
+
diff --git a/pulse/test/error_messages/WithLocalError.fst b/pulse/test/error_messages/WithLocalError.fst
new file mode 100644
index 00000000000..d6662686eaf
--- /dev/null
+++ b/pulse/test/error_messages/WithLocalError.fst
@@ -0,0 +1,14 @@
+module WithLocalError
+#lang-pulse
+open Pulse.Lib.Pervasives
+
+// Error within a with_local block
+[@@expect_failure [189]]
+fn with_local_err ()
+  requires emp
+  ensures emp
+{
+  let mut x = 0;
+  x := 5;
+  assert (pure (x == 0))  // ERROR: x is 5, not 0
+}
diff --git a/pulse/test/error_messages/WithLocalError.fst.output.expected b/pulse/test/error_messages/WithLocalError.fst.output.expected
new file mode 100644
index 00000000000..5bddca1f74f
--- /dev/null
+++ b/pulse/test/error_messages/WithLocalError.fst.output.expected
@@ -0,0 +1,7 @@
+* Info at WithLocalError.fst(13,21-13,22):
+  - Expected failure:
+  - Ill-typed term
+  - Expected expression of type Pulse.Lib.Reference.ref Prims.int
+    got expression 0
+    of type Prims.int
+
diff --git a/pulse/test/nolib/RewriteNopWarning.fst.output.expected b/pulse/test/nolib/RewriteNopWarning.fst.output.expected
index 1132fb77c38..68ef378155c 100644
--- a/pulse/test/nolib/RewriteNopWarning.fst.output.expected
+++ b/pulse/test/nolib/RewriteNopWarning.fst.output.expected
@@ -1,9 +1,9 @@
-* Warning <unknown> at RewriteNopWarning.fst(12,1-13,21):
+* Warning <unknown> at RewriteNopWarning.fst(13,2-13,21):
   - No rewrites performed.
   - Rewriting in:
       foo 1
 
-* Warning <unknown> at RewriteNopWarning.fst(21,1-22,22):
+* Warning <unknown> at RewriteNopWarning.fst(22,2-22,22):
   - No rewrites performed.
   - Rewriting in:
       foo y ** foo 1
diff --git a/pulse/test/nolib/Test.RewriteBy.fst.output.expected b/pulse/test/nolib/Test.RewriteBy.fst.output.expected
index c2b9fb61c4c..dc23de5171d 100644
--- a/pulse/test/nolib/Test.RewriteBy.fst.output.expected
+++ b/pulse/test/nolib/Test.RewriteBy.fst.output.expected
@@ -1,4 +1,4 @@
-* Info at Test.RewriteBy.fst(31,1-37,8):
+* Info at Test.RewriteBy.fst(32,2-37,8):
   - Expected failure:
   - rewrite: could not prove equality of
   - p
diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst
index 4e4076765fc..15534ed099c 100644
--- a/src/parser/FStarC.Parser.Dep.fst
+++ b/src/parser/FStarC.Parser.Dep.fst
@@ -583,7 +583,7 @@ let is_valid_namespace deps ns =
   let res = Some? (SMap.try_find deps.valid_namespaces (String.lowercase (Ident.string_of_lid ns))) in
   if not res
   then Format.print2 "Could not resolve namespace %s\n valid namespaces are %s\n"
-      (show ns) (show <| SMap.keys deps.valid_namespaces);
+      (show ns) (show <| List.sortWith String.compare (SMap.keys deps.valid_namespaces));
   res
 
 let interface_of deps key =