diff --git a/Cslib/Foundations/Syntax/HasWellFormed.lean b/Cslib/Foundations/Syntax/HasWellFormed.lean
index 94ca81629..1dd2a6330 100644
--- a/Cslib/Foundations/Syntax/HasWellFormed.lean
+++ b/Cslib/Foundations/Syntax/HasWellFormed.lean
@@ -20,6 +20,6 @@ class HasWellFormed (α : Type u) where
   wf (x : α) : Prop
 
 /-- Notation for well-formedness. -/
-notation x:max "✓" => HasWellFormed.wf x
+macro x:term:max noWs "✓" : term => `(HasWellFormed.wf $x)
 
 end Cslib
diff --git a/CslibTests.lean b/CslibTests.lean
index 90903a188..b26f3aa5d 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -7,6 +7,7 @@ import CslibTests.GrindLint
 import CslibTests.HML
 import CslibTests.HasFresh
 import CslibTests.HasSubstitution
+import CslibTests.HasWellFormed
 import CslibTests.ImportWithMathlib
 import CslibTests.LTS
 import CslibTests.LambdaCalculus
diff --git a/CslibTests/HasWellFormed.lean b/CslibTests/HasWellFormed.lean
new file mode 100644
index 000000000..e408cb3d2
--- /dev/null
+++ b/CslibTests/HasWellFormed.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Sean D. Stoneburner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sean D. Stoneburner
+-/
+import Cslib.Algorithms.Lean.TimeM
+import Cslib.Foundations.Syntax.HasWellFormed
+
+open Cslib.Algorithms.Lean
+
+/-!
+# Syntax Collision Test
+This file tests that the `✓` prefix macro from `TimeM` does not collide with
+the `✓` postfix notation from `HasWellFormed` across line breaks.
+-/
+
+def testParserCollision (n : Nat) : TimeM Nat Nat := do
+  let m := n
+  ✓ return m
+
+-- Ensure the postfix notation still functions correctly when attached without whitespace
+variable {α : Type*} [Cslib.HasWellFormed α] (x : α)
+
+/-- info: Cslib.HasWellFormed.wf x : Prop -/
+#guard_msgs in
+#check x✓