diff --git a/Strata/Backends/CBMC/GOTO.lean b/Strata/Backends/CBMC/GOTO.lean
index 132440f8af..77eab4f29e 100644
--- a/Strata/Backends/CBMC/GOTO.lean
+++ b/Strata/Backends/CBMC/GOTO.lean
@@ -5,6 +5,7 @@
 -/
 module
 
+import Strata.Backends.CBMC.GOTO.CoreCFGToGOTOPipeline
 import Strata.Backends.CBMC.GOTO.CoreToCProverGOTO
 import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
 import Strata.Backends.CBMC.GOTO.DefaultSymbols
diff --git a/Strata/Backends/CBMC/GOTO/CoreCFGToGOTOPipeline.lean b/Strata/Backends/CBMC/GOTO/CoreCFGToGOTOPipeline.lean
new file mode 100644
index 0000000000..d102b85238
--- /dev/null
+++ b/Strata/Backends/CBMC/GOTO/CoreCFGToGOTOPipeline.lean
@@ -0,0 +1,305 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Backends.CBMC.CollectSymbols
+public import Strata.Backends.CBMC.GOTO.CoreToCProverGOTO
+import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
+import Strata.Transform.StructuredToUnstructured
+import Strata.Languages.Core.StatementSemantics
+
+/-! ## Core-to-GOTO translation via CFG
+
+Alternative pipeline that translates Core procedures to CProver GOTO by going
+through the CFG representation:
+
+- **Structured body** → `stmtsToCFG` → `coreCFGToGotoTransform`
+- **CFG body** → `coreCFGToGotoTransform`
+
+This coexists with the direct path in `CoreToGOTOPipeline.lean`.
+-/
+
+namespace Strata
+
+public section
+
+/-! ### Rename helpers for Core commands (CmdExt) -/
+
+private def renameCoreCallArg
+    (rn : Std.HashMap String String)
+    : Core.CallArg Core.Expression → Core.CallArg Core.Expression
+  | .inArg e => .inArg (renameExpr rn e)
+  | .inoutArg id => .inoutArg (renameIdent rn id)
+  | .outArg id => .outArg (renameIdent rn id)
+
+private def renameCoreCommand
+    (rn : Std.HashMap String String)
+    : Core.Command → Core.Command
+  | .cmd c => .cmd (renameCmd rn c)
+  | .call procName callArgs md =>
+    .call procName (callArgs.map (renameCoreCallArg rn)) md
+
+private partial def renameCoreStmt
+    (rn : Std.HashMap String String)
+    : Core.Statement → Core.Statement
+  | .cmd c => .cmd (renameCoreCommand rn c)
+  | .block l stmts md =>
+    .block l (stmts.map (renameCoreStmt rn)) md
+  | .ite c t e md =>
+    .ite (c.map (renameExpr rn)) (t.map (renameCoreStmt rn)) (e.map (renameCoreStmt rn)) md
+  | .loop g m i body md =>
+    .loop (g.map (renameExpr rn)) (m.map (renameExpr rn))
+      (i.map (fun (l, e) => (l, renameExpr rn e)))
+      (body.map (renameCoreStmt rn)) md
+  | .exit l md => .exit l md
+  | .funcDecl d md => .funcDecl d md
+  | .typeDecl tc md => .typeDecl tc md
+
+private def renameCoreDetCFG
+    (rn : Std.HashMap String String)
+    (cfg : Core.DetCFG) : Core.DetCFG :=
+  { cfg with blocks := cfg.blocks.map fun (label, block) =>
+    (label, { cmds := block.cmds.map (renameCoreCommand rn),
+              transfer := match block.transfer with
+                | .condGoto cond lt lf md =>
+                  .condGoto (renameExpr rn cond) lt lf md
+                | .finish md => .finish md }) }
+
+/-! ### Core-specific CFG-to-GOTO translation -/
+
+/--
+Translate a Core `DetCFG` to CProver GOTO instructions.
+
+Like `detCFGToGotoTransform` but handles `Core.Command` (which includes
+`CmdExt.call`). The CFG should already have identifiers renamed via
+`renameCoreDetCFG`.
+-/
+def coreCFGToGotoTransform
+    (_Env : Core.Expression.TyEnv) (functionName : String)
+    (cfg : Core.DetCFG)
+    (trans : Imperative.GotoTransform Core.Expression.TyEnv)
+    : Except Std.Format (Imperative.GotoTransform Core.Expression.TyEnv) := do
+  let toExpr := Lambda.LExpr.toGotoExprCtx
+    (TBase := ⟨Core.ExpressionMetadata, Unit⟩) []
+  -- Verify entry block is first
+  match cfg.blocks with
+  | (firstLabel, _) :: _ =>
+    if firstLabel != cfg.entry then
+      throw f!"[coreCFGToGotoTransform] Entry label '{cfg.entry}' does not match \
+               first block label '{firstLabel}'."
+  | [] => pure ()
+  let mut trans := trans
+  let mut pendingPatches : Array (Nat × String) := #[]
+  let mut labelMap : Std.HashMap String Nat := {}
+  let mut loopContracts : Std.HashMap String (Imperative.MetaData Core.Expression) := {}
+  for (label, block) in cfg.blocks do
+    labelMap := labelMap.insert label trans.nextLoc
+    let srcLoc : CProverGOTO.SourceLocation :=
+      { CProverGOTO.SourceLocation.nil with function := functionName }
+    trans := Imperative.emitLabel label srcLoc trans
+    -- Translate each command
+    for cmd in block.cmds do
+      match cmd with
+      | .cmd c =>
+        trans ← Imperative.Cmd.toGotoInstructions trans.T functionName c trans
+      | .call procName callArgs _md =>
+        let lhs := Core.CallArg.getLhs callArgs
+        let args := Core.CallArg.getInputExprs callArgs
+        let argExprs ← args.mapM toExpr
+        let lhsExpr := match lhs with
+          | id :: _ =>
+            let name := Core.CoreIdent.toPretty id
+            let ty := match trans.T.context.types.find? id with
+              | some lty =>
+                match lty.toMonoTypeUnsafe.toGotoType with
+                | .ok gty => gty
+                | .error _ =>
+                  dbg_trace s!"warning: type conversion failed for {name}, defaulting to Integer"
+                  .Integer
+              | none =>
+                dbg_trace s!"warning: no type found for {name}, defaulting to Integer"
+                .Integer
+            CProverGOTO.Expr.symbol name ty
+          | [] => CProverGOTO.Expr.symbol "" .Empty
+        let calleeExpr := CProverGOTO.Expr.symbol procName
+          (CProverGOTO.Ty.mkCode (argExprs.map (·.type)) lhsExpr.type)
+        let callCode := CProverGOTO.Code.functionCall lhsExpr calleeExpr argExprs
+        let inst : CProverGOTO.Instruction :=
+          { type := .FUNCTION_CALL, code := callCode, locationNum := trans.nextLoc }
+        trans := { trans with
+          instructions := trans.instructions.push inst
+          nextLoc := trans.nextLoc + 1 }
+    -- Translate the transfer command
+    match block.transfer with
+    | .condGoto cond lt lf md =>
+      let transferSrcLoc := Imperative.metadataToSourceLoc md functionName trans.sourceText
+      let cond_expr ← toExpr cond
+      let hasLoopContract := md.any fun elem =>
+        elem.fld == Imperative.MetaData.specLoopInvariant ||
+        elem.fld == Imperative.MetaData.specDecreases
+      if hasLoopContract then
+        loopContracts := loopContracts.insert label md
+      let (trans', falseIdx) :=
+        Imperative.emitCondGoto (CProverGOTO.Expr.not cond_expr) transferSrcLoc trans
+      trans := trans'
+      pendingPatches := pendingPatches.push (falseIdx, lf)
+      let (trans', trueIdx) := Imperative.emitUncondGoto transferSrcLoc trans
+      trans := trans'
+      pendingPatches := pendingPatches.push (trueIdx, lt)
+    | .finish _md =>
+      pure ()
+  -- Second pass: resolve labels and annotate backward-edge GOTOs with loop contracts
+  let mut resolvedPatches : List (Nat × Nat) := []
+  for (idx, label) in pendingPatches do
+    match labelMap[label]? with
+    | some targetLoc =>
+      resolvedPatches := (idx, targetLoc) :: resolvedPatches
+      if let some md := loopContracts[label]? then
+        let instLoc := trans.instructions[idx]!.locationNum
+        if targetLoc ≤ instLoc then
+          let mut guard := trans.instructions[idx]!.guard
+          for elem in md do
+            if elem.fld == Imperative.MetaData.specLoopInvariant then
+              if let .expr e := elem.value then
+                let gotoExpr ← toExpr e
+                guard := guard.setNamedField "#spec_loop_invariant" gotoExpr
+            if elem.fld == Imperative.MetaData.specDecreases then
+              if let .expr e := elem.value then
+                let gotoExpr ← toExpr e
+                guard := guard.setNamedField "#spec_decreases" gotoExpr
+          trans := { trans with
+            instructions := trans.instructions.set! idx
+              { trans.instructions[idx]! with guard := guard } }
+    | none =>
+      throw f!"[coreCFGToGotoTransform] Unresolved label '{label}' referenced \
+               by GOTO at instruction index {idx}."
+  return Imperative.patchGotoTargets trans resolvedPatches
+
+/-! ### Pipeline wrapper -/
+
+/--
+Translate a Core procedure to CProver GOTO via the CFG representation.
+
+Mirrors `procedureToGotoCtx` but routes through `stmtsToCFG` +
+`coreCFGToGotoTransform` instead of the direct Stmt-to-GOTO path.
+-/
+def procedureToGotoCtxViaCFG
+    (Env : Core.Expression.TyEnv) (p : Core.Procedure)
+    (sourceText : Option String := none)
+    (axioms : List Core.Axiom := [])
+    (distincts :
+      List (Core.Expression.Ident × List Core.Expression.Expr) := [])
+    : Except Std.Format
+        (CoreToGOTO.CProverGOTO.Context × List Core.Function) := do
+  let pname := Core.CoreIdent.toPretty p.header.name
+  if !p.header.typeArgs.isEmpty then
+    .error f!"[procedureToGotoCtxViaCFG] Polymorphic procedures unsupported."
+  let ret_ty := CProverGOTO.Ty.Empty
+  let formals := p.header.inputs.keys.map Core.CoreIdent.toPretty
+  let formals_tys ← p.header.inputs.values.mapM Lambda.LMonoTy.toGotoType
+  let new_formals := formals.map (CProverGOTO.mkFormalSymbol pname ·)
+  let formals_tys : Map String CProverGOTO.Ty := formals.zip formals_tys
+  let outputs := p.header.outputs.keys.map Core.CoreIdent.toPretty
+  let new_outputs := outputs.map (CProverGOTO.mkLocalSymbol pname ·)
+  let locals_from_body := match p.body with
+    | .structured ss => (Imperative.Block.definedVars ss false).map Core.CoreIdent.toPretty
+    | .cfg c => c.blocks.flatMap (fun (_, blk) =>
+        blk.cmds.flatMap Core.Command.definedVars)
+      |>.map Core.CoreIdent.toPretty
+  let new_locals := locals_from_body.map (CProverGOTO.mkLocalSymbol pname ·)
+  let rn : Std.HashMap String String :=
+    (formals.zip new_formals ++ outputs.zip new_outputs ++ locals_from_body.zip new_locals).foldl
+      (init := {}) fun m (k, v) => m.insert k v
+  -- Seed the type environment with renamed input and output parameter types
+  let inputEntries : Map Core.Expression.Ident Core.Expression.Ty :=
+    (new_formals.zip p.header.inputs.values).map fun (n, ty) =>
+      (((n : Core.CoreIdent)), .forAll [] ty)
+  let outputEntries : Map Core.Expression.Ident Core.Expression.Ty :=
+    (new_outputs.zip p.header.outputs.values).map fun (n, ty) =>
+      (((n : Core.CoreIdent)), .forAll [] ty)
+  let Env' : Core.Expression.TyEnv :=
+    Lambda.TEnv.addInNewestContext (T := ⟨Core.ExpressionMetadata, Unit⟩)
+      Env (inputEntries ++ outputEntries)
+  -- Emit axioms as ASSUME instructions
+  let mut axiomInsts : Array CProverGOTO.Instruction := #[]
+  let mut axiomLoc : Nat := 0
+  for ax in axioms do
+    let gotoExpr ← Lambda.LExpr.toGotoExprCtx
+      (TBase := ⟨Core.ExpressionMetadata, Unit⟩) [] ax.e
+    if gotoExpr.hasUnsupportedQuantifierTypes then continue
+    axiomInsts := axiomInsts.push
+      { type := .ASSUME, locationNum := axiomLoc,
+        guard := gotoExpr,
+        sourceLoc := { CProverGOTO.SourceLocation.nil with
+          function := pname, comment := s!"axiom {ax.name}" } }
+    axiomLoc := axiomLoc + 1
+  -- Emit distinct declarations as pairwise != ASSUME instructions
+  for (dname, exprs) in distincts do
+    let gotoExprs ← exprs.mapM
+      (Lambda.LExpr.toGotoExprCtx (TBase := ⟨Core.ExpressionMetadata, Unit⟩) [])
+    for i in List.range gotoExprs.length do
+      for j in List.range gotoExprs.length do
+        if i < j then
+          let ei := gotoExprs[i]!
+          let ej := gotoExprs[j]!
+          let neqExpr : CProverGOTO.Expr :=
+            { id := .binary .NotEqual, type := .Boolean, operands := [ei, ej] }
+          let srcLoc : CProverGOTO.SourceLocation :=
+            { CProverGOTO.SourceLocation.nil with
+                function := pname
+                comment := s!"distinct {Core.CoreIdent.toPretty dname}" }
+          axiomInsts := axiomInsts.push
+            { type := .ASSUME, locationNum := axiomLoc, guard := neqExpr, sourceLoc := srcLoc }
+          axiomLoc := axiomLoc + 1
+  -- Build the CFG (from structured body or use existing CFG)
+  let (cfg, liftedFuncs) ← match p.body with
+    | .structured ss => do
+      let (liftedFuncs, body) ← collectFuncDecls ss
+      let renamedBody := body.map (renameCoreStmt rn)
+      let cfg := Imperative.stmtsToCFG renamedBody
+      pure (cfg, liftedFuncs)
+    | .cfg c => do
+      let cfg := renameCoreDetCFG rn c
+      pure (cfg, [])
+  -- Translate CFG to GOTO
+  let ans ← coreCFGToGotoTransform Env' pname cfg
+    { instructions := axiomInsts, nextLoc := axiomLoc, T := Env', sourceText := sourceText }
+  let ending_insts : Array CProverGOTO.Instruction :=
+    #[{ type := .END_FUNCTION, locationNum := ans.nextLoc + 1 }]
+  let pgm := { name := pname,
+               parameterIdentifiers := new_formals.toArray,
+               instructions := ans.instructions ++ ending_insts }
+  -- Translate procedure contracts
+  let mut contracts : List (String × Lean.Json) := []
+  let preExprs := p.spec.preconditions.values.filter (fun c => c.attr == .Default)
+    |>.map (fun c => renameExpr rn c.expr)
+  let postExprs := p.spec.postconditions.values.filter (fun c => c.attr == .Default)
+    |>.map (fun c => renameExpr rn c.expr)
+  let toGotoExpr := Lambda.LExpr.toGotoExprCtx
+    (TBase := ⟨Core.ExpressionMetadata, Unit⟩) []
+  if !preExprs.isEmpty then
+    let preGoto ← preExprs.mapM toGotoExpr
+    let preJson ← (preGoto.mapM CProverGOTO.exprToJson).mapError (fun e => f!"{e}")
+    contracts := contracts ++ [("#spec_requires",
+      Lean.Json.mkObj [("id", ""), ("sub", Lean.Json.arr preJson.toArray)])]
+  if !postExprs.isEmpty then
+    let postGoto ← postExprs.mapM toGotoExpr
+    let postJson ← (postGoto.mapM CProverGOTO.exprToJson).mapError (fun e => f!"{e}")
+    contracts := contracts ++ [("#spec_ensures",
+      Lean.Json.mkObj [("id", ""), ("sub", Lean.Json.arr postJson.toArray)])]
+  -- Build localTypes map for output parameters
+  let output_tys ← p.header.outputs.values.mapM Lambda.LMonoTy.toGotoType
+  let localTypes : Std.HashMap String CProverGOTO.Ty :=
+    (outputs.zip output_tys).foldl (init := {}) fun m (k, v) => m.insert k v
+  let ctx : CoreToGOTO.CProverGOTO.Context :=
+    { program := pgm, formals := formals_tys, ret := ret_ty,
+      locals := outputs ++ locals_from_body, contracts := contracts,
+      localTypes := localTypes }
+  return (ctx, liftedFuncs)
+
+end -- public section
+
+end Strata
diff --git a/Strata/DL/Imperative/BasicBlock.lean b/Strata/DL/Imperative/BasicBlock.lean
index 564652f1dc..1c398002ed 100644
--- a/Strata/DL/Imperative/BasicBlock.lean
+++ b/Strata/DL/Imperative/BasicBlock.lean
@@ -30,17 +30,17 @@ where `n` is the total number of blocks in the graph.
 where execution should proceed next, if anywhere. -/
 inductive DetTransferCmd (Label : Type) (P : PureExpr) where
   /-- Transfer to `lt` if `p` is true, or `lf` is `p` is false. -/
-  | condGoto (p : P.Expr) (lt lf : Label) (md : MetaData P := .empty)
+  | condGoto (p : P.Expr) (lt lf : Label) (md : MetaData P)
   /-- Stop execution of the current unstructured program. If in a procedure
   body, this can be interpreted as returning to the caller. -/
-  | finish (md : MetaData P := .empty)
+  | finish (md : MetaData P)
 
 /-- For the moment, we don't have an unconditional jump in the language, and
 model it instead using `condGoto`. By defining this function, we can easily
 create unconditional jumps, and future proof against the possibility of adding
 it as a constructor in the future.  -/
-def DetTransferCmd.goto [HasBool P] (l : Label) : DetTransferCmd Label P :=
-  condGoto HasBool.tt l l
+def DetTransferCmd.goto [HasBool P] (l : Label) (md : MetaData P) : DetTransferCmd Label P :=
+  condGoto HasBool.tt l l md
 
 /-- A `NondetTransfer` command terminates a non-deterministic basic block,
 indicating the list of possible blocks where execution could proceed next, if
@@ -48,7 +48,7 @@ anywhere. -/
 inductive NondetTransferCmd (Label : Type) (P : PureExpr) where
   /-- Transfer to any one of a list of labels, non-deterministically. `goto`
   with no labels is equivalent to `finish` in `DetTransferCmd` -/
-  | goto (ls : List Label) (md : MetaData P := .empty)
+  | goto (ls : List Label) (md : MetaData P)
   deriving Inhabited
 
 def NondetTransferCmd.targets : NondetTransferCmd Label P → List Label
@@ -79,6 +79,26 @@ structure CFG (Label Block : Type) where
 
 --------
 
+/-- Strip metadata from a deterministic transfer command. -/
+def DetTransferCmd.stripMetaData : DetTransferCmd Label P → DetTransferCmd Label P
+  | .condGoto p lt lf _ => .condGoto p lt lf .empty
+  | .finish _ => .finish .empty
+
+/-- Strip metadata from a non-deterministic transfer command. -/
+def NondetTransferCmd.stripMetaData : NondetTransferCmd Label P → NondetTransferCmd Label P
+  | .goto ls _ => .goto ls .empty
+
+/-- Strip transfer metadata from a deterministic basic block. -/
+def DetBlock.stripMetaData (blk : DetBlock Label Cmd P) : DetBlock Label Cmd P :=
+  { blk with transfer := blk.transfer.stripMetaData }
+
+/-- Strip transfer metadata from all blocks in a deterministic CFG. -/
+def CFG.stripDetMetaData (cfg : CFG Label (DetBlock Label Cmd P)) :
+    CFG Label (DetBlock Label Cmd P) :=
+  { cfg with blocks := cfg.blocks.map fun (lbl, blk) => (lbl, blk.stripMetaData) }
+
+--------
+
 open Std (ToFormat Format format)
 
 def formatDetTransferCmd (P : PureExpr) (c : DetTransferCmd Label P)
diff --git a/Strata/DL/Imperative/CFGSemantics.lean b/Strata/DL/Imperative/CFGSemantics.lean
index b7a0476986..b55346660b 100644
--- a/Strata/DL/Imperative/CFGSemantics.lean
+++ b/Strata/DL/Imperative/CFGSemantics.lean
@@ -20,18 +20,6 @@ This module defines small-step operational semantics for the Imperative
 dialect's control-flow graph representation.
 -/
 
-inductive EvalCmds
-  {CmdT : Type}
-  (P : PureExpr)
-  (EvalCmd : EvalCmdParam P CmdT) :
-  SemanticEval P → SemanticStore P → List CmdT → SemanticStore P → Bool → Prop where
-  | eval_cmds_none :
-    EvalCmds P EvalCmd δ σ [] σ false
-  | eval_cmds_some :
-    EvalCmd δ σ c σ' failed →
-    EvalCmds P EvalCmd δ σ' cs σ'' failed' →
-    EvalCmds P EvalCmd δ σ (c :: cs) σ'' (failed || failed')
-
 /--
 Configuration for small-step semantics, representing the current execution
 state. A configuration consists of a store and a failure indication flag paired
@@ -46,11 +34,24 @@ inductive CFGConfig (l : Type) (P : PureExpr): Type where
   /-- A terminal configuration, indicating that execution has finished. -/
   | terminal : SemanticStore P → Bool → CFGConfig l P
 
-/-- Small-step operational semantics for deterministic basic blocks. Each case
-first evaluates the commands in the block. A block ending in `.condGoto` results
-in a configuration pointing to the true or false label, depending on the
-evaluation of the condition. A block ending in `.finish` results in a terminal
-configuration. -/
+/-- Monotonically update the `failure` flag in a `CFGConfig`. It will be set to
+`true` if the provided Boolean is `true`. -/
+def updateFailure : CFGConfig l P → Bool → CFGConfig l P
+| .cont t σ failed, failed' => .cont t σ (failed || failed')
+| .terminal σ failed, failed' => .terminal σ (failed || failed')
+
+/-- Small-step operational semantics for deterministic basic blocks. Evaluates
+commands sequentially, then transfers control based on the block's terminator.
+
+This is a single recursive inductive that combines command evaluation with
+transfer semantics. The `cmd` constructor evaluates one command and recurses
+on the remaining commands. The terminal constructors handle the transfer once
+all commands are exhausted.
+
+Structuring it this way (rather than delegating to a separate `EvalCmds`
+inductive) ensures that `EvalCmd` is referenced directly in a constructor,
+which is required for Lean 4's kernel to accept this type as a nested
+inductive in mutual blocks. -/
 inductive EvalDetBlock
   {CmdT : Type}
   (P : PureExpr)
@@ -59,31 +60,31 @@ inductive EvalDetBlock
   [HasBoolOps P] :
   SemanticStore P → DetBlock l CmdT P → CFGConfig l P → Prop where
 
-  | step_goto_true :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
+  | cmd :
+    EvalCmd δ σ c σ' failed →
+    EvalDetBlock P EvalCmd extendEval σ' ⟨cs, transfer⟩ config →
+    EvalDetBlock P EvalCmd extendEval
+      σ ⟨ c :: cs, transfer ⟩ (updateFailure config failed)
+
+  | goto_true :
     δ σ c = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →
     EvalDetBlock P EvalCmd extendEval
-      σ ⟨ cs, .condGoto c t e _ ⟩ (.cont t σ' failed)
+      σ ⟨ [], .condGoto c t e _ ⟩ (.cont t σ false)
 
-  | step_goto_false :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
+  | goto_false :
     δ σ c = .some HasBool.ff →
     WellFormedSemanticEvalBool δ →
     EvalDetBlock P EvalCmd extendEval
-      σ ⟨ cs, .condGoto c t e _ ⟩ (.cont e σ' failed)
+      σ ⟨ [], .condGoto c t e _ ⟩ (.cont e σ false)
 
-  | step_terminal :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
+  | terminal :
     EvalDetBlock P EvalCmd extendEval
-      σ ⟨ cs, .finish _ ⟩ (.terminal σ' failed)
+      σ ⟨ [], .finish _ ⟩ (.terminal σ false)
 
 /--
-Small-step operational semantics for non-deterministic basic blocks. Each case
-first evaluates the commands in the block. A block ending in `.goto` with no
-labels results in a terminal configuration. A block ending in `.goto` with a
-non-empty list of labels results in a configuration pointing to a
-non-deterministic choice of one of the labels.
+Small-step operational semantics for non-deterministic basic blocks. Evaluates
+commands sequentially, then transfers control nondeterministically.
 -/
 inductive EvalNondetBlock
   {CmdT : Type}
@@ -93,24 +94,20 @@ inductive EvalNondetBlock
   [HasBoolOps P] :
   SemanticStore P → NondetBlock l CmdT P → CFGConfig l P → Prop where
 
-  | step_goto_none :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
+  | cmd :
+    EvalCmd δ σ c σ' failed →
+    EvalNondetBlock P EvalCmd extendEval σ' ⟨cs, transfer⟩ config →
     EvalNondetBlock P EvalCmd extendEval
-      σ ⟨ cs, .goto [] _ ⟩ (.terminal σ' failed)
+      σ ⟨ c :: cs, transfer ⟩ (updateFailure config failed)
 
-  | step_goto_some :
-    EvalCmds P EvalCmd δ σ cs σ' failed →
-    lt ∈ ls →
+  | goto_none :
     EvalNondetBlock P EvalCmd extendEval
-      σ ⟨ cs, .goto ls _ ⟩ (.cont lt σ' failed)
+      σ ⟨ [], .goto [] _ ⟩ (.terminal σ false)
 
-/--
-Monotonically update the `failure` flag in a `CFGConfig`. It will be set to
-`true` if the provided Boolean is `true`.
--/
-def updateFailure : CFGConfig l P → Bool → CFGConfig l P
-| .cont t σ failed, failed' => .cont t σ (failed || failed')
-| .terminal σ failed, failed' => .terminal σ (failed || failed')
+  | goto_some :
+    lt ∈ ls →
+    EvalNondetBlock P EvalCmd extendEval
+      σ ⟨ [], .goto ls _ ⟩ (.cont lt σ false)
 
 /--
 Operational semantics to step between two configurations of a control-flow
diff --git a/Strata/DL/Imperative/CFGToCProverGOTO.lean b/Strata/DL/Imperative/CFGToCProverGOTO.lean
index 4faeb5f1db..8b3ad750bf 100644
--- a/Strata/DL/Imperative/CFGToCProverGOTO.lean
+++ b/Strata/DL/Imperative/CFGToCProverGOTO.lean
@@ -29,27 +29,9 @@ of any particular backend.
 
 ## Gaps relative to the direct `Stmt.toGotoInstructions` path
 
-The following features are not yet supported via the CFG path, and would need
-to be addressed before it can fully replace the direct path:
-
-- **Source locations on control flow**: `DetTransferCmd` already carries a
-  `MetaData` field, but `StructuredToUnstructured.stmtsToBlocks` currently
-  passes `MetaData.empty` when constructing transfer commands (the metadata
-  from `ite`/`loop`/`block`/`exit` statements is discarded as `_md`).
-  Once `stmtsToBlocks` propagates the metadata, this module will pick it up
-  automatically via `metadataToSourceLoc`.
-- **Loop contracts**: The direct path emits `#spec_loop_invariant` and
-  `#spec_decreases` as named sub-expressions on the backward-edge GOTO
-  instruction (recognized by CBMC's DFCC). In the CFG, invariants are lowered
-  to plain `assert` commands and measures are discarded entirely.
-  To fix: `StructuredToUnstructured.stmtsToBlocks` (the `.loop` case) would
-  need to preserve invariants and measures in the `DetTransferCmd` (or in a
-  side channel), and this module would need to emit them as named
-  sub-expressions on the backward-edge GOTO, mirroring the logic in the
-  `.loop` case of `Stmt.toGotoInstructions` in `ToCProverGOTO.lean`.
 - **`Core.CmdExt.call`**: This translation handles `Imperative.Cmd` only.
-  Core procedure calls (`CmdExt.call`) would need a command translator
-  analogous to `coreStmtsToGoto` in `CoreToGOTOPipeline.lean`.
+  Core procedure calls (`CmdExt.call`) are handled by the Core-specific
+  wrapper `coreCFGToGotoTransform` in `CoreCFGToGOTOPipeline.lean`.
 -/
 
 namespace Imperative
@@ -92,49 +74,64 @@ def detCFGToGotoTransform {P} [G : ToGoto P] [BEq P.Ident]
   -- Pending GOTO patches: (instruction array index, target label)
   let mut pendingPatches : Array (Nat × String) := #[]
   let mut labelMap : Std.HashMap String Nat := {}
+  -- Loop contract metadata: maps loop entry labels to their contract metadata.
+  -- Used in the second pass to annotate backward-edge GOTOs.
+  let mut loopContracts : Std.HashMap String (MetaData P) := {}
   for (label, block) in cfg.blocks do
     -- Record this block's entry location
     labelMap := labelMap.insert label trans.nextLoc
-    -- Emit a LOCATION marker for the block
-    -- NOTE(source-locations): `DetTransferCmd` already carries a `MetaData`
-    -- field, but `StructuredToUnstructured.stmtsToBlocks` currently fills it
-    -- with `MetaData.empty`. Once `stmtsToBlocks` propagates the metadata
-    -- from `ite`/`loop`/`block`/`exit` statements, use `metadataToSourceLoc`
-    -- here (see `Stmt.toGotoInstructions` in ToCProverGOTO.lean for the
-    -- pattern).
     let srcLoc : SourceLocation := { SourceLocation.nil with function := functionName }
     trans := emitLabel label srcLoc trans
     -- Translate each command via the existing Cmd-to-GOTO mapping.
-    -- NOTE: This only handles `Imperative.Cmd`. To support `Core.CmdExt.call`,
-    -- either:
-    --   (a) generalize this function over the command type and accept a
-    --       command translator as a parameter, or
-    --   (b) create a Core-specific wrapper (like `coreStmtsToGoto` in
-    --       `CoreToGOTOPipeline.lean`) that pattern-matches on `CmdExt` and
-    --       emits `FUNCTION_CALL` instructions for `.call`, delegating `.cmd`
-    --       to `Cmd.toGotoInstructions`.
     for cmd in block.cmds do
       trans ← Cmd.toGotoInstructions trans.T functionName cmd trans
     -- Translate the transfer command
     match block.transfer with
-    | .condGoto cond lt lf _md =>
+    | .condGoto cond lt lf md =>
+      let transferSrcLoc := metadataToSourceLoc md functionName trans.sourceText
       let cond_expr ← G.toGotoExpr cond
+      -- Record loop contracts if present (invariants and/or decreases on this
+      -- transfer indicate a loop entry block).
+      let hasLoopContract := md.any fun elem =>
+        elem.fld == MetaData.specLoopInvariant || elem.fld == MetaData.specDecreases
+      if hasLoopContract then
+        loopContracts := loopContracts.insert label md
       -- Emit: GOTO [!cond] lf
-      let (trans', falseIdx) := emitCondGoto (Expr.not cond_expr) srcLoc trans
+      let (trans', falseIdx) := emitCondGoto (Expr.not cond_expr) transferSrcLoc trans
       trans := trans'
       pendingPatches := pendingPatches.push (falseIdx, lf)
       -- Emit: GOTO lt (unconditional)
-      let (trans', trueIdx) := emitUncondGoto srcLoc trans
+      let (trans', trueIdx) := emitUncondGoto transferSrcLoc trans
       trans := trans'
       pendingPatches := pendingPatches.push (trueIdx, lt)
     | .finish _md =>
       -- No instruction needed; the caller appends END_FUNCTION
       pure ()
-  -- Second pass: resolve all pending labels, then patch in one call
+  -- Second pass: resolve all pending labels and annotate backward-edge GOTOs
+  -- with loop contracts when the target is a loop entry block.
   let mut resolvedPatches : List (Nat × Nat) := []
   for (idx, label) in pendingPatches do
     match labelMap[label]? with
-    | some targetLoc => resolvedPatches := (idx, targetLoc) :: resolvedPatches
+    | some targetLoc =>
+      resolvedPatches := (idx, targetLoc) :: resolvedPatches
+      -- If this GOTO targets a loop entry with contracts, annotate its guard.
+      if let some md := loopContracts[label]? then
+        let instLoc := trans.instructions[idx]!.locationNum
+        -- Only annotate backward edges (target location <= source location).
+        if targetLoc ≤ instLoc then
+          let mut guard := trans.instructions[idx]!.guard
+          for elem in md do
+            if elem.fld == MetaData.specLoopInvariant then
+              if let .expr e := elem.value then
+                let gotoExpr ← G.toGotoExpr e
+                guard := guard.setNamedField "#spec_loop_invariant" gotoExpr
+            if elem.fld == MetaData.specDecreases then
+              if let .expr e := elem.value then
+                let gotoExpr ← G.toGotoExpr e
+                guard := guard.setNamedField "#spec_decreases" gotoExpr
+          trans := { trans with
+            instructions := trans.instructions.set! idx
+              { trans.instructions[idx]! with guard := guard } }
     | none =>
       throw f!"[detCFGToGotoTransform] Unresolved label '{label}' referenced \
                by GOTO at instruction index {idx}."
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index 21a1db7857..d46484241d 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -330,6 +330,14 @@ def MetaData.getPropertyType {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Op
     | _ => none
   | none => none
 
+/-- Metadata field for a loop invariant expression preserved during structured-to-CFG
+    lowering. Multiple entries may appear when a loop has multiple invariants. -/
+def MetaData.specLoopInvariant : MetaDataElem.Field P := .label "#spec_loop_invariant"
+
+/-- Metadata field for a loop decreases (measure) expression preserved during
+    structured-to-CFG lowering. -/
+def MetaData.specDecreases : MetaDataElem.Field P := .label "#spec_decreases"
+
 /-- Metadata field for property summaries attached to assert/requires/ensures clauses. -/
 def MetaData.propertySummary : MetaDataElem.Field P := .label "propertySummary"
 
diff --git a/Strata/Languages/Core/DDMTransform/FormatCore.lean b/Strata/Languages/Core/DDMTransform/FormatCore.lean
index 6015bb1832..4cced884a5 100644
--- a/Strata/Languages/Core/DDMTransform/FormatCore.lean
+++ b/Strata/Languages/Core/DDMTransform/FormatCore.lean
@@ -920,6 +920,61 @@ partial def invariantsToCST {M} [Inhabited M]
     let restCST ← invariantsToCST rest
     pure (.consInvariants default labelAnn exprCST restCST)
 
+/-- Convert a `DetTransferCmd` to its CFG-specific CST `Transfer` node.
+Always produces a deterministic CST: `transfer_goto` when both targets coincide,
+otherwise `transfer_cond_goto` over the condition expression. Nondeterministic
+gotos belong to `NondetTransferCmd`; see `nondetTransferToCST`. -/
+partial def transferToCST {M} [Inhabited M]
+    (t : Imperative.DetTransferCmd String Expression) : ToCSTM M (CoreDDM.Transfer M) := do
+  match t with
+  | .condGoto cond lt lf _ =>
+    if lt == lf then
+      pure (.transfer_goto default ⟨default, lt⟩)
+    else
+      let condCST ← lexprToExpr cond 0
+      pure (.transfer_cond_goto default condCST ⟨default, lt⟩ ⟨default, lf⟩)
+  | .finish _ => pure (.transfer_return default)
+
+/-- Convert a `NondetTransferCmd` to its CFG-specific CST `Transfer` node.
+A two-target nondeterministic goto becomes `transfer_nondet_goto`; a single
+target becomes `transfer_goto`; an empty target list becomes `transfer_return`.
+Other arities are not representable in the current concrete syntax. -/
+partial def nondetTransferToCST {M} [Inhabited M]
+    (t : Imperative.NondetTransferCmd String Expression) : ToCSTM M (CoreDDM.Transfer M) := do
+  match t with
+  | .goto [] _ => pure (.transfer_return default)
+  | .goto [l] _ => pure (.transfer_goto default ⟨default, l⟩)
+  | .goto [l1, l2] _ =>
+    pure (.transfer_nondet_goto default ⟨default, l1⟩ ⟨default, l2⟩)
+  | .goto labels _ =>
+    ToCSTM.logError "nondetTransferToCST"
+      "nondeterministic goto arity not representable in concrete syntax"
+      s!"got {labels.length} targets, expected 0, 1, or 2"
+    pure (.transfer_return default)
+
+/-- Convert a single `DetBlock` to a CST `CFGBlock`. -/
+partial def detBlockToCST {M} [Inhabited M]
+    (label : String) (blk : Imperative.DetBlock String Core.Command Expression)
+    : ToCSTM M (CoreDDM.CFGBlock M) := do
+  modify ToCSTContext.pushScope
+  let cmdStmts ← blk.cmds.toArray.mapM (stmtToCST ∘ Imperative.Stmt.cmd)
+  let transfer ← transferToCST blk.transfer
+  modify ToCSTContext.popScope
+  pure (.cfg_block default ⟨default, label⟩ ⟨default, cmdStmts⟩ transfer)
+
+/-- Convert a `DetCFG` to a CST `CFGBody`. -/
+partial def detCFGToCST {M} [Inhabited M] (cfg : Core.DetCFG)
+    : ToCSTM M (CoreDDM.CFGBody M) := do
+  let cfgBlocks ← cfg.blocks.mapM fun (label, blk) => detBlockToCST label blk
+  let blocks := cfgBlocks.foldr (init := none) fun blk acc =>
+    match acc with
+    | none => some (.cfg_blocks_one default blk)
+    | some rest => some (.cfg_blocks_cons default blk rest)
+  match blocks with
+  | some bs => pure (.cfg_body default ⟨default, cfg.entry⟩ bs)
+  | none => pure (.cfg_body default ⟨default, cfg.entry⟩
+      (.cfg_blocks_one default (.cfg_block default ⟨default, cfg.entry⟩ ⟨default, #[]⟩ (.transfer_return default))))
+
 partial def measureToCST {M} [Inhabited M]
     (measure : Option (Lambda.LExpr CoreLParams.mono)) :
     ToCSTM M (Ann (Option (Measure M)) M) := do
@@ -989,15 +1044,16 @@ def procToCST {M} [Inhabited M] (proc : Core.Procedure) : ToCSTM M (Command M) :
       ⟨default, none⟩
     else
       ⟨default, some (Spec.spec_mk default specAnn)⟩
-  let bodyStmts ← match proc.body with
-    | .structured ss => pure ss
-    | .cfg _ => do
-        ToCSTM.logError "procToCST" "CFG bodies not yet supported in CST conversion" proc.header.name.toPretty
-        pure []
-  let bodyCST ← blockToCST bodyStmts
-  let body : Ann (Option (CoreDDM.Block M)) M := ⟨default, some bodyCST⟩
+  let cmd ← match proc.body with
+    | .structured ss =>
+      let bodyCST ← blockToCST ss
+      let body : Ann (Option (CoreDDM.Block M)) M := ⟨default, some bodyCST⟩
+      pure (.command_procedure default name typeArgs arguments spec body)
+    | .cfg c =>
+      let cfgBody ← detCFGToCST c
+      pure (.command_cfg_procedure default name typeArgs arguments spec cfgBody)
   modify ToCSTContext.popScope
-  pure (.command_procedure default name typeArgs arguments spec body)
+  pure cmd
 
 -- Recreate enough of `GlobalContext` from `ToCSTContext` obtained from
 -- `programToCST`, purely for formatting.
diff --git a/Strata/Languages/Core/ObligationExtraction.lean b/Strata/Languages/Core/ObligationExtraction.lean
index fa8ecb2b37..f469d8bdd3 100644
--- a/Strata/Languages/Core/ObligationExtraction.lean
+++ b/Strata/Languages/Core/ObligationExtraction.lean
@@ -46,6 +46,21 @@ def isValidObligationInput : Statements → Bool
   | s :: rest => isValidObligationStatement s && isValidObligationInput rest
 end
 
+/-- Extract proof obligations from a single command, accumulating path conditions. -/
+def extractFromCmd (pc : PathConditions Expression) (cmd : Command)
+    : PathConditions Expression × Array (ProofObligation Expression) :=
+  match cmd with
+  | .cmd (.assert label e md) =>
+    let propType := convertMetaDataPropertyType md
+    (pc, #[ProofObligation.mk label propType pc e md])
+  | .cmd (.cover label e md) =>
+    (pc, #[ProofObligation.mk label .cover pc e md])
+  | .cmd (.assume label e _md) =>
+    (pc.addInNewest [.assumption label e], #[])
+  | .cmd (.init name ty e _md) =>
+    (pc.addEntry (.varDecl name ty e), #[])
+  | _ => (pc, #[])
+
 mutual
 /-- Core recursive worker for `extractFromStatements`. Walks the statement list,
     accumulating path conditions and collecting proof obligations. -/
@@ -55,24 +70,15 @@ def extractGo (pc : PathConditions Expression) : Statements →
   | [], acc => .ok acc
   | s :: rest, acc =>
     match s with
-    | .cmd (.cmd (.assert label e md)) =>
-      let propType := convertMetaDataPropertyType md
-      extractGo pc rest (acc.push (ProofObligation.mk label propType pc e md))
-
-    | .cmd (.cmd (.cover label e md)) =>
-      extractGo pc rest (acc.push (ProofObligation.mk label .cover pc e md))
-
-    | .cmd (.cmd (.assume label e _md)) =>
-      extractGo (pc.addInNewest [.assumption label e]) rest acc
+    | .cmd c =>
+      let (newPc, newObs) := extractFromCmd pc c
+      extractGo newPc rest (acc ++ newObs)
 
     | .ite .nondet thenSs elseSs _md => do
       let thenObs ← extractFromStatements pc thenSs
       let elseObs ← extractFromStatements pc elseSs
       extractGo pc rest (acc ++ thenObs ++ elseObs)
 
-    | .cmd (.cmd (.init name ty e _md)) =>
-      extractGo (pc.addEntry (.varDecl name ty e)) rest acc
-
     | _other =>
       .error s!"ObligationExtraction: unsupported statement"
 
@@ -89,6 +95,21 @@ def extractFromStatements
   extractGo pathConditions ss #[]
 end
 
+/-- Extract proof obligations from a deterministic CFG by walking all blocks.
+    Path conditions restart from the global `pc` for each block independently, so
+    obligations are over-approximated (no false negatives — every real bug is caught).
+    However, obligations in block B that depend on `assume` from block A will fail to
+    discharge, surfacing as false alarms (false positives) to the user.
+    TODO: dominator-based path-condition propagation to reduce false alarms. -/
+def extractFromDetCFG (pc : PathConditions Expression) (cfg : DetCFG)
+    : Except String (Array (ProofObligation Expression)) :=
+  let obs := cfg.blocks.foldl (init := #[]) fun acc (_, blk) =>
+    let (_, blockObs) := blk.cmds.foldl (init := (pc, #[])) fun (curPc, obs) cmd =>
+      let (newPc, newObs) := extractFromCmd curPc cmd
+      (newPc, obs ++ newObs)
+    acc ++ blockObs
+  .ok obs
+
 /-- Extract proof obligations from a program. Axioms become global assumptions
     that are prepended to the path conditions of every obligation. -/
 def extractObligations (p : Program) : Except String (ProofObligations Expression) := do
@@ -102,8 +123,7 @@ def extractObligations (p : Program) : Except String (ProofObligations Expressio
       let globalPc : PathConditions Expression := [axiomPc]
       let obs ← match proc.body with
         | .structured ss => extractFromStatements globalPc ss
-        -- CFG bodies are not supported on procedure-body branch.
-        | .cfg _ => .ok #[]
+        | .cfg c => extractFromDetCFG globalPc c
       .ok (axiomPc, allObs ++ obs)
     | _ => .ok (axiomPc, allObs)
   return allObs
@@ -124,8 +144,6 @@ private theorem extractGo_ok (pc : PathConditions Expression) (ss : Statements)
     obtain ⟨hs, hrest⟩ := h
     unfold extractGo; split
     · exact extractGo_ok _ _ _ hrest
-    · exact extractGo_ok _ _ _ hrest
-    · exact extractGo_ok _ _ _ hrest
     · rename_i thenSs elseSs _
       unfold isValidObligationStatement at hs
       simp [Bool.and_eq_true] at hs
@@ -140,8 +158,8 @@ private theorem extractGo_ok (pc : PathConditions Expression) (ss : Statements)
         cases extractGo pc elseSs #[] with
         | error => intro _ h; simp [Except.isOk, Except.toBool] at h
         | ok v2 => intro _ _; simp; exact extractGo_ok _ _ _ hrest
-    · exact extractGo_ok _ _ _ hrest
     · unfold isValidObligationStatement at hs; simp at hs
+      split at hs <;> simp at *
 
 /-- If the input satisfies `isValidObligationInput`, then `extractFromStatements`
     never returns an error. -/
diff --git a/Strata/Languages/Core/Procedure.lean b/Strata/Languages/Core/Procedure.lean
index 16161be5f4..508a84b985 100644
--- a/Strata/Languages/Core/Procedure.lean
+++ b/Strata/Languages/Core/Procedure.lean
@@ -402,10 +402,7 @@ def DetCFG.eraseTypes (cfg : DetCFG) : DetCFG :=
 -- assume, init, set, cover) is not included in formatted output — formatCmd
 -- discards it. Transfer metadata, however, appears in CFG formatting.
 def DetCFG.stripMetaData (cfg : DetCFG) : DetCFG :=
-  { cfg with blocks := cfg.blocks.map fun (lbl, blk) =>
-      (lbl, { blk with transfer := match blk.transfer with
-                          | .condGoto p lt lf _ => .condGoto p lt lf .empty
-                          | .finish _ => .finish .empty }) }
+  Imperative.CFG.stripDetMetaData cfg
 
 def Procedure.eraseTypes (p : Procedure) : Procedure :=
   let body' := match p.body with
diff --git a/Strata/Languages/Core/ProcedureEval.lean b/Strata/Languages/Core/ProcedureEval.lean
index 4fbc16aa27..57e4f5aa5a 100644
--- a/Strata/Languages/Core/ProcedureEval.lean
+++ b/Strata/Languages/Core/ProcedureEval.lean
@@ -57,6 +57,100 @@ private def mergeResults (fallback : Env) (results : List Env) : Env :=
       deferred := allDeferred,
       exprEnv  := { E.exprEnv with config := { E.exprEnv.config with usedNames := mergedNames } } }
 
+private def evalBlockCmds (E : Env) (old_var_subst : SubstMap)
+    (cmds : List Command) : Env :=
+  cmds.foldl (fun env cmd =>
+    if env.error.isSome then env
+    else (Statement.Command.eval env old_var_subst cmd).snd) E
+
+private def evalCFGStep (cfg : DetCFG) (old_var_subst : SubstMap)
+    (active : List (String × Env)) :
+    List (String × Env) × List Env × Statistics :=
+  active.foldl (fun (newActive, finished, stats) (label, env) =>
+    if env.error.isSome then
+      (newActive, env :: finished, stats)
+    else
+      match cfg.blocks.lookup label with
+      | none =>
+        let env' := { env with error := some (.Misc
+            s!"evalCFG: block '{label}' not found in CFG") }
+        (newActive, env' :: finished, stats)
+      | some blk =>
+        let env' := evalBlockCmds env old_var_subst blk.cmds
+        if env'.error.isSome then
+          (newActive, env' :: finished, stats)
+        else
+          let stats := stats.increment s!"{Evaluator.Stats.simulatedStmts}"
+          match blk.transfer with
+          | .finish _ =>
+            (newActive, env' :: finished, stats)
+          | .condGoto cond lt lf _ =>
+            let cond' := env'.exprEval cond
+            match cond' with
+            | .true _ => ((lt, env') :: newActive, finished, stats)
+            | .false _ => ((lf, env') :: newActive, finished, stats)
+            | _ =>
+              let condErased := cond.eraseTypes
+              let label_t := toString (f!"<cfgBranch_true: {condErased}>")
+              let label_f := toString (f!"<cfgBranch_false: !({condErased})>")
+              let env_t := { env' with pathConditions :=
+                (env'.pathConditions.addInNewest
+                  [.assumption label_t cond']) }
+              -- Mirror processIteBranches at StatementEval.lean: clear
+              -- `deferred` on the false branch so pre-split obligations
+              -- aren't duplicated across both branches. Without this, every
+              -- symbolic condGoto multiplies the deferred-obligation count
+              -- by 2, producing exponential blowup across procedures.
+              let env_f := { env' with
+                deferred := #[]
+                pathConditions :=
+                  (env'.pathConditions.addInNewest
+                    [.assumption label_f
+                      (Lambda.LExpr.ite () cond' (LExpr.false ()) (LExpr.true ()))]) }
+              ((lt, env_t) :: (lf, env_f) :: newActive, finished, stats))
+    ([], [], {})
+
+private def evalCFGBlocks (cfg : DetCFG) (old_var_subst : SubstMap)
+    (fuel : Nat) (active : List (String × Env)) (finished : List Env)
+    (stats : Statistics) : List Env × Statistics :=
+  match active with
+  | [] => (finished, stats)
+  | _ =>
+    match fuel with
+    | 0 =>
+      let errorEnvs := active.map fun (_, e) =>
+        { e with error := some .OutOfFuel }
+      (errorEnvs ++ finished,
+       stats.increment s!"{Evaluator.Stats.simulatingStmtHitOutOfFuel}" active.length)
+    | fuel' + 1 =>
+      let (newActive, newFinished, stepStats) :=
+        evalCFGStep cfg old_var_subst active
+      evalCFGBlocks cfg old_var_subst fuel' newActive
+        (newFinished ++ finished) (stats.merge stepStats)
+  termination_by fuel
+
+private def evalCFGBody (E : Env) (old_var_subst : SubstMap)
+    (precond_assumes postcond_asserts : Statements)
+    (cfg : DetCFG) (fuel : Nat) : List Env × Statistics :=
+  let (preEnvs, preStats) := Statement.eval E old_var_subst precond_assumes
+  let emptyAcc : List Env × Statistics := ([], {})
+  let (cfgResultsRev, cfgStats) :=
+    preEnvs.foldl (fun acc preEnv =>
+      let (accEnvs, accStats) := acc
+      let (envs, stats) :=
+        evalCFGBlocks cfg old_var_subst fuel [(cfg.entry, preEnv)] [] {}
+      (envs.reverse ++ accEnvs, accStats.merge stats)) emptyAcc
+  let cfgResults := cfgResultsRev.reverse
+  let (postResultsRev, postStats) :=
+    cfgResults.foldl (fun acc cfgEnv =>
+      let (accEnvs, accStats) := acc
+      if cfgEnv.error.isSome then
+        (cfgEnv :: accEnvs, accStats)
+      else
+        let (envs, stats) := Statement.eval cfgEnv old_var_subst postcond_asserts
+        (envs.reverse ++ accEnvs, accStats.merge stats)) emptyAcc
+  (postResultsRev.reverse, preStats.merge (cfgStats.merge postStats))
+
 /--
 Evaluate a single procedure: generate fresh variables for parameters,
 execute the body, check postconditions, and collect proof obligations.
@@ -113,13 +207,17 @@ def eval (E : Env) (p : Procedure) : Env × Statistics :=
       (.assume label check.expr check.md))
       p.spec.preconditions
   match p.body with
+  | .cfg cfgBody =>
+    -- 100 iterations per block: enough to unroll moderate loops while keeping
+    -- symbolic execution bounded.  Fuel is consumed per block visit, so a
+    -- single-block loop unrolls ~100 times and a 4-block diamond uses ~400.
+    let fuel := cfgBody.blocks.length * 100
+    let (ssEs, evalStats) :=
+      evalCFGBody E old_g_subst precond_assumes postcond_asserts cfgBody fuel
+    (mergeResults E (ssEs.map (fun sE => fixupError sE)), evalStats)
   | .structured bodyStmts =>
     let (ssEs, evalStats) := Statement.eval E old_g_subst (precond_assumes ++ bodyStmts ++ postcond_asserts)
     (mergeResults E (ssEs.map (fun sE => fixupError sE)), evalStats)
-  | .cfg _ =>
-    -- CFG bodies are not supported here.
-    let errEnv := { E with error := some (.Misc s!"procedure '{p.header.name}': CFG bodies not supported yet") }
-    (errEnv, {})
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/Languages/Core/ProcedureType.lean b/Strata/Languages/Core/ProcedureType.lean
index 2059f60c05..a923cae19a 100644
--- a/Strata/Languages/Core/ProcedureType.lean
+++ b/Strata/Languages/Core/ProcedureType.lean
@@ -50,6 +50,73 @@ private def setupInputEnv (C : Core.Expression.TyContext) (Env : Core.Expression
   let Env := Env.addInNewestContext inp_lty_sig
   return (inp_mty_sig, Env)
 
+private def checkUniqueLabels (procName : CoreIdent) (cfg : DetCFG) (sourceLoc : FileRange) :
+    Except DiagnosticModel Unit := do
+  let labels := cfg.blocks.map (·.1)
+  if !labels.Nodup then
+    let dups := labels.filter (fun l => labels.countP (· == l) > 1) |>.eraseDups
+    .error <| DiagnosticModel.withRange sourceLoc
+      f!"[{procName}]: Duplicate block labels in CFG: {dups}"
+
+private def checkEntryExists (procName : CoreIdent) (cfg : DetCFG) (sourceLoc : FileRange) :
+    Except DiagnosticModel Unit := do
+  let labels := cfg.blocks.map (·.1)
+  if !labels.contains cfg.entry then
+    .error <| DiagnosticModel.withRange sourceLoc
+      f!"[{procName}]: Entry label \"{cfg.entry}\" not found in CFG blocks. \
+         Available labels: {labels}"
+
+private def checkTargetLabels (procName : CoreIdent) (cfg : DetCFG) (sourceLoc : FileRange) :
+    Except DiagnosticModel Unit := do
+  let labels := cfg.blocks.map (·.1)
+  for (lbl, blk) in cfg.blocks do
+    match blk.transfer with
+    | .condGoto _ lt lf _ =>
+      if !labels.contains lt then
+        .error <| DiagnosticModel.withRange sourceLoc
+          f!"[{procName}]: Block \"{lbl}\" branches to unknown label \"{lt}\". \
+             Available labels: {labels}"
+      if !labels.contains lf then
+        .error <| DiagnosticModel.withRange sourceLoc
+          f!"[{procName}]: Block \"{lbl}\" branches to unknown label \"{lf}\". \
+             Available labels: {labels}"
+    | .finish _ => pure ()
+
+-- Type environment flows sequentially through all blocks in list order,
+-- regardless of control-flow reachability.  This is a sound over-approximation:
+-- it may accept a program that uses an uninitialized variable at runtime (the
+-- verifier will still catch the error), but it never misses a real type error.
+-- Per-block scoping would require a dataflow fixpoint over the CFG.
+open Lambda Lambda.LTy.Syntax in
+private def typeCheckCFG (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv)
+    (P : Program) (proc : Procedure) (cfg : DetCFG) (sourceLoc : FileRange) :
+    Except DiagnosticModel (DetCFG × Core.Expression.TyEnv) := do
+  checkUniqueLabels proc.header.name cfg sourceLoc
+  checkEntryExists proc.header.name cfg sourceLoc
+  checkTargetLabels proc.header.name cfg sourceLoc
+  let mut currentEnv := Env
+  let mut annotatedBlocks : List (String × Imperative.DetBlock String Command Expression) := []
+  for (lbl, blk) in cfg.blocks do
+    let mut cmds' := []
+    for cmd in blk.cmds do
+      let (cmd', newEnv) ← Statement.typeCheckCmd C currentEnv P cmd
+      currentEnv := newEnv
+      cmds' := cmds' ++ [cmd']
+    let transfer' ← match blk.transfer with
+      | .condGoto p lt lf md =>
+        let (pa, newEnv) ← LExpr.resolve C currentEnv p
+          |>.mapError DiagnosticModel.fromFormat
+        currentEnv := newEnv
+        if pa.toLMonoTy != mty[bool] then
+          .error <| DiagnosticModel.withRange sourceLoc
+            f!"[{proc.header.name}]: Branch condition in block \"{lbl}\" \
+               is not of type bool, got {pa.toLMonoTy}"
+        pure (Imperative.DetTransferCmd.condGoto pa.unresolved lt lf md)
+      | .finish md => pure (.finish md)
+    annotatedBlocks := annotatedBlocks ++ [(lbl, { cmds := cmds', transfer := transfer' })]
+  let annotatedCFG : DetCFG := { entry := cfg.entry, blocks := annotatedBlocks }
+  return (annotatedCFG, currentEnv)
+
 -- Error message prefix for errors in processing procedure pre/post conditions.
 def conditionErrorMsgPrefix (procName : CoreIdent) (condName : CoreLabel)
     (md : MetaData Expression) : DiagnosticModel :=
@@ -111,12 +178,13 @@ def typeCheck (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p :
   -- Type check body.
   -- Note that `Statement.typeCheck` already reports source locations in
   -- error messages.
-  let bodyStmts : List Statement ← match proc.body with
-    | .structured ss => pure ss
-    | .cfg _ =>
-      Except.error (DiagnosticModel.withRange fileRange
-        f!"[{proc.header.name}]: CFG procedures not supported yet")
-  let (annotated_body, finalEnv) ← Statement.typeCheck C envAfterPostconds p (.some proc) bodyStmts
+  let (annotated_body, annotated_cfg, finalEnv) ← match proc.body with
+    | .structured ss =>
+      let (ss', env') ← Statement.typeCheck C envAfterPostconds p (.some proc) ss
+      pure (ss', none, env')
+    | .cfg cfgBody =>
+      let (cfg', env') ← typeCheckCFG C envAfterPostconds p proc cfgBody fileRange
+      pure ([], some cfg', env')
 
   -- Remove formals and returns from the context -- they ought to be local to
   -- the procedure body.
@@ -131,7 +199,10 @@ def typeCheck (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p :
                                     outputs := out_mty_sig }
   let new_spec := { proc.spec with preconditions := finalPreconditions,
                                    postconditions := finalPostconditions }
-  let new_proc := { proc with header := new_hdr, spec := new_spec, body := .structured annotated_body }
+  let new_body := match annotated_cfg with
+    | some cfg' => .cfg cfg'
+    | none => .structured annotated_body
+  let new_proc := { proc with header := new_hdr, spec := new_spec, body := new_body }
 
   return (new_proc, finalEnv)
 
diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 3e32b77a80..f7fdb364a2 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -246,52 +246,34 @@ def Statements.containsAsserts (ss : Statements) : Bool :=
     (fun c => match c with | .assert _ _ _ => true | _ => false) ss
 
 mutual
-/--
-Collect all `cover` commands from a statement `s` with their labels and metadata.
--/
-def Statement.collectCovers (s : Statement) : List (String × Imperative.MetaData Expression) :=
+def Statement.collectCmds (f : Imperative.Cmd Expression → Option α) (s : Statement) : List α :=
   match s with
-  | .cmd (.cmd (.cover label _expr md)) => [(label, md)]
+  | .cmd (.cmd c) => (f c).toList
   | .cmd _ => []
-  | .block _ inner_ss _ => Statements.collectCovers inner_ss
-  | .ite _ then_ss else_ss _ => Statements.collectCovers then_ss ++ Statements.collectCovers else_ss
-  | .loop _ _ _ body_ss _ => Statements.collectCovers body_ss
-  | .funcDecl _ _ | .exit _ _ | .typeDecl _ _ => []  -- Function/type declarations and exits don't contain cover commands
+  | .block _ inner_ss _ => Statements.collectCmds f inner_ss
+  | .ite _ then_ss else_ss _ => Statements.collectCmds f then_ss ++ Statements.collectCmds f else_ss
+  | .loop _ _ _ body_ss _ => Statements.collectCmds f body_ss
+  | .funcDecl _ _ | .exit _ _ | .typeDecl _ _ => []
   termination_by Imperative.Stmt.sizeOf s
-/--
-Collect all `cover` commands from statements `ss` with their labels and metadata.
--/
-def Statements.collectCovers (ss : Statements) : List (String × Imperative.MetaData Expression) :=
+def Statements.collectCmds (f : Imperative.Cmd Expression → Option α) (ss : Statements) : List α :=
   match ss with
   | [] => []
   | s :: ss =>
-    Statement.collectCovers s ++ Statements.collectCovers ss
+    Statement.collectCmds f s ++ Statements.collectCmds f ss
   termination_by Imperative.Block.sizeOf ss
 end
 
-mutual
-/--
-Collect all `assert` commands from a statement `s` with their labels and metadata.
--/
+def Statement.collectCovers (s : Statement) : List (String × Imperative.MetaData Expression) :=
+  Statement.collectCmds (fun | .cover label _expr md => some (label, md) | _ => none) s
+
+def Statements.collectCovers (ss : Statements) : List (String × Imperative.MetaData Expression) :=
+  Statements.collectCmds (fun | .cover label _expr md => some (label, md) | _ => none) ss
+
 def Statement.collectAsserts (s : Statement) : List (String × Imperative.MetaData Expression) :=
-  match s with
-  | .cmd (.cmd (.assert label _expr md)) => [(label, md)]
-  | .cmd _ => []
-  | .block _ inner_ss _ => Statements.collectAsserts inner_ss
-  | .ite _ then_ss else_ss _ => Statements.collectAsserts then_ss ++ Statements.collectAsserts else_ss
-  | .loop _ _ _ body_ss _ => Statements.collectAsserts body_ss
-  | .funcDecl _ _ | .exit _ _ | .typeDecl _ _ => []  -- Function/type declarations and exits don't contain assert commands
-  termination_by Imperative.Stmt.sizeOf s
-/--
-Collect all `assert` commands from statements `ss` with their labels and metadata.
--/
+  Statement.collectCmds (fun | .assert label _expr md => some (label, md) | _ => none) s
+
 def Statements.collectAsserts (ss : Statements) : List (String × Imperative.MetaData Expression) :=
-  match ss with
-  | [] => []
-  | s :: ss =>
-    Statement.collectAsserts s ++ Statements.collectAsserts ss
-  termination_by Imperative.Block.sizeOf ss
-end
+  Statements.collectCmds (fun | .assert label _expr md => some (label, md) | _ => none) ss
 
 /--
 Create cover obligations for covers in an unreachable (dead) branch, including
@@ -750,11 +732,42 @@ def evalOne (E : Env) (old_var_subst : SubstMap) (ss : Statements) : Env :=
 
 mutual
 
+/--
+Execute a CFG by following control flow from the entry block. For each block,
+translate the commands within it to a sequence of command statements and evaluate
+those using the structured interpreter, then dispatch on the block's transfer to
+either finish or jump to the next block. -/
+private def runCFG (cfg : Core.DetCFG) (fuel : Nat) (env : Env)
+    (ops : Imperative.RunOps Expression Command Env) : Env :=
+  go cfg.entry fuel env
+where
+  go (label : String) (fuel : Nat) (env : Env) : Env :=
+    match fuel with
+    | 0 => CmdEval.updateError env (.Misc s!"runCFG: fuel exhausted (possible infinite loop)")
+    | fuel' + 1 =>
+      match cfg.blocks.lookup label with
+      | none => CmdEval.updateError env (.Misc s!"runCFG: block '{label}' not found in CFG")
+      | some blk =>
+        let cmdStmts := blk.cmds.map (Imperative.Stmt.cmd ·)
+        match Imperative.runStmt ops fuel' (.stmts cmdStmts env) with
+        | .terminal env' =>
+          match blk.transfer with
+          | .finish _ => env'
+          | .condGoto cond lt lf _ =>
+            match ops.evalExpr env' cond with
+            | some (.boolConst _ true) => go lt fuel' env'
+            | some (.boolConst _ false) => go lf fuel' env'
+            | _ => CmdEval.updateError env'
+                (.Misc s!"runCFG: branch condition in block '{label}' is symbolic (e.g. nondeterministic goto); concrete execution requires deterministic conditions")
+        | _ => CmdEval.updateError env
+              (.Misc s!"runCFG: block '{label}' did not reach terminal (possibly inner-loop fuel exhaustion or unexpected exit)")
+
 /--
 Interpret a single procedure call.
 
 Importantly, this creates a separate Env to execute the body of the procedure with,
 which initially only contains input/output variables.
+
 The resulting Env is the original passed in Env with the output variables copied back into it.
 -/
 def Command.runCall (lhs : List Expression.Ident) (procName : String) (args : List Expression.Expr)
@@ -805,15 +818,15 @@ def Command.runCall (lhs : List Expression.Ident) (procName : String) (args : Li
               hasError := fun E => E.error.isSome
               addError := fun E msg => CmdEval.updateError E (.Misc msg)
             }
-            let configAfter := match proc.body with
+            let callEnvAfter := match proc.body with
               | .structured ss =>
                 let config : Imperative.RunConfig Expression Command Env :=
                   .stmts ss callEnv
                 Imperative.runStmt ops fuel' config
-              | .cfg _ =>
-                .terminal (CmdEval.updateError callEnv
-                  (.Misc s!"procedure '{procName}': CFG bodies not supported yet"))
-            match configAfter with
+              | .cfg cfgBody =>
+                -- Interpret CFG by following control flow from the entry block.
+                .terminal (runCFG cfgBody fuel' callEnv ops)
+            match callEnvAfter with
             | .terminal callEnv' =>
               match callEnv'.error with
               | some _ => { E with error := callEnv'.error }
@@ -840,5 +853,3 @@ end Statement
 end Core
 
 end -- public section
-
----------------------------------------------------------------------
diff --git a/Strata/Languages/Core/StatementSemantics.lean b/Strata/Languages/Core/StatementSemantics.lean
index 76545a3cc5..1a47f38324 100644
--- a/Strata/Languages/Core/StatementSemantics.lean
+++ b/Strata/Languages/Core/StatementSemantics.lean
@@ -328,14 +328,35 @@ inductive CoreStepStar
     ----
     CoreStepStar π φ c₁ c₃
 
-/-- Execution of a procedure body. Only structured bodies have an executable
-    semantics; the `.cfg` arm of `Procedure.Body` has no inhabitant of
-    `CoreBodyExec`.
+/-- Reflexive-transitive closure of CFG steps for the Core language.
+    Each step looks up a block by label and evaluates it using the generic
+    `Imperative.EvalDetBlock` instantiated with `EvalCommand`. This works
+    because `EvalDetBlock` has a `cmd` constructor that directly references
+    `EvalCmd`, satisfying the Lean kernel's nested inductive requirement. -/
+inductive CoreCFGStepStar
+    (π : String → Option Procedure)
+    (φ : CoreEval → PureFunc Expression → CoreEval) :
+    DetCFG → CFGConfig String Expression →
+    CFGConfig String Expression → Prop where
+  | refl : CoreCFGStepStar π φ cfg c c
+  | step :
+    List.lookup t cfg.blocks = .some b →
+    Imperative.EvalDetBlock Expression (EvalCommand π φ) (EvalPureFunc φ) σ b config →
+    CoreCFGStepStar π φ cfg (updateFailure config failed) c₃ →
+    ----
+    CoreCFGStepStar π φ cfg (.cont t σ failed) c₃
+
+/-- Execution of a procedure body: either structured (via `CoreStepStar`)
+    or unstructured CFG (via `CoreCFGStepStar`).
 
     For structured bodies, the body is wrapped in `Stmt.block "" ss #[]` so that
     `funcDecl` extensions and other inner scoping introduced by the body do not
     leak past the procedure boundary.  This wrapping mirrors
-    `Specification.AssertValidInProcedure` and the `procToVerifyStmt` pipeline. -/
+    `Specification.AssertValidInProcedure` and the `procToVerifyStmt` pipeline.
+
+    The `cfg` constructor passes through the initial eval `δ` as terminal eval
+    because `CoreCFGStepStar` does not track eval changes. If CFG execution
+    ever needs `funcDecl` support, `CoreCFGStepStar` would need enrichment. -/
 inductive CoreBodyExec
     (π : String → Option Procedure)
     (φ : CoreEval → PureFunc Expression → CoreEval) :
@@ -345,6 +366,11 @@ inductive CoreBodyExec
       (.stmt (Stmt.block "" ss #[]) ⟨σ, δ, false⟩)
       (.terminal ρ') →
     CoreBodyExec π φ (.structured ss) σ δ ρ'.store ρ'.eval ρ'.hasFailure
+  | cfg :
+    CoreCFGStepStar π φ cfg
+      (.cont cfg.entry σ false)
+      (.terminal σ' failed) →
+    CoreBodyExec π φ (.cfg cfg) σ δ σ' δ failed
 
 inductive EvalCommand (π : String → Option Procedure) (φ : CoreEval → PureFunc Expression → CoreEval) : CoreEval →
   CoreStore → Command → CoreStore → Bool → Prop where
diff --git a/Strata/Transform/ANFEncoder.lean b/Strata/Transform/ANFEncoder.lean
index 7d37a35879..29a45a1bcf 100644
--- a/Strata/Transform/ANFEncoder.lean
+++ b/Strata/Transform/ANFEncoder.lean
@@ -279,7 +279,8 @@ def anfEncodeProgram (p : Program) : Bool × Program :=
         let (body', idx') := anfEncodeBody ss idx
         (.proc { proc with body := .structured body' } md :: acc, idx', changed || idx' > idx)
       | .cfg _ =>
-        -- CFG bodies are not transformed by ANF encoding for now.
+        -- CSE on CFGs would require dominator analysis to determine where to
+        -- place hoisted var declarations. Skipped for now.
         (.proc proc md :: acc, idx, changed)
     | other => (other :: acc, idx, changed)
   ) ([], 0, false)
diff --git a/Strata/Transform/CoreSpecification.lean b/Strata/Transform/CoreSpecification.lean
index 25dd9cbece..d151086fdd 100644
--- a/Strata/Transform/CoreSpecification.lean
+++ b/Strata/Transform/CoreSpecification.lean
@@ -38,6 +38,47 @@ open Core Imperative
   Imperative.Specification.Lang.imperative
     Expression Command (EvalCommand π φ) (EvalPureFunc φ) coreIsAtAssert
 
+/-! ## Core CFG `Lang` bundle -/
+
+/-- Configuration for CFG specification: pairs a `CFGConfig` with the eval
+    function so that `getEnv` can reconstruct a full `Env Expression`. -/
+structure CoreCFGSpecConfig where
+  cfgConfig : CFGConfig String Expression
+  eval : CoreEval
+
+/-- Extract an `Env Expression` from a CFG specification config. -/
+def CoreCFGSpecConfig.toEnv (c : CoreCFGSpecConfig) : Env Expression :=
+  match c.cfgConfig with
+  | .cont _ σ f => ⟨σ, c.eval, f⟩
+  | .terminal σ f => ⟨σ, c.eval, f⟩
+
+/-- Assert detection in a CFG: an assert is reachable if the current block
+    (looked up by the continuation label in a given CFG) contains an assert
+    command with the matching label and expression. -/
+def coreCFGIsAtAssert (cfg : DetCFG) : CoreCFGSpecConfig → AssertId Expression → Prop
+  | ⟨.cont lbl _ _, _⟩, aid =>
+    match cfg.blocks.lookup lbl with
+    | some blk => blk.cmds.any fun
+        | .cmd (.assert l e _) => l == aid.label && e == aid.expr
+        | _ => false
+    | none => False
+  | ⟨.terminal _ _, _⟩, _ => False
+
+/-- The `Lang Expression` bundle for Core CFG small-step semantics. -/
+@[expose] def Lang.coreCFG
+    (π : String → Option Procedure)
+    (φ : CoreEval → PureFunc Expression → CoreEval)
+    (cfg : DetCFG) :
+    Imperative.Specification.Lang Expression where
+  StmtT := DetCFG
+  CfgT := CoreCFGSpecConfig
+  star := fun c₁ c₂ => CoreCFGStepStar π φ cfg c₁.cfgConfig c₂.cfgConfig
+  stmtCfg := fun _ ρ => ⟨.cont cfg.entry ρ.store false, ρ.eval⟩
+  terminalCfg := fun ρ => ⟨.terminal ρ.store ρ.hasFailure, ρ.eval⟩
+  exitingCfg := fun _ ρ => ⟨.terminal ρ.store ρ.hasFailure, ρ.eval⟩
+  isAtAssert := coreCFGIsAtAssert cfg
+  getEnv := CoreCFGSpecConfig.toEnv
+
 /-! ## Well-formed program state at the entry of procedure -/
 
 /-- The list of variables that must have been declared,
@@ -86,15 +127,9 @@ variable (φ : CoreEval → PureFunc Expression → CoreEval)
   | .structured ss =>
     Imperative.Specification.AssertValidWhen (Specification.Lang.core π φ)
       (ProcEnvWF proc) (Stmt.block "" ss #[]) a
-  -- CFG bodies don't yet have a small-step semantics, so there is nothing to
-  -- certify.  We pick `False` rather than `True` to be conservative: a CFG
-  -- procedure cannot be claimed asserts-valid (and hence cannot be proven
-  -- `ProcedureCorrect`) until CFG bodies gain an executable semantics.  This
-  -- is sound against the current proofs because the only producer of
-  -- `ProcedureCorrect` (`procBodyVerify_procedureCorrect`) is gated on
-  -- `procToVerifyStmt` succeeding, which forces `proc.body = .structured _`
-  -- (see `procToVerifyStmt_is_structured`), so this arm is never entered.
-  | .cfg _ => False
+  | .cfg cfg =>
+    Imperative.Specification.AssertValidWhen (Specification.Lang.coreCFG π φ cfg)
+      (ProcEnvWF proc) cfg a
 
 /-- A procedure is correct with respect to its specification.
 
diff --git a/Strata/Transform/CoreTransform.lean b/Strata/Transform/CoreTransform.lean
index 9b5415e01f..d962f9b043 100644
--- a/Strata/Transform/CoreTransform.lean
+++ b/Strata/Transform/CoreTransform.lean
@@ -330,6 +330,12 @@ def runProgram
           currentProcedureName := .some proc.header.name.1
         })
 
+        -- TODO: A `runCFGRec` counterpart could be added to apply command-level
+        -- transforms to CFG bodies. Since `f` returns `Option (List Statement)`
+        -- and a CFG block holds `List Command`, each returned statement would
+        -- need to be unwrapped as `.cmd`. If `f` returns nested structures
+        -- (blocks, if-then-else, loops), those can't be represented in a basic
+        -- block, so such cases would need to be rejected or left untransformed.
         let bodyStmts ← match proc.body with
           | .structured ss => pure ss
           | .cfg _ => throw (Strata.DiagnosticModel.fromMessage
diff --git a/Strata/Transform/PrecondElim.lean b/Strata/Transform/PrecondElim.lean
index 6f68e8d479..15e902ca28 100644
--- a/Strata/Transform/PrecondElim.lean
+++ b/Strata/Transform/PrecondElim.lean
@@ -89,9 +89,9 @@ so expression-level metadata carries no source location. We therefore inherit
 the enclosing statement's `md` (with `propertySummary` stripped to prevent
 user-facing messages from leaking into generated checks).
 -/
-def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr)
+def collectPrecondAssertCmds (F : @Lambda.Factory CoreLParams) (e : Expression.Expr)
 (labelPrefix : String) (md : Imperative.MetaData Expression)
-: List Statement :=
+: List (Imperative.Cmd Expression) :=
   let wfObs := Lambda.collectWFObligations F e
   -- Strip propertySummary: the enclosing statement's user-facing message
   -- (e.g., a Python assert message) should not propagate to generated
@@ -101,7 +101,7 @@ def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr
   -- For nested calls like SafeSDiv(SafeSDiv(x,y),z), obligations arrive as
   -- [inner-0, inner-1, outer-0, outer-1] with the same funcName throughout.
   -- Without modulo, the index would be 0,1,2,3 instead of 0,1,0,1.
-  let (_, _, result) := wfObs.foldl (init := ("", 0, ([] : List Statement)))
+  let (_, _, result) := wfObs.foldl (init := ("", 0, ([] : List (Imperative.Cmd Expression))))
     fun (prevFunc, prevIdx, acc) ob =>
       let rawIdx := if ob.funcName == prevFunc then prevIdx + 1 else 0
       let precondCount := F[ob.funcName]?.map (·.preconditions.length) |>.getD 1
@@ -110,32 +110,52 @@ def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr
       let md' := match classifyPrecondition ob.funcName precondIdx with
         | some pt => md.pushElem Imperative.MetaData.propertyType (.msg pt)
         | none => md
-      let stmt := Statement.assert
+      let cmd := Imperative.Cmd.assert
         s!"{labelPrefix}_calls_{ob.funcName}_{globalIdx}" ob.obligation md'
-      (ob.funcName, rawIdx, stmt :: acc)
+      (ob.funcName, rawIdx, cmd :: acc)
   result.reverse
 
+private def cmdsToStatements (cs : List (Imperative.Cmd Expression)) : List Statement :=
+  cs.map (fun c => Imperative.Stmt.cmd (CmdExt.cmd c))
+
+private def cmdsToCommands (cs : List (Imperative.Cmd Expression)) : List Command :=
+  cs.map CmdExt.cmd
+
+def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr)
+(labelPrefix : String) (md : Imperative.MetaData Expression)
+: List Statement :=
+  cmdsToStatements (collectPrecondAssertCmds F e labelPrefix md)
+
 /--
 Collect assertions for all expressions in a command.
 -/
-def collectCmdPrecondAsserts (F : @Lambda.Factory CoreLParams)
-  (cmd : Imperative.Cmd Expression) : List Statement :=
+def collectCmdPrecondAssertCmds (F : @Lambda.Factory CoreLParams)
+  (cmd : Imperative.Cmd Expression) : List (Imperative.Cmd Expression) :=
   match cmd with
-  | .init _ _ (.det e) md => collectPrecondAsserts F e "init" md
+  | .init _ _ (.det e) md => collectPrecondAssertCmds F e "init" md
   | .init _ _ .nondet _ => []
-  | .set x (.det e) md => collectPrecondAsserts F e s!"set_{x.name}" md
+  | .set x (.det e) md => collectPrecondAssertCmds F e s!"set_{x.name}" md
   | .set _ .nondet _ => []
-  | .assert l e md => collectPrecondAsserts F e s!"assert_{l}" md
-  | .assume l e md => collectPrecondAsserts F e s!"assume_{l}" md
-  | .cover l e md => collectPrecondAsserts F e s!"cover_{l}" md
+  | .assert l e md => collectPrecondAssertCmds F e s!"assert_{l}" md
+  | .assume l e md => collectPrecondAssertCmds F e s!"assume_{l}" md
+  | .cover l e md => collectPrecondAssertCmds F e s!"cover_{l}" md
+
+def collectCmdPrecondAsserts (F : @Lambda.Factory CoreLParams)
+  (cmd : Imperative.Cmd Expression) : List Statement :=
+  cmdsToStatements (collectCmdPrecondAssertCmds F cmd)
 
 /--
 Collect assertions for call arguments.
 -/
+def collectCallPrecondAssertCmds (F : @Lambda.Factory CoreLParams) (pname : String)
+  (args : List Expression.Expr) (md : Imperative.MetaData Expression)
+  : List (Imperative.Cmd Expression) :=
+  args.flatMap fun arg => collectPrecondAssertCmds F arg s!"call_{pname}_arg" md
+
 def collectCallPrecondAsserts (F : @Lambda.Factory CoreLParams) (pname : String)
   (args : List Expression.Expr) (md : Imperative.MetaData Expression)
   : List Statement :=
-  args.flatMap fun arg => collectPrecondAsserts F arg s!"call_{pname}_arg" md
+  cmdsToStatements (collectCallPrecondAssertCmds F pname args md)
 
 /-! ## Processing contract conditions -/
 
@@ -342,6 +362,46 @@ def transformStmt (s : Statement)
   decreasing_by all_goals term_by_mem
 end
 
+/-! ## CFG transformation -/
+
+/-- Transform a single command in a CFG block, prepending precondition asserts. -/
+def transformCFGCmd (F : @Lambda.Factory CoreLParams) (cmd : Command)
+    : Bool × List Command :=
+  match cmd with
+  | .cmd c =>
+    let asserts := collectCmdPrecondAssertCmds F c
+    (!asserts.isEmpty, cmdsToCommands asserts ++ [.cmd c])
+  | .call pname callArgs md =>
+    let asserts := collectCallPrecondAssertCmds F pname (CallArg.getInputExprs callArgs) md
+    (!asserts.isEmpty, cmdsToCommands asserts ++ [.call pname callArgs md])
+
+/-- Transform all commands in a CFG block. -/
+def transformCFGCmds (F : @Lambda.Factory CoreLParams) (cmds : List Command)
+    : Bool × List Command :=
+  cmds.foldl (fun (changed, acc) cmd =>
+    let (c, cmds') := transformCFGCmd F cmd
+    (changed || c, acc ++ cmds')) (false, [])
+
+/-- Transform a DetBlock: transform commands and add asserts for the transfer condition. -/
+def transformDetBlock (F : @Lambda.Factory CoreLParams)
+    (blk : Imperative.DetBlock String Command Expression)
+    : Bool × Imperative.DetBlock String Command Expression :=
+  let (changed, cmds') := transformCFGCmds F blk.cmds
+  let (transferChanged, transferAsserts) := match blk.transfer with
+    | .condGoto cond _ _ md =>
+      let asserts := collectPrecondAssertCmds F cond "branch_cond" md
+      (!asserts.isEmpty, cmdsToCommands asserts)
+    | .finish _ => (false, [])
+  (changed || transferChanged, ⟨cmds' ++ transferAsserts, blk.transfer⟩)
+
+/-- Transform an entire DetCFG. -/
+def transformDetCFG (F : @Lambda.Factory CoreLParams) (cfg : DetCFG)
+    : Bool × DetCFG :=
+  let (changed, blocks') := cfg.blocks.foldl (fun (changed, acc) (label, blk) =>
+    let (c, blk') := transformDetBlock F blk
+    (changed || c, acc ++ [(label, blk')])) (false, [])
+  (changed, { cfg with blocks := blocks' })
+
 /-! ## Main transformation -/
 
 /-- Add a precondition-WF procedure as a leaf node in the cached call graph.
@@ -385,13 +445,15 @@ where
           acc := acc.push d
         else
           let F ← getFactory
-          let (bodyChanged, proc') ← match proc.body with
-            | .structured ss =>
-              let (c, body') ← transformStmts ss
-              pure (c, { proc with body := .structured body' })
-            -- CFG bodies pass through untouched.
-            | .cfg _ => pure (false, proc)
+          let (bodyChanged, body') ← match proc.body with
+            | .structured ss => do
+              let (c, ss') ← transformStmts ss
+              pure (c, Procedure.Body.structured ss')
+            | .cfg cfg =>
+              let (c, cfg') := transformDetCFG F cfg
+              pure (c, Procedure.Body.cfg cfg')
           setFactory F
+          let proc' := { proc with body := body' }
           let procDecl := Decl.proc proc' md
           match mkContractWFProc F proc md with
           | some wfDecl => do
diff --git a/Strata/Transform/ProcBodyVerify.lean b/Strata/Transform/ProcBodyVerify.lean
index 2d0b030c5d..264654a770 100644
--- a/Strata/Transform/ProcBodyVerify.lean
+++ b/Strata/Transform/ProcBodyVerify.lean
@@ -87,7 +87,8 @@ open Core Imperative Transform
 
   -- ProcBodyVerify expects a structured body: the prefix (inits + assumes) and
   -- suffix (postcondition asserts) are statement-level constructs that embed
-  -- around the body. Unstructured CFG bodies are not supported here.
+  -- around the body. Unstructured CFG bodies require a different verification
+  -- strategy (e.g., encoding the contract directly in the CFG).
   let bodyStmts ← proc.body.getStructured.mapError Strata.DiagnosticModel.fromMessage
   -- Wrap body in labeled block
   let bodyBlock := Stmt.block bodyLabel bodyStmts #[]
diff --git a/Strata/Transform/StructuredToUnstructured.lean b/Strata/Transform/StructuredToUnstructured.lean
index 3da0a61310..caa0a4dc23 100644
--- a/Strata/Transform/StructuredToUnstructured.lean
+++ b/Strata/Transform/StructuredToUnstructured.lean
@@ -19,9 +19,12 @@ namespace Imperative
 
 abbrev DetBlocks (Label CmdT : Type) (P : PureExpr) := List (Label × DetBlock Label CmdT P)
 
-def detCmdBlock [HasBool P] (c : CmdT) (k : Label) :
+private abbrev synthesizedMd {P : PureExpr} : MetaData P :=
+  MetaData.ofProvenance (.synthesized .structuredToUnstructured)
+
+def detCmdBlock [HasBool P] (c : CmdT) (k : Label) (md : MetaData P) :
   DetBlock Label CmdT P :=
-  { cmds := [c], transfer := .goto k }
+  { cmds := [c], transfer := .goto k md }
 
 open LabelGen
 
@@ -43,16 +46,13 @@ def flushCmds
       pure (k, [])
     else
       let l ← StringGenState.gen pfx
-      let b := (l, { cmds := accum.reverse, transfer := .goto k })
+      let b := (l, { cmds := accum.reverse, transfer := .goto k synthesizedMd })
       pure (l, [b])
   | some tr =>
     let l ← StringGenState.gen pfx
     let b := (l, { cmds := accum.reverse, transfer := tr })
     pure (l, [b])
 
-private abbrev synthesizedMd {P : PureExpr} : MetaData P :=
-  MetaData.ofProvenance (.synthesized .structuredToUnstructured)
-
 /-- Translate a list of statements to basic blocks, accumulating commands -/
 def stmtsToBlocks
   [HasBool P] [HasPassiveCmds P CmdT] [HasInit P CmdT]
@@ -75,7 +75,7 @@ match ss with
 | .typeDecl _ _ :: rest => do
   -- Not yet supported, so just continue with `rest`.
   stmtsToBlocks k rest exitConts accum
-| .block l bss _md :: rest => do
+| .block l bss md :: rest => do
   -- Process rest first
   let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
   -- Process block body, extending the list of exit continuations.
@@ -87,9 +87,9 @@ match ss with
     -- Empty accumulated block
     pure (accumEntry, accumBlocks ++ bbs ++ bsNext)
   else
-    let b := (l, { cmds := [], transfer := .goto bl })
+    let b := (l, { cmds := [], transfer := .goto bl md })
     pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ bsNext)
-| .ite c tss fss _md :: rest => do
+| .ite c tss fss md :: rest => do
   -- Process rest first
   let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
   -- Create ite block
@@ -105,9 +105,9 @@ match ss with
       let initCmd := HasInit.init ident HasBool.boolTy .nondet synthesizedMd
       pure (HasFvar.mkFvar ident, [initCmd])
   let (accumEntry, accumBlocks) ← flushCmds "ite$" (accum ++ extraCmds)
-    (.some (.condGoto condExpr tl fl)) l
+    (.some (.condGoto condExpr tl fl md)) l
   pure (accumEntry, accumBlocks ++ tbs ++ fbs ++ bsNext)
-| .loop c m is bss _md :: rest => do
+| .loop c m is bss md :: rest => do
   -- Process rest first
   let (kNext, bsNext) ← stmtsToBlocks k rest exitConts []
   -- Create loop entry block
@@ -129,7 +129,7 @@ match ss with
       let decCmd   := HasPassiveCmds.assert s!"measure_decrease_{mLabel}"
                          (HasIntOps.lt mExpr mOldExpr) synthesizedMd
       let ldec ← StringGenState.gen "measure_decrease$"
-      let decBlock := (ldec, { cmds := [decCmd], transfer := .goto lentry })
+      let decBlock := (ldec, { cmds := [decCmd], transfer := .goto lentry synthesizedMd })
       pure ([initCmd, assumeCmd, lbCmd], ldec, [decBlock])
   -- Body jumps to bodyK (either directly to lentry, or through the decrease block).
   let (bl, bbs) ← stmtsToBlocks bodyK bss ((.none, kNext) :: exitConts) []
@@ -142,10 +142,18 @@ match ss with
         if srcLabel.isEmpty then StringGenState.gen "inv$"
         else pure srcLabel
       pure (HasPassiveCmds.assert assertLabel i synthesizedMd))
+  -- Attach loop contract (invariants + measure) to the transfer metadata so
+  -- downstream CFG passes can recover the original spec without relying on the
+  -- lowered assert commands alone.
+  let contractMd := is.foldl (fun md (_, inv) =>
+      md.pushElem MetaData.specLoopInvariant (.expr inv)) md
+  let contractMd := match m with
+    | some mExpr => contractMd.pushElem MetaData.specDecreases (.expr mExpr)
+    | none => contractMd
   -- For nondet guards, introduce a fresh boolean variable
   match c with
   | .det e =>
-    let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto e bl kNext })
+    let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto e bl kNext contractMd })
     let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry
     pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext)
   | .nondet => do
@@ -153,10 +161,10 @@ match ss with
     let ident := HasIdent.ident (P := P) freshName
     let initCmd := HasInit.init ident HasBool.boolTy .nondet synthesizedMd
     let b := (lentry, { cmds := [initCmd] ++ invCmds ++ measureCmds,
-                        transfer := .condGoto (HasFvar.mkFvar ident) bl kNext })
+                        transfer := .condGoto (HasFvar.mkFvar ident) bl kNext contractMd })
     let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry
     pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext)
-| .exit l _md :: _ => do
+| .exit l md :: _ => do
   -- Find the continuation of the block labeled `l`.
   let bk :=
     match exitConts.lookup (.some l) with
@@ -167,7 +175,7 @@ match ss with
   -- Flush the accumulated commands, going to the continuation calculated above.
   -- Any statements after the `.exit` are skipped.
   let exitName := s!"block${l}$"
-  flushCmds exitName accum .none bk
+  flushCmds exitName accum (.some (.goto bk md)) bk
 
 def stmtsToCFGM
   [HasBool P] [HasPassiveCmds P CmdT] [HasInit P CmdT]
@@ -175,7 +183,7 @@ def stmtsToCFGM
   (ss : List (Stmt P CmdT)) :
   StringGenM (CFG String (DetBlock String CmdT P)) := do
   let lend ← StringGenState.gen "end$"
-  let bend := (lend, { cmds := [], transfer := .finish })
+  let bend := (lend, { cmds := [], transfer := .finish synthesizedMd })
   let (l, bs) ← stmtsToBlocks lend ss [] []
   pure { entry := l, blocks := bs ++ [bend] }
 
diff --git a/StrataBoole/StrataBooleTest/FeatureRequests/seq_empty_literal.lean b/StrataBoole/StrataBooleTest/FeatureRequests/seq_empty_literal.lean
index 4e082856d4..fa27c8475c 100644
--- a/StrataBoole/StrataBooleTest/FeatureRequests/seq_empty_literal.lean
+++ b/StrataBoole/StrataBooleTest/FeatureRequests/seq_empty_literal.lean
@@ -75,8 +75,11 @@ private def seqEmptyTysIn (p : StrataDDM.Program) : Except String (List String)
   for d in cp.decls do
     match d with
     | .proc proc _ =>
-      for stmt in proc.body do
-        out := out ++ (collectFromStmt stmt).map fmtSeqEmptyTy
+      match proc.body with
+      | .structured ss =>
+        for stmt in ss do
+          out := out ++ (collectFromStmt stmt).map fmtSeqEmptyTy
+      | .cfg _ => pure ()  -- Boole doesn't produce CFG bodies; skip if encountered
     | _ => pure ()
   return out
 
diff --git a/StrataTest/Backends/CBMC/GOTO/E2E_CFGPipeline.lean b/StrataTest/Backends/CBMC/GOTO/E2E_CFGPipeline.lean
new file mode 100644
index 0000000000..be41de6643
--- /dev/null
+++ b/StrataTest/Backends/CBMC/GOTO/E2E_CFGPipeline.lean
@@ -0,0 +1,299 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import Strata.Backends.CBMC.CollectSymbols
+import Strata.Backends.CBMC.GOTO.CoreCFGToGOTOPipeline
+import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
+import StrataDDM.Integration.Lean.HashCommands
+import Strata.Languages.Core.DDMTransform.Translate
+import Lean.Server.Utils
+
+/-! ## Equivalence tests: direct path vs. CFG path
+
+Run both `procedureToGotoCtx` (direct) and `procedureToGotoCtxViaCFG` (CFG)
+on the same programs and compare outputs.
+
+The CFG path produces additional GOTO instructions for explicit block-to-block
+transfers that the direct path handles implicitly via fall-through. Comparisons
+therefore focus on **semantic** instructions (DECL, ASSIGN, ASSERT, ASSUME,
+FUNCTION_CALL, END_FUNCTION) and contract annotations, ignoring cosmetic GOTO
+and LOCATION differences.
+-/
+
+open Strata
+
+private def translateCore (p : StrataDDM.Program) : Core.Program :=
+  (TransM.run Inhabited.default (translateProgram p)).fst
+
+/-! ### Instruction-level comparison helpers -/
+
+private def isSemanticInst (inst : CProverGOTO.Instruction) : Bool :=
+  match inst.type with
+  | .DECL | .ASSIGN | .ASSERT | .ASSUME | .FUNCTION_CALL
+  | .SET_RETURN_VALUE | .END_FUNCTION => true
+  | _ => false
+
+private def compareSemanticInstructions
+    (directInsts cfgInsts : Array CProverGOTO.Instruction)
+    : Except String Unit := do
+  let dSemantic := directInsts.filter isSemanticInst
+  let cSemantic := cfgInsts.filter isSemanticInst
+  if dSemantic.size != cSemantic.size then
+    throw s!"Semantic instruction count mismatch: direct={dSemantic.size} cfg={cSemantic.size}"
+  for i in List.range dSemantic.size do
+    if dSemantic[i]!.type != cSemantic[i]!.type then
+      throw s!"Semantic instruction type mismatch at index {i}: \
+               direct={dSemantic[i]!.type} cfg={cSemantic[i]!.type}"
+  return ()
+
+/-! ### Pipeline runners -/
+
+private def runDirectPipeline (cprog : Core.Program) (procName : String := "main")
+    : Except Std.Format (CoreToGOTO.CProverGOTO.Context × List Core.Function) := do
+  let Env := Lambda.TEnv.default
+  let procs := cprog.decls.filterMap fun d => d.getProc?
+  let axioms := cprog.decls.filterMap fun d => d.getAxiom?
+  let distincts := cprog.decls.filterMap fun d => match d with
+    | .distinct name es _ => some (name, es) | _ => none
+  let some proc := procs.find? (fun p => Core.CoreIdent.toPretty p.header.name == procName)
+    | .error f!"procedure {procName} not found"
+  procedureToGotoCtx Env proc (axioms := axioms) (distincts := distincts)
+
+private def runCFGPipeline (cprog : Core.Program) (procName : String := "main")
+    : Except Std.Format (CoreToGOTO.CProverGOTO.Context × List Core.Function) := do
+  let Env := Lambda.TEnv.default
+  let procs := cprog.decls.filterMap fun d => d.getProc?
+  let axioms := cprog.decls.filterMap fun d => d.getAxiom?
+  let distincts := cprog.decls.filterMap fun d => match d with
+    | .distinct name es _ => some (name, es) | _ => none
+  let some proc := procs.find? (fun p => Core.CoreIdent.toPretty p.header.name == procName)
+    | .error f!"procedure {procName} not found"
+  procedureToGotoCtxViaCFG Env proc (axioms := axioms) (distincts := distincts)
+
+private def toJson (ctx : CoreToGOTO.CProverGOTO.Context) (pname : String)
+    : Except Std.Format (Lean.Json × Lean.Json) := do
+  let json ← (CoreToGOTO.CProverGOTO.Context.toJson pname ctx).mapError (fun e => f!"{e}")
+  return (json.symtab, json.goto)
+
+/-- Run both pipelines and compare semantic instructions + contracts + JSON validity. -/
+private def testEquivalence (prog : StrataDDM.Program) (procName : String := "main")
+    : IO Unit := do
+  let cprog := translateCore prog
+  let directResult := runDirectPipeline cprog procName
+  let cfgResult := runCFGPipeline cprog procName
+  match directResult, cfgResult with
+  | .error e, _ => IO.throwServerError s!"Direct pipeline failed: {e}"
+  | _, .error e => IO.throwServerError s!"CFG pipeline failed: {e}"
+  | .ok (dctx, _), .ok (cctx, _) =>
+    -- Instruction-level: compare semantic instructions (ignoring GOTO/LOCATION)
+    match compareSemanticInstructions dctx.program.instructions cctx.program.instructions with
+    | .error e => IO.throwServerError s!"Instruction mismatch: {e}"
+    | .ok () => pure ()
+    -- Contract annotations must match
+    if dctx.contracts.length != cctx.contracts.length then
+      IO.throwServerError s!"Contract count mismatch: direct={dctx.contracts.length} cfg={cctx.contracts.length}"
+    for (dk, dv) in dctx.contracts do
+      match cctx.contracts.find? (·.1 == dk) with
+      | some (_, cv) =>
+        if dv != cv then
+          IO.throwServerError s!"Contract value mismatch for {dk}"
+      | none =>
+        IO.throwServerError s!"Contract key {dk} missing from CFG path"
+    -- JSON-level: both produce valid, non-null output
+    let pname := "main"
+    match toJson dctx pname, toJson cctx pname with
+    | .error e, _ => IO.throwServerError s!"Direct JSON failed: {e}"
+    | _, .error e => IO.throwServerError s!"CFG JSON failed: {e}"
+    | .ok (dSym, dGoto), .ok (cSym, cGoto) =>
+      assert! dSym != Lean.Json.null
+      assert! cSym != Lean.Json.null
+      assert! dGoto != Lean.Json.null
+      assert! cGoto != Lean.Json.null
+
+-------------------------------------------------------------------------------
+
+-- Test 1: Simple assert
+def CFGEq_SimpleAssert :=
+#strata
+program Core;
+procedure main(x : int) {
+  assert (x > 0);
+};
+#end
+
+#eval testEquivalence CFGEq_SimpleAssert
+
+-------------------------------------------------------------------------------
+
+-- Test 2: Variable declaration and assignment
+def CFGEq_VarDeclAssign :=
+#strata
+program Core;
+procedure main(x : int) {
+  var z : int := x + 1;
+  assert (z > 0);
+};
+#end
+
+#eval testEquivalence CFGEq_VarDeclAssign
+
+-------------------------------------------------------------------------------
+
+-- Test 3: If-then-else
+def CFGEq_IfThenElse :=
+#strata
+program Core;
+procedure main(x : int) {
+  var r : int;
+  if (x > 0) {
+    r := 1;
+  } else {
+    r := 0;
+  }
+  assert (r >= 0);
+};
+#end
+
+#eval testEquivalence CFGEq_IfThenElse
+
+-------------------------------------------------------------------------------
+
+-- Test 4: Preconditions and postconditions
+def CFGEq_Contracts :=
+#strata
+program Core;
+procedure main(x : int)
+spec {
+  requires (x > 0);
+  ensures (x >= 0);
+} {
+  assert (x > 0);
+};
+#end
+
+#eval testEquivalence CFGEq_Contracts
+
+-------------------------------------------------------------------------------
+
+-- Test 5: Axioms and distinct declarations
+def CFGEq_AxiomDistinct :=
+#strata
+program Core;
+const a : int;
+const b : int;
+axiom [ax1]: (a > 0);
+distinct [ab]: [a, b];
+procedure main() {
+  assert (a != b);
+};
+#end
+
+#eval testEquivalence CFGEq_AxiomDistinct
+
+-------------------------------------------------------------------------------
+
+-- Test 6: Free specs are skipped (same in both paths)
+def CFGEq_FreeSpecs :=
+#strata
+program Core;
+procedure main(x : int)
+spec {
+  free requires (x > 10);
+  requires (x >= 0);
+  free ensures (x > 5);
+  ensures (x >= 0);
+} {
+  assert (x >= 0);
+};
+#end
+
+#eval testEquivalence CFGEq_FreeSpecs
+
+-------------------------------------------------------------------------------
+
+-- Test 7: Cover command
+def CFGEq_Cover :=
+#strata
+program Core;
+procedure main(x : int) {
+  cover (x > 0);
+};
+#end
+
+#eval testEquivalence CFGEq_Cover
+
+-------------------------------------------------------------------------------
+
+-- Test 8: Bitvector operations
+def CFGEq_BVOps :=
+#strata
+program Core;
+procedure main(x : bv32, y : bv32) {
+  var z : bv32 := x + y;
+  assert (z > bv{32}(0));
+};
+#end
+
+#eval testEquivalence CFGEq_BVOps
+
+-------------------------------------------------------------------------------
+
+-- Test 9: Assume command
+def CFGEq_Assume :=
+#strata
+program Core;
+procedure main(x : int) {
+  assume (x > 0);
+  assert (x > 0);
+};
+#end
+
+#eval testEquivalence CFGEq_Assume
+
+-------------------------------------------------------------------------------
+
+-- Test 10: Multiple sequential commands
+def CFGEq_MultipleCommands :=
+#strata
+program Core;
+procedure main(x : int) {
+  var a : int := x + 1;
+  var b : int := a + 2;
+  assert (b > x);
+};
+#end
+
+#eval testEquivalence CFGEq_MultipleCommands
+
+-------------------------------------------------------------------------------
+
+-- Test 11: CFG path only — verify the CFG-only pipeline produces valid output
+-- (no direct path comparison since .cfg bodies aren't supported by the direct path)
+#eval do
+  let prog :=
+    #strata
+    program Core;
+    procedure main(x : int) {
+      var r : int;
+      if (x > 0) {
+        r := 1;
+      } else {
+        r := 0;
+      }
+      assert (r >= 0);
+    };
+    #end
+  let cprog := translateCore prog
+  match runCFGPipeline cprog with
+  | .error e => IO.throwServerError s!"CFG pipeline failed: {e}"
+  | .ok (ctx, _) =>
+    match toJson ctx "main" with
+    | .error e => IO.throwServerError s!"JSON failed: {e}"
+    | .ok (symtab, goto) =>
+      assert! symtab != Lean.Json.null
+      assert! goto != Lean.Json.null
+      let gotoStr := goto.pretty
+      assert! (gotoStr.splitOn "GOTO").length > 1
+      assert! (gotoStr.splitOn "ASSERT").length > 1
diff --git a/StrataTest/DL/Imperative/CFGToCProverGOTO.lean b/StrataTest/DL/Imperative/CFGToCProverGOTO.lean
index c2a0069802..e76171b93c 100644
--- a/StrataTest/DL/Imperative/CFGToCProverGOTO.lean
+++ b/StrataTest/DL/Imperative/CFGToCProverGOTO.lean
@@ -290,8 +290,8 @@ info: ok: #[LOCATION 0,
   -- Construct a CFG where entry label doesn't match the first block
   let cfg : Imperative.CFG String (Imperative.DetBlock String (Imperative.Cmd LExprTP) LExprTP) :=
     { entry := "second",
-      blocks := [("first", { cmds := [], transfer := .finish }),
-                 ("second", { cmds := [], transfer := .finish })] }
+      blocks := [("first", { cmds := [], transfer := .finish .empty }),
+                 ("second", { cmds := [], transfer := .finish .empty })] }
   match Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg with
   | .error e => assert! (s!"{e}".splitOn "Entry label").length > 1
   | .ok _ => assert! false
@@ -319,7 +319,7 @@ info: ok: ()
   let trueExpr : LExprTP.Expr :=
     .const { underlying := (), type := mty[bool] } (.boolConst true)
   let blk : Imperative.DetBlock String (Imperative.Cmd LExprTP) LExprTP :=
-    { cmds := [], transfer := .condGoto trueExpr "missing_label" "also_missing" }
+    { cmds := [], transfer := .condGoto trueExpr "missing_label" "also_missing" .empty }
   let cfg : Imperative.CFG String (Imperative.DetBlock String (Imperative.Cmd LExprTP) LExprTP) :=
     { entry := "entry", blocks := [("entry", blk)] }
   match Imperative.detCFGToGotoTransform Lambda.TEnv.default "test" cfg with
diff --git a/StrataTest/DL/Imperative/StepStmtTest.lean b/StrataTest/DL/Imperative/StepStmtTest.lean
index a4f53a1d6d..fee5199553 100644
--- a/StrataTest/DL/Imperative/StepStmtTest.lean
+++ b/StrataTest/DL/Imperative/StepStmtTest.lean
@@ -563,7 +563,7 @@ theorem loopScopeTest :
   -- Need to reconcile the env shape.
   conv => rhs; rw [show Env.mk storeWithX miniEval false =
     { Env.mk (projectStore storeWithX storeWithXY) miniEval false with
-      hasFailure := false || false } from by simp [hproj]]
+      hasFailure := false || false } from by simp [hproj, Bool.or_false]]
   exact .step _ _ _ StepStmt.step_stmts_nil (.refl _)
 
 ---------------------------------------------------------------------
diff --git a/StrataTest/Languages/Core/Examples/Exit.lean b/StrataTest/Languages/Core/Examples/Exit.lean
index 96093e85d8..1f1f501ec2 100644
--- a/StrataTest/Languages/Core/Examples/Exit.lean
+++ b/StrataTest/Languages/Core/Examples/Exit.lean
@@ -117,48 +117,52 @@ Result: ✅ pass
 info: Entry: block$l1$_2
 
 l1:
-  condGoto true block$l1$_2 block$l1$_2
+  #[<[provenance]: :416-531>] condGoto true block$l1$_2 block$l1$_2
 block$l1$_2:
   assert [a1]: x == x;
-  condGoto true l$_1 l$_1
+  #[<[provenance]: :455-463>] condGoto true l$_1 l$_1
 l$_1:
   assert [a3]: x == x;
-  condGoto true end$_0 end$_0
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true end$_0 end$_0
 end$_0:
-  finish
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] finish
 -/
 #guard_msgs in
 #eval (Std.format (singleCFG exitPgm 0))
 
 /--
-info: Entry: ite$_5
+info: Entry: ite$_7
 
 l5:
-  condGoto true ite$_5 ite$_5
+  #[<[provenance]: :606-1085>] condGoto true ite$_7 ite$_7
 l4:
-  condGoto true ite$_5 ite$_5
+  #[<[provenance]: :618-1079>] condGoto true ite$_7 ite$_7
 l4_before:
-  condGoto true ite$_5 ite$_5
+  #[<[provenance]: :632-1025>] condGoto true ite$_7 ite$_7
 l3_before:
-  condGoto true ite$_5 ite$_5
+  #[<[provenance]: :655-962>] condGoto true ite$_7 ite$_7
 l1:
-  condGoto true ite$_5 ite$_5
-ite$_5:
+  #[<[provenance]: :680-864>] condGoto true ite$_7 ite$_7
+ite$_7:
   assert [a4]: x == x;
-  condGoto x > 0 block$l5$_2 block$l5$_1
+  #[<[provenance]: :735-850>] condGoto x > 0 block$l3_before$_5 block$l4_before$_6
+block$l3_before$_5:
+  #[<[provenance]: :764-779>] condGoto true block$l5$_2 block$l5$_2
+block$l4_before$_6:
+  #[<[provenance]: :819-834>] condGoto true block$l5$_1 block$l5$_1
 l2:
-  condGoto true l$_3 l$_3
+  #[<[provenance]: :877-950>] condGoto true l$_3 l$_3
 l$_3:
   assert [a5]: !(x == x);
-  condGoto true block$l5$_2 block$l5$_2
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true block$l5$_2 block$l5$_2
 block$l5$_2:
   assert [a6]: x * 2 > x;
-  condGoto true end$_0 end$_0
+  #[<[provenance]: :1007-1015>] condGoto true end$_0 end$_0
 block$l5$_1:
   assert [a7]: x <= 0;
-  condGoto true end$_0 end$_0
+  #[<[provenance]: :1063-1071>] condGoto true end$_0 end$_0
 end$_0:
-  finish
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] finish
 -/
 #guard_msgs in
 #eval (Std.format (singleCFG exitPgm 1))
diff --git a/StrataTest/Languages/Core/Examples/Loops.lean b/StrataTest/Languages/Core/Examples/Loops.lean
index 9bcba599b8..3f591585ab 100644
--- a/StrataTest/Languages/Core/Examples/Loops.lean
+++ b/StrataTest/Languages/Core/Examples/Loops.lean
@@ -59,22 +59,25 @@ info: Entry: before_loop$_7
 
 before_loop$_7:
   i := 0;
-  condGoto true loop_entry$_1 loop_entry$_1
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true loop_entry$_1 loop_entry$_1
 loop_entry$_1:
   assert [inv$_5]: 0 <= i;
   assert [inv$_6]: i <= n;
   var loop_measure$_2 : int;
   assume [assume_loop_measure$_2]: loop_measure$_2 == n;
   assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
-  condGoto i < n l$_4 end$_0
+  #[<[provenance]: :1312-1418>,
+ <[#spec_loop_invariant]: 0 <= i>,
+ <[#spec_loop_invariant]: i <= n>,
+ <[#spec_decreases]: n>] condGoto i < n l$_4 end$_0
 l$_4:
   i := i + 1;
-  condGoto true measure_decrease$_3 measure_decrease$_3
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true measure_decrease$_3 measure_decrease$_3
 measure_decrease$_3:
   assert [measure_decrease_loop_measure$_2]: n < loop_measure$_2;
-  condGoto true loop_entry$_1 loop_entry$_1
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true loop_entry$_1 loop_entry$_1
 end$_0:
-  finish
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] finish
 -/
 #guard_msgs in
 #eval (Std.format (singleCFG measureFailExamplePgm 0))
@@ -146,7 +149,7 @@ before_loop$_8:
   var i : int;
   i := 0;
   s := 0;
-  condGoto true loop_entry$_1 loop_entry$_1
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true loop_entry$_1 loop_entry$_1
 loop_entry$_1:
   assert [inv$_5]: 0 <= i;
   assert [inv$_6]: i <= n;
@@ -154,16 +157,20 @@ loop_entry$_1:
   var loop_measure$_2 : int;
   assume [assume_loop_measure$_2]: loop_measure$_2 == n - i;
   assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
-  condGoto i < n l$_4 end$_0
+  #[<[provenance]: :3280-3436>,
+ <[#spec_loop_invariant]: 0 <= i>,
+ <[#spec_loop_invariant]: i <= n>,
+ <[#spec_loop_invariant]: s == i * (i + 1) / 2>,
+ <[#spec_decreases]: n - i>] condGoto i < n l$_4 end$_0
 l$_4:
   i := i + 1;
   s := s + i;
-  condGoto true measure_decrease$_3 measure_decrease$_3
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true measure_decrease$_3 measure_decrease$_3
 measure_decrease$_3:
   assert [measure_decrease_loop_measure$_2]: n - i < loop_measure$_2;
-  condGoto true loop_entry$_1 loop_entry$_1
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true loop_entry$_1 loop_entry$_1
 end$_0:
-  finish
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] finish
 -/
 #guard_msgs in
 #eval (Std.format (singleCFG gaussPgm 0))
@@ -393,7 +400,7 @@ before_loop$_15:
   var x : int;
   var y : int;
   x := 0;
-  condGoto true loop_entry$_1 loop_entry$_1
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true loop_entry$_1 loop_entry$_1
 loop_entry$_1:
   assert [inv$_12]: x >= 0;
   assert [inv$_13]: x <= n;
@@ -406,31 +413,38 @@ Context: Global scope:
   var loop_measure$_2 : int;
   assume [assume_loop_measure$_2]: loop_measure$_2 == n - x;
   assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0);
-  condGoto x < n before_loop$_11 end$_0
+  #[<[provenance]: :9390-9643>,
+ <[#spec_loop_invariant]: x >= 0>,
+ <[#spec_loop_invariant]: x <= n>,
+ <[#spec_loop_invariant]: n < top>,
+ <[#spec_decreases]: n - x>] condGoto x < n before_loop$_11 end$_0
 before_loop$_11:
   y := 0;
-  condGoto true loop_entry$_5 loop_entry$_5
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true loop_entry$_5 loop_entry$_5
 loop_entry$_5:
   assert [inv$_9]: y >= 0;
   assert [inv$_10]: y <= x;
   var loop_measure$_6 : int;
   assume [assume_loop_measure$_6]: loop_measure$_6 == x - y;
   assert [measure_lb_loop_measure$_6]: !(loop_measure$_6 < 0);
-  condGoto y < x l$_8 l$_4
+  #[<[provenance]: :9510-9623>,
+ <[#spec_loop_invariant]: y >= 0>,
+ <[#spec_loop_invariant]: y <= x>,
+ <[#spec_decreases]: x - y>] condGoto y < x l$_8 l$_4
 l$_8:
   y := y + 1;
-  condGoto true measure_decrease$_7 measure_decrease$_7
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true measure_decrease$_7 measure_decrease$_7
 measure_decrease$_7:
   assert [measure_decrease_loop_measure$_6]: x - y < loop_measure$_6;
-  condGoto true loop_entry$_5 loop_entry$_5
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true loop_entry$_5 loop_entry$_5
 l$_4:
   x := x + 1;
-  condGoto true measure_decrease$_3 measure_decrease$_3
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true measure_decrease$_3 measure_decrease$_3
 measure_decrease$_3:
   assert [measure_decrease_loop_measure$_2]: n - x < loop_measure$_2;
-  condGoto true loop_entry$_1 loop_entry$_1
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] condGoto true loop_entry$_1 loop_entry$_1
 end$_0:
-  finish
+  #[<[provenance]: <synthesized:structured-to-unstructured>>] finish
 -/
 #guard_msgs in
 #eval (Std.format (singleCFG nestedPgm 2))
diff --git a/StrataTest/Languages/Core/Tests/CFGParseTests.lean b/StrataTest/Languages/Core/Tests/CFGParseTests.lean
new file mode 100644
index 0000000000..a32f4db73d
--- /dev/null
+++ b/StrataTest/Languages/Core/Tests/CFGParseTests.lean
@@ -0,0 +1,406 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import StrataDDM.Elab
+import StrataDDM.BuiltinDialects.Init
+import Strata.Languages.Core.DDMTransform.Grammar
+import Strata.Languages.Core.Verifier
+import Strata.SimpleAPI
+
+/-! # Tests for CFG (unstructured) procedure parsing -/
+
+open Strata
+open StrataDDM.Elab (parseStrataProgramFromDialect)
+
+private def parseCoreText (input : String) : IO Core.Program := do
+  let inputCtx := StrataDDM.Parser.stringInputContext "inline" input
+  let dialects := StrataDDM.Elab.LoadedDialects.ofDialects! #[StrataDDM.initDialect, Strata.Core]
+  let strataProgram ← parseStrataProgramFromDialect dialects Strata.Core.name inputCtx
+  let (program, errors) := Core.getProgram strataProgram inputCtx
+  if errors.isEmpty then
+    pure program
+  else
+    throw (IO.userError s!"Core DDM translation errors:\n{String.intercalate "\n" errors.toList}")
+
+private def printCFGProcInfo (prog : Core.Program) : IO Unit := do
+  for d in prog.decls do
+    match d with
+    | .proc p _ =>
+      IO.println s!"Procedure: {Core.CoreIdent.toPretty p.header.name}"
+      match p.body with
+      | .cfg c =>
+        IO.println s!"  CFG entry: {c.entry}, {c.blocks.length} blocks"
+        for (lbl, blk) in c.blocks do
+          let transferDesc := match blk.transfer with
+            | .condGoto _ l1 l2 _ => if l1 == l2 then s!"goto {l1}" else s!"branch → {l1}/{l2}"
+            | .finish _ => "return"
+          IO.println s!"  Block '{lbl}': {blk.cmds.length} cmds, {transferDesc}"
+      | .structured _ => IO.println "  ERROR: expected CFG body"
+    | _ => pure ()
+
+/-! ## Deterministic CFG with conditional branch -/
+
+/--
+info: Procedure: Max
+  CFG entry: entry, 4 blocks
+  Block 'entry': 0 cmds, branch → then_branch/else_branch
+  Block 'then_branch': 1 cmds, goto done
+  Block 'else_branch': 1 cmds, goto done
+  Block 'done': 0 cmds, return
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure Max(x : int, y : int, out m : int)
+spec {
+  ensures (m >= x);
+  ensures (m >= y);
+}
+cfg entry {
+  entry: {
+    branch (x >= y) goto then_branch else goto else_branch;
+  }
+  then_branch: {
+    m := x;
+    goto done;
+  }
+  else_branch: {
+    m := y;
+    goto done;
+  }
+  done: {
+    return;
+  }
+};
+"
+  printCFGProcInfo prog
+
+/-! ## Nondeterministic CFG with multi-target goto -/
+
+/--
+info: Procedure: NondetChoice
+  CFG entry: entry, 4 blocks
+  Block 'entry': 1 cmds, branch → left/right
+  Block 'left': 1 cmds, goto done
+  Block 'right': 1 cmds, goto done
+  Block 'done': 0 cmds, return
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure NondetChoice(out y : int)
+cfg entry {
+  entry: {
+    goto left, right;
+  }
+  left: {
+    y := 1;
+    goto done;
+  }
+  right: {
+    y := 2;
+    goto done;
+  }
+  done: {
+    return;
+  }
+};
+"
+  printCFGProcInfo prog
+
+/-! ## CFG loop pattern -/
+
+/--
+info: Procedure: CountUp
+  CFG entry: entry, 4 blocks
+  Block 'entry': 1 cmds, goto loop
+  Block 'loop': 0 cmds, branch → body/done
+  Block 'body': 1 cmds, goto loop
+  Block 'done': 0 cmds, return
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure CountUp(n : int, out y : int)
+spec {
+  requires (n >= 0);
+}
+cfg entry {
+  entry: {
+    y := 0;
+    goto loop;
+  }
+  loop: {
+    branch (y < n) goto body else goto done;
+  }
+  body: {
+    y := y + 1;
+    goto loop;
+  }
+  done: {
+    return;
+  }
+};
+"
+  printCFGProcInfo prog
+
+/-! ## Empty block (just a transfer) -/
+
+/--
+info: Procedure: Trivial
+  CFG entry: start, 1 blocks
+  Block 'start': 0 cmds, return
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure Trivial()
+cfg start {
+  start: {
+    return;
+  }
+};
+"
+  printCFGProcInfo prog
+
+/-! ## End-to-end: type-checking accepts well-formed CFG procedures -/
+
+/--
+info: type-check accepted CFG procedure
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure Trivial()
+cfg start {
+  start: {
+    return;
+  }
+};
+"
+  match Core.typeCheck .quiet prog with
+  | .error dm => IO.println s!"ERROR: type-check rejected CFG procedure: {dm.message}"
+  | .ok _ => IO.println "type-check accepted CFG procedure"
+
+/-! ## End-to-end: type-checking accepts Max (branches + assignments) -/
+
+/--
+info: type-check accepted Max with CFG body preserved (4 blocks)
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure Max(x : int, y : int, out m : int)
+spec {
+  ensures (m >= x);
+  ensures (m >= y);
+}
+cfg entry {
+  entry: {
+    branch (x >= y) goto then_branch else goto else_branch;
+  }
+  then_branch: {
+    m := x;
+    goto done;
+  }
+  else_branch: {
+    m := y;
+    goto done;
+  }
+  done: {
+    return;
+  }
+};
+"
+  match Core.typeCheck .quiet prog with
+  | .error dm => IO.println s!"ERROR: {dm.message}"
+  | .ok prog' =>
+    for d in prog'.decls do
+      match d with
+      | .proc p _ =>
+        match p.body with
+        | .cfg c =>
+          IO.println s!"type-check accepted Max with CFG body preserved ({c.blocks.length} blocks)"
+        | .structured ss =>
+          IO.println s!"ERROR: body collapsed to .structured with {ss.length} statements"
+      | _ => pure ()
+
+/-! ## End-to-end: type-checking accepts CountUp (loop pattern with init) -/
+
+/--
+info: type-check accepted CountUp
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure CountUp(n : int, out y : int)
+spec {
+  requires (n >= 0);
+}
+cfg entry {
+  entry: {
+    y := 0;
+    goto loop;
+  }
+  loop: {
+    branch (y < n) goto body else goto done;
+  }
+  body: {
+    y := y + 1;
+    goto loop;
+  }
+  done: {
+    return;
+  }
+};
+"
+  match Core.typeCheck .quiet prog with
+  | .error dm => IO.println s!"ERROR: {dm.message}"
+  | .ok _ => IO.println "type-check accepted CountUp"
+
+/-! ## Error: duplicate block labels -/
+
+/--
+info: rejected: Duplicate block labels in CFG
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure Bad()
+cfg start {
+  start: { return; }
+  start: { return; }
+};
+"
+  match Core.typeCheck .quiet prog with
+  | .error dm =>
+    if dm.message.contains "Duplicate block labels" then
+      IO.println "rejected: Duplicate block labels in CFG"
+    else
+      IO.println s!"ERROR: unexpected message: {dm.message}"
+  | .ok _ => IO.println "ERROR: expected type-check to fail"
+
+/-! ## Error: unknown target label -/
+
+/--
+info: rejected: branches to unknown label
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure Bad(out y : int)
+cfg start {
+  start: {
+    y := 0;
+    goto nonexistent;
+  }
+};
+"
+  match Core.typeCheck .quiet prog with
+  | .error dm =>
+    if dm.message.contains "branches to unknown label" then
+      IO.println "rejected: branches to unknown label"
+    else
+      IO.println s!"ERROR: unexpected message: {dm.message}"
+  | .ok _ => IO.println "ERROR: expected type-check to fail"
+
+/-! ## Error: type mismatch in CFG command -/
+
+/--
+info: rejected: type error in CFG command
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure Bad(x : bool, out y : int)
+cfg start {
+  start: {
+    y := x;
+    return;
+  }
+};
+"
+  match Core.typeCheck .quiet prog with
+  | .error _ =>
+    IO.println "rejected: type error in CFG command"
+  | .ok _ => IO.println "ERROR: expected type-check to fail"
+
+/-! ## Error: modification rights violation in CFG -/
+
+/--
+info: rejected: modifies disallowed variable
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure Bad(x : int)
+cfg start {
+  start: {
+    x := 42;
+    return;
+  }
+};
+"
+  match Core.typeCheck .quiet prog with
+  | .error dm =>
+    if dm.message.contains "modifies variables" then
+      IO.println "rejected: modifies disallowed variable"
+    else
+      IO.println s!"ERROR: unexpected message: {dm.message}"
+  | .ok _ => IO.println "ERROR: expected type-check to fail"
+
+/-! ## Multiple nondet gotos get distinct condition variables -/
+
+open Std (format) in
+private def getTransferCondStr (blk : Imperative.DetBlock String Core.Command Core.Expression)
+    : Option String :=
+  match blk.transfer with
+  | .condGoto cond l1 l2 _ =>
+    if l1 != l2 then some (toString (format cond)) else none
+  | _ => none
+
+/--
+info: nondet condition names are distinct across blocks
+-/
+#guard_msgs in
+#eval do
+  let prog ← parseCoreText "
+procedure MultiNondet(out y : int)
+cfg entry {
+  entry: {
+    goto a, b;
+  }
+  a: {
+    goto c, d;
+  }
+  b: {
+    y := 1;
+    goto done;
+  }
+  c: {
+    y := 2;
+    goto done;
+  }
+  d: {
+    y := 3;
+    goto done;
+  }
+  done: {
+    return;
+  }
+};
+"
+  for d in prog.decls do
+    match d with
+    | .proc p _ =>
+      match p.body with
+      | .cfg cfg =>
+        let condNames := cfg.blocks.filterMap fun (pair : String × _) => getTransferCondStr pair.2
+        if condNames.length == 2 && condNames.Nodup then
+          IO.println "nondet condition names are distinct across blocks"
+        else
+          IO.println s!"ERROR: expected 2 distinct nondet conditions, got {condNames}"
+      | .structured _ => IO.println "ERROR: expected CFG body"
+    | _ => pure ()
diff --git a/StrataTest/Languages/Core/Tests/ProcedureEvalCFGTests.lean b/StrataTest/Languages/Core/Tests/ProcedureEvalCFGTests.lean
new file mode 100644
index 0000000000..8447e5a2d5
--- /dev/null
+++ b/StrataTest/Languages/Core/Tests/ProcedureEvalCFGTests.lean
@@ -0,0 +1,316 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Core.ProcedureEval
+
+namespace Core
+
+section CFGEvalTests
+
+open Std (ToFormat Format format)
+open Procedure Statement Lambda Lambda.LTy.Syntax Lambda.LExpr.SyntaxMono Core.Syntax
+open Imperative
+
+private def cfgEval (p : Procedure) : String :=
+  let E := Env.init (empty_factory := true)
+  let (E, _stats) := eval E p
+  toString (format E)
+
+/-! ## Trivial CFG: single block with finish, no parameters -/
+
+/--
+info: Error:
+none
+Subst Map:
+
+Expression Env:
+State:
+
+
+Evaluation Config:
+Eval Depth: 200
+Factory Functions:
+
+
+
+Datatypes:
+
+Path Conditions:
+
+
+Warnings:
+[]
+Deferred Proof Obligations:
+-/
+#guard_msgs in
+#eval IO.println (cfgEval
+  { header := {name := "Trivial", typeArgs := [], inputs := [], outputs := [] },
+    spec := { preconditions := [], postconditions := [] },
+    body := .cfg { entry := "start",
+                   blocks := [("start", { cmds := [], transfer := .finish .empty })] } })
+
+/-! ## Linear CFG: assignment via goto, postcondition holds -/
+
+/--
+info: Error:
+none
+Subst Map:
+
+Expression Env:
+State:
+
+
+Evaluation Config:
+Eval Depth: 200
+Factory Functions:
+
+
+
+Datatypes:
+
+Path Conditions:
+
+
+Warnings:
+[]
+Deferred Proof Obligations:
+Label: y_eq_42
+Property: assert
+Assumptions:
+
+Proof Obligation:
+true
+-/
+#guard_msgs in
+#eval IO.println (cfgEval
+  { header := {name := "Linear", typeArgs := [],
+               inputs := [], outputs := [("y", mty[int])] },
+    spec := { preconditions := [],
+              postconditions := [("y_eq_42", ⟨eb[y == #42], .Default, #[]⟩)] },
+    body := .cfg { entry := "entry",
+                   blocks := [
+                     ("entry", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[#42]) .empty)],
+                                 transfer := .goto "done" .empty }),
+                     ("done", { cmds := [], transfer := .finish .empty })
+                   ] } })
+
+/-! ## Missing block error -/
+
+/--
+info: Error:
+some [ERROR] evalCFG: block 'nonexistent' not found in CFG
+Subst Map:
+
+Expression Env:
+State:
+[]
+
+Evaluation Config:
+Eval Depth: 200
+Factory Functions:
+
+
+
+Datatypes:
+
+Path Conditions:
+
+
+
+Warnings:
+[]
+Deferred Proof Obligations:
+-/
+#guard_msgs in
+#eval IO.println (cfgEval
+  { header := {name := "MissingBlock", typeArgs := [], inputs := [], outputs := [] },
+    spec := { preconditions := [], postconditions := [] },
+    body := .cfg { entry := "start",
+                   blocks := [("start", { cmds := [],
+                                          transfer := .goto "nonexistent" .empty })] } })
+
+/-! ## Fuel exhaustion: loop back-edge -/
+
+/--
+info: has error: true
+-/
+#guard_msgs in
+#eval do
+  let E := Env.init (empty_factory := true)
+  let p : Procedure :=
+    { header := {name := "Loop", typeArgs := [],
+                 inputs := [], outputs := [("y", mty[int])] },
+      spec := { preconditions := [], postconditions := [] },
+      body := .cfg { entry := "loop",
+                     blocks := [
+                       ("loop", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[#1]) .empty)],
+                                  transfer := .goto "loop" .empty })
+                     ] } }
+  let (E, _stats) := eval E p
+  IO.println s!"has error: {E.error.isSome}"
+
+/-! ## Postcondition failure: non-trivial proof obligation -/
+
+/--
+info: Error:
+none
+Subst Map:
+
+Expression Env:
+State:
+
+
+Evaluation Config:
+Eval Depth: 200
+Factory Functions:
+
+
+
+Datatypes:
+
+Path Conditions:
+
+
+Warnings:
+[]
+Deferred Proof Obligations:
+Label: y_eq_0
+Property: assert
+Assumptions:
+
+Proof Obligation:
+false
+-/
+#guard_msgs in
+#eval IO.println (cfgEval
+  { header := {name := "PostFail", typeArgs := [],
+               inputs := [], outputs := [("y", mty[int])] },
+    spec := { preconditions := [],
+              postconditions := [("y_eq_0", ⟨eb[y == #0], .Default, #[]⟩)] },
+    body := .cfg { entry := "entry",
+                   blocks := [
+                     ("entry", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[#42]) .empty)],
+                                 transfer := .finish .empty })
+                   ] } })
+
+/-! ## Diamond CFG: symbolic branch produces two proof obligations -/
+
+/--
+info: Error:
+none
+Subst Map:
+
+Expression Env:
+State:
+
+
+Evaluation Config:
+Eval Depth: 200
+Factory Functions:
+
+
+
+Datatypes:
+
+Path Conditions:
+
+
+Warnings:
+[]
+Deferred Proof Obligations:
+Label: y_ge_0
+Property: assert
+Assumptions:
+(<cfgBranch_true: x >= 0>, x@1 >= 0)
+Proof Obligation:
+x@1 >= 0
+
+Label: y_ge_0
+Property: assert
+Assumptions:
+(<cfgBranch_false: !(x >= 0)>, if x@1 >= 0 then false else true)
+Proof Obligation:
+0 - x@1 >= 0
+-/
+#guard_msgs in
+#eval IO.println (cfgEval
+  { header := {name := "Diamond", typeArgs := [],
+               inputs := [("x", mty[int])],
+               outputs := [("y", mty[int])] },
+    spec := { preconditions := [],
+              postconditions := [("y_ge_0", ⟨eb[((~Int.Ge y) #0)], .Default, #[]⟩)] },
+    body := .cfg { entry := "entry",
+                   blocks := [
+                     ("entry", { cmds := [],
+                                 transfer := .condGoto eb[((~Int.Ge x) #0)] "pos" "neg" .empty }),
+                     ("pos", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[x]) .empty)],
+                               transfer := .goto "done" .empty }),
+                     ("neg", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[((~Int.Sub #0) x)]) .empty)],
+                               transfer := .goto "done" .empty }),
+                     ("done", { cmds := [], transfer := .finish .empty })
+                   ] } })
+
+/-! ## Pre-split assert deduped across symbolic condGoto
+
+An `assert` evaluated *before* a symbolic `condGoto` lands in the parent
+env's `deferred` array. Both branches inherit `env'` by record-update, so
+without dedup the pre-split obligation would appear once per terminal
+path after `mergeResults` concatenates them. Each `ProofObligation`
+captures its assumptions at creation time (see
+`Strata/DL/Imperative/CmdEval.lean`), so duplicates are redundant: the
+fix in `evalCFGStep` clears the false-branch's `deferred`, mirroring
+`Strata/Languages/Core/StatementEval.lean` for the structured `.ite`
+path. This test exercises that dedup — the `pre_assert` obligation must
+appear exactly once in the merged output.
+-/
+
+/--
+info: Error:
+none
+Subst Map:
+
+Expression Env:
+State:
+
+
+Evaluation Config:
+Eval Depth: 200
+Factory Functions:
+
+
+
+Datatypes:
+
+Path Conditions:
+
+
+Warnings:
+[]
+Deferred Proof Obligations:
+Label: pre_assert
+Property: assert
+Assumptions:
+
+Proof Obligation:
+x@1 >= 0
+-/
+#guard_msgs in
+#eval IO.println (cfgEval
+  { header := {name := "PreSplitAssert", typeArgs := [],
+               inputs := [("x", mty[int])],
+               outputs := [] },
+    spec := { preconditions := [],
+              postconditions := [] },
+    body := .cfg { entry := "entry",
+                   blocks := [
+                     ("entry", { cmds := [CmdExt.cmd (Cmd.assert "pre_assert" eb[((~Int.Ge x) #0)] .empty)],
+                                 transfer := .condGoto eb[((~Int.Ge x) #0)] "left" "right" .empty }),
+                     ("left",  { cmds := [], transfer := .finish .empty }),
+                     ("right", { cmds := [], transfer := .finish .empty })
+                   ] } })
+
+end CFGEvalTests
+end Core
diff --git a/StrataTest/Transform/ProcedureInlining.lean b/StrataTest/Transform/ProcedureInlining.lean
index ace24853b7..7c8ce6e36b 100644
--- a/StrataTest/Transform/ProcedureInlining.lean
+++ b/StrataTest/Transform/ProcedureInlining.lean
@@ -214,6 +214,37 @@ def alphaEquivStatement (s1 s2: Core.Statement) (map:IdMap)
 
 end
 
+private def alphaEquivCmds (cmds1 cmds2 : List Core.Command) (map : IdMap)
+    : Except Format IdMap := do
+  if cmds1.length ≠ cmds2.length then
+    .error f!"CFG block command count mismatch: {cmds1.length} vs {cmds2.length}"
+  else
+    (cmds1.zip cmds2).foldlM (fun map (c1, c2) =>
+      alphaEquivStatement (.cmd c1) (.cmd c2) map) map
+
+private def alphaEquivTransfer (t1 t2 : Imperative.DetTransferCmd String Core.Expression)
+    (map : IdMap) : Except Format IdMap := do
+  match t1, t2 with
+  | .condGoto c1 lt1 lf1 _, .condGoto c2 lt2 lf2 _ =>
+    if ¬ alphaEquivExprs c1 c2 map then
+      .error f!"CFG transfer condition mismatch"
+    else
+      let map ← IdMap.updateLabel map lt1 lt2
+      IdMap.updateLabel map lf1 lf2
+  | .finish _, .finish _ => .ok map
+  | _, _ => .error "CFG transfer type mismatch"
+
+private def alphaEquivCFG (cfg1 cfg2 : Core.DetCFG) (map : IdMap)
+    : Except Format IdMap := do
+  let map ← IdMap.updateLabel map cfg1.entry cfg2.entry
+  if cfg1.blocks.length ≠ cfg2.blocks.length then
+    .error f!"CFG block count mismatch: {cfg1.blocks.length} vs {cfg2.blocks.length}"
+  else
+    (cfg1.blocks.zip cfg2.blocks).foldlM (fun map ((lbl1, blk1), (lbl2, blk2)) => do
+      let map ← IdMap.updateLabel map lbl1 lbl2
+      let map ← alphaEquivCmds blk1.cmds blk2.cmds map
+      alphaEquivTransfer blk1.transfer blk2.transfer map) map
+
 private def alphaEquiv (p1 p2:Core.Procedure):Except Format Bool := do
   match p1.body, p2.body with
   | .structured ss1, .structured ss2 =>
@@ -227,7 +258,12 @@ private def alphaEquiv (p1 p2:Core.Procedure):Except Format Bool := do
           alphaEquivStatement s1 s2 map)
         newmap (ss1.zip ss2)
       return ((p1.header.outputs.zip p2.header.outputs).map (fun ((x, _), (y, _)) => alphaEquivIdents x y m)).all id
-  | _, _ => .error f!"alphaEquiv: CFG procedure bodies are not supported in the inlining test harness"
+  | .cfg cfg1, .cfg cfg2 =>
+    let newmap:IdMap := IdMap.mk ([], []) []
+    let m ← alphaEquivCFG cfg1 cfg2 newmap
+    return ((p1.header.outputs.zip p2.header.outputs).map (fun ((x, _), (y, _)) => alphaEquivIdents x y m)).all id
+  | .structured _, .cfg _ => .error "body type mismatch: structured vs cfg"
+  | .cfg _, .structured _ => .error "body type mismatch: cfg vs structured"
 
 
 
diff --git a/StrataTest/Transform/StructuredToUnstructuredTests.lean b/StrataTest/Transform/StructuredToUnstructuredTests.lean
new file mode 100644
index 0000000000..c7e78e91e5
--- /dev/null
+++ b/StrataTest/Transform/StructuredToUnstructuredTests.lean
@@ -0,0 +1,172 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Transform.StructuredToUnstructured
+import Strata.DL.Lambda
+
+/-! ## Tests for loop contract metadata preservation in StructuredToUnstructured -/
+
+section
+open Std (ToFormat Format format)
+open Lambda.LTy.Syntax
+open Imperative (MetaData MetaDataElem)
+
+private abbrev TP : Lambda.LExprParams := ⟨Unit, Unit⟩
+
+private abbrev P : Imperative.PureExpr :=
+   { Ident := TP.Identifier,
+     Expr := Lambda.LExprT TP.mono,
+     Ty := Lambda.LMonoTy,
+     ExprMetadata := TP.Metadata,
+     TyEnv := @Lambda.TEnv TP.IDMeta,
+     TyContext := @Lambda.LContext TP,
+     EvalEnv := Lambda.LState TP
+     EqIdent := inferInstanceAs (DecidableEq TP.Identifier) }
+
+private abbrev mdB : Lambda.Typed Unit := { underlying := (), type := mty[bool] }
+
+instance : Imperative.HasVal P where
+  value _ := True
+
+instance : Imperative.HasBool P where
+  tt := .const mdB (.boolConst true)
+  ff := .const mdB (.boolConst false)
+  tt_is_not_ff := by simp
+  boolTy := mty[bool]
+  boolIsVal := ⟨trivial, trivial⟩
+
+instance : Imperative.HasIdent P where
+  ident s := ⟨s, ()⟩
+
+instance : Imperative.HasFvar P where
+  mkFvar := (.fvar mdB · none)
+  getFvar | .fvar _ v _ => some v | _ => none
+
+instance : Imperative.HasFvars P where
+  getFvars := Lambda.LExpr.LExpr.getVars
+
+instance : Imperative.HasInt P where
+  zero := .intConst mdB 0
+  intTy := mty[int]
+  isNumeral
+    | .const _ (.intConst _) => true
+    | _ => false
+  numeralIsValue _ _ := trivial
+  zeroIsNumeral := rfl
+  numeralHasNoFvars n hn := by
+    cases n with
+    | const _ c => cases c <;> first | rfl | simp_all
+    | _ => simp_all
+
+instance : Imperative.HasIntOps P where
+  eq e1 e2 := .eq mdB e1 e2
+  lt e1 e2 := .app mdB (.app mdB (.op mdB ⟨"Int.Lt", ()⟩ none) e1) e2
+
+instance : Imperative.HasBoolOps P where
+  not e := .app mdB (.op mdB ⟨"Bool.Not", ()⟩ none) e
+  and e1 e2 := .app mdB (.app mdB (.op mdB ⟨"Bool.And", ()⟩ none) e1) e2
+  imp e1 e2 := .app mdB (.app mdB (.op mdB ⟨"Bool.Implies", ()⟩ none) e1) e2
+
+instance : Imperative.HasPassiveCmds P (Imperative.Cmd P) where
+  assert l e md := .assert l e md
+  assume l e md := .assume l e md
+
+instance : Imperative.HasInit P (Imperative.Cmd P) where
+  init i ty e md := .init i ty e md
+
+private def mkFvar (name : String) : P.Expr := .fvar mdB ⟨name, ()⟩ none
+private def trueExpr : P.Expr := .const mdB (.boolConst true)
+
+private abbrev Stmt' := Imperative.Stmt P (Imperative.Cmd P)
+private abbrev CFG' := Imperative.CFG String (Imperative.DetBlock String (Imperative.Cmd P) P)
+
+private def toCFG (ss : List Stmt') : CFG' := Imperative.stmtsToCFG ss
+
+private def findLoopEntry (cfg : CFG') :
+    Option (Imperative.DetBlock String (Imperative.Cmd P) P) :=
+  cfg.blocks.find? (fun (lbl, _) => lbl.startsWith "loop_entry$") |>.map (·.2)
+
+private def getTransferMd (blk : Imperative.DetBlock String (Imperative.Cmd P) P) :
+    MetaData P :=
+  match blk.transfer with
+  | .condGoto _ _ _ md => md
+  | .finish md => md
+
+private def countField (md : MetaData P) (fld : MetaDataElem.Field P) : Nat :=
+  md.filter (fun e => e.fld == fld) |>.size
+
+private def loopEntryMd (ss : List Stmt') : MetaData P :=
+  match findLoopEntry (toCFG ss) with
+  | some blk => getTransferMd blk
+  | none => .empty
+
+private def setCmd (name : String) : Imperative.Cmd P :=
+  .set ⟨name, ()⟩ (.det (mkFvar name)) .empty
+
+/-! ### Simple loop with one invariant: specLoopInvariant in transfer metadata -/
+
+#guard countField (loopEntryMd [
+    .loop (.det trueExpr) none [("inv0", mkFvar "x")] [.cmd (setCmd "x")] .empty
+  ]) MetaData.specLoopInvariant == 1
+
+/-! ### Loop with multiple invariants: one entry per invariant -/
+
+#guard countField (loopEntryMd [
+    .loop (.det trueExpr) none [("inv_a", mkFvar "a"), ("inv_b", mkFvar "b")]
+      [.cmd (setCmd "x")] .empty
+  ]) MetaData.specLoopInvariant == 2
+
+/-! ### Loop with decreases measure: specDecreases in metadata -/
+
+#guard countField (loopEntryMd [
+    .loop (.det trueExpr) (some (mkFvar "n")) [("inv", mkFvar "x")]
+      [.cmd (setCmd "x")] .empty
+  ]) MetaData.specDecreases == 1
+
+/-! ### Loop with both invariants and decreases -/
+
+#guard
+  let md := loopEntryMd [
+    .loop (.det trueExpr) (some (mkFvar "n")) [("inv_a", mkFvar "a"), ("inv_b", mkFvar "b")]
+      [.cmd (setCmd "x")] .empty
+  ]
+  countField md MetaData.specLoopInvariant == 2 &&
+  countField md MetaData.specDecreases == 1
+
+/-! ### Loop without contract: no spec metadata in transfer -/
+
+#guard
+  let md := loopEntryMd [
+    .loop (.det trueExpr) none [] [.cmd (setCmd "x")] .empty
+  ]
+  countField md MetaData.specLoopInvariant == 0 &&
+  countField md MetaData.specDecreases == 0
+
+/-! ### Invariant assert commands still emitted (both behaviors coexist) -/
+
+#guard
+  let cfg := toCFG [
+    .loop (.det trueExpr) none [("my_inv", mkFvar "x")]
+      [.cmd (setCmd "x")] .empty
+  ]
+  match findLoopEntry cfg with
+  | some blk => blk.cmds.any (fun cmd =>
+      match cmd with
+      | .assert label _ _ => label == "my_inv"
+      | _ => false)
+  | none => false
+
+/-! ### Nondet loop guard: contract metadata still present -/
+
+#guard
+  let md := loopEntryMd [
+    .loop .nondet (some (mkFvar "n")) [("inv", mkFvar "x")]
+      [.cmd (setCmd "x")] .empty
+  ]
+  countField md MetaData.specLoopInvariant == 1 &&
+  countField md MetaData.specDecreases == 1
+
+end