diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean
index c8c46aeb8..7048ac4d4 100644
--- a/Strata/DDM/AST.lean
+++ b/Strata/DDM/AST.lean
@@ -16,6 +16,7 @@ set_option autoImplicit false
 
 public section
 namespace Strata
+open Std (ToFormat Format format)
 
 abbrev DialectName := String
 
@@ -233,7 +234,25 @@ 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
+
+instance : ToFormat SourceRange where
+ format fr := f!"{fr.start}-{fr.stop}"
+
+inductive Uri where
+  | file (path: String)
+  deriving DecidableEq, Repr
+
+instance : ToFormat Uri where
+ format fr := match fr with | .file path => path
+
+structure FileRange where
+  file: Uri
+  range: Strata.SourceRange
+  deriving DecidableEq, Repr
+
+instance : ToFormat FileRange where
+ format fr := f!"{fr.file}:{fr.range}"
 
 namespace SourceRange
 
diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean
index b691d2e29..e0fcee0e5 100644
--- a/Strata/DDM/Ion.lean
+++ b/Strata/DDM/Ion.lean
@@ -183,7 +183,7 @@ private protected def asList (v : Ion SymbolId) : FromIonM { a : Array (Ion Symb
   match v with
   | .mk (.list args) =>
     return .mk args (by simp; omega)
-  | _ => throw s!"Expected list"
+  | x => throw s!"Expected list but got {repr x}"
 
 private protected def asSexp (name : String) (v : Ion SymbolId) : FromIonM ({ a : Array (Ion SymbolId) // a.size > 0 ∧ sizeOf a < sizeOf v}) :=
   match v with
@@ -284,7 +284,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 {repr a}."
   let entries := a[0]
   let .isTrue p := inferInstanceAs (Decidable (entries.size = 2))
     | throw s!"Expected symbol table and value in dialect."
@@ -1294,6 +1294,11 @@ private instance : FromIon Dialect where
 
 end Dialect
 
+structure StrataFile where
+  filePath : String
+  program : Program
+  deriving Inhabited
+
 namespace Program
 
 private instance : CachedToIon Program where
@@ -1319,7 +1324,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 =>
@@ -1334,5 +1339,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 p : 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 f1f6726ea..b77f9152c 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
-
-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
-
-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,8 +73,7 @@ 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)
 
 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}"
diff --git a/Strata/DL/Imperative/SMTUtils.lean b/Strata/DL/Imperative/SMTUtils.lean
index 832238382..8373de3ab 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 VC_folder_name: String := "vcs"
 
@@ -169,8 +170,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/Boogie/DDMTransform/Translate.lean b/Strata/Languages/Boogie/DDMTransform/Translate.lean
index c5104f923..677327978 100644
--- a/Strata/Languages/Boogie/DDMTransform/Translate.lean
+++ b/Strata/Languages/Boogie/DDMTransform/Translate.lean
@@ -47,10 +47,8 @@ def TransM.error [Inhabited α] (msg : String) : TransM α := do
 
 def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative.MetaData Boogie.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 := ⟨ MetaData.fileRange, .fileRange ⟨ uri, startPos, endPos ⟩ ⟩
+  let fileRangeElt := ⟨ MetaData.fileRange, .fileRange ⟨ uri, sr.start, sr.stop ⟩ ⟩
   #[fileRangeElt]
 
 def getOpMetaData (op : Operation) : TransM (Imperative.MetaData Boogie.Expression) :=
diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean
index a23a544c1..67b893f2c 100644
--- a/Strata/Languages/Boogie/Verifier.lean
+++ b/Strata/Languages/Boogie/Verifier.lean
@@ -11,12 +11,14 @@ import Strata.Languages.Boogie.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 encodeBoogie (ctx : Boogie.SMT.Context) (prelude : SolverM Unit) (ts : List Term) :
@@ -113,7 +115,7 @@ instance : ToFormat Result where
 
 def VC_folder_name: String := "vcs"
 
-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
@@ -121,14 +123,15 @@ 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 (vars : List (IdentT LMonoTy Visibility)) (ans : String)
+def solverResult (vars : List (IdentT LMonoTy Visibility)) (output : IO.Process.Output)
     (ctx : SMT.Context) (E : EncoderState) :
   Except Format Result := do
-  let pos := (ans.find (fun c => c == '\n')).byteIdx
-  let verdict := (ans.take pos).trim
-  let rest := ans.drop pos
+  let stdout := output.stdout
+  let pos := (stdout.find (fun c => c == '\n')).byteIdx
+  let verdict := (stdout.take pos).trim
+  let rest := stdout.drop pos
   match verdict with
   | "sat"     =>
     let rawModel ← getModel rest
@@ -141,17 +144,21 @@ def solverResult (vars : List (IdentT LMonoTy Visibility)) (ans : String)
     | .error _model_err => (.ok (.sat []))
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | _     =>  .error ans
+  | _     =>  .error s!"stderr:{output.stderr}\nsolver stdout: {output.stdout}\n"
 
 open Imperative
 
-def formatPositionMetaData [BEq P.Ident] [ToFormat P.Expr] (md : MetaData P): Option Format := do
+def formatPositionMetaData [BEq P.Ident] [ToFormat P.Expr]
+  (files: Map Strata.Uri Lean.FileMap)
+  (md : MetaData P): Option Format := do
   let fileRangeElem ← md.findElem MetaData.fileRange
   match fileRangeElem.value with
-  | .fileRange m =>
-    let baseName := match m.file with
+  | .fileRange fileRange =>
+    let fileMap := (files.find? fileRange.file).get!
+    let startPos := fileMap.toPosition fileRange.range.start
+    let baseName := match fileRange.file with
                     | .file path => (path.splitToList (· == '/')).getLast!
-    return f!"{baseName}({m.start.line}, {m.start.column})"
+    return f!"{baseName}({startPos.line}, {startPos.column})"
   | _ => none
 
 structure VCResult where
@@ -220,8 +227,8 @@ def dischargeObligation
   let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter
   if options.verbose then IO.println s!"Wrote problem to {filename}."
   let flags := getSolverFlags options smtsolver
-  let solver_out ← runSolver smtsolver (#[filename] ++ flags)
-  match solverResult vars solver_out ctx estate with
+  let output ← runSolver smtsolver (#[filename] ++ flags)
+  match solverResult vars output ctx estate with
   | .error e => return .error e
   | .ok result => return .ok (result, estate)
 
@@ -290,7 +297,7 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
         -- let rand_suffix ← IO.rand 0 0xFFFFFFFF
         let ans ←
             IO.toEIO
-              (fun e => f!"{e}")
+              (fun e => f!"IO error: {e}")
               (dischargeObligation options
                 (ProofObligation.getVars obligation) smtsolver
                   (Imperative.smt2_filename obligation.label)
@@ -364,35 +371,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 : Boogie.VCResult) : Option Diagnostic := do
-  -- Only create a diagnostic if the result is not .unsat (i.e., verification failed)
+def toDiagnosticModel (vcr : Boogie.VCResult) : Option DiagnosticModel := do
   match vcr.result with
   | .unsat => none  -- Verification succeeded, no diagnostic
   | result =>
-    -- Extract file range from metadata
     let fileRangeElem ← vcr.obligation.metadata.findElem Imperative.MetaData.fileRange
     match fileRangeElem.value with
-    | .fileRange range =>
+    | .fileRange fileRange =>
       let message := match result with
         | .sat _ => "assertion does not hold"
         | .unknown => "assertion verification result is unknown"
         | .err msg => s!"verification error: {msg}"
         | _ => "verification failed"
+
       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 : Boogie.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 937f39684..a0d33169c 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -14,34 +14,30 @@ namespace Laurel
 
 open 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 := StateM TransState
 
-def TransM.run (ictx : InputContext) (m : TransM α) : (α × Array String) :=
-  let (v, s) := StateT.run m { inputCtx := ictx, errors := #[] }
+def TransM.run (uri : Uri) (m : TransM α) : (α × Array String) :=
+  let (v, s) := StateT.run m { uri := uri, errors := #[] }
   (v, s.errors)
 
 def TransM.error [Inhabited α] (msg : String) : TransM α := do
   modify fun s => { s with errors := s.errors.push msg }
   return panic msg
 
-def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative.MetaData Boogie.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 Boogie.Expression :=
+  let fileRangeElt := ⟨ Imperative.MetaDataElem.Field.label "fileRange", .fileRange ⟨ uri, sr.start, sr.stop ⟩ ⟩
   #[fileRangeElt]
 
 def getArgMetaData (arg : Arg) : TransM (Imperative.MetaData Boogie.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
@@ -64,16 +60,16 @@ def translateIdent (arg : Arg) : TransM Identifier := do
 def translateBool (arg : Arg) : TransM Bool := do
   match arg with
   | .expr (.fn _ name) =>
-    if name == q`Laurel.boolTrue then
+    if name == q`Init.boolTrue then
       return true
-    else if name == q`Laurel.boolFalse then
+    else if name == q`Init.boolFalse then
       return false
     else
       TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr name}"
   | .op op =>
-    if op.name == q`Laurel.boolTrue then
+    if op.name == q`Init.boolTrue then
       return true
-    else if op.name == q`Laurel.boolFalse then
+    else if op.name == q`Init.boolFalse then
       return false
     else
       TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr op.name}"
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 860a5b675..81cdc79a3 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -7,25 +7,7 @@
 -- Minimal Laurel dialect for AssertFalse example
 import Strata
 
-#dialect
-dialect Laurel;
+namespace Strata
+namespace Laurel
 
-
-// Boolean literals
-type bool;
-fn boolTrue : bool => "true";
-fn boolFalse : bool => "false";
-
-category StmtExpr;
-op literalBool (b: bool): StmtExpr => b;
-
-op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";\n";
-op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";\n";
-op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{\n" stmts "}\n";
-
-category Procedure;
-op procedure (name : Ident, body : StmtExpr) : Procedure => "procedure " name "() " 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 000000000..3c638618e
--- /dev/null
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -0,0 +1,13 @@
+dialect Laurel;
+
+category StmtExpr;
+op literalBool (b: Bool): StmtExpr => b;
+
+op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";\n";
+op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";\n";
+op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{\n" stmts "}\n";
+
+category Procedure;
+op procedure (name : Ident, body : StmtExpr) : Procedure => "procedure " name "() " body:0;
+
+op program (staticProcedures: Seq Procedure): Command => staticProcedures;
diff --git a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
index 06921f0b6..6a055ffd8 100644
--- a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
@@ -82,8 +82,12 @@ def verifyToVcResults (smtsolver : String) (program : Program)
   EIO.toIO (fun f => IO.Error.userError (toString f))
       (Boogie.verify smtsolver boogieProgram 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 92b0247dc..2bc09f1df 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -13,8 +13,12 @@ import Strata.Languages.Python.Python
 import Strata.DDM.Integration.Java.Gen
 import StrataTest.Transform.ProcedureInlining
 
+import Strata.Languages.Laurel.Grammar.LaurelGrammar
+import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
+import Strata.Languages.Laurel.LaurelToBoogieTranslator
+
 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
@@ -173,7 +177,7 @@ def readPythonStrata (path : String) : IO Strata.Program := do
   let bytes ← Strata.Util.readBinInputSource path
   if ! bytes.startsWith Ion.binaryVersionMarker 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
 
@@ -229,6 +233,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 (laurelProgram, transErrors) := Laurel.TransM.run (Strata.Uri.file strataFile.filePath) (Laurel.parseProgram strataFile.program)
+      if transErrors.size > 0 then
+        exitFailure s!"Translation errors in {strataFile.filePath}: {transErrors}"
+
+      combinedProgram := {
+        staticProcedures := combinedProgram.staticProcedures ++ laurelProgram.staticProcedures
+        staticFields := combinedProgram.staticFields ++ laurelProgram.staticFields
+        types := combinedProgram.types ++ laurelProgram.types
+      }
+
+    let diagnostics ← Laurel.verifyToDiagnosticModels "z3" combinedProgram
+
+    -- Print diagnostics to stdout
+    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,
@@ -237,6 +281,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 64c6a5e3d..924995c8f 100644
--- a/StrataTest/DDM/Integration/Java/TestGen.lean
+++ b/StrataTest/DDM/Integration/Java/TestGen.lean
@@ -290,7 +290,7 @@ elab "#testCompile" : command => do
 
   let result ← IO.Process.output {
     cmd := "javac"
-    args := #["--enable-preview", "--release", "17"] ++ filePaths
+    args := filePaths
   }
 
   IO.FS.removeDirAll dir
@@ -309,7 +309,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
@@ -321,4 +321,58 @@ elab "#testRoundtrip" : command => do
 
 #testRoundtrip
 
+-- Test 13: Roundtrip with fromIonFiles - verify Lean can read Java-generated Ion array format
+-- Depends on testdata/comprehensive-files.ion (generated by Tools/Java/regenerate-testdata.sh)
+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/testdata/comprehensive-files.ion b/StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion
new file mode 100644
index 000000000..9361a13ce
Binary files /dev/null and b/StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion differ
diff --git a/StrataTest/Languages/Laurel/Grammar/TestGrammar.lean b/StrataTest/Languages/Laurel/Grammar/TestGrammar.lean
index 441fd7aae..a56d3faa0 100644
--- a/StrataTest/Languages/Laurel/Grammar/TestGrammar.lean
+++ b/StrataTest/Languages/Laurel/Grammar/TestGrammar.lean
@@ -15,7 +15,7 @@ open StrataTest.DDM
 namespace Laurel
 
 def testAssertFalse : IO Unit := do
-  let laurelDialect: Strata.Dialect := Laurel
+  let laurelDialect: Strata.Dialect := Strata.Laurel.Laurel
   let filePath := "StrataTest/Languages/Laurel/Examples/Fundamentals/1. AssertFalse.lr.st"
   let result ← testGrammarFile laurelDialect filePath
 
@@ -23,4 +23,4 @@ def testAssertFalse : IO Unit := do
     throw (IO.userError "Test failed: formatted output does not match input")
 
 #guard_msgs in
-#eval testAssertFalse
+#eval! testAssertFalse
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index b674c2cbb..715e64923 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -16,19 +16,20 @@ open StrataTest.Util
 open Strata
 open Strata.Elab (parseStrataProgramFromDialect)
 
+namespace Strata
 namespace Laurel
 
 def processLaurelFile (filePath : String) : IO (Array Diagnostic) := do
   let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
   let (inputContext, strataProgram) ← parseStrataProgramFromDialect dialects Laurel.name filePath
 
-  -- Convert to Laurel.Program using parseProgram (handles unwrapping the program operation)
-  let (laurelProgram, transErrors) := Laurel.TransM.run inputContext (Laurel.parseProgram strataProgram)
+  let uri := Strata.Uri.file filePath
+  let (laurelProgram, transErrors) := Laurel.TransM.run uri (Laurel.parseProgram strataProgram)
   if transErrors.size > 0 then
     throw (IO.userError s!"Translation errors: {transErrors}")
 
-  -- Verify the program
-  let diagnostics ← Laurel.verifyToDiagnostics "z3" laurelProgram
+  let files := Map.insert Map.empty uri inputContext.fileMap
+  let diagnostics ← Laurel.verifyToDiagnostics "z3" files laurelProgram
 
   pure diagnostics
 
diff --git a/StrataVerify.lean b/StrataVerify.lean
index 65f71a6a0..87b076058 100644
--- a/StrataVerify.lean
+++ b/StrataVerify.lean
@@ -58,6 +58,7 @@ def main (args : List String) : IO UInt32 := do
   | .ok (opts, file) => do
     let text ← Strata.Util.readInputSource file
     let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file)
+    let files := Map.insert Map.empty (Strata.Uri.file file) inputCtx.fileMap
     let dctx := Elab.LoadedDialects.builtin
     let dctx := dctx.addDialect! Boogie
     let dctx := dctx.addDialect! C_Simp
@@ -87,7 +88,7 @@ def main (args : List String) : IO UInt32 := do
             else
               verify "z3" pgm inputCtx opts
         for vcResult in vcResults do
-          let posStr := match Boogie.formatPositionMetaData vcResult.obligation.metadata with
+          let posStr := match Boogie.formatPositionMetaData files vcResult.obligation.metadata with
                         | .none => "<none>"
                         | .some str => s!"{str}"
           println! f!"{posStr} [{vcResult.obligation.label}]: {vcResult.result}"
diff --git a/Tools/Java/.gitignore b/Tools/Java/.gitignore
index ea3c65522..20e2c280f 100644
--- a/Tools/Java/.gitignore
+++ b/Tools/Java/.gitignore
@@ -1,6 +1,7 @@
 # Generated during regenerate-testdata.sh (cleaned up after)
 src/main/java/com/strata/simple/
 *.class
+build/
 
 # Downloaded dependency
 ion-java-*.jar
diff --git a/Tools/Java/regenerate-testdata.sh b/Tools/Java/regenerate-testdata.sh
index 34dcbc361..114501184 100755
--- a/Tools/Java/regenerate-testdata.sh
+++ b/Tools/Java/regenerate-testdata.sh
@@ -31,4 +31,4 @@ echo "=== Verifying with Lean ==="
 (cd "$STRATA_ROOT" && lake exe strata print --include "$TESTDATA" "$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/Tools/Java/src/main/java/com/strata/test/GenerateTestData.java b/Tools/Java/src/main/java/com/strata/test/GenerateTestData.java
index ef95bcde1..372890a6d 100644
--- a/Tools/Java/src/main/java/com/strata/test/GenerateTestData.java
+++ b/Tools/Java/src/main/java/com/strata/test/GenerateTestData.java
@@ -12,26 +12,77 @@ 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(
             assign("x", add(num(1), neg(num(2)))),
             print("hello"),
             ifStmt(true, data(new byte[]{0x01, (byte)0xFF}), Optional.of(decimal(3.14))),
             ifStmt(false, block(List.of()), Optional.empty())));
-        
+
         IonList program = ion.newEmptyList();
         IonSexp header = ion.newEmptySexp();
         header.add(ion.newSymbol("program"));
         header.add(ion.newString("Simple"));
         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);
     }
 }