diff --git a/.kiro/steering/structure.md b/.kiro/steering/structure.md
index 4445fa325..9a90e562a 100644
--- a/.kiro/steering/structure.md
+++ b/.kiro/steering/structure.md
@@ -180,8 +180,7 @@ Program-to-program translations for simplification and verification. Each has op
 **Main module:** `Strata.lean`
 
 **Executables:**
-- `strata` - Main CLI (includes `verify`, `check`, `toIon`, `print`, etc.)
-- `StrataCoreToGoto` - Strata Core to GOTO translation
+- `strata` - Main CLI (includes `verify`, `coreToGoto`, `check`, `toIon`, `print`, etc.)
 - `StrataToCBMC` - CBMC backend
 
 **Commands:**
diff --git a/README.md b/README.md
index 42203dc30..9d602b99b 100644
--- a/README.md
+++ b/README.md
@@ -42,7 +42,7 @@ Unit tests are run with `#guard_msgs` commands. No output means the tests passed
 To build executable files only and omit proof checks that might take a long time, use
 
 ```bash
-lake build strata:exe strata StrataToCBMC StrataCoreToGoto
+lake build strata:exe strata StrataToCBMC
 ```
 
 ## Running Analyses on Existing Strata Programs
diff --git a/StrataCoreToGoto.lean b/StrataCoreToGoto.lean
deleted file mode 100644
index 0aa2ac279..000000000
--- a/StrataCoreToGoto.lean
+++ /dev/null
@@ -1,82 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
-import Strata.Backends.CBMC.GOTO.CoreToCProverGOTO
-import Strata.Languages.Core.Verifier
-import Strata.Util.IO
-
-open Strata
-
-def usageMessage : Std.Format :=
-  f!"Usage: StrataCoreToGoto [OPTIONS] <file.core.st>{Std.Format.line}\
-  {Std.Format.line}\
-  Translates a Strata Core program to CProver GOTO JSON files.{Std.Format.line}\
-  {Std.Format.line}\
-  Options:{Std.Format.line}\
-  {Std.Format.line}  \
-  --output-dir <dir>    Directory for output files (default: current directory){Std.Format.line}  \
-  --program-name <name> Program name for GOTO output (default: derived from filename)"
-
-structure GotoOptions where
-  outputDir : String := "."
-  programName : Option String := none
-
-def parseOptions (args : List String) : Except Std.Format (GotoOptions × String) :=
-  go {} args
-  where
-    go : GotoOptions → List String → Except Std.Format (GotoOptions × String)
-    | opts, "--output-dir" :: dir :: rest => go {opts with outputDir := dir} rest
-    | opts, "--program-name" :: name :: rest => go {opts with programName := some name} rest
-    | opts, [file] => .ok (opts, file)
-    | _, [] => .error "StrataCoreToGoto requires a .core.st file as input"
-    | _, args => .error f!"Unknown options: {args}"
-
-def deriveBaseName (file : String) : String :=
-  let name := System.FilePath.fileName file |>.getD file
-  -- Strip .core.st or .st suffix
-  if name.endsWith ".core.st" then (name.dropEnd 8).toString
-  else if name.endsWith ".st" then (name.dropEnd 3).toString
-  else name
-
-def main (args : List String) : IO UInt32 := do
-  match parseOptions args with
-  | .ok (opts, file) =>
-    unless file.endsWith ".core.st" do
-      IO.println "Error: expected a .core.st file"
-      IO.println f!"{usageMessage}"
-      return 1
-    let baseName := deriveBaseName file
-    let programName := opts.programName.getD baseName
-    if programName.any "/" || programName.any ".." then
-      IO.println "Error: --program-name must be a simple filename without path separators"
-      return 1
-    let dir := System.FilePath.mk opts.outputDir
-    IO.FS.createDirAll dir
-    let text ← Strata.Util.readInputSource file
-    let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file)
-    let dctx := Elab.LoadedDialects.builtin
-    let dctx := dctx.addDialect! Core
-    let leanEnv ← Lean.mkEmptyEnvironment 0
-    match Strata.Elab.elabProgram dctx leanEnv inputCtx with
-    | .ok pgm =>
-      let symTabFile := dir / s!"{programName}.symtab.json"
-      let gotoFile := dir / s!"{programName}.goto.json"
-      CoreToGOTO.writeToGotoJson
-        (programName := programName)
-        (symTabFileName := symTabFile.toString)
-        (gotoFileName := gotoFile.toString)
-        pgm
-      IO.println s!"Written {symTabFile} and {gotoFile}"
-      return 0
-    | .error errors =>
-      for e in errors do
-        let msg ← e.toString
-        IO.println s!"Error: {msg}"
-      return 1
-  | .error msg =>
-    IO.println f!"{msg}"
-    IO.println f!"{usageMessage}"
-    return 1
diff --git a/StrataMain.lean b/StrataMain.lean
index c3be67030..8526f7a17 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -26,7 +26,9 @@ import Strata.Languages.Python.PythonRuntimeLaurelPart
 import Strata.Languages.Python.PythonLaurelCorePrelude
 import Strata.Backends.CBMC.CollectSymbols
 import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
