diff --git a/compiler/src/parser.ts b/compiler/src/parser.ts
index c25e995..8a26e13 100644
--- a/compiler/src/parser.ts
+++ b/compiler/src/parser.ts
@@ -271,8 +271,8 @@ function parseSpeck(lines: string[], startIndex: number): SpeckNode | null {
     }
 
     // Handle constraint/verify blocks that may span multiple lines without braces
-    // (e.g. constraint Name: forall r in [0..4]:)
-    if (line.startsWith('constraint ') || line.startsWith('verify ')) {
+    // (e.g. constraint Name: forall r in [0..4]:, verify: always(implies(\n  ...\n)))
+    if (line.startsWith('constraint ') || line.startsWith('verify ') || line.startsWith('verify:')) {
       const member = parseMultiLineConstraintVerify(lines, i);
       if (member) {
         members.push(member);
@@ -1110,18 +1110,130 @@ function parseInterfaceBlockMultiline(lines: string[], startIndex: number, start
  */
 function parseMultiLineConstraintVerify(lines: string[], startIndex: number): MemberNode | null {
   const line = lines[startIndex].trim();
-  
+
   if (line.startsWith('verify ')) {
     return parseVerifyAnyForm(lines, startIndex);
   }
-  
+
+  // Multi-line `verify:` form: verify: always(implies(\n  ...\n))
+  // The body opens parens that span multiple lines; collect continuation
+  // lines until parens balance to zero, then return the joined string as
+  // the temporalExpr. speckl#54.
+  if (line.startsWith('verify:')) {
+    return parseVerifyColonBlock(lines, startIndex);
+  }
+
   if (line.startsWith('constraint ')) {
     return parseConstraintAnyForm(lines, startIndex);
   }
-  
+
   return null;
 }
 
+/**
+ * Parse the `verify: <expr>` form (speckl#54) where the body can span
+ * multiple lines:
+ *
+ *   verify: always(implies(
+ *     cond1,
+ *     cond2
+ *   ))
+ *
+ * The whole expression (the part after `verify:`) is collected by
+ * appending subsequent non-empty, non-keyword-starting lines until
+ * parens/brackets/braces balance to zero. The joined string is stored
+ * in `temporalExpr` so the downstream LTL translator (typescript-state-machine
+ * verifyN()) sees a well-formed formula.
+ *
+ * The `name` is derived from the LTL operator's argument when it matches
+ * `always(Name)` / `eventually(Name)`. When the body is a richer expression
+ * (e.g. `always(implies(...))`) we fall back to `unnamed` — the generator
+ * still emits a working verifyN() that uses the full expression.
+ */
+function parseVerifyColonBlock(lines: string[], startIndex: number): VerifyNode | null {
+  const firstLine = lines[startIndex].trim();
+  // Strip the `verify:` prefix.
+  const head = firstLine.substring(firstLine.indexOf(':') + 1).trim();
+  if (!head) return null;
+
+  // If the head is already balanced on its own (single-line verify: expr),
+  // just return it directly — no continuation needed.
+  if (isExpressionComplete(head)) {
+    const nameMatch = head.match(/^(?:always|Always|eventually|Eventually)\s*\(\s*(\w+)\s*\)$/);
+    return {
+      type: 'verify',
+      name: nameMatch ? nameMatch[1] : 'unnamed',
+      temporalExpr: head,
+    };
+  }
+
+  // Multi-line: collect continuation lines until parens balance. The same
+  // break-condition list used in the parseSpeck skip-loop applies (don't
+  // swallow the next member's keyword). We additionally stop at any
+  // standalone `}` so a verify inside a brace-block still terminates.
+  const parts: string[] = [head];
+  let parens = 0, brackets = 0, braces = 0;
+  for (const ch of head) {
+    if (ch === '(') parens++;
+    else if (ch === ')') parens--;
+    else if (ch === '[') brackets++;
+    else if (ch === ']') brackets--;
+    else if (ch === '{') braces++;
+    else if (ch === '}') braces--;
+  }
+
+  let lastConsumed = startIndex;
+  for (let j = startIndex + 1; j < lines.length; j++) {
+    const raw = lines[j];
+    const nl = raw.trim();
+    if (!nl) {
+      // Empty line still updates counters (none) and advances lastConsumed
+      lastConsumed = j;
+      continue;
+    }
+    if (nl.startsWith('//') || nl.startsWith('/*')) {
+      // Skip standalone comments but treat them as part of the block
+      // (the LTL translator doesn't care about comments in temporalExpr).
+      lastConsumed = j;
+      continue;
+    }
+    // Stop at a new top-level member keyword — that's the next member.
+    if (
+      nl.startsWith('constraint ') || nl.startsWith('verify ') ||
+      nl.startsWith('constraint:') || nl.startsWith('verify:') ||
+      nl.startsWith('state') || nl.startsWith('init') ||
+      nl.startsWith('action ') || nl.startsWith('event ') ||
+      nl.startsWith('interface ') || nl.startsWith('provenance ') ||
+      nl.startsWith('bom ') || nl === '}' ||
+      nl.startsWith('next:') || nl.startsWith('invariant ')
+    ) {
+      break;
+    }
+    // Update depth counters.
+    for (const ch of raw) {
+      if (ch === '(') parens++;
+      else if (ch === ')') parens--;
+      else if (ch === '[') brackets++;
+      else if (ch === ']') brackets--;
+      else if (ch === '{') braces++;
+      else if (ch === '}') braces--;
+    }
+    parts.push(nl);
+    lastConsumed = j;
+    if (parens === 0 && brackets === 0 && braces === 0) {
+      break;
+    }
+  }
+
+  const joined = parts.join(' ').replace(/\s+/g, ' ').trim();
+  const nameMatch = joined.match(/^(?:always|Always|eventually|Eventually)\s*\(\s*(\w+)\s*\)$/);
+  return {
+    type: 'verify',
+    name: nameMatch ? nameMatch[1] : 'unnamed',
+    temporalExpr: joined,
+  };
+}
+
 function parseConstraintAnyForm(lines: string[], startIndex: number): ConstraintNode | null {
   const line = lines[startIndex].trim();