diff --git a/Test/Func/pretty_print.mlir b/Test/Func/pretty_print.mlir
new file mode 100644
index 000000000..5bf547bd7
--- /dev/null
+++ b/Test/Func/pretty_print.mlir
@@ -0,0 +1,23 @@
+// Custom (pretty) printing of the func dialect via the declarative assembly
+// format. The input is in generic form; with --pretty the func ops are printed
+// in their custom syntax.
+
+// RUN: veir-opt --pretty %s | filecheck %s
+
+"builtin.module"() ({
+  "func.func"() <{function_type = (i32) -> i32, sym_name = "callee"}> ({
+  ^bb0(%arg0: i32):
+    "func.return"(%arg0) : (i32) -> ()
+  }) : () -> ()
+  "func.func"() <{function_type = (i32) -> i32, sym_name = "caller"}> ({
+  ^bb0(%arg0: i32):
+    %0 = "func.call"(%arg0) <{callee = @callee}> : (i32) -> i32
+    "func.return"(%0) : (i32) -> ()
+  }) : () -> ()
+}) : () -> ()
+
+// CHECK:      func.func @callee(%arg{{[0-9]+_[0-9]+}}: i32) -> i32 {
+// CHECK-NEXT:   func.return %arg{{[0-9]+_[0-9]+}} : i32
+// CHECK:      func.func @caller(%arg{{[0-9]+_[0-9]+}}: i32) -> i32 {
+// CHECK:        %{{[0-9]+}} = func.call @callee(%arg{{[0-9]+_[0-9]+}}) : (i32) -> i32
+// CHECK-NEXT:   func.return %{{[0-9]+}} : i32
diff --git a/Veir.lean b/Veir.lean
index 54f6d0ab3..93830f580 100644
--- a/Veir.lean
+++ b/Veir.lean
@@ -8,6 +8,7 @@ import Veir.Rewriter.WellFormed
 import Veir.Rewriter.InlineBlock
 import Veir.Rewriter.WfRewriter
 import Veir.Printer
+import Veir.AssemblyFormat
 import Veir.PatternRewriter.Basic
 import Veir.Passes.RISCVCombines.Proofs
 import Veir.Benchmarks