+import Strata.Backends.CBMC.GOTO.DefaultSymbols
 
+import Strata.Transform.CallElim
 import Strata.SimpleAPI
 
 open Strata
@@ -486,7 +488,7 @@ private def printPyAnalyzeSummary (vcResults : Array Core.VCResult)
 
 private def deriveBaseName (file : String) : String :=
   let name := System.FilePath.fileName file |>.getD file
-  let suffixes := [".python.st.ion", ".py.ion", ".st.ion", ".st"]
+  let suffixes := [".python.st.ion", ".py.ion", ".core.st", ".st.ion", ".st"]
   match suffixes.find? (name.endsWith ·) with
   | some sfx => (name.dropEnd sfx.length).toString
   | none     => name
@@ -1265,9 +1267,164 @@ def verifyCommand : Command where
       println! f!"Finished with {errors.size} errors."
       IO.Process.exit 1
 
+/-- Sanitize a program name to prevent path traversal in output filenames. -/
+private def sanitizeProgramName (name : String) : Option String :=
+  let s := name.replace "/" "" |>.replace "\\" "" |>.replace ".." ""
+  if s.isEmpty then none else some s
+
+def coreToGotoCommand : Command where
+  name := "coreToGoto"
+  args := [ "file" ]
+  flags := [
+    { name := "output-dir", help := "Directory for output files (default: current directory).",
+      takesArg := .arg "dir" },
+    { name := "program-name", help := "Program name for GOTO output (default: derived from filename).",
+      takesArg := .arg "name" },
+    { name := "no-call-elim", help := "Skip call elimination (keep raw calls for external DFCC)." } ]
+  help := "Translate a Strata Core program (.core.st) to CProver GOTO JSON files."
+  callback := fun v pflags => do
+    let file := v[0]
+    unless file.endsWith ".core.st" do
+      exitCmdFailure "coreToGoto" "expected a .core.st file"
+    let baseName := deriveBaseName file
+    let programName ← match sanitizeProgramName (pflags.getString "program-name" |>.getD baseName) with
+      | some n => pure n
+      | none => exitCmdFailure "coreToGoto" "invalid program name"
+    let dir := System.FilePath.mk (pflags.getString "output-dir" |>.getD ".")
+    IO.FS.createDirAll dir
+    let callElim := !pflags.getBool "no-call-elim"
+
+    let text ← Strata.Util.readInputSource file
+    let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file)
+    let dctx := Elab.LoadedDialects.builtin |>.addDialect! Core
+    let leanEnv ← Lean.mkEmptyEnvironment 0
+    match Strata.Elab.elabProgram dctx leanEnv inputCtx with
+    | .error errors =>
+      for e in errors do IO.println s!"Error: {← e.toString}"
+      exitUserError "parsing failed"
+    | .ok pgm =>
+      let Env := Lambda.TEnv.default
+      let tcPgm ← match Strata.typeCheck inputCtx pgm with
+        | .ok p => pure p
+        | .error e => exitUserError s!"Type check error: {e.message}"
+      IO.println "[Strata.Core] Type Checking Succeeded!"
+
+      let tcPgm ← if callElim then
+        match Core.Transform.run tcPgm (fun p => do
+              let (_, p) ← Core.CallElim.callElim' p; return p) with
+        | .ok p => pure p
+        | .error e => exitInternalError s!"Call elimination error: {e}"
+      else pure tcPgm
+
+      let tcPgm ← match Core.typeCheck .default tcPgm with
+        | .ok p => pure p
+        | .error e => exitInternalError s!"Re-type-check error: {e}"
+
+      let tcPgm := inlineFuncDefsInProgram tcPgm
+      let tcPgm := inlineRecFuncDefsInProgram tcPgm
+      let tcPgm := partialEvalDatatypesInProgram tcPgm
+
+      let procs := tcPgm.decls.filterMap fun d => d.getProc?
+      let funcs := tcPgm.decls.filterMap fun d =>
+        match d.getFunc? with
+        | some f =>
+          let name := Core.CoreIdent.toPretty f.name
+          if f.body.isSome && f.typeArgs.isEmpty
+            && name != "Int.DivT" && name != "Int.ModT"
+          then some f else none
+        | none => none
+
+      if procs.isEmpty && funcs.isEmpty then
+        exitUserError "No procedures or functions found"
+
+      let axioms := tcPgm.decls.filterMap fun d => d.getAxiom?
+      let dtAxioms := generateDatatypeAxioms tcPgm
+      let recAxioms := generateRecFuncAxioms tcPgm (unrollDepth := 0)
+      let axioms := axioms ++ dtAxioms ++ recAxioms
+      let distincts := tcPgm.decls.filterMap fun d => match d with
+        | .distinct name es _ => some (name, es) | _ => none
+      let typeSyms ← match collectExtraSymbols tcPgm with
+        | .ok s => pure s
+        | .error e => exitInternalError s!"Error collecting symbols: {e}"
+      let gotoDtInfo := collectGotoDatatypeInfo tcPgm
+
+      let mut symtabPairs : Array (String × Lean.Json) := #[]
+      let mut gotoFns : Array Lean.Json := #[]
+      let mut errors : Nat := 0
+      let globalVarEntries : Map Core.Expression.Ident Core.Expression.Ty :=
+        tcPgm.decls.filterMap fun d =>
+          match d with
+          | .var name ty _ _ => some (name, ty)
+          | _ => none
+      let Env := Lambda.TEnv.addInNewestContext
+        (T := ⟨Core.ExpressionMetadata, Unit⟩) Env globalVarEntries
+
+      let mut allLiftedFuncs : List Core.Function := []
+
+      for p in procs do
+        let procName := Core.CoreIdent.toPretty p.header.name
+        match procedureToGotoCtx Env p (axioms := axioms) (distincts := distincts)
+              (varTypes := tcPgm.getVarTy?) with
+        | .error e => IO.println s!"Error: skipping procedure {procName}: {e}"; errors := errors + 1
+        | .ok (ctx, liftedFuncs) =>
+          allLiftedFuncs := allLiftedFuncs ++ liftedFuncs
+          let ctx := rewriteDatatypeExprsInCtx gotoDtInfo ctx
+          let ctx ← lowerAddressOfInCtx ctx
+          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx)
+          match json.symtab with
+          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+          | _ => pure ()
+          match json.goto with
+          | .obj m =>
+            match m.toList.find? (·.1 == "functions") with
+            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
+            | _ => pure ()
+          | _ => pure ()
+
+      for f in funcs ++ allLiftedFuncs do
+        let funcName := Core.CoreIdent.toPretty f.name
+        match functionToGotoCtx Env f with
+        | .error e => IO.println s!"Error: skipping function {funcName}: {e}"; errors := errors + 1
+        | .ok ctx =>
+          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx)
+          match json.symtab with
+          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+          | _ => pure ()
+          match json.goto with
+          | .obj m =>
+            match m.toList.find? (·.1 == "functions") with
+            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
+            | _ => pure ()
+          | _ => pure ()
+
+      if errors > 0 then
+        exitInternalError s!"{errors} procedure/function translation(s) failed"
+
+      match Lean.toJson typeSyms with
+      | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+      | _ => pure ()
+
+      let mut symtabMap : Std.HashMap String Lean.Json := {}
+      for (k, v) in symtabPairs do
+        symtabMap := symtabMap.insert k v
+
+      for (k, v) in CProverGOTO.defaultSymbols (moduleName := programName) do
+        if !symtabMap.contains k then
+          symtabMap := symtabMap.insert k (Lean.toJson v)
+
+      let symtab := Lean.Json.mkObj [("symbolTable", Lean.Json.mkObj symtabMap.toList)]
+      let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)]
+
+      let symTabFile := dir / s!"{programName}.symtab.json"
+      let gotoFile := dir / s!"{programName}.goto.json"
+      IO.FS.writeFile symTabFile symtab.pretty
+      IO.FS.writeFile gotoFile goto.pretty
+      IO.println s!"Translated {procs.length} procedures and {funcs.length} functions"
+      IO.println s!"Written {symTabFile} and {gotoFile}"
+
 def commandGroups : List CommandGroup := [
   { name := "Core"
-    commands := [verifyCommand, checkCommand, toIonCommand, printCommand, diffCommand]
+    commands := [verifyCommand, coreToGotoCommand, checkCommand, toIonCommand, printCommand, diffCommand]
     commonFlags := [includeFlag] },
   { name := "Code Generation"
     commands := [javaGenCommand] },
diff --git a/StrataTest/Backends/CBMC/GOTO/test_multi_proc.core.st b/StrataTest/Backends/CBMC/GOTO/test_multi_proc.core.st
new file mode 100644
index 000000000..5629e70fe
--- /dev/null
+++ b/StrataTest/Backends/CBMC/GOTO/test_multi_proc.core.st
@@ -0,0 +1,23 @@
+program Core;
+
+var g : int;
+
+procedure helper(x : int) returns (r : int)
+spec {
+  ensures (r > x);
+  modifies g;
+}
+{
+  g := x;
+  r := x + 1;
+};
+
+procedure checker(a : int) returns (result : int)
+spec {
+  requires (a > 0);
+  ensures (result > a);
+}
+{
+  result := a + 1;
+  assert (result > a);
+};
diff --git a/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh b/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
new file mode 100755
index 000000000..cc066a78f
--- /dev/null
+++ b/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
@@ -0,0 +1,76 @@
+#!/bin/bash
+# Test: strata coreToGoto translates multi-procedure programs with contracts.
+#
+# Exercises:
+# 1. Multi-procedure translation (two procedures)
+# 2. Global variable in symbol table
+# 3. Contract annotations on procedures
+# 4. Assertions in GOTO output
+
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)"
+STRATA="$PROJECT_ROOT/.lake/build/bin/strata"
+PYTHON=${PYTHON:-python3}
+
+WORK=$(mktemp -d)
+trap 'rm -rf "$WORK"' EXIT
+
+INPUT="$SCRIPT_DIR/test_multi_proc.core.st"
+
+# Test 1: Multi-procedure translation succeeds
+echo "Test 1: Multi-procedure translation"
+"$STRATA" coreToGoto --output-dir "$WORK" "$INPUT" 2>&1 | grep -q "Translated 2 procedures"
+echo "  OK: translated 2 procedures"
+
+# Test 2: Both procedures in symbol table
+"$PYTHON" -c "
+import json, sys
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+assert 'helper' in st, 'helper not in symtab'
+assert 'checker' in st, 'checker not in symtab'
+print('  OK: helper and checker in symbol table')
+"
+
+# Test 3: Global variable in symbol table with correct attributes
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+assert 'g' in st, 'global variable g not in symtab'
+assert st['g'].get('isStaticLifetime') is True, 'global variable g does not have static lifetime'
+print('  OK: global variable g with static lifetime in symbol table')
+"
+
+# Test 4: Contract annotations present
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+helper_type = json.dumps(st['helper']['type'])
+assert '#spec_ensures' in helper_type, 'No ensures on helper'
+assert '#spec_assigns' in helper_type, 'No assigns on helper'
+checker_type = json.dumps(st['checker']['type'])
+assert '#spec_requires' in checker_type, 'No requires on checker'
+print('  OK: contract annotations present')
+"
+
+# Test 5: GOTO output has assertions
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.goto.json') as f:
+    data = json.load(f)
+fn_names = [fn['name'] for fn in data['functions']]
+assert 'helper' in fn_names, f'helper not in goto functions: {fn_names}'
+assert 'checker' in fn_names, f'checker not in goto functions: {fn_names}'
+for fn in data['functions']:
+    if fn['name'] == 'checker':
+        types = [i['instructionId'] for i in fn['instructions']]
+        assert 'ASSERT' in types, f'No ASSERT in checker: {types}'
+        print('  OK: checker has ASSERT instruction')
+        break
+"
+
+echo "PASS: all strata coreToGoto tests passed"
diff --git a/StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh b/StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh
index 3d642c219..cbaf0a508 100755
--- a/StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh
+++ b/StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh
@@ -6,7 +6,7 @@ rm -f *.gb
 
 echo "Writing out JSON files from a Strata Core program SimpleAdd"
 pushd ../../../../
-lake exe StrataCoreToGoto --output-dir StrataTest/Backends/CBMC/SimpleAdd StrataTest/Backends/CBMC/SimpleAdd/simpleAdd.core.st
+lake exe strata coreToGoto --output-dir StrataTest/Backends/CBMC/SimpleAdd StrataTest/Backends/CBMC/SimpleAdd/simpleAdd.core.st
 popd
 
 # The symtab.json now includes CBMC default symbols directly.
diff --git a/lakefile.toml b/lakefile.toml
index 60070b7d0..4c1625c98 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,6 +1,6 @@
 name = "Strata"
 version = "0.1.0"
-defaultTargets = ["Strata", "strata", "StrataMain", "StrataToCBMC", "StrataCoreToGoto"]
+defaultTargets = ["Strata", "strata", "StrataMain", "StrataToCBMC"]
 testDriver = "StrataTest"
 
 [[require]]
@@ -26,8 +26,5 @@ globs = ["StrataTest.+"]
 [[lean_exe]]
 name = "StrataToCBMC"
 
-[[lean_exe]]
-name = "StrataCoreToGoto"
-
 [[lean_exe]]
 name = "DiffTestCore"