diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean
index 255be4b4..1077807c 100644
--- a/Strata/DDM/AST.lean
+++ b/Strata/DDM/AST.lean
@@ -8,6 +8,7 @@ module
 public import Std.Data.HashMap.Basic
 public import Strata.DDM.Util.ByteArray
 public import Strata.DDM.Util.Decimal
+public import Lean.Data.Position
 public import Strata.DDM.AST.Datatype
 
 import Std.Data.HashMap
@@ -18,6 +19,7 @@ set_option autoImplicit false
 
 public section
 namespace Strata
+open Std (ToFormat Format format)
 
 abbrev DialectName := String
 
@@ -271,7 +273,7 @@ structure SourceRange where
   start : String.Pos.Raw
   /-- One past the end of the range. -/
   stop : String.Pos.Raw
-deriving BEq, Inhabited, Repr
+deriving DecidableEq, Inhabited, Repr
 
 namespace SourceRange
 
@@ -279,8 +281,38 @@ def none : SourceRange := { start := 0, stop := 0 }
 
 def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0
 
+instance : ToFormat SourceRange where
+ format fr := f!"{fr.start}-{fr.stop}"
+
 end SourceRange
 
+inductive Uri where
+  | file (path: String)
+  deriving DecidableEq, Repr, Inhabited
+
+instance : ToFormat Uri where
+ format fr := match fr with | .file path => path
+
+structure FileRange where
+  file: Uri
+  range: Strata.SourceRange
+  deriving DecidableEq, Repr, Inhabited
+
+instance : ToFormat FileRange where
+ format fr := f!"{fr.file}:{fr.range}"
+
+structure File2dRange where
+  file: Uri
+  start: Lean.Position
+  ending: Lean.Position
+  deriving DecidableEq, Repr
+
+instance : ToFormat File2dRange where
+ format fr :=
+    let baseName := match fr.file with
+                    | .file path => (path.splitToList (· == '/')).getLast!
+    f!"{baseName}({fr.start.line}, {fr.start.column})-({fr.ending.line}, {fr.ending.column})"
+
 abbrev Arg := ArgF SourceRange
 abbrev Expr := ExprF SourceRange
 abbrev Operation := OperationF SourceRange
diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean
index 0c6bf973..34313c03 100644
--- a/Strata/DDM/Ion.lean
+++ b/Strata/DDM/Ion.lean
@@ -294,7 +294,7 @@ private def deserializeValue {α} (bs : ByteArray) (act : Ion SymbolId → FromI
       throw s!"Error reading Ion: {msg} (offset = {off})"
     | .ok a => pure a
   let .isTrue p := inferInstanceAs (Decidable (a.size = 1))
-    | throw s!"Expected single Ion value."
+    | throw s!"Expected single Ion value, but got {a.size} values."
   let entries := a[0]
   let .isTrue p := inferInstanceAs (Decidable (entries.size = 2))
     | throw s!"Expected symbol table and value in dialect."
@@ -1411,6 +1411,11 @@ private instance : FromIon Dialect where
 
 end Dialect
 
+structure StrataFile where
+  filePath : String
+  program : Program
+  deriving Inhabited
+
 namespace Program
 
 private instance : CachedToIon Program where
@@ -1436,7 +1441,7 @@ def fromIonFragment (f : Ion.Fragment)
     commands := ← fromIonFragmentCommands f
   }
 
-def fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
+def fileFromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
   let (hdr, frag) ←
     match Strata.Ion.Header.parse bytes with
     | .error msg =>
@@ -1451,5 +1456,60 @@ def fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray)
       throw s!"{name} program found when {dialect} expected."
     fromIonFragment frag dialects dialect
 
+def filesFromIon (dialects : DialectMap) (bytes : ByteArray) : Except String (List StrataFile) := do
+  let ctx ←
+    match Ion.deserialize bytes with
+    | .error (off, msg) => throw s!"Error reading Ion: {msg} (offset = {off})"
+    | .ok a =>
+      if h : a.size = 1 then
+        pure a[0]
+      else
+        throw s!"Expected single Ion value"
+
+  let .isTrue p := inferInstanceAs (Decidable (ctx.size = 2))
+    | throw "Expected symbol table and value"
+
+  let symbols ←
+    match SymbolTable.ofLocalSymbolTable ctx[0] with
+    | .error (p, msg) => throw s!"Error at {p}: {msg}"
+    | .ok symbols => pure symbols
+
+  let ionCtx : FromIonContext := ⟨symbols⟩
+
+  let ⟨filesList, _⟩ ← FromIonM.asList ctx[1]! ionCtx
+
+  let tbl := symbols
+  let filePathId := tbl.symbolId! "filePath"
+  let programId := tbl.symbolId! "program"
+
+  filesList.toList.mapM fun fileEntry => do
+    let fields ← FromIonM.asStruct0 fileEntry ionCtx
+
+    let some (_, filePathData) := fields.find? (·.fst == filePathId)
+      | throw "Could not find 'filePath' field"
+
+    let some (_, programData) := fields.find? (·.fst == programId)
+      | throw "Could not find 'program' field"
+
+    let filePath ← FromIonM.asString "filePath" filePathData ionCtx
+
+    let ⟨programValues, _⟩ ← FromIonM.asList programData ionCtx
+    let .isTrue ne := inferInstanceAs (Decidable (programValues.size ≥ 1))
+      | throw "Expected program header"
+
+    let hdr ← Ion.Header.fromIon programValues[0] ionCtx
+    let dialect ← match hdr with
+      | .program name => pure name
+      | .dialect _ => throw "Expected program, not dialect"
+
+    let frag : Ion.Fragment := {
+      symbols := symbols,
+      values := programValues,
+      offset := 1
+    }
+
+    let program ← fromIonFragment frag dialects dialect
+
+    pure { filePath := filePath, program := program }
+
 end Strata.Program