diff --git a/Veir/AssemblyFormat.lean b/Veir/AssemblyFormat.lean
new file mode 100644
index 000000000..73eeb2317
--- /dev/null
+++ b/Veir/AssemblyFormat.lean
@@ -0,0 +1,267 @@
+module
+
+/-
+# Declarative assembly format DSL
+
+This module implements a small declarative DSL, modelled closely on MLIR's
+[`assemblyFormat`](https://mlir.llvm.org/docs/DefiningDialects/Operations/#declarative-assembly-format),
+for describing the *custom* (pretty) syntax of an operation. The intent is that
+a format string written for MLIR's `assemblyFormat` can be reused in VeIR with
+little to no change.
+
+The DSL is interpreted at runtime: `Format.parse` turns a format string into a
+`Format` AST, and the printer (`Veir/Printer.lean`) and parser
+(`Veir/Parser/MlirParser.lean`) walk that AST. The set of supported directives
+is the minimal subset needed for nice function syntax (`func.return`,
+`func.call`); operations whose syntax cannot be expressed declaratively (most
+notably `func.func`, which mirrors MLIR's `hasCustomAssemblyFormat`) are handled
+by dedicated hooks instead.
+
+Supported elements:
+* literals: `` `keyword` `` / `` `:` `` etc.
+* attribute/property variables: `$name` (bound to a key in the op's property /
+  attribute dictionary, exactly like an ODS-declared attribute).
+* directives: `attr-dict`, `attr-dict-with-keyword`, `operands`, `results`,
+  `type(...)`, `functional-type(..., ...)`, `regions`, `successors`.
+* optional groups: `( ... ^ ... )?` with a single anchor element, plus an
+  optional else-group `( ... )? : ( ... )`.
+
+Notable differences from MLIR (VeIR has no per-op named operand/result schema,
+so it cannot resolve a `$name` to an operand or result the way ODS does):
+* `$name` always denotes an attribute/property (looked up by key `name`). SSA
+  operands and results are referred to only via the `operands` / `results`
+  directives, including inside `type(...)` / `functional-type(...)`.
+* Because there are no operand/result *variables*, the anchor of an optional
+  group may be the `operands` / `results` directive (MLIR only permits a
+  variable or type directive as the anchor). This is a deliberate VeIR
+  extension to compensate for the missing schema.
+-/
+
+public import Veir.OpCode
+public import Veir.GlobalOpInfo
+
+namespace Veir.AssemblyFormat
+
+public section
+
+/-- Which positional collection a `type`/`functional-type` argument refers to. -/
+inductive TypeArg where
+  | operands
+  | results
+deriving Repr, DecidableEq, Inhabited
+
+/-- A builtin directive in the assembly format DSL. -/
+inductive Directive where
+  /-- `attr-dict`: the operation's discardable attribute dictionary. -/
+  | attrDict
+  /-- `attr-dict-with-keyword`: same, prefixed by the `attributes` keyword. -/
+  | attrDictWithKeyword
+  /-- `operands`: all of the operation's operands. -/
+  | operands
+  /-- `results`: all of the operation's results (usable only for types). -/
+  | results
+  /-- `type(arg)`: the type(s) of the given collection. -/
+  | typeOf (arg : TypeArg)
+  /-- `functional-type(ins, outs)`: prints `(ins) -> (outs)`. -/
+  | functionalType (ins : TypeArg) (outs : TypeArg)
+  /-- `regions`: all of the operation's regions. -/
+  | regions
+  /-- `successors`: all of the operation's successor blocks. -/
+  | successors
+deriving Repr, Inhabited
+
+/-- A single element of an assembly format. -/
+inductive Element where
+  /-- A literal keyword or punctuation, written `` `...` `` in the DSL. -/
+  | literal (s : String)
+  /-- A `$name` variable, bound to the property/attribute key `name`. -/
+  | attrVar (name : String)
+  /-- A builtin directive. -/
+  | directive (d : Directive)
+  /-- An optional group `( then ... )? : ( else ... )` anchored on `anchor`. -/
+  | optional (thenElems : Array Element) (anchor : Nat) (elseElems : Array Element)
+deriving Repr, Inhabited
+
+/-- A parsed assembly format: a flat sequence of elements. -/
+abbrev Format := Array Element
+
+/-! ## Tokenizer -/
+
+/-- A lexical token of the format DSL. -/
+inductive Tok where
+  | lit (s : String)
+  | dollar (name : String)
+  | word (s : String)
+  | lparen | rparen | langle | rangle | comma | question | caret | colon
+deriving Repr, DecidableEq, Inhabited
+
+private def isWordChar (c : Char) : Bool := c.isAlphanum || c == '-' || c == '_'
+
+/-- Tokenize a format string. Whitespace outside backticks is insignificant. -/
+private partial def tokenize (s : String) : Except String (Array Tok) :=
+  go s.toList #[]
+where
+  readLit (cs : List Char) (acc : String) : String × List Char :=
+    match cs with
+    | [] => (acc, [])
+    | c :: rest => if c == '`' then (acc, rest) else readLit rest (acc.push c)
+  readWord (cs : List Char) (acc : String) : String × List Char :=
+    match cs with
+    | [] => (acc, [])
+    | c :: rest => if isWordChar c then readWord rest (acc.push c) else (acc, c :: rest)
+  go (cs : List Char) (acc : Array Tok) : Except String (Array Tok) := do
+    match cs with
+    | [] => return acc
+    | c :: rest =>
+      if c == ' ' || c == '\t' || c == '\n' || c == '\r' then go rest acc
+      else if c == '`' then
+        let (content, rest') := readLit rest ""
+        go rest' (acc.push (.lit content))
+      else if c == '$' then
+        let (name, rest') := readWord rest ""
+        if name.isEmpty then throw "expected identifier after '$'"
+        go rest' (acc.push (.dollar name))
+      else if c == '(' then go rest (acc.push .lparen)
+      else if c == ')' then go rest (acc.push .rparen)
+      else if c == '<' then go rest (acc.push .langle)
+      else if c == '>' then go rest (acc.push .rangle)
+      else if c == ',' then go rest (acc.push .comma)
+      else if c == '?' then go rest (acc.push .question)
+      else if c == '^' then go rest (acc.push .caret)
+      else if c == ':' then go rest (acc.push .colon)
+      else if isWordChar c then
+        let (w, rest') := readWord (c :: rest) ""
+        go rest' (acc.push (.word w))
+      else throw s!"unexpected character '{c}' in assembly format"
+
+/-! ## Parser (tokens → AST) -/
+
+private def parseTypeArg : List Tok → Except String (TypeArg × List Tok)
+  | .word "operands" :: rest => return (.operands, rest)
+  | .word "results" :: rest => return (.results, rest)
+  | _ => throw "expected 'operands' or 'results' as the argument of a type directive"
+
+mutual
+
+/-- Parse a sequence of elements until a stopping token (`)`, `?`, `: (`, or
+    end of input). Detects a single `^` anchor marker. -/
+private partial def parseElements (toks : List Tok) (stopAtRParen : Bool) :
+    Except String (Array Element × Option Nat × List Tok) := do
+  let mut acc : Array Element := #[]
+  let mut anchor : Option Nat := none
+  let mut toks := toks
+  repeat
+    match toks with
+    | [] => break
+    | .rparen :: _ => if stopAtRParen then break else throw "unexpected ')' in assembly format"
+    | .question :: _ => break
+    | .colon :: .lparen :: _ => break
+    | _ =>
+      let (el, toks') ← parseElement toks
+      acc := acc.push el
+      toks := toks'
+      match toks with
+      | .caret :: rest =>
+        if anchor.isSome then throw "multiple anchors '^' in optional group"
+        anchor := some (acc.size - 1)
+        toks := rest
+      | _ => pure ()
+  return (acc, anchor, toks)
+
+/-- Parse a single element. -/
+private partial def parseElement : List Tok → Except String (Element × List Tok)
+  | .lit s :: rest => return (.literal s, rest)
+  | .dollar name :: rest => return (.attrVar name, rest)
+  | .word "attr-dict" :: rest => return (.directive .attrDict, rest)
+  | .word "attr-dict-with-keyword" :: rest => return (.directive .attrDictWithKeyword, rest)
+  | .word "operands" :: rest => return (.directive .operands, rest)
+  | .word "results" :: rest => return (.directive .results, rest)
+  | .word "regions" :: rest => return (.directive .regions, rest)
+  | .word "successors" :: rest => return (.directive .successors, rest)
+  | .word "type" :: .lparen :: rest => do
+      let (arg, rest) ← parseTypeArg rest
+      match rest with
+      | .rparen :: rest => return (.directive (.typeOf arg), rest)
+      | _ => throw "expected ')' after type(...) argument"
+  | .word "functional-type" :: .lparen :: rest => do
+      let (ins, rest) ← parseTypeArg rest
+      match rest with
+      | .comma :: rest =>
+        let (outs, rest) ← parseTypeArg rest
+        match rest with
+        | .rparen :: rest => return (.directive (.functionalType ins outs), rest)
+        | _ => throw "expected ')' after functional-type(...) arguments"
+      | _ => throw "expected ',' in functional-type(ins, outs)"
+  | .word w :: _ => throw s!"unknown directive '{w}'"
+  | .lparen :: rest => do
+      let (thenElems, anchor, rest) ← parseElements rest true
+      let (elseElems, rest) ←
+        match rest with
+        | .rparen :: .colon :: .lparen :: rest2 => do
+            let (elseEls, _, rest3) ← parseElements rest2 true
+            match rest3 with
+            | .rparen :: rest4 => pure (elseEls, rest4)
+            | _ => throw "expected ')' to close else-group"
+        | .rparen :: rest2 => pure (#[], rest2)
+        | _ => throw "expected ')' to close optional group"
+      match rest with
+      | .question :: rest =>
+          let some a := anchor | throw "optional group requires an anchor (mark an element with '^')"
+          return (.optional thenElems a elseElems, rest)
+      | _ => throw "expected '?' after optional group"
+  | [] => throw "unexpected end of assembly format"
+  | t :: _ => throw s!"unexpected token {repr t} in assembly format"
+
+end
+
+/-- Parse a format string into a `Format` AST. -/
+public def Format.parse (s : String) : Except String Format := do
+  let toks ← tokenize s
+  let (elems, anchor, rest) ← parseElements toks.toList false
+  if anchor.isSome then throw "anchor '^' is only allowed inside an optional group"
+  unless rest.isEmpty do throw s!"unexpected trailing tokens in assembly format"
+  return elems
+
+/-- All `$name` variables referenced anywhere in the format (including nested
+    optional groups). These keys are "consumed" by the format and therefore
+    elided from the `attr-dict` directive, mirroring MLIR. -/
+public partial def Format.attrVarNames (fmt : Format) : List String :=
+  fmt.foldl (init := []) fun acc el =>
+    match el with
+    | .attrVar name => acc ++ [name]
+    | .optional thenElems _ elseElems =>
+        acc ++ Format.attrVarNames thenElems ++ Format.attrVarNames elseElems
+    | _ => acc
+
+/-! ## Registry
+
+The set of operations that have a declarative custom syntax. This is a plain
+hand-written function over `OpCode`, matching the style of `OpCode.isTerminator`
+and friends in `Veir/GlobalOpInfo.lean`. Operations not listed here fall back to
+the generic MLIR form (and, for `func.func`, to a dedicated hook).
+
+These format strings are copied essentially verbatim from MLIR's `FuncOps.td`.
+-/
+
+/-- The declarative assembly format string for an operation, if it has one. -/
+public def OpCode.assemblyFormatString? : OpCode → Option String
+  | .func .return => some "attr-dict (operands^ `:` type(operands))?"
+  | .func .call => some "$callee `(` operands `)` attr-dict `:` functional-type(operands, results)"
+  | _ => none
+
+/-- The parsed declarative assembly format for an operation, if it has one and
+    parses successfully. -/
+public def OpCode.assemblyFormat? (op : OpCode) : Option Format :=
+  match OpCode.assemblyFormatString? op with
+  | none => none
+  | some s => (Format.parse s).toOption
+
+end -- public section
+
+/- Compile-time validation: every registered format string must parse. These
+   `#guard`s fail the build if a format string is malformed, giving the DSL the
+   same early-error behaviour as MLIR's tablegen-time checking. -/
+#guard (Format.parse "attr-dict (operands^ `:` type(operands))?").toOption.isSome
+#guard (Format.parse "$callee `(` operands `)` attr-dict `:` functional-type(operands, results)").toOption.isSome
+
+end Veir.AssemblyFormat
diff --git a/Veir/Printer.lean b/Veir/Printer.lean
index 2c433f1fb..1220fa2b0 100644
--- a/Veir/Printer.lean
+++ b/Veir/Printer.lean
@@ -3,6 +3,7 @@ module
 public import Veir.IR.Basic
 public import Veir.Properties
 public import Veir.GlobalOpInfo
+public import Veir.AssemblyFormat
 
 import Veir.IR.Grind
 import Veir.Rewriter.Basic
@@ -120,16 +121,153 @@ def printOpProperties (ctx : IRContext OpCode) (op : OperationPtr) : IO Unit :=
   IO.print (DictionaryAttr.fromArray attrDict.toArray)
   IO.print ">"
 
+/-!
+  ## Declarative assembly format printing
+
+  The helpers below interpret a parsed `AssemblyFormat.Format` to print an
+  operation in its custom (pretty) syntax. Spacing follows MLIR's convention: a
+  space is inserted before each element except where punctuation should hug the
+  surrounding tokens.
+-/
+
+open Veir.AssemblyFormat in
+/-- Literals that should not be preceded by a space (they hug the left token). -/
+def Printer.noSpaceBefore (s : String) : Bool := s == ")" || s == "]" || s == ">" || s == "," || s == "("
+
+/-- Literals that suppress the space after them (the next element glues on). -/
+def Printer.gluesNext (s : String) : Bool := s == "(" || s == "[" || s == "<"
+
+/-- Emit a literal with MLIR-style spacing; returns the new pending-space flag. -/
+def Printer.emitLiteral (s : String) (pending : Bool) : IO Bool := do
+  if pending && !Printer.noSpaceBefore s then IO.print " "
+  IO.print s
+  return !Printer.gluesNext s
+
+/-- The types of all operands of `op`. -/
+def Printer.operandTypes (ctx : IRContext OpCode) (op : OperationPtr) : Array TypeAttr := Id.run do
+  let mut tys : Array TypeAttr := #[]
+  for i in 0...(op.getNumOperands! ctx) do
+    tys := tys.push ((op.getOperand! ctx i).getType! ctx)
+  return tys
+
+/-- The types of all results of `op`. -/
+def Printer.resultTypes (ctx : IRContext OpCode) (op : OperationPtr) : Array TypeAttr := Id.run do
+  let mut tys : Array TypeAttr := #[]
+  for i in 0...(op.getNumResults! ctx) do
+    tys := tys.push (((op.getResult i).get! ctx).type)
+  return tys
+
+/-- Print a comma-separated list of operands `%a, %b` (no surrounding parens). -/
+def Printer.printOperandsFormat (ctx : IRContext OpCode) (op : OperationPtr) (pending : Bool) : IO Bool := do
+  let n := op.getNumOperands! ctx
+  if n = 0 then return pending
+  if pending then IO.print " "
+  printValue ctx (op.getOperand! ctx 0)
+  for i in 1...n do
+    IO.print ", "
+    printValue ctx (op.getOperand! ctx i)
+  return true
+
+/-- Print a comma-separated list of types `t1, t2` (no surrounding parens). -/
+def Printer.printCommaTypes (tys : Array TypeAttr) (pending : Bool) : IO Bool := do
+  if tys.size = 0 then return pending
+  if pending then IO.print " "
+  IO.print s!"{tys[0]!}"
+  for i in 1...tys.size do
+    IO.print s!", {tys[i]!}"
+  return true
+
+/-- Print a function type `(ins) -> outs`, matching `printOperationType`'s
+    result-side conventions (single result is printed without parens). -/
+def Printer.printFunctionalTypeBody (ins outs : Array TypeAttr) (pending : Bool) : IO Bool := do
+  if pending then IO.print " "
+  IO.print "("
+  if ins.size ≠ 0 then
+    IO.print s!"{ins[0]!}"
+    for i in 1...ins.size do
+      IO.print s!", {ins[i]!}"
+  IO.print ") -> "
+  if outs.size = 0 then
+    IO.print "()"
+  else if outs.size = 1 then
+    match outs[0]!.val with
+    | .functionType _ => IO.print s!"({outs[0]!})"
+    | _ => IO.print s!"{outs[0]!}"
+  else
+    IO.print "("
+    IO.print s!"{outs[0]!}"
+    for i in 1...outs.size do
+      IO.print s!", {outs[i]!}"
+    IO.print ")"
+  return true
+
+/-- Print the value of a `$name` variable, looked up first in the operation's
+    properties (inherent attributes) and then in its discardable attributes.
+    Absent variables print nothing. -/
+def Printer.printAttrVar (ctx : IRContext OpCode) (op : OperationPtr) (opType : OpCode)
+    (name : String) (pending : Bool) : IO Bool := do
+  let key := name.toUTF8
+  let props := op.getProperties! ctx opType
+  let propDict := Properties.toAttrDict opType props
+  let value : Option Attribute :=
+    match propDict[key]? with
+    | some v => some v
+    | none => (((op.get! ctx).attrs).entries.find? (fun e => e.1 = key)).map (·.2)
+  match value with
+  | none => return pending
+  | some v =>
+    if pending then IO.print " "
+    IO.print (toString v)
+    return true
+
+/-- Print the `attr-dict` (or `attr-dict-with-keyword`) directive: the merge of
+    inherent properties and discardable attributes, excluding keys consumed by
+    `$var`s elsewhere in the format. -/
+def Printer.printAttrDictFormat (ctx : IRContext OpCode) (op : OperationPtr) (opType : OpCode)
+    (consumed : List String) (withKeyword : Bool) (pending : Bool) : IO Bool := do
+  let props := op.getProperties! ctx opType
+  let propDict := Properties.toAttrDict opType props
+  let mut entries : Array (ByteArray × Attribute) := #[]
+  for (k, v) in propDict.toArray do
+    if !consumed.contains (String.fromUTF8! k) then
+      entries := entries.push (k, v)
+  for (k, v) in ((op.get! ctx).attrs).entries do
+    if !consumed.contains (String.fromUTF8! k) then
+      entries := entries.push (k, v)
+  if entries.size = 0 then return pending
+  if pending then IO.print " "
+  if withKeyword then IO.print "attributes "
+  IO.print (DictionaryAttr.fromArray entries)
+  return true
+
+/-- Is the anchor element of an optional group "present" (so the group should be
+    printed)? Mirrors MLIR: variadic operands/results/regions/successors are
+    present when non-empty; an attribute variable is present when its key
+    exists. -/
+def Printer.isAnchorPresent (ctx : IRContext OpCode) (op : OperationPtr) (opType : OpCode)
+    (el : AssemblyFormat.Element) : Bool :=
+  match el with
+  | .directive .operands => op.getNumOperands! ctx > 0
+  | .directive .results => op.getNumResults! ctx > 0
+  | .directive .regions => op.getNumRegions! ctx > 0
+  | .directive .successors => op.getNumSuccessors! ctx > 0
+  | .attrVar name =>
+      let key := name.toUTF8
+      let props := op.getProperties! ctx opType
+      let propDict := Properties.toAttrDict opType props
+      propDict.contains key || ((op.get! ctx).attrs).entries.any (fun e => e.1 = key)
+  | _ => true
+
 mutual
-partial def printOpList (ctx: IRContext OpCode) (op: OperationPtr) (indent: Nat := 0) : IO Unit := do
-  printOperation ctx op indent
+partial def printOpList (ctx: IRContext OpCode) (op: OperationPtr) (pretty : Bool := false) (indent: Nat := 0) : IO Unit := do
+  printOperation ctx op pretty indent
   match _ : (op.get! ctx).next with
   | some nextOp =>
-    printOpList ctx nextOp indent
+    printOpList ctx nextOp pretty indent
   | none =>
     pure ()
 
-partial def printBlock (ctx: IRContext OpCode) (block: BlockPtr) (indent: Nat := 0) : IO Unit := do
+partial def printBlock (ctx: IRContext OpCode) (block: BlockPtr) (pretty : Bool := false) (indent: Nat := 0) : IO Unit := do
   printIndent indent
   IO.print s!"^{block.id}("
   for i in 0...(block.getNumArguments! ctx) do
@@ -140,19 +278,19 @@ partial def printBlock (ctx: IRContext OpCode) (block: BlockPtr) (indent: Nat :=
   IO.println s!"):"
   match _ : (block.get! ctx).firstOp with
   | some firstOp =>
-    printOpList ctx firstOp (indent + 1)
+    printOpList ctx firstOp pretty (indent + 1)
   | none =>
     pure ()
 
-partial def printBlockList (ctx: IRContext OpCode) (block: BlockPtr) (indent: Nat := 0) : IO Unit := do
-  printBlock ctx block indent
+partial def printBlockList (ctx: IRContext OpCode) (block: BlockPtr) (pretty : Bool := false) (indent: Nat := 0) : IO Unit := do
+  printBlock ctx block pretty indent
   match _ : (block.get! ctx).next with
   | some nextBlock =>
-    printBlockList ctx nextBlock indent
+    printBlockList ctx nextBlock pretty indent
   | none =>
     pure ()
 
-partial def printRegion (ctx: IRContext OpCode) (region: Region) (indent: Nat := 0) : IO Unit := do
+partial def printRegion (ctx: IRContext OpCode) (region: Region) (pretty : Bool := false) (indent: Nat := 0) : IO Unit := do
   IO.print "{"
   match region.firstBlock with
   | none =>
@@ -160,22 +298,155 @@ partial def printRegion (ctx: IRContext OpCode) (region: Region) (indent: Nat :=
     IO.print "}"
   | some blockPtr =>
     IO.println ""
-    printBlockList ctx blockPtr (indent + 1)
+    printBlockList ctx blockPtr pretty (indent + 1)
     printIndent indent
     IO.print "}"
 
-partial def printRegions (ctx: IRContext OpCode) (op: OperationPtr) (indent: Nat := 0) : IO Unit := do
+partial def printRegions (ctx: IRContext OpCode) (op: OperationPtr) (pretty : Bool := false) (indent: Nat := 0) : IO Unit := do
   if op.getNumRegions! ctx = 0 then return
   IO.print "("
   for i in 0...((op.getNumRegions! ctx) - 1) do
     let region := (op.getRegion! ctx i).get! ctx
-    printRegion ctx region indent
+    printRegion ctx region pretty indent
     IO.print ", "
-  printRegion ctx ((op.getRegion! ctx (op.getNumRegions! ctx - 1)).get! ctx) indent
+  printRegion ctx ((op.getRegion! ctx (op.getNumRegions! ctx - 1)).get! ctx) pretty indent
   IO.print ")"
 
-partial def printOperation (ctx: IRContext OpCode) (op: OperationPtr) (indent: Nat := 0) : IO Unit := do
+/-- Print a single assembly-format element. Returns the new pending-space flag. -/
+partial def printFormatElement (ctx : IRContext OpCode) (op : OperationPtr) (opType : OpCode)
+    (consumed : List String) (el : AssemblyFormat.Element) (pretty : Bool) (indent : Nat)
+    (pending : Bool) : IO Bool := do
+  match el with
+  | .literal s => Printer.emitLiteral s pending
+  | .attrVar name => Printer.printAttrVar ctx op opType name pending
+  | .directive .attrDict => Printer.printAttrDictFormat ctx op opType consumed false pending
+  | .directive .attrDictWithKeyword => Printer.printAttrDictFormat ctx op opType consumed true pending
+  | .directive .operands => Printer.printOperandsFormat ctx op pending
+  | .directive .results => return pending
+  | .directive (.typeOf .operands) => Printer.printCommaTypes (Printer.operandTypes ctx op) pending
+  | .directive (.typeOf .results) => Printer.printCommaTypes (Printer.resultTypes ctx op) pending
+  | .directive (.functionalType ins outs) =>
+      let insTys := match ins with
+        | .operands => Printer.operandTypes ctx op
+        | .results => Printer.resultTypes ctx op
+      let outTys := match outs with
+        | .operands => Printer.operandTypes ctx op
+        | .results => Printer.resultTypes ctx op
+      Printer.printFunctionalTypeBody insTys outTys pending
+  | .directive .regions =>
+      let n := op.getNumRegions! ctx
+      if n = 0 then return pending
+      if pending then IO.print " "
+      for i in 0...n do
+        if i > 0 then IO.print " "
+        printRegion ctx ((op.getRegion! ctx i).get! ctx) pretty indent
+      return true
+  | .directive .successors =>
+      let n := op.getNumSuccessors! ctx
+      if n = 0 then return pending
+      if pending then IO.print " "
+      IO.print s!"^{(op.getSuccessor! ctx 0).id}"
+      for i in 1...n do
+        IO.print s!", ^{(op.getSuccessor! ctx i).id}"
+      return true
+  | .optional thenElems anchor elseElems =>
+      let present := match thenElems[anchor]? with
+        | some a => Printer.isAnchorPresent ctx op opType a
+        | none => false
+      if present then printFormatElements ctx op opType consumed thenElems pretty indent pending
+      else printFormatElements ctx op opType consumed elseElems pretty indent pending
+
+partial def printFormatElements (ctx : IRContext OpCode) (op : OperationPtr) (opType : OpCode)
+    (consumed : List String) (elems : Array AssemblyFormat.Element) (pretty : Bool) (indent : Nat)
+    (pending : Bool) : IO Bool := do
+  let mut p := pending
+  for el in elems do
+    p ← printFormatElement ctx op opType consumed el pretty indent p
+  return p
+
+/-- Print an operation using a declarative assembly format. -/
+partial def printWithFormat (ctx : IRContext OpCode) (op : OperationPtr) (opType : OpCode)
+    (fmt : AssemblyFormat.Format) (pretty : Bool) (indent : Nat) : IO Unit := do
+  let consumed := AssemblyFormat.Format.attrVarNames fmt
+  let _ ← printFormatElements ctx op opType consumed fmt pretty indent true
+  pure ()
+
+/-- Print a function body region, eliding the entry block's label and arguments
+    (they appear in the function signature). -/
+partial def printFuncBodyRegion (ctx : IRContext OpCode) (entryPtr : BlockPtr) (pretty : Bool)
+    (indent : Nat) : IO Unit := do
+  IO.println "{"
+  match (entryPtr.get! ctx).firstOp with
+  | some firstOp => printOpList ctx firstOp pretty (indent + 1)
+  | none => pure ()
+  match (entryPtr.get! ctx).next with
+  | some nextBlock => printBlockList ctx nextBlock pretty (indent + 1)
+  | none => pure ()
+  printIndent indent
+  IO.print "}"
+
+/-- Custom (pretty) printer for `func.func`, mirroring MLIR's
+    `hasCustomAssemblyFormat`. Prints `func.func @name(%args) -> results { body }`. -/
+partial def printFuncFunc (ctx : IRContext OpCode) (op : OperationPtr) (pretty : Bool)
+    (indent : Nat) : IO Unit := do
+  let props := op.getProperties! ctx (.func .func)
+  let symName := match props.sym_name with
+    | some s => String.fromUTF8! s.value
+    | none => ""
+  let funcType? : Option FunctionType :=
+    match props.extra.entries.find? (fun e => e.1 = "function_type".toUTF8) with
+    | some (_, .functionType ft) => some ft
+    | _ => none
+  IO.print s!"func.func @{symName}("
+  match (op.getRegion! ctx 0).get! ctx |>.firstBlock with
+  | some entryPtr =>
+    let nargs := entryPtr.getNumArguments! ctx
+    for i in 0...nargs do
+      if i > 0 then IO.print ", "
+      let arg := entryPtr.getArgument i
+      IO.print s!"%arg{entryPtr.id}_{i}: {(arg.get! ctx).type}"
+    IO.print ")"
+    let outs := (funcType?.map (·.outputs)).getD #[]
+    if outs.size = 1 then
+      IO.print s!" -> {outs[0]!}"
+    else if outs.size > 1 then
+      IO.print " -> ("
+      IO.print s!"{outs[0]!}"
+      for i in 1...outs.size do
+        IO.print s!", {outs[i]!}"
+      IO.print ")"
+    let extraEntries := props.extra.entries.filter (fun e => e.1 ≠ "function_type".toUTF8)
+    if extraEntries.size > 0 then
+      IO.print " attributes "
+      IO.print (DictionaryAttr.fromArray extraEntries)
+    IO.print " "
+    printFuncBodyRegion ctx entryPtr pretty indent
+  | none =>
+    IO.print ") {}"
+
+partial def printOperation (ctx: IRContext OpCode) (op: OperationPtr) (pretty : Bool := false) (indent: Nat := 0) : IO Unit := do
   let opStruct := op.get! ctx
+  let opType := opStruct.opType
+  /- Custom (pretty) syntax dispatch. Operations with a dedicated hook
+     (`func.func`) or a registered declarative assembly format are printed in
+     their custom form; everything else falls through to the generic form. -/
+  if pretty then
+    match opType with
+    | .func .func =>
+        printIndent indent
+        printFuncFunc ctx op pretty indent
+        IO.println ""
+        return
+    | _ =>
+      match AssemblyFormat.OpCode.assemblyFormat? opType with
+      | some fmt =>
+          printIndent indent
+          printOpResults ctx op
+          IO.print s!"{String.fromUTF8! opType.name}"
+          printWithFormat ctx op opType fmt pretty indent
+          IO.println ""
+          return
+      | none => pure ()
   printIndent indent
   printOpResults ctx op
   /- Unregistered operations store their original operation name in the properties. -/
@@ -190,11 +461,11 @@ partial def printOperation (ctx: IRContext OpCode) (op: OperationPtr) (indent: N
   printOpProperties ctx op
   if op.getNumRegions! ctx > 0 then
     IO.print " "
-    printRegions ctx op indent
+    printRegions ctx op pretty indent
   printOpAttrDict ctx op
   printOperationType ctx op
   IO.println ""
 end
 
-partial def printModule (ctx: IRContext OpCode) (op: OperationPtr) : IO Unit := do
-  printOperation ctx op
+partial def printModule (ctx: IRContext OpCode) (op: OperationPtr) (pretty : Bool := false) : IO Unit := do
+  printOperation ctx op pretty
diff --git a/VeirOpt.lean b/VeirOpt.lean
index 3cd256079..c8b9f0cad 100644
--- a/VeirOpt.lean
+++ b/VeirOpt.lean
@@ -49,6 +49,8 @@ structure VeirOptArgs where
   passes : PassPipeline OpCode
   /-- Whether to accept ops/types/attrs from unregistered dialects. -/
   allowUnregisteredDialect : Bool
+  /-- Whether to print operations using their custom (pretty) assembly format. -/
+  pretty : Bool
 
 /--
   Parse the `-p` flag to construct a pass pipeline.
@@ -76,20 +78,23 @@ def parseArgs (args : List String) : Except String VeirOptArgs := do
   -- Consume `--allow-unregistered-dialect` if present.
   let allowUnregisteredDialect := flags.contains "--allow-unregistered-dialect"
   let flags := flags.filter (· != "--allow-unregistered-dialect")
+  -- Consume `--pretty` if present.
+  let pretty := flags.contains "--pretty"
+  let flags := flags.filter (· != "--pretty")
   -- If anything survived, it was unrecognized and we error out.
   if let some flag := flags.head? then
     .error s!"Unrecognized flag '{flag}'."
 
   if positional.length == 0 then -- read from stdin
-    return { filename := none, passes := pipeline, allowUnregisteredDialect }
+    return { filename := none, passes := pipeline, allowUnregisteredDialect, pretty }
 
   let [filename] := positional
     | .error "Expected exactly one positional argument for the input filename."
 
   if filename == "-" then
-    return { filename := none, passes := pipeline, allowUnregisteredDialect }
+    return { filename := none, passes := pipeline, allowUnregisteredDialect, pretty }
 
-  return { filename := some filename, passes := pipeline, allowUnregisteredDialect }
+  return { filename := some filename, passes := pipeline, allowUnregisteredDialect, pretty }
 
 def getFileContent (filename : Option String) : ExceptT String IO ByteArray := do
   if let some f := filename then
@@ -126,7 +131,7 @@ def main (args : List String) : IO Unit := do
     IO.eprintln s!"Error: {errMsg}"
     IO.eprintln "Usage: veir-opt <filename> [-p=\"pass1,pass2,...\"] [--allow-unregistered-dialect]"
     IO.Process.exit 1
-  | .ok { filename, passes, allowUnregisteredDialect } =>
+  | .ok { filename, passes, allowUnregisteredDialect, pretty } =>
     match ← parseOperation filename allowUnregisteredDialect with
     | .error errMsg =>
       IO.eprintln errMsg
@@ -142,4 +147,5 @@ def main (args : List String) : IO Unit := do
           IO.eprintln s!"Error: {errMsg}"
           IO.Process.exit 1
         | .ok finalCtx =>
-          Veir.Printer.printOperation finalCtx op
+          Veir.Printer.printOperation finalCtx op pretty
+