diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
index fc7a2f34d7b..253db017c6b 100644
--- a/Source/DafnyCore/Dafny.atg
+++ b/Source/DafnyCore/Dafny.atg
@@ -1771,8 +1771,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
                   "a formal [ ] declaration is only allowed for least and greatest predicates");
         .)
       ]
-      [ Formals<true, true, isTwoState, true, formals>
-      ]
+      Formals<true, true, isTwoState, true, formals>
       [ PredicateResult<"predicate", out result> ]
     | ellipsis   (. signatureEllipsis = t; .)
     )
diff --git a/Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs b/Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs
index 04c17dbd88c..f85e501f978 100644
--- a/Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs
+++ b/Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs
@@ -65,7 +65,7 @@ method TestMethod() returns (x: int) {
 
 trait TestTrait {}
 
-predicate TestPredicate { false }", "test-workspace-symbols.dfy", false);
+predicate TestPredicate() { false }", "test-workspace-symbols.dfy", false);
 
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy
index ae6b63178aa..1f3ebe08358 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy
@@ -273,6 +273,26 @@ module ArrowTypes {
   }
 }
 
+// ---------------------- missing parentheses for `predicate` -----------------------------------
+
+module MissingPredicateParens0 {
+  predicate P<A>
+} // error: expecting open paren
+
+module MissingPredicateParens1 {
+  predicate P<A> { // error: expecting open paren
+    true
+  }
+}
+
+module MissingPredicateParens2 {
+  predicate P<A> { // error: expecting open paren
+    true
+  } by method {
+    return true;
+  }
+}
+
 // ---------------------- invalid newtype definition -----------------------------------
 
 newtype T {} // error: newtype is expected to have an '='
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy.expect
index f0b35782750..26dacfd1124 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy.expect
@@ -79,5 +79,8 @@ ParseErrors.dfy(261,28): Error: formal cannot be declared 'older' in this contex
 ParseErrors.dfy(267,12): Error: arrow-type arguments may not be declared as 'ghost'
 ParseErrors.dfy(272,18): Error: arrow-type arguments may not be declared as 'ghost'
 ParseErrors.dfy(272,35): Error: arrow-type arguments may not be declared as 'ghost'
-ParseErrors.dfy(278,10): Error: invalid NewtypeDecl
-77 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(280,0): Error: openparen expected
+ParseErrors.dfy(283,17): Error: openparen expected
+ParseErrors.dfy(289,17): Error: openparen expected
+ParseErrors.dfy(298,10): Error: invalid NewtypeDecl
+80 parse errors detected in ParseErrors.dfy
diff --git a/docs/dev/news/5069.fix b/docs/dev/news/5069.fix
new file mode 100644
index 00000000000..5ff6f59545e
--- /dev/null
+++ b/docs/dev/news/5069.fix
@@ -0,0 +1 @@
+The syntax of a predicate definition must always include parentheses.