diff --git a/Strata/DDM/Integration/Lean/OfAstM.lean b/Strata/DDM/Integration/Lean/OfAstM.lean
index 1b14f117e..48315bd02 100644
--- a/Strata/DDM/Integration/Lean/OfAstM.lean
+++ b/Strata/DDM/Integration/Lean/OfAstM.lean
@@ -222,6 +222,9 @@ def ofOptionM {α β} [Repr α] [SizeOf α]
       pure { ann := ann, val := none }
     | some v =>
       (fun v => { ann := ann, val := some v }) <$> act v (by decreasing_tactic)
+  -- Treat Init.boolFalse as none (used by some generators to represent absent optional values)
+  | .op ⟨ann, q`Init.boolFalse, #[]⟩ =>
+      pure { ann := ann, val := none }
   | _ => throwExpected "option" arg
 
 def ofSeqM {α β} [Repr α] [SizeOf α]
diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index 62b22179f..be67a015d 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -375,6 +375,10 @@ def Body.isExternal : Body → Bool
   | .External => true
   | _ => false
 
+def Body.isTransparent : Body → Bool
+  | .Transparent _ => true
+  | _ => false
+
 def HighTypeMd.isBool (t : HighTypeMd) : Bool := t.val.isBool
 
 /--
diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean
index d1fbadf17..2f0f4fd98 100644
--- a/Strata/Languages/Python/PySpecPipeline.lean
+++ b/Strata/Languages/Python/PySpecPipeline.lean
@@ -31,6 +31,8 @@ public structure PySpecLaurelResult where
   laurelProgram : Laurel.Program
   overloads : OverloadTable
   functionSignatures : List Python.PythonFunctionDecl := []
+  /-- Maps unprefixed class names to prefixed names for type resolution. -/
+  typeAliases : Std.HashMap String String := {}
 
 /-! ### Private Helpers -/
 
@@ -110,6 +112,7 @@ public def buildPySpecLaurel (pyspecPaths : Array String)
   let mut combinedTypes : Array (Laurel.TypeDefinition × String) := #[]
   let mut allOverloads := overloads
   let mut funcSigs : List Python.PythonFunctionDecl := []
+  let mut allTypeAliases : Std.HashMap String String := {}
   for ionPath in pyspecPaths do
     let ionFile : System.FilePath := ionPath
     let some mod := ionFile.fileStem
@@ -121,7 +124,7 @@ public def buildPySpecLaurel (pyspecPaths : Array String)
       match ← Python.Specs.readDDM ionFile |>.toBaseIO with
       | .ok t => pure t
       | .error msg => throw s!"Could not read {ionFile}: {msg}"
-    let { program, errors, overloads } :=
+    let { program, errors, overloads, typeAliases } :=
       Python.Specs.ToLaurel.signaturesToLaurel ionPath sigs modulePrefix
     if errors.size > 0 then
       let _ ← IO.eprintln
@@ -129,6 +132,7 @@ public def buildPySpecLaurel (pyspecPaths : Array String)
       for err in errors do
         let _ ← IO.eprintln s!"  {err.file}: {err.message}" |>.toBaseIO
     allOverloads := mergeOverloads allOverloads overloads
+    allTypeAliases := typeAliases.fold (init := allTypeAliases) fun m k v => m.insert k v
     match extractFunctionSignatures sigs modulePrefix with
     | .ok fs => funcSigs := funcSigs ++ fs
     | .error msg => throw msg
@@ -163,7 +167,7 @@ public def buildPySpecLaurel (pyspecPaths : Array String)
     constants := []
   }
   return { laurelProgram := combinedLaurel, overloads := allOverloads
-           functionSignatures := funcSigs }
+           functionSignatures := funcSigs, typeAliases := allTypeAliases }
 
 /-- Read dispatch Ion files and merge their overload tables. -/
 public def readDispatchOverloads
@@ -237,7 +241,8 @@ public def buildPreludeInfo (result : PySpecLaurelResult) : Python.PreludeInfo :
     (Python.PreludeInfo.ofLaurelProgram result.laurelProgram)
   { merged with
     functionSignatures :=
-      result.functionSignatures ++ merged.functionSignatures }
+      result.functionSignatures ++ merged.functionSignatures
+    typeAliases := result.typeAliases }
 
 /-- Combine PySpec and user Laurel programs into a single program,
     prepending External stubs so the Laurel `resolve` pass can see
diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index fe442a52a..3b77056d0 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -91,6 +91,10 @@ structure TranslationContext where
   filePath : String := ""
   /-- Known composite type names (user-defined classes + PySpec types) -/
   compositeTypeNames : Std.HashSet String := {}
+  /-- Maps unprefixed class names to prefixed names (from pyspec). -/
+  typeAliases : Std.HashMap String String := {}
+  /-- Procedure names with transparent bodies (can be inlined / emit StaticCall). -/
+  inlinableProcedures : Std.HashSet String := {}
   /-- Track current class during method translation -/
   currentClassName : Option String := none
   loopBreakLabel : Option String := none
@@ -99,6 +103,11 @@ deriving Inhabited
 
 /-! ## Error Handling -/
 
+/-- Resolve a type name through aliases. Returns the prefixed name if an alias
+    exists, otherwise the original name. -/
+def resolveTypeName (ctx : TranslationContext) (name : String) : String :=
+  ctx.typeAliases.getD name name
+
 /-- Translation errors with context -/
 inductive TranslationError where
   | unsupportedConstruct (msg : String) (pyAst : String)
@@ -658,7 +667,8 @@ partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr
         if callerTy == PyLauType.Any then
           return ("AnyTyInstance" ++ "@" ++ callname, some v, true)
         else
-          return (callerTy ++ "_" ++ callname, some v, false)
+          let resolvedTy := resolveTypeName ctx callerTy
+          return (resolvedTy ++ "_" ++ callname, some v, false)
     | _ => throw (.internalError s!"{repr func} is not a function")
 
 --Kwargs can be a single Dict variable: func_call (**var) or a normal Kwargs (key1 = val1, key2 =val2 ...)
@@ -792,8 +802,12 @@ partial def translateCall (ctx : TranslationContext)
   | .Attribute _ val _attr _ =>
       let _target_trans ← translateExpr ctx val
       if opt_firstarg.isSome then
-        return mkStmtExprMd (.Hole)
-        --return mkStmtExprMd (StmtExpr.InstanceCall target_trans attr.val (trans_args ++ trans_kwords_exprs))
+        -- Emit StaticCall only for procedures with transparent bodies
+        -- (e.g. pyspec with precondition assertions). Opaque procedures stay as Hole.
+        if funcName ∈ ctx.inlinableProcedures then
+          return mkStmtExprMd (StmtExpr.StaticCall funcName (trans_args ++ trans_kwords_exprs))
+        else
+          return mkStmtExprMd (.Hole)
       else
         return mkStmtExprMd (StmtExpr.StaticCall funcName (trans_args ++ trans_kwords_exprs))
   | _ =>  throw (.unsupportedConstruct "Invalid call construct" (toString (repr f)))
@@ -848,8 +862,15 @@ partial def translateAssign  (ctx : TranslationContext)
         let targetExpr := mkStmtExprMd (StmtExpr.Identifier n.val)
         return (ctx, [mkStmtExprMd (StmtExpr.Assign [targetExpr] rhs_trans)])
       else
-        let initStmt := mkStmtExprMd (StmtExpr.LocalVariable n.val AnyTy (mkStmtExprMd .Hole))
-        let newctx := {ctx with variableTypes:=(n.val, "Any")::ctx.variableTypes}
+        -- Use type annotation if it matches a known composite type
+        let annType := annotation.map (fun a => pyExprToString a) |>.getD "Any"
+        let resolvedType := resolveTypeName ctx annType
+        let (varTy, trackType) :=
+          if annType ∈ ctx.compositeTypeNames then
+            (mkHighTypeMd (.UserDefined (mkId resolvedType)), resolvedType)
+          else (AnyTy, "Any")
+        let initStmt := mkStmtExprMd (StmtExpr.LocalVariable n.val varTy (mkStmtExprMd .Hole))
+        let newctx := {ctx with variableTypes:=(n.val, trackType)::ctx.variableTypes}
         return (newctx, [initStmt])
     | _ => return (ctx, [mkStmtExprMd .Hole])
   }
@@ -860,8 +881,9 @@ partial def translateAssign  (ctx : TranslationContext)
         let assignStmts := match rhs_trans.val with
         | .StaticCall fnname args =>
             if fnname.text ∈ ctx.compositeTypeNames then
-              let newExpr := mkStmtExprMd (StmtExpr.New fnname)
-              let varType := mkHighTypeMd (.UserDefined fnname)
+              let resolvedId := mkId (resolveTypeName ctx fnname.text)
+              let newExpr := mkStmtExprMd (StmtExpr.New resolvedId)
+              let varType := mkHighTypeMd (.UserDefined resolvedId)
               if n.val ∈ ctx.variableTypes.unzip.1 then
                 let assignStmt := mkStmtExprMd (StmtExpr.Assign [targetExpr] newExpr)
                 let initStmt := mkStmtExprMd (StmtExpr.InstanceCall (mkStmtExprMd (StmtExpr.Identifier n.val)) "__init__" args)
@@ -884,7 +906,8 @@ partial def translateAssign  (ctx : TranslationContext)
         newctx := match rhs_trans.val with
         | .StaticCall fnname _ =>
             if fnname.text ∈ ctx.compositeTypeNames then
-              {newctx with variableTypes:= newctx.variableTypes ++ [(n.val, fnname.text)]}
+              let resolved := resolveTypeName ctx fnname.text
+              {newctx with variableTypes:= newctx.variableTypes ++ [(n.val, resolved)]}
             else newctx
         | .New className =>
             {newctx with variableTypes:= newctx.variableTypes ++ [(n.val, className.text)]}
@@ -1546,6 +1569,10 @@ structure PreludeInfo where
   functions : List String := []
   /-- Procedure names (non-function callables) -/
   procedureNames : List String := []
+  /-- Maps unprefixed class names to prefixed names (from pyspec). -/
+  typeAliases : Std.HashMap String String := {}
+  /-- Names of procedures with transparent bodies (can be inlined). -/
+  inlinableProcedures : Std.HashSet String := {}
 
 /-- Extract `PreludeInfo` from a `Core.Program`. -/
 def PreludeInfo.ofCoreProgram (prelude : Core.Program) : PreludeInfo where
@@ -1618,6 +1645,9 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
   procedureNames :=
     prog.staticProcedures.filterMap fun p =>
       if p.body.isExternal || p.isFunctional then none else some p.name.text
+  inlinableProcedures :=
+    prog.staticProcedures.foldl (init := {}) fun s p =>
+      if p.body.isTransparent then s.insert p.name.text else s
 
 /-- Merge two `PreludeInfo` values by concatenating each field. -/
 def PreludeInfo.merge (a b : PreludeInfo) : PreludeInfo where
@@ -1627,6 +1657,8 @@ def PreludeInfo.merge (a b : PreludeInfo) : PreludeInfo where
   functionSignatures := a.functionSignatures ++ b.functionSignatures
   functions := a.functions ++ b.functions
   procedureNames := a.procedureNames ++ b.procedureNames
+  typeAliases := b.typeAliases.fold (init := a.typeAliases) fun m k v => m.insert k v
+  inlinableProcedures := b.inlinableProcedures.fold (init := a.inlinableProcedures) fun s n => s.insert n
 
 /-- Translate Python module to Laurel Program using pre-extracted prelude info. -/
 def pythonToLaurel' (info : PreludeInfo)
@@ -1681,9 +1713,28 @@ def pythonToLaurel' (info : PreludeInfo)
     let mut ctx : TranslationContext := match prev_ctx with
     | some prev_ctx => prev_ctx
     | _ =>
+    -- Add unprefixed method names as procedure aliases
+    -- e.g. MessageService_send → same signature as prefix_MessageService_send
+    let preludeProcedures := info.typeAliases.fold (init := info.procedures)
+      fun procs unprefixed prefixed =>
+        info.procedures.fold (init := procs) fun procs' name sig =>
+          if name.startsWith (prefixed ++ "_") then
+            let unprefixedName := unprefixed ++ name.drop prefixed.length
+            procs'.insert unprefixedName sig
+          else procs'
+    -- Add unprefixed class names so Python type annotations resolve
+    let compositeTypeNames := info.typeAliases.fold (init := compositeTypeNames)
+      fun s unprefixed _ => s.insert unprefixed
+    -- Add unprefixed procedure names to inlinableProcedures
+    let inlinableProcedures := info.typeAliases.fold (init := info.inlinableProcedures)
+      fun s unprefixed prefixed =>
+        info.inlinableProcedures.fold (init := s) fun s' name =>
+          if name.startsWith (prefixed ++ "_") then
+            s'.insert (unprefixed ++ name.drop prefixed.length)
+          else s'
     {
       currentClassName := none,
-      preludeProcedures := info.procedures,
+      preludeProcedures := preludeProcedures,
       functionSignatures := info.functionSignatures
       preludeFunctions := info.functions
       preludeTypes := info.types,
@@ -1691,6 +1742,8 @@ def pythonToLaurel' (info : PreludeInfo)
       compositeTypeNames := compositeTypeNames,
       classFieldHighType := classFieldHighType,
       overloadTable := overloadTable,
+      inlinableProcedures := inlinableProcedures,
+      typeAliases := info.typeAliases,
       filePath := filePath
     }
 
diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean
index c2a9b5fb3..a87aabae6 100644
--- a/Strata/Languages/Python/Specs/ToLaurel.lean
+++ b/Strata/Languages/Python/Specs/ToLaurel.lean
@@ -61,6 +61,8 @@ structure ToLaurelState where
   procedures : Array Procedure := #[]
   types : Array TypeDefinition := #[]
   overloads : OverloadTable := {}
+  /-- Maps unprefixed class names to prefixed names for type resolution. -/
+  typeAliases : Std.HashMap String String := {}
 
 /-- Monad for PySpec to Laurel translation. -/
 @[expose] abbrev ToLaurelM := ReaderT ToLaurelContext (StateM ToLaurelState)
@@ -259,6 +261,139 @@ def specTypeToLaurelType (ty : SpecType) : ToLaurelM HighTypeMd := do
     | .stringLiteral _ => return mkTy .TString
     | .typedDict _ _ _ => return mkCore "DictStrAny"
 
+/-! ## SpecExpr to Laurel Translation -/
+
+/-- Wrap a StmtExpr with default metadata. -/
+private def mkStmt (e : StmtExpr) : StmtExprMd :=
+  { val := e, md := .empty }
+
+/-- Create metadata with a file range from the current pyspec file. -/
+private def mkMdWithFileRange (loc : SourceRange) (msg : String := "")
+    : ToLaurelM (Imperative.MetaData Core.Expression) := do
+  let ctx ← read
+  let fr : FileRange := { file := .file ctx.filepath.toString, range := loc }
+  let mut md : Imperative.MetaData Core.Expression := #[⟨Imperative.MetaData.fileRange, .fileRange fr⟩]
+  if !msg.isEmpty then
+    md := md.push ⟨.label "message", .msg msg⟩
+  return md
+
+/-- Wrap a StmtExpr with metadata containing a file range and optional message. -/
+private def mkStmtWithLoc (e : StmtExpr) (loc : SourceRange) (msg : String := "")
+    : ToLaurelM StmtExprMd := do
+  let md ← mkMdWithFileRange loc msg
+  return { val := e, md := md }
+
+/-- Translate a SpecExpr to a Laurel StmtExpr.
+    All values are assumed to be Any-typed (the Python prelude's universal type).
+    Returns `none` for unsupported expressions (placeholders).
+    Uses Core prelude function names (Any_len, DictStrAny_contains, etc.)
+    which are resolved after the Core prelude is prepended. -/
+partial def specExprToLaurel (e : SpecExpr) : ToLaurelM (Option StmtExprMd) :=
+  match e with
+  | .placeholder => do
+    reportError default "Placeholder expression not translatable"
+    return none
+  | .var name => return some (mkStmt (.Identifier (mkId name)))
+  | .intLit v => return some (mkStmt (.StaticCall (mkId "from_int") [mkStmt (.LiteralInt v)]))
+  | .floatLit _ => do
+    reportError default "Float literals not yet supported in preconditions"
+    return none
+  | .getIndex subject field =>
+    match subject with
+    | .var "kwargs" => return some (mkStmt (.Identifier (mkId field)))
+    | _ => do
+      let s? ← specExprToLaurel subject
+      return s?.map fun s => mkStmt (.FieldSelect s (mkId field))
+  | .isInstanceOf _ typeName => do
+    reportError default s!"isinstance check for '{typeName}' not yet supported in preconditions"
+    return none
+  | .len subject => do
+    -- len(x) where x is Any: Str.Length(Any..as_string!(x)) wrapped as from_int
+    let s? ← specExprToLaurel subject
+    return s?.map fun s =>
+      let unwrapped := mkStmt (.StaticCall (mkId "Any..as_string!") [s])
+      mkStmt (.StaticCall (mkId "from_int") [mkStmt (.StaticCall (mkId "Str.Length") [unwrapped])])
+  | .intGe subject bound => do
+    let s? ← specExprToLaurel subject; let b? ← specExprToLaurel bound
+    return do
+      let s ← s?; let b ← b?
+      some (mkStmt (.PrimitiveOp .Geq [mkStmt (.StaticCall (mkId "Any..as_int!") [s]), mkStmt (.StaticCall (mkId "Any..as_int!") [b])]))
+  | .intLe subject bound => do
+    let s? ← specExprToLaurel subject; let b? ← specExprToLaurel bound
+    return do
+      let s ← s?; let b ← b?
+      some (mkStmt (.PrimitiveOp .Leq [mkStmt (.StaticCall (mkId "Any..as_int!") [s]), mkStmt (.StaticCall (mkId "Any..as_int!") [b])]))
+  | .floatGe subject bound => do
+    let s? ← specExprToLaurel subject; let b? ← specExprToLaurel bound
+    return do let s ← s?; let b ← b?; some (mkStmt (.PrimitiveOp .Geq [s, b]))
+  | .floatLe subject bound => do
+    let s? ← specExprToLaurel subject; let b? ← specExprToLaurel bound
+    return do let s ← s?; let b ← b?; some (mkStmt (.PrimitiveOp .Leq [s, b]))
+  | .not inner => do
+    let i? ← specExprToLaurel inner
+    return i?.map fun i => mkStmt (.PrimitiveOp .Not [i])
+  | .implies cond body => do
+    let c? ← specExprToLaurel cond; let b? ← specExprToLaurel body
+    return do let c ← c?; let b ← b?; some (mkStmt (.PrimitiveOp .Implies [c, b]))
+  | .enumMember subject values => do
+    let s? ← specExprToLaurel subject
+    return s?.map fun s =>
+      let sStr := mkStmt (.StaticCall (mkId "Any..as_string!") [s])
+      let eqs := values.toList.map fun v =>
+        mkStmt (.PrimitiveOp .Eq [sStr, mkStmt (.LiteralString v)])
+      eqs.foldl (init := mkStmt (.LiteralBool false)) fun acc eq =>
+        mkStmt (.PrimitiveOp .Or [acc, eq])
+  | .containsKey container key => do
+    match container with
+    | .var "kwargs" =>
+      -- containsKey(kwargs, "key") → parameter was provided (not None)
+      return some (mkStmt (.PrimitiveOp .Not
+        [mkStmt (.StaticCall (mkId "Any..isfrom_none") [mkStmt (.Identifier (mkId key))])]))
+    | _ =>
+      let c? ← specExprToLaurel container
+      return c?.map fun c =>
+        let unwrapped := mkStmt (.StaticCall (mkId "Any..as_Dict!") [c])
+        mkStmt (.StaticCall (mkId "DictStrAny_contains") [unwrapped, mkStmt (.LiteralString key)])
+  | .regexMatch _ _ => do
+    reportError default "regexMatch not yet supported (requires PR #623)"
+    return none
+  | .forallList _ _ _ => do
+    reportError default "forallList quantifier not yet supported in preconditions"
+    return none
+  | .forallDict _ _ _ _ => do
+    reportError default "forallDict quantifier not yet supported in preconditions"
+    return none
+
+private def formatAssertionMessage (msg : Array MessagePart) : String :=
+  let parts := msg.map fun
+    | .str s => s
+    | .expr _ => "<expr>"
+  String.join parts.toList
+
+/-- Build a procedure body that asserts preconditions.
+    Outputs are already initialized non-deterministically. -/
+def buildSpecBody (preconditions : Array Assertion) (requiredParams : Array String := #[])
+    : ToLaurelM Body := do
+  let mut stmts : List StmtExprMd := []
+  -- Assert that required parameters are provided (not None)
+  for param in requiredParams do
+    let cond := mkStmt (.PrimitiveOp .Not
+      [mkStmt (.StaticCall (mkId "Any..isfrom_none") [mkStmt (.Identifier (mkId param))])])
+    let assertStmt ← mkStmtWithLoc (.Assert cond) default s!"Required parameter '{param}' is missing"
+    stmts := assertStmt :: stmts
+  for assertion in preconditions do
+    let msg := formatAssertionMessage assertion.message
+    match ← specExprToLaurel assertion.formula with
+    | some condExpr =>
+      let assertStmt ← mkStmtWithLoc (.Assert condExpr) default msg
+      stmts := assertStmt :: stmts
+    | none =>
+      reportError default s!"Untranslatable precondition (emitting assert true): {msg}"
+      let assertStmt ← mkStmtWithLoc (.Assert (mkStmt (.LiteralBool true))) default msg
+      stmts := assertStmt :: stmts
+  let body := mkStmt (.Block stmts.reverse none)
+  return .Transparent body
+
 /-! ## Declaration Translation -/
 
 /-- Convert an Arg to a Laurel Parameter. -/
@@ -300,8 +435,21 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl)
     match retType.val with
     | .TVoid => []
     | _ => [{ name := "result", type := retType }]
-  if func.preconditions.size > 0 || func.postconditions.size > 0 then
-    reportError func.loc "Preconditions/postconditions not yet supported"
+  if func.postconditions.size > 0 then
+    reportError func.loc "Postconditions not yet supported"
+  -- When preconditions exist, use TCore "Any" for all parameters and outputs
+  -- to match the Python→Laurel pipeline's Any-wrapping convention.
+  let (inputs, outputs, body) ←
+    if func.preconditions.size > 0 then do
+      let anyTy : HighTypeMd := mkCore "Any"
+      let anyInputs := inputs.map fun p => { p with type := anyTy }
+      let anyOutputs := outputs.map fun p => { p with type := anyTy }
+      let body ← buildSpecBody func.preconditions
+        (requiredParams := allArgs.filterMap fun a =>
+          if a.default.isNone then some a.name else none)
+      pure (anyInputs, anyOutputs, body)
+    else
+      pure (inputs, outputs, Body.Opaque [] none [])
   return {
     name := procName
     inputs := inputs.toList
@@ -310,13 +458,16 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl)
     determinism := .nondeterministic
     decreases := none
     isFunctional := false
-    body := .Opaque [] none []
+    body := body
     md := .empty
   }
 
 /-- Convert a class definition to Laurel types and procedures. -/
 def classDefToLaurel (cls : ClassDef) : ToLaurelM Unit := do
   let prefixedName ← prefixName cls.name
+  -- Register alias from unprefixed to prefixed name for type resolution
+  if prefixedName != cls.name then
+    modify fun s => { s with typeAliases := s.typeAliases.insert cls.name prefixedName }
   let laurelFields ← cls.fields.toList.mapM fun f => do
     let ty ← specTypeToLaurelType f.type
     pure { name := f.name, isMutable := true, type := ty : Laurel.Field }
@@ -414,6 +565,8 @@ structure TranslationResult where
   program : Laurel.Program
   errors : Array SpecError
   overloads : OverloadTable
+  /-- Maps unprefixed class names to prefixed names for type resolution. -/
+  typeAliases : Std.HashMap String String := {}
 
 /-- Run the translation and return a Laurel Program, dispatch table,
     and any errors. -/
@@ -430,7 +583,8 @@ def signaturesToLaurel (filepath : System.FilePath) (sigs : Array Signature)
   }
   { program := pgm
     errors := state.errors
-    overloads := state.overloads }
+    overloads := state.overloads
+    typeAliases := state.typeAliases }
 
 /-- Extract only the overload dispatch table from PySpec signatures.
     Processes `@overload` function declarations, ignoring classDef,
diff --git a/StrataMain.lean b/StrataMain.lean
index 977d9d5c8..7439b8a94 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -435,6 +435,23 @@ def pyAnalyzeLaurelCommand : Command where
       IO.println "\n==== Core Program ===="
       IO.print coreProgram
 
+    -- Inline pyspec procedures so their precondition assertions are checked
+    -- at call sites with concrete arguments.
+    let pyspecFiles := pflags.getRepeated "pyspec"
+    let coreProgram ←
+      if pyspecFiles.size > 0 then
+        match Core.Transform.runProgram (targetProcList := .none)
+              (Core.ProcedureInlining.inlineCallCmd
+                (doInline := λ name _ => name ≠ "__main__"))
+              coreProgram .emp with
+        | ⟨.error e, _⟩ => exitInternalError s!"Inlining failed: {e}"
+        | ⟨.ok (_, inlined), _⟩ => do
+          if verbose then
+            IO.println "\n==== Core Program (after inlining) ===="
+            IO.print inlined
+          pure inlined
+      else pure coreProgram
+
     -- Verify using Core verifier
     let checkMode ← parseCheckMode pflags
     let checkLevel ← parseCheckLevel pflags
diff --git a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
index 16ffc9efc..9d593c75a 100644
--- a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
+++ b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
@@ -7,6 +7,7 @@ module
 
 meta import Strata.SimpleAPI
 meta import Strata.Languages.Python.PySpecPipeline
+meta import Strata.Transform.ProcedureInlining
 meta import StrataTest.Util.Python
 
 /-! ## End-to-end tests for `pyAnalyzeLaurel` with dispatch
@@ -65,16 +66,17 @@ private meta def compilePython
   return ionPath
 
 /-- Set up the test fixture: compile all pyspec files and the dispatch file.
-    Returns (dispatchIonPath, pyspecDir). -/
+    Returns (dispatchIonPath, pyspecPaths). -/
 private meta def setupFixture (_pythonCmd : System.FilePath)
-    (outDir : System.FilePath) : IO System.FilePath := do
+    (outDir : System.FilePath) : IO (System.FilePath × Array String) := do
   IO.FS.withTempFile fun _handle dialectFile => do
     IO.FS.writeBinFile dialectFile Python.Python.toIon
     -- Compile service specs
     let _ ← compilePySpec dialectFile (testDir / "Storage.py") outDir
     let _ ← compilePySpec dialectFile (testDir / "Messaging.py") outDir
     -- Compile dispatch file
-    compilePySpec dialectFile (testDir / "servicelib.py") outDir
+    let dispatchIon ← compilePySpec dialectFile (testDir / "servicelib.py") outDir
+    return (dispatchIon, #[])
 
 /-- Compile a test Python file to Ion format. -/
 private meta def compileTestScript (pyFile : System.FilePath)
@@ -86,11 +88,13 @@ private meta def compileTestScript (pyFile : System.FilePath)
 /-- Run pyAnalyzeLaurel on a test script within the shared fixture. -/
 private meta def runAnalyze (dispatchIon : System.FilePath)
     (tmpDir : System.FilePath) (scriptName : String)
+    (pyspecPaths : Array String := #[])
     : IO (Except String Core.Program) := do
   let testIon ← compileTestScript (testDir / scriptName) tmpDir
   let laurel ←
     match ← Strata.pyAnalyzeLaurel testIon.toString
-        (dispatchPaths := #[dispatchIon.toString]) |>.toBaseIO with
+        (dispatchPaths := #[dispatchIon.toString])
+        (pyspecPaths := pyspecPaths) |>.toBaseIO with
     | .ok r => pure r
     | .error err => return .error (toString err)
   match Strata.translateCombinedLaurel laurel with
@@ -101,6 +105,38 @@ private meta def runAnalyze (dispatchIon : System.FilePath)
     | .ok _ => return .ok core
   | (_, errors) => return .error s!"Laurel to Core translation failed: {errors}"
 
+/-- Run pyAnalyzeLaurel with inlining and verification, returning the formatted results. -/
+private meta def runAnalyzeAndVerify (dispatchIon : System.FilePath)
+    (tmpDir : System.FilePath) (scriptName : String)
+    (pyspecPaths : Array String := #[])
+    : IO (Except String (Array Core.VCResult)) := do
+  let testIon ← compileTestScript (testDir / scriptName) tmpDir
+  let laurel ←
+    match ← Strata.pyAnalyzeLaurel testIon.toString
+        (dispatchPaths := #[dispatchIon.toString])
+        (pyspecPaths := pyspecPaths) |>.toBaseIO with
+    | .ok r => pure r
+    | .error err => return .error (toString err)
+  let (coreProgramOption, _) := Strata.translateCombinedLaurel laurel
+  let coreProgram ← match coreProgramOption with
+    | none => return .error "Laurel to Core translation failed"
+    | some core => pure core
+  -- Inline all non-main procedures
+  let coreProgram ← match Core.Transform.runProgram (targetProcList := .none)
+        (Core.ProcedureInlining.inlineCallCmd
+          (doInline := λ name _ => name ≠ "__main__"))
+        coreProgram .emp with
+    | ⟨.error e, _⟩ => return .error s!"Inlining failed: {e}"
+    | ⟨.ok (_, inlined), _⟩ => pure inlined
+  -- Verify
+  let options : Core.VerifyOptions :=
+    { Core.VerifyOptions.default with
+      stopOnFirstError := false, verbose := .quiet, solver := "z3",
+      checkMode := .bugFinding, checkLevel := .full }
+  match ← Strata.verifyCore coreProgram options |>.toBaseIO with
+  | .ok results => return .ok results
+  | .error msg => return .error (toString msg)
+
 /-- Expected outcome for a test case. -/
 private inductive Expected where
   | success
@@ -138,8 +174,9 @@ private meta def testCases : List (String × Expected) := [
 
 /-- Run a single test case and return an error message on failure, or `none` on success. -/
 private meta def runTestCase (dispatchIon tmpDir : System.FilePath)
-    (scriptName : String) (expected : Expected) : IO (Option String) := do
-  let result ← runAnalyze dispatchIon tmpDir scriptName
+    (scriptName : String) (expected : Expected)
+    (pyspecPaths : Array String := #[]) : IO (Option String) := do
+  let result ← runAnalyze dispatchIon tmpDir scriptName pyspecPaths
   match expected, result with
   | .success, .ok _ => return none
   | .success, .error msg =>
@@ -152,7 +189,7 @@ private meta def runTestCase (dispatchIon tmpDir : System.FilePath)
 
 #eval withPython fun _pythonCmd => do
   IO.FS.withTempDir fun tmpDir => do
-    let dispatchIon ← setupFixture _pythonCmd tmpDir
+    let (dispatchIon, pyspecPaths) ← setupFixture _pythonCmd tmpDir
     -- Launch all tests concurrently, checking for duplicate filenames
     let mut seen : Std.HashSet String := {}
     let mut tasks : Array (String × Task (Except IO.Error (Option String))) := #[]
@@ -160,7 +197,7 @@ private meta def runTestCase (dispatchIon tmpDir : System.FilePath)
       if scriptName ∈ seen then
         throw <| IO.userError s!"Duplicate test filename: {scriptName}"
       seen := seen.insert scriptName
-      let task ← IO.asTask (runTestCase dispatchIon tmpDir scriptName expected)
+      let task ← IO.asTask (runTestCase dispatchIon tmpDir scriptName expected pyspecPaths)
       tasks := tasks.push (scriptName, task)
     -- Collect results
     let mut errors : Array String := #[]
@@ -172,4 +209,34 @@ private meta def runTestCase (dispatchIon tmpDir : System.FilePath)
     if errors.size > 0 then
       throw <| IO.userError ("\n".intercalate errors.toList)
 
+/-! ## Precondition violation test
+
+Verifies that calling `put_item(Bucket="", ...)` produces a `✖️ always false`
+result for the `len(Bucket) >= 1` assertion. -/
+
+/--
+info: Storage_Storage_put_item_assert(0)_8: ✔️ always true if reached (Required parameter 'Bucket' is missing)
+Storage_Storage_put_item_assert(0)_8: ✔️ always true if reached (Required parameter 'Key' is missing)
+Storage_Storage_put_item_assert(0)_8: ✔️ always true if reached (Required parameter 'Data' is missing)
+Storage_Storage_put_item_assert(0)_8: ✖️ always false if reached (Bucket must not be empty)
+Storage_Storage_put_item_assert(0)_8: ✔️ always true if reached (Key must not be empty)
+-/
+#guard_msgs in
+#eval withPython fun _pythonCmd => do
+  IO.FS.withTempDir fun tmpDir => do
+    let (dispatchIon, pyspecPaths) ← setupFixture _pythonCmd tmpDir
+    let result ← runAnalyzeAndVerify dispatchIon tmpDir
+      "test_precondition_violation.py" pyspecPaths
+    match result with
+    | .error msg => IO.println s!"error: {msg}"
+    | .ok vcResults =>
+      for r in vcResults do
+        if r.obligation.label.startsWith "Storage_" then
+          let msg := r.obligation.metadata.findSome? fun elem =>
+            match elem.fld, elem.value with
+            | .label "message", .msg s => some s
+            | _, _ => none
+          let msgStr := msg.map (s!" ({·})") |>.getD ""
+          IO.println s!"{r.obligation.label}: {r.formatOutcome}{msgStr}"
+
 end Strata.Python.AnalyzeLaurelTest
diff --git a/StrataTest/Languages/Python/Specs/dispatch_test/Storage.py b/StrataTest/Languages/Python/Specs/dispatch_test/Storage.py
index bc2826555..87957b39b 100644
--- a/StrataTest/Languages/Python/Specs/dispatch_test/Storage.py
+++ b/StrataTest/Languages/Python/Specs/dispatch_test/Storage.py
@@ -24,9 +24,11 @@
 
 class Storage:
     def put_item(self, **kwargs: Unpack[PutItemRequest]) -> None:
-        ...
+        assert len(kwargs["Bucket"]) >= 1, "Bucket must not be empty"
+        assert len(kwargs["Key"]) >= 1, "Key must not be empty"
     def get_item(self, **kwargs: Unpack[GetItemRequest]) -> GetItemResponse:
-        ...
+        assert len(kwargs["Bucket"]) >= 1, "Bucket must not be empty"
+        assert len(kwargs["Key"]) >= 1, "Key must not be empty"
     def delete_item(self, Bucket: str, Key: str) -> None:
         ...
     def list_items(self, **kwargs: Unpack[ListItemsRequest]) -> None:
diff --git a/StrataTest/Languages/Python/Specs/dispatch_test/test_precondition_violation.py b/StrataTest/Languages/Python/Specs/dispatch_test/test_precondition_violation.py
new file mode 100644
index 000000000..940c798bf
--- /dev/null
+++ b/StrataTest/Languages/Python/Specs/dispatch_test/test_precondition_violation.py
@@ -0,0 +1,6 @@
+import servicelib
+
+def store_empty_bucket() -> bool:
+    client = servicelib.connect("storage")
+    client.put_item(Bucket="", Key="mykey", Data="hello")
+    return True