-end
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index 71e2fc5a..9a47ba58 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -6,6 +6,7 @@
 
 import Strata.DL.Imperative.PureExpr
 import Strata.DL.Util.DecidableEq
+import Strata.DDM.AST
 import Lean.Data.Position
 
 namespace Imperative
@@ -65,22 +66,6 @@ instance [Repr P.Ident] : Repr (MetaDataElem.Field P) where
       | .label s => f!"MetaDataElem.Field.label {s}"
     Repr.addAppParen res prec
 
-inductive Uri where
-  | file (path: String)
-  deriving DecidableEq, Repr, Inhabited
-
-instance : ToFormat Uri where
- format fr := match fr with | .file path => path
-
-structure FileRange where
-  file: Uri
-  start: Lean.Position
-  ending: Lean.Position
-  deriving DecidableEq, Repr, Inhabited
-
-instance : ToFormat FileRange where
- format fr := f!"{fr.file}:{fr.start}-{fr.ending}"
-
 /-- A metadata value, which can be either an expression, a message, or a fileRange -/
 inductive MetaDataElem.Value (P : PureExpr) where
   /-- Metadata value in the form of a structured expression. -/
@@ -88,13 +73,16 @@ inductive MetaDataElem.Value (P : PureExpr) where
   /-- Metadata value in the form of an arbitrary string. -/
   | msg (s : String)
   /-- Metadata value in the form of a fileRange. -/
-  | fileRange (r: FileRange)
+  | fileRange (r: Strata.FileRange)
+  /-- Metadata value in the form of a fileRange. -/
+  | file2dRange (r: Strata.File2dRange)
 
 instance [ToFormat P.Expr] : ToFormat (MetaDataElem.Value P) where
   format f := match f with
               | .expr e => f!"{e}"
               | .msg s => f!"{s}"
               | .fileRange r => f!"{r}"
+              | .file2dRange r => f!"{r}"
 
 instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
   reprPrec v prec :=
@@ -103,6 +91,7 @@ instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
       | .expr e => f!".expr {reprPrec e prec}"
       | .msg s => f!".msg {s}"
       | .fileRange fr => f!".fileRange {fr}"
+      | .file2dRange fr => f!".file2dRange {fr}"
     Repr.addAppParen res prec
 
 def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
@@ -110,6 +99,7 @@ def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
   | .expr e1, .expr e2 => e1 == e2
   | .msg m1, .msg m2 => m1 == m2
   | .fileRange r1, .fileRange r2 => r1 == r2
+  | .file2dRange r1, .file2dRange r2 => r1 == r2
   | _, _ => false
 
 instance [BEq P.Expr] : BEq (MetaDataElem.Value P) where
@@ -185,7 +175,7 @@ instance [Repr P.Expr] [Repr P.Ident] : Repr (MetaDataElem P) where
 
 def MetaData.fileRange : MetaDataElem.Field P := .label "fileRange"
 
-def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option Imperative.FileRange := do
+def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option Strata.FileRange := do
   let fileRangeElement <- md.findElem Imperative.MetaData.fileRange
   match fileRangeElement.value with
     | .fileRange fileRange =>
@@ -196,7 +186,7 @@ def MetaData.formatFileRange? {P} [BEq P.Ident] (md : MetaData P) (includeEnd? :
     Option Std.Format := do
   let fileRangeElem ← md.findElem MetaData.fileRange
   match fileRangeElem.value with
-  | .fileRange m =>
+  | .file2dRange m =>
     let baseName := match m.file with
                     | .file path => (path.splitToList (· == '/')).getLast!
     if includeEnd? then
diff --git a/Strata/DL/Imperative/SMTUtils.lean b/Strata/DL/Imperative/SMTUtils.lean
index 81c72f98..89a57819 100644
--- a/Strata/DL/Imperative/SMTUtils.lean
+++ b/Strata/DL/Imperative/SMTUtils.lean
@@ -115,7 +115,7 @@ def processModel {P : PureExpr} [ToFormat P.Ident]
     | none => .error f!"Cannot find model for id: {id}"
     | some p => .ok p.value
 
-def runSolver (solver : String) (args : Array String) : IO String := do
+def runSolver (solver : String) (args : Array String) : IO IO.Process.Output := do
   let output ← IO.Process.output {
     cmd := solver
     args := args
@@ -123,15 +123,16 @@ def runSolver (solver : String) (args : Array String) : IO String := do
   -- dbg_trace f!"runSolver: exitcode: {repr output.exitCode}\n\
   --                         stderr: {repr output.stderr}\n\
   --                         stdout: {repr output.stdout}"
-  return output.stdout
+  return output
 
 def solverResult {P : PureExpr} [ToFormat P.Ident]
     (typedVarToSMTFn : P.Ident → P.Ty → Except Format (String × Strata.SMT.TermType))
-    (vars : List P.TypedIdent) (ans : String)
+    (vars : List P.TypedIdent) (output : IO.Process.Output)
     (E : Strata.SMT.EncoderState) : Except Format (Result P.TypedIdent) := do
-  let pos := (ans.find (fun c => c == '\n' || c == '\r')).byteIdx
-  let verdict := ans.take pos
-  let rest := ans.drop pos
+  let stdout := output.stdout
+  let pos := (stdout.find (fun c => c == '\n' || c == '\r')).byteIdx
+  let verdict := stdout.take pos
+  let rest := stdout.drop pos
   match verdict with
   | "sat"     =>
     let rawModel ← getModel rest
@@ -139,7 +140,7 @@ def solverResult {P : PureExpr} [ToFormat P.Ident]
     .ok (.sat model)
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | other     =>  .error other
+  | _     =>  .error s!"stderr:{output.stderr}\nsolver stdout: {output.stdout}\n"
 
 def dischargeObligation {P : PureExpr} [ToFormat P.Ident]
   (encodeTerms : List Strata.SMT.Term → Strata.SMT.SolverM (List String × Strata.SMT.EncoderState))
@@ -160,8 +161,8 @@ def dischargeObligation {P : PureExpr} [ToFormat P.Ident]
       .ok "--produce-models"
     else
       return .error f!"Unsupported SMT solver: {smtsolver}"
-  let solver_out ← runSolver smtsolver #[filename, produce_models]
-  match solverResult typedVarToSMTFn vars solver_out estate with
+  let solver_output ← runSolver smtsolver #[filename, produce_models]
+  match solverResult typedVarToSMTFn vars solver_output estate with
   | .error e => return .error e
   | .ok result => return .ok (result, estate)
 
diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean
index 0ab640b0..f5deb5f9 100644
--- a/Strata/Languages/Core/DDMTransform/Translate.lean
+++ b/Strata/Languages/Core/DDMTransform/Translate.lean
@@ -50,7 +50,7 @@ def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative
   let startPos := ictx.fileMap.toPosition sr.start
   let endPos := ictx.fileMap.toPosition sr.stop
   let uri: Uri := .file file
-  let fileRangeElt := ⟨ MetaData.fileRange, .fileRange ⟨ uri, startPos, endPos ⟩ ⟩
+  let fileRangeElt := ⟨ MetaData.fileRange, .file2dRange ⟨ uri, startPos, endPos ⟩ ⟩
   #[fileRangeElt]
 
 def getOpMetaData (op : Operation) : TransM (Imperative.MetaData Core.Expression) :=
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 84038fdc..dd878074 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -11,12 +11,14 @@ import Strata.Languages.Core.SMTEncoder
 import Strata.DL.Imperative.MetaData
 import Strata.DL.Imperative.SMTUtils
 import Strata.DL.SMT.CexParser
+import Strata.DDM.AST
 
 ---------------------------------------------------------------------
 
 namespace Strata.SMT.Encoder
 
 open Strata.SMT.Encoder
+open Strata
 
 -- Derived from Strata.SMT.Encoder.encode.
 def encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit) (ts : List Term) :
@@ -135,7 +137,7 @@ def runSolver (solver : String) (args : Array String) : IO IO.Process.Output :=
   --                         stdout: {repr output.stdout}"
   return output
 
-def solverResult (vars : List (IdentT LMonoTy Visibility)) (output: IO.Process.Output)
+def solverResult (vars : List (IdentT LMonoTy Visibility)) (output : IO.Process.Output)
     (ctx : SMT.Context) (E : EncoderState) :
   Except Format Result := do
   let stdout := output.stdout
@@ -154,7 +156,7 @@ def solverResult (vars : List (IdentT LMonoTy Visibility)) (output: IO.Process.O
     | .error _model_err => (.ok (.sat []))
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | _     =>  .error (stdout ++ output.stderr)
+  | _     =>  .error s!"stderr:{output.stderr}\nsolver stdout: {output.stdout}\n"
 
 def getSolverPrelude : String → SolverM Unit
 | "z3" => do
@@ -463,46 +465,50 @@ def verify
   else
     panic! s!"DDM Transform Error: {repr errors}"
 
----------------------------------------------------------------------
-
-/-- A diagnostic produced by analyzing a file -/
-structure Diagnostic where
-  start : Lean.Position
-  ending : Lean.Position
+structure DiagnosticModel where
+  fileRange : Strata.FileRange
   message : String
   deriving Repr, BEq
 
-def toDiagnostic (vcr : Core.VCResult) : Option Diagnostic := do
-  -- Only create a diagnostic if verification failed.
+def toDiagnosticModel (vcr : Core.VCResult) : Option DiagnosticModel := do
   match vcr.result with
   | .pass => none  -- Verification succeeded, no diagnostic
-  | _ =>
-    -- Extract file range from metadata
+  | result =>
     let fileRangeElem ← vcr.obligation.metadata.findElem Imperative.MetaData.fileRange
     match fileRangeElem.value with
-    | .fileRange range =>
-      let message :=
-      match vcr.obligation.property with
-      | .assert =>
-          match vcr.smtResult with
-          | .sat _ => "assertion does not hold"
-          | .unknown => "assertion verification result is unknown"
-          | .err msg => s!"verification error: {msg}"
-          | _ => "verification failed"
-      | .cover =>
-          match vcr.smtResult with
-          | .unsat => "cover failed"
-          | .unknown => "cover status is unknown"
-          | .err msg => s!"verification error: {msg}"
-          | _ => "verification failed"
+    | .fileRange fileRange =>
+      let message := match result with
+        | .fail => "assertion does not hold"
+        | .unknown => "assertion could not be proved"
+        | .implementationError msg => s!"verification error: {msg}"
+        | _ => panic "impossible"
+
       some {
         -- Subtract headerOffset to account for program header we added
-        start := { line := range.start.line, column := range.start.column }
-        ending := { line := range.ending.line, column := range.ending.column }
+        fileRange := fileRange
         message := message
       }
     | _ => none
 
+structure Diagnostic where
+  start : Lean.Position
+  ending : Lean.Position
+  message : String
+  deriving Repr, BEq
+
+def toDiagnostic (files: Map Strata.Uri Lean.FileMap) (vcr : Core.VCResult) : Option Diagnostic := do
+  let modelOption := toDiagnosticModel vcr
+  modelOption.map (fun dm =>
+      let fileMap := (files.find? dm.fileRange.file).get!
+      let startPos := fileMap.toPosition dm.fileRange.range.start
+      let endPos := fileMap.toPosition dm.fileRange.range.stop
+      {
+        start := { line := startPos.line, column := startPos.column }
+        ending := { line := endPos.line, column := endPos.column }
+        message := dm.message
+      }
+    )
+
 end Strata
 
 ---------------------------------------------------------------------
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index 6ba5474f..ae117f67 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -13,33 +13,30 @@ import Strata.Languages.Core.Expressions
 namespace Laurel
 
 open Std (ToFormat Format format)
-open Strata (QualifiedIdent Arg SourceRange)
+open Strata (QualifiedIdent Arg SourceRange Uri FileRange)
 open Lean.Parser (InputContext)
-open Imperative (MetaData Uri FileRange)
+open Imperative (MetaData)
 
 structure TransState where
-  inputCtx : InputContext
+  uri : Uri
+  errors : Array String
 
 abbrev TransM := StateT TransState (Except String)
 
-def TransM.run (ictx : InputContext) (m : TransM α) : Except String α :=
-  match StateT.run m { inputCtx := ictx } with
+def TransM.run (uri : Uri) (m : TransM α) : Except String α :=
+  match StateT.run m { uri := uri, errors := #[] } with
   | .ok (v, _) => .ok v
   | .error e => .error e
 
 def TransM.error (msg : String) : TransM α :=
   throw msg
 
-def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative.MetaData Core.Expression :=
-  let file := ictx.fileName
-  let startPos := ictx.fileMap.toPosition sr.start
-  let endPos := ictx.fileMap.toPosition sr.stop
-  let uri : Uri := .file file
-  let fileRangeElt := ⟨ Imperative.MetaDataElem.Field.label "fileRange", .fileRange ⟨ uri, startPos, endPos ⟩ ⟩
+def SourceRange.toMetaData (uri : Uri) (sr : SourceRange) : Imperative.MetaData Core.Expression :=
+  let fileRangeElt := ⟨ Imperative.MetaDataElem.Field.label "fileRange", .fileRange ⟨ uri, sr.start, sr.stop ⟩ ⟩
   #[fileRangeElt]
 
 def getArgMetaData (arg : Arg) : TransM (Imperative.MetaData Core.Expression) :=
-  return SourceRange.toMetaData (← get).inputCtx arg.ann
+  return SourceRange.toMetaData (← get).uri arg.ann
 
 def checkOp (op : Strata.Operation) (name : QualifiedIdent) (argc : Nat) :
   TransM Unit := do
@@ -63,13 +60,13 @@ def translateBool (arg : Arg) : TransM Bool := do
   match arg with
   | .expr (.fn _ name) =>
     match name with
-    | q`Laurel.boolTrue => return true
-    | q`Laurel.boolFalse => return false
+    | q`Init.boolTrue => return true
+    | q`Init.boolFalse => return false
     | _ => TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr name}"
   | .op op =>
     match op.name with
-    | q`Laurel.boolTrue => return true
-    | q`Laurel.boolFalse => return false
+    | q`Init.boolTrue => return true
+    | q`Init.boolFalse => return false
     | _ => TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr op.name}"
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
@@ -151,8 +148,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
     | q`Laurel.block, #[arg0] =>
       let stmts ← translateSeqCommand arg0
       return .Block stmts none
-    | q`Laurel.boolTrue, _ => return .LiteralBool true
-    | q`Laurel.boolFalse, _ => return .LiteralBool false
+    | q`Laurel.literalBool, #[arg0] => return .LiteralBool (← translateBool arg0)
     | q`Laurel.int, #[arg0] =>
       let n ← translateNat arg0
       return .LiteralInt n
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 54e60016..81cdc79a 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -7,72 +7,7 @@
 -- Minimal Laurel dialect for AssertFalse example
 import Strata
 
-#dialect
-dialect Laurel;
+namespace Strata
+namespace Laurel
 
-// Types
-category LaurelType;
-op intType : LaurelType => "int";
-op boolType : LaurelType => "bool";
-
-category StmtExpr;
-
-op boolTrue() : StmtExpr => "true";
-op boolFalse() : StmtExpr => "false";
-op int(n : Num) : StmtExpr => n;
-
-// Variable declarations
-category OptionalType;
-op optionalType(varType: LaurelType): OptionalType => ":" varType;
-
-category OptionalAssignment;
-op optionalAssignment(value: StmtExpr): OptionalAssignment => ":=" value:0;
-
-op varDecl (name: Ident, varType: Option OptionalType, assignment: Option OptionalAssignment): StmtExpr
-  => @[prec(0)] "var " name varType assignment ";";
-
-// Identifiers/Variables
-op identifier (name: Ident): StmtExpr => name;
-op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
-
-// Assignment
-op assign (target: StmtExpr, value: StmtExpr): StmtExpr => target ":=" value ";";
-
-// Binary operators
-op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60)] lhs "+" rhs;
-op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "==" rhs;
-op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "!=" rhs;
-op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">" rhs;
-op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<" rhs;
-op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<=" rhs;
-op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">=" rhs;
-
-op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
-
-// If-else
-category OptionalElse;
-op optionalElse(stmts : StmtExpr) : OptionalElse => "else" stmts;
-
-op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option OptionalElse): StmtExpr =>
-  @[prec(20)] "if (" cond ") " thenBranch:0 elseBranch:0;
-
-op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";";
-op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";";
-op return (value : StmtExpr) : StmtExpr => "return " value ";";
-op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
-
-category Parameter;
-op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
-
-category ReturnParameters;
-op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")";
-
-category Procedure;
-op procedure (name : Ident, parameters: CommaSepBy Parameter,
-  returnParameters: Option ReturnParameters,
-  body : StmtExpr) : Procedure =>
-  "procedure " name "(" parameters ")" returnParameters body:0;
-
-op program (staticProcedures: Seq Procedure): Command => staticProcedures;
-
-#end
+#load_dialect "./LaurelGrammar.st"
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
new file mode 100644
index 00000000..6efdcaeb
--- /dev/null
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -0,0 +1,64 @@
+dialect Laurel;
+
+// Types
+category LaurelType;
+op intType : LaurelType => "int";
+op boolType : LaurelType => "bool";
+
+category StmtExpr;
+op literalBool (b: Bool): StmtExpr => b;
+op int(n : Num) : StmtExpr => n;
+
+// Variable declarations
+category OptionalType;
+op optionalType(varType: LaurelType): OptionalType => ":" varType;
+
+category OptionalAssignment;
+op optionalAssignment(value: StmtExpr): OptionalAssignment => ":=" value:0;
+
+op varDecl (name: Ident, varType: Option OptionalType, assignment: Option OptionalAssignment): StmtExpr
+  => @[prec(0)] "var " name varType assignment ";";
+
+// Identifiers/Variables
+op identifier (name: Ident): StmtExpr => name;
+op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
+
+// Assignment
+op assign (target: StmtExpr, value: StmtExpr): StmtExpr => target ":=" value ";";
+
+// Binary operators
+op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60)] lhs "+" rhs;
+op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "==" rhs;
+op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "!=" rhs;
+op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">" rhs;
+op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<" rhs;
+op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<=" rhs;
+op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">=" rhs;
+
+op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
+
+// If-else
+category OptionalElse;
+op optionalElse(stmts : StmtExpr) : OptionalElse => "else" stmts;
+
+op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option OptionalElse): StmtExpr =>
+  @[prec(20)] "if (" cond ") " thenBranch:0 elseBranch:0;
+
+op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";";
+op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";";
+op return (value : StmtExpr) : StmtExpr => "return " value ";";
+op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
+
+category Parameter;
+op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
+
+category ReturnParameters;
+op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")";
+
+category Procedure;
+op procedure (name : Ident, parameters: CommaSepBy Parameter,
+  returnParameters: Option ReturnParameters,
+  body : StmtExpr) : Procedure =>
+  "procedure " name "(" parameters ")" returnParameters body:0;
+
+op program (staticProcedures: Seq Procedure): Command => staticProcedures;
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index 7061bf5c..39da64e5 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -89,7 +89,7 @@ def translateExpr (expr : StmtExpr) : Core.Expression.Expr :=
 
 def getNameFromMd (md : Imperative.MetaData Core.Expression): String :=
   let fileRange := (Imperative.getFileRange md).get!
-  s!"({fileRange.start.column},{fileRange.start.line})"
+  s!"({fileRange.range.start})"
 
 /--
 Translate Laurel StmtExpr to Core Statements
@@ -222,8 +222,12 @@ def verifyToVcResults (smtsolver : String) (program : Program)
     EIO.toIO (fun f => IO.Error.userError (toString f))
       (Core.verify smtsolver coreProgram tempDir options))
 
-def verifyToDiagnostics (smtsolver : String) (program : Program): IO (Array Diagnostic)  := do
+def verifyToDiagnostics (smtsolver : String) (files: Map Strata.Uri Lean.FileMap) (program : Program): IO (Array Diagnostic) := do
   let results <- verifyToVcResults smtsolver program
-  return results.filterMap toDiagnostic
+  return results.filterMap (toDiagnostic files)
+
+def verifyToDiagnosticModels (smtsolver : String) (program : Program): IO (Array DiagnosticModel) := do
+  let results <- verifyToVcResults smtsolver program
+  return results.filterMap toDiagnosticModel
 
 end Laurel
diff --git a/StrataMain.lean b/StrataMain.lean
index d0ded56c..b57098d8 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -15,8 +15,12 @@ import Strata.Languages.Python.Python
 import Strata.Transform.CoreTransform
 import Strata.Transform.ProcedureInlining
 
+import Strata.Languages.Laurel.Grammar.LaurelGrammar
+import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
+import Strata.Languages.Laurel.LaurelToCoreTranslator
+
 def exitFailure {α} (message : String) : IO α := do
-  IO.eprintln (message  ++ "\n\nRun strata --help for additional help.")
+  IO.eprintln ("Exception: " ++ message  ++ "\n\nRun strata --help for additional help.")
   IO.Process.exit 1
 
 namespace Strata
@@ -175,7 +179,7 @@ def readPythonStrata (path : String) : IO Strata.Program := do
   let bytes ← Strata.Util.readBinInputSource path
   if ! Ion.isIonFile bytes then
     exitFailure s!"pyAnalyze expected Ion file"
-  match Strata.Program.fromIon Strata.Python.Python_map Strata.Python.Python.name bytes with
+  match Strata.Program.fileFromIon Strata.Python.Python_map Strata.Python.Python.name bytes with
   | .ok p => pure p
   | .error msg => exitFailure msg
 
@@ -242,6 +246,46 @@ def javaGenCommand : Command where
     | .program _ =>
       exitFailure "Expected a dialect file, not a program file."
 
+def deserializeIonToLaurelFiles (bytes : ByteArray) : IO (List Strata.StrataFile) := do
+  match Strata.Program.filesFromIon Strata.Laurel.Laurel_map bytes with
+  | .ok files => pure files
+  | .error msg => exitFailure msg
+
+def laurelAnalyzeCommand : Command where
+  name := "laurelAnalyze"
+  args := []
+  help := "Analyze a Laurel Ion program from stdin. Write diagnostics to stdout."
+  callback := fun _ _ => do
+    -- Read bytes from stdin
+    let stdinBytes ← (← IO.getStdin).readBinToEnd
+
+    let strataFiles ← deserializeIonToLaurelFiles stdinBytes
+
+    let mut combinedProgram : Laurel.Program := {
+      staticProcedures := []
+      staticFields := []
+      types := []
+    }
+
+    for strataFile in strataFiles do
+
+      let transResult := Laurel.TransM.run (Strata.Uri.file strataFile.filePath) (Laurel.parseProgram strataFile.program)
+      match transResult with
+      | .error transErrors => exitFailure s!"Translation errors in {strataFile.filePath}: {transErrors}"
+      | .ok laurelProgram =>
+
+        combinedProgram := {
+          staticProcedures := combinedProgram.staticProcedures ++ laurelProgram.staticProcedures
+          staticFields := combinedProgram.staticFields ++ laurelProgram.staticFields
+          types := combinedProgram.types ++ laurelProgram.types
+        }
+
+    let diagnostics ← Laurel.verifyToDiagnosticModels "z3" combinedProgram
+
+    IO.println s!"==== DIAGNOSTICS ===="
+    for diag in diagnostics do
+      IO.println s!"{Std.format diag.fileRange.file}:{diag.fileRange.range.start}-{diag.fileRange.range.stop}: {diag.message}"
+
 def commandList : List Command := [
       javaGenCommand,
       checkCommand,
@@ -250,6 +294,7 @@ def commandList : List Command := [
       diffCommand,
       pyAnalyzeCommand,
       pyTranslateCommand,
+      laurelAnalyzeCommand,
     ]
 
 def commandMap : Std.HashMap String Command :=
diff --git a/StrataTest/DDM/Integration/Java/TestGen.lean b/StrataTest/DDM/Integration/Java/TestGen.lean
index 439808ea..710223cf 100644
--- a/StrataTest/DDM/Integration/Java/TestGen.lean
+++ b/StrataTest/DDM/Integration/Java/TestGen.lean
@@ -300,7 +300,7 @@ elab "#testCompile" : command => do
 #testCompile
 
 -- Test 13: Roundtrip - verify Lean can read Java-generated Ion
--- Depends on testdata/comprehensive.ion (generated by Tools/Java/regenerate-testdata.sh)
+-- Depends on testdata/comprehensive.ion
 elab "#testRoundtrip" : command => do
   let env ← Lean.getEnv
   let state := Strata.dialectExt.getState env
@@ -308,7 +308,7 @@ elab "#testRoundtrip" : command => do
     | Lean.logError "Simple dialect not found"; return
   let dm := Strata.DialectMap.ofList! [Strata.initDialect, simple]
   let ionBytes ← IO.FS.readBinFile "StrataTest/DDM/Integration/Java/testdata/comprehensive.ion"
-  match Strata.Program.fromIon dm "Simple" ionBytes with
+  match Strata.Program.fileFromIon dm "Simple" ionBytes with
   | .error e => Lean.logError s!"Roundtrip test failed: {e}"
   | .ok prog =>
     if prog.commands.size != 1 then Lean.logError "Expected 1 command"; return
@@ -320,4 +320,58 @@ elab "#testRoundtrip" : command => do
 
 #testRoundtrip
 
+-- Test 14: Roundtrip with fromIonFiles - verify Lean can read Java-generated Ion array format
+-- Depends on testdata/comprehensive-files.ion
+elab "#testRoundtripFiles" : command => do
+  let env ← Lean.getEnv
+  let state := Strata.dialectExt.getState env
+  let some simple := state.loaded.dialects["Simple"]?
+    | Lean.logError "Simple dialect not found"; return
+  let dm := Strata.DialectMap.ofList! [Strata.initDialect, simple]
+  let ionBytes ← IO.FS.readBinFile "StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion"
+  match Strata.Program.filesFromIon dm ionBytes with
+  | .error e => Lean.logError s!"Roundtrip files test failed: {e}"
+  | .ok files =>
+    if files.length != 2 then
+      Lean.logError s!"Expected 2 files, got {files.length}"
+      return
+
+    -- Check first file
+    let file1 := files[0]!
+    if file1.filePath != "file1.st" then
+      Lean.logError s!"File 1: Expected path 'file1.st', got '{file1.filePath}'"
+      return
+    if file1.program.commands.size != 1 then
+      Lean.logError s!"File 1: Expected 1 command, got {file1.program.commands.size}"
+      return
+    let cmd1 := file1.program.commands[0]!
+    if cmd1.name != (⟨"Simple", "block"⟩ : Strata.QualifiedIdent) then
+      Lean.logError "File 1: Expected block command"; return
+    if let .seq _ _ stmts := cmd1.args[0]! then
+      if stmts.size != 2 then
+        Lean.logError s!"File 1: Expected 2 statements, got {stmts.size}"
+        return
+    else
+      Lean.logError "File 1: Expected seq argument"; return
+
+    -- Check second file
+    let file2 := files[1]!
+    if file2.filePath != "file2.st" then
+      Lean.logError s!"File 2: Expected path 'file2.st', got '{file2.filePath}'"
+      return
+    if file2.program.commands.size != 1 then
+      Lean.logError s!"File 2: Expected 1 command, got {file2.program.commands.size}"
+      return
+    let cmd2 := file2.program.commands[0]!
+    if cmd2.name != (⟨"Simple", "block"⟩ : Strata.QualifiedIdent) then
+      Lean.logError "File 2: Expected block command"; return
+    if let .seq _ _ stmts := cmd2.args[0]! then
+      if stmts.size != 3 then
+        Lean.logError s!"File 2: Expected 3 statements, got {stmts.size}"
+        return
+    else
+      Lean.logError "File 2: Expected seq argument"; return
+
+#testRoundtripFiles
+
 end Strata.Java.Test
diff --git a/StrataTest/DDM/Integration/Java/regenerate-testdata.sh b/StrataTest/DDM/Integration/Java/regenerate-testdata.sh
index d4acc313..7163658d 100755
--- a/StrataTest/DDM/Integration/Java/regenerate-testdata.sh
+++ b/StrataTest/DDM/Integration/Java/regenerate-testdata.sh
@@ -21,7 +21,7 @@ echo "=== Compiling Java ==="
 javac -cp "$JAR" $GEN_DIR/com/strata/simple/*.java $TESTDATA/GenerateTestData.java
 
 echo "=== Generating test data ==="
-java -cp "$JAR:$GEN_DIR:$TESTDATA" GenerateTestData "$TESTDATA/comprehensive.ion"
+java -cp "$JAR:$GEN_DIR:$TESTDATA" GenerateTestData "$TESTDATA/comprehensive.ion" "$TESTDATA/comprehensive-files.ion"
 
 echo "=== Cleaning up ==="
 rm -rf "$GEN_DIR"
@@ -31,4 +31,4 @@ echo "=== Verifying with Lean ==="
 (cd "$STRATA_ROOT" && lake exe strata print --include "$STRATA_ROOT/StrataTest/DDM/Integration/Java/$TESTDATA" "$STRATA_ROOT/StrataTest/DDM/Integration/Java/$TESTDATA/comprehensive.ion" 2>&1 | tail -1)
 
 echo ""
-echo "Done! Regenerated $TESTDATA/comprehensive.ion"
+echo "Done! Regenerated $TESTDATA/comprehensive.ion and $TESTDATA/comprehensive-files.ion"
diff --git a/StrataTest/DDM/Integration/Java/testdata/GenerateTestData.java b/StrataTest/DDM/Integration/Java/testdata/GenerateTestData.java
index e451b183..395ac4c7 100644
--- a/StrataTest/DDM/Integration/Java/testdata/GenerateTestData.java
+++ b/StrataTest/DDM/Integration/Java/testdata/GenerateTestData.java
@@ -10,6 +10,14 @@ public class GenerateTestData {
     public static void main(String[] args) throws Exception {
         var ion = IonSystemBuilder.standard().build();
         var serializer = new IonSerializer(ion);
+        generateSingleProgram(ion, serializer, args[0]);
+
+        if (args.length > 1) {
+            generateMultipleFiles(ion, serializer, args[1]);
+        }
+    }
+
+    private static void generateSingleProgram(IonSystem ion, IonSerializer serializer, String outPath) throws Exception {
         
         // AST covering: Num, Str, Ident, Bool, Decimal, ByteArray, Option, Seq, nesting
         Node ast = block(List.of(
@@ -25,11 +33,55 @@ public static void main(String[] args) throws Exception {
         program.add(header);
         program.add(serializer.serializeCommand(ast));
         
-        try (var out = new FileOutputStream(args[0])) {
+        try (var out = new FileOutputStream(outPath)) {
             var writer = IonBinaryWriterBuilder.standard().build(out);
             program.writeTo(writer);
             writer.close();
         }
-        System.out.println("Generated: " + args[0]);
+        System.out.println("Generated: " + outPath);
+    }
+
+    private static void generateMultipleFiles(IonSystem ion, IonSerializer serializer, String outPath) throws Exception {
+        Node ast1 = block(List.of(
+            assign("x", num(42)),
+            print("first file")));
+
+        IonList program1 = ion.newEmptyList();
+        IonSexp header1 = ion.newEmptySexp();
+        header1.add(ion.newSymbol("program"));
+        header1.add(ion.newString("Simple"));
+        program1.add(header1);
+        program1.add(serializer.serializeCommand(ast1));
+
+        Node ast2 = block(List.of(
+            assign("y", add(num(1), num(2))),
+            print("second file"),
+            ifStmt(true, block(List.of()), Optional.empty())));
+
+        IonList program2 = ion.newEmptyList();
+        IonSexp header2 = ion.newEmptySexp();
+        header2.add(ion.newSymbol("program"));
+        header2.add(ion.newString("Simple"));
+        program2.add(header2);
+        program2.add(serializer.serializeCommand(ast2));
+
+        IonList files = ion.newEmptyList();
+
+        IonStruct file1 = ion.newEmptyStruct();
+        file1.put("filePath", ion.newString("file1.st"));
+        file1.put("program", program1);
+        files.add(file1);
+
+        IonStruct file2 = ion.newEmptyStruct();
+        file2.put("filePath", ion.newString("file2.st"));
+        file2.put("program", program2);
+        files.add(file2);
+
+        try (var out = new FileOutputStream(outPath)) {
+            var writer = IonBinaryWriterBuilder.standard().build(out);
+            files.writeTo(writer);
+            writer.close();
+        }
+        System.out.println("Generated: " + outPath);
     }
 }
diff --git a/StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion b/StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion
new file mode 100644
index 00000000..9361a13c
Binary files /dev/null and b/StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion differ
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
index 03a18be6..05e80d79 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
@@ -10,6 +10,7 @@ import StrataTest.Languages.Laurel.TestExamples
 open StrataTest.Util
 open Strata
 
+namespace Strata
 namespace Laurel
 
 def program := r"
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index 04d65834..a35a49ba 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -10,6 +10,7 @@ import StrataTest.Languages.Laurel.TestExamples
 open StrataTest.Util
 open Strata
 
+namespace Strata
 namespace Laurel
 
 def program: String := r"
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
index f0467c36..27decdde 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
@@ -10,6 +10,7 @@ import StrataTest.Languages.Laurel.TestExamples
 open StrataTest.Util
 open Strata
 
+namespace Strata
 namespace Laurel
 
 def program := r"
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index d333b6a9..76d21655 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -17,20 +17,21 @@ open Strata
 open Strata.Elab (parseStrataProgramFromDialect)
 open Lean.Parser (InputContext)
 
+namespace Strata
 namespace Laurel
 
 def processLaurelFile (input : InputContext) : IO (Array Diagnostic) := do
   let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
   let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name input
 
-  -- Convert to Laurel.Program using parseProgram (handles unwrapping the program operation)
-  let laurelProgram ← match Laurel.TransM.run input (Laurel.parseProgram strataProgram) with
-    | .ok program => pure program
-    | .error errMsg => throw (IO.userError s!"Translation error: {errMsg}")
+  let uri := Strata.Uri.file input.fileName
+  let transResult := Laurel.TransM.run uri (Laurel.parseProgram strataProgram)
+  match transResult with
+  | .error transErrors => throw (IO.userError s!"Translation errors: {transErrors}")
+  | .ok laurelProgram =>
+    let files := Map.insert Map.empty uri input.fileMap
+    let diagnostics ← Laurel.verifyToDiagnostics "z3" files laurelProgram
 
-  -- Verify the program
-  let diagnostics ← Laurel.verifyToDiagnostics "z3" laurelProgram
-
-  pure diagnostics
+    pure diagnostics
 
 end Laurel