diff --git a/Examples/StringTest.laurel.st b/Examples/StringTest.laurel.st
index a2674aba5a..2b6d087d32 100644
--- a/Examples/StringTest.laurel.st
+++ b/Examples/StringTest.laurel.st
@@ -1,6 +1,7 @@
 procedure testString()
 returns (result: string)
 requires true
+  opaque
 {
   var message: string := "Hello, World!";
   return message
@@ -9,6 +10,7 @@ requires true
 procedure testStringConcat()
 returns (result: string)
 requires true
+  opaque
 {
   var hello: string := "Hello";
   var world: string := "World";
diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
index 4658d5876b..8b88fef462 100644
--- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean
+++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
@@ -92,8 +92,8 @@ def resolveExprNode (ptMap : ConstrainedTypeMap) (expr : StmtExprMd) : StmtExprM
   let source := expr.source
   let md := expr.md
   match expr.val with
-  | .LocalVariable n ty init =>
-    ⟨.LocalVariable n (resolveType ptMap ty) init, source, md⟩
+  | .LocalVariable params init =>
+    ⟨.LocalVariable (params.map fun p => { p with type := resolveType ptMap p.type }) init, source, md⟩
   | .Forall param trigger body =>
     let param' := { param with type := resolveType ptMap param.type }
     -- With bottom-up traversal, `body` is already recursed into. The newly
@@ -127,15 +127,18 @@ def elimStmt (ptMap : ConstrainedTypeMap)
   let source := stmt.source
   let md := stmt.md
   match _h : stmt.val with
-  | .LocalVariable name ty init =>
-    let callOpt := constraintCallFor ptMap ty.val name md (src := source)
-    if callOpt.isSome then modify fun pv => pv.insert name.text ty.val
+  | .LocalVariable params init =>
+    for p in params do
+      let callOpt := constraintCallFor ptMap p.type.val p.name md (src := source)
+      if callOpt.isSome then modify fun pv => pv.insert p.name.text p.type.val
     let (init', check) : Option StmtExprMd × List StmtExprMd := match init with
-      | none => match callOpt with
-        | some c => (none, [⟨.Assume c, source, md⟩])
-        | none => (none, [])
-      | some _ => (init, callOpt.toList.map fun c => ⟨.Assert c, source, md⟩)
-    pure ([⟨.LocalVariable name ty init', source, md⟩] ++ check)
+      | none =>
+        let calls := params.filterMap fun p => constraintCallFor ptMap p.type.val p.name md (src := source)
+        (none, calls.map fun c => ⟨.Assume c, source, md⟩)
+      | some _ =>
+        let calls := params.filterMap fun p => constraintCallFor ptMap p.type.val p.name md (src := source)
+        (init, calls.map fun c => ⟨.Assert c, source, md⟩)
+    pure ([⟨.LocalVariable params init', source, md⟩] ++ check)
 
   | .Assign [target] _ => match target.val with
     | .Identifier name => do
@@ -209,13 +212,13 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
   let md := ct.witness.md
   let witnessId : Identifier := mkId "$witness"
   let witnessInit : StmtExprMd :=
-    ⟨.LocalVariable witnessId (resolveType ptMap ct.base) (some ct.witness), src, md⟩
+    ⟨.LocalVariable [{ name := witnessId, type := resolveType ptMap ct.base }] (some ct.witness), src, md⟩
   let assert : StmtExprMd :=
     ⟨.Assert (constraintCallFor ptMap (.UserDefined ct.name) witnessId md (src := src)).get!, src, md⟩
   { name := mkId s!"$witness_{ct.name.text}"
     inputs := []
     outputs := []
-    body := .Transparent ⟨.Block [witnessInit, assert] none, src, md⟩
+    body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src, md⟩) []
     preconditions := []
     isFunctional := false
     decreases := none }
diff --git a/Strata/Languages/Laurel/ContractPass.lean b/Strata/Languages/Laurel/ContractPass.lean
new file mode 100644
index 0000000000..14cefdfddc
--- /dev/null
+++ b/Strata/Languages/Laurel/ContractPass.lean
@@ -0,0 +1,328 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+
+/-!
+## Contract Pass (Laurel → Laurel)
+
+Removes pre- and postconditions from all procedures and replaces them with
+explicit precondition/postcondition helper procedures, assumptions, and
+assertions.
+
+For each procedure with contracts:
+- Generate a precondition procedure (`foo$pre`) returning the conjunction of preconditions.
+- Generate a postcondition procedure (`foo$post`) that takes only the *input*
+  parameters, internally calls the original procedure to obtain the outputs,
+  and returns the conjunction of postconditions.
+- Insert `assume foo$pre(inputs)` at the start of the body.
+- Insert `assert foo$post(inputs)` at the end of the body.
+
+For each call to a contracted procedure:
+- Insert `assert foo$pre(args)` before the call (precondition check).
+- Insert `assume foo$post(args)` after the call (postcondition assumption).
+
+The postcondition procedure calls the original procedure internally so that
+the `assume` at call sites only references pre-call arguments. This avoids
+a soundness issue where mutable variables (e.g. `$heap`) are overwritten by
+the call's result destructuring before the `assume` is evaluated.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+private def emptyMd : MetaData := .empty
+
+private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none }
+
+/-- Create a `StmtExprMd` with a property summary in its metadata. -/
+private def mkMdWithSummary (e : StmtExpr) (summary : String) : StmtExprMd :=
+  ⟨e, none, emptyMd.withPropertySummary summary⟩
+
+/-- Build a conjunction of expressions. Returns `LiteralBool true` for an empty list. -/
+private def conjoin (exprs : List StmtExprMd) : StmtExprMd :=
+  match exprs with
+  | [] => mkMd (.LiteralBool true)
+  | [e] => e
+  | e :: rest => rest.foldl (fun acc x =>
+      mkMd (.PrimitiveOp .And [acc, x])) e
+
+/-- Name for the precondition helper procedure. -/
+def preCondProcName (procName : String) : String := s!"{procName}$pre"
+
+/-- Name for the postcondition helper procedure. -/
+def postCondProcName (procName : String) : String := s!"{procName}$post"
+
+/-- Get postconditions from a procedure body. -/
+private def getPostconditions (body : Body) : List StmtExprMd :=
+  match body with
+  | .Opaque postconds _ _ => postconds
+  | .Abstract postconds => postconds
+  | _ => []
+
+/-- Build a call expression. -/
+private def mkCall (callee : String) (args : List StmtExprMd) : StmtExprMd :=
+  mkMd (.StaticCall (mkId callee) args)
+
+/-- Convert parameters to identifier expressions. -/
+private def paramsToArgs (params : List Parameter) : List StmtExprMd :=
+  params.map fun p => mkMd (.Identifier p.name)
+
+/-- Build a helper function that returns the conjunction of the given conditions. -/
+private def mkConditionProc (name : String) (params : List Parameter)
+    (conditions : List StmtExprMd) : Procedure :=
+  -- Use "$result" as the output name to avoid clashing with user-defined
+  -- parameter names (user names cannot contain '$').
+  { name := mkId name
+    inputs := params
+    outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩] -- TODO, enable anonymous output parameters
+    preconditions := []
+    decreases := none
+    isFunctional := true
+    body := .Transparent (conjoin conditions) }
+
+/-- Build a postcondition procedure that takes only the *input* parameters
+    and internally calls the original procedure to obtain the outputs.
+
+    For a procedure `foo(a, b) returns (x, y)` with postcondition `P(a, b, x, y)`,
+    generates:
+    ```
+    procedure foo$post(a, b) returns ($result : bool) {
+      var x, y : Tx := foo(a, b);
+      P(a, b, x, y)
+    }
+    ```
+
+    This ensures the `assume` at call sites only references pre-call arguments,
+    avoiding a soundness issue where mutable variables (e.g. `$heap`) are
+    overwritten by the call's result destructuring before the `assume` is
+    evaluated. -/
+private def mkPostConditionProc (name : String) (originalProcName : String)
+    (inputParams : List Parameter) (outputParams : List Parameter)
+    (conditions : List StmtExprMd) : Procedure :=
+  let inputArgs := paramsToArgs inputParams
+  let callExpr := mkMd (.StaticCall (mkId originalProcName) inputArgs)
+  let localVarStmt := mkMd (.LocalVariable outputParams (some callExpr))
+  -- Body: single initialized local variable, then postcondition conjunction
+  let bodyStmts := [localVarStmt, conjoin conditions]
+  let body := mkMd (.Block bodyStmts none)
+  { name := mkId name
+    inputs := inputParams
+    outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
+    preconditions := []
+    decreases := none
+    isFunctional := false
+    body := .Transparent body }
+
+/-- Extract a combined summary from a list of contract clauses. -/
+private def combinedSummary (clauses : List StmtExprMd) : Option String :=
+  let summaries := clauses.filterMap fun c => c.md.getPropertySummary
+  match summaries with
+  | [] => none
+  | [s] => some s
+  | ss => some (String.intercalate ", " ss)
+
+/-- Information about a procedure's contracts. -/
+private structure ContractInfo where
+  hasPreCondition : Bool
+  hasPostCondition : Bool
+  preName : String
+  postName : String
+  preSummary : Option String
+  postSummary : Option String
+  /-- The original procedure's input parameters (needed for postcondition generation). -/
+  inputParams : List Parameter
+  /-- The original procedure's output parameters (needed for postcondition generation). -/
+  outputParams : List Parameter
+
+/-- Collect contract info for all procedures with contracts. -/
+private def collectContractInfo (procs : List Procedure) : Std.HashMap String ContractInfo :=
+  procs.foldl (fun m proc =>
+    let postconds := getPostconditions proc.body
+    let hasPre := !proc.preconditions.isEmpty
+    let hasPost := !postconds.isEmpty
+    if hasPre || hasPost then
+      m.insert proc.name.text {
+        hasPreCondition := hasPre
+        hasPostCondition := hasPost
+        preName := preCondProcName proc.name.text
+        postName := postCondProcName proc.name.text
+        preSummary := combinedSummary proc.preconditions
+        postSummary := combinedSummary postconds
+        inputParams := proc.inputs
+        outputParams := proc.outputs
+      }
+    else m) {}
+
+/-- Transform a procedure body to add assume/assert for its own contracts. -/
+private def transformProcBody (proc : Procedure) (info : ContractInfo) : Body :=
+  let inputArgs := paramsToArgs proc.inputs
+  let postconds := getPostconditions proc.body
+  -- Use the source location from the first precondition for the assume node
+  let preAssume : List StmtExprMd :=
+    if info.hasPreCondition then
+      let (preSrc, preMd) := match proc.preconditions.head? with
+        | some pc => (pc.source, pc.md)
+        | none => (none, emptyMd)
+      [⟨.Assume (mkCall info.preName inputArgs), preSrc, preMd⟩]
+    else []
+  let postAssert : List StmtExprMd :=
+    if info.hasPostCondition then
+      -- Use the source location and metadata from the first postcondition so
+      -- the diagnostic carries the source location of the `ensures` clause.
+      let (baseSrc, baseMd) := match postconds.head? with
+        | some pc => (pc.source, pc.md)
+        | none => (none, emptyMd)
+      let summary := info.postSummary.getD "postcondition"
+      -- Directly assert the postcondition conjunction rather than calling $post.
+      -- The $post procedure re-invokes the original (opaque) procedure to obtain
+      -- outputs, which is correct at *call sites* but wrong inside the body:
+      -- here the output variables (e.g. $heap) are already in scope with their
+      -- actual values, so we assert the postcondition directly.
+      [⟨.Assert (conjoin postconds),
+        baseSrc, baseMd.withPropertySummary summary⟩]
+    else []
+  match proc.body with
+  | .Transparent body =>
+    .Transparent ⟨.Block (preAssume ++ [body] ++ postAssert) none, body.source, emptyMd ⟩
+  | .Opaque _ (some impl) _ =>
+    .Opaque [] (some ⟨.Block (preAssume ++ [impl] ++ postAssert) none, impl.source, emptyMd⟩)  []
+  | .Opaque _ none _ | .Abstract _ =>
+    .Opaque [] (some ⟨ .Block [] none, none, emptyMd⟩)  []
+  | b => b
+
+/-- Rewrite a single statement that may be a call to a contracted procedure.
+    Returns a list of statements (the original plus any inserted assert/assume).
+    Uses the call site's metadata for generated assert/assume nodes.
+    The postcondition assume passes only the call arguments (not the results),
+    since the $post procedure internally calls the original to obtain outputs. -/
+private def rewriteStmt (contractInfoMap : Std.HashMap String ContractInfo)
+    (e : StmtExprMd) : List StmtExprMd :=
+  let md := e.md
+  let src := e.source
+  let mkWithMd (se : StmtExpr) : StmtExprMd := ⟨se, src, md⟩
+  let mkWithMdSummary (se : StmtExpr) (summary : String) : StmtExprMd :=
+    ⟨se, src, md.withPropertySummary summary⟩
+  match e.val with
+  | .Assign _targets (.mk (.StaticCall callee args) ..) =>
+    match contractInfoMap.get? callee.text with
+    | some info =>
+      let preAssert := if info.hasPreCondition
+        then [mkWithMdSummary (.Assert (mkCall info.preName args)) (info.preSummary.getD "precondition")] else []
+      -- Assume $post *before* the assignment so that args still reference
+      -- pre-call values (e.g. $heap before it is overwritten by the call result).
+      -- The $post procedure internally calls the original to obtain outputs.
+      let postAssume := if info.hasPostCondition
+        then [mkWithMd (.Assume (mkCall info.postName args))] else []
+      preAssert ++ postAssume ++ [e]
+    | none => [e]
+  | .LocalVariable _params (some (.mk (.StaticCall callee args) ..)) =>
+    match contractInfoMap.get? callee.text with
+    | some info =>
+      let preAssert := if info.hasPreCondition
+        then [mkWithMdSummary (.Assert (mkCall info.preName args)) (info.preSummary.getD "precondition")] else []
+      -- Assume $post *before* the local variable binding so that args still
+      -- reference pre-call values.  The $post procedure internally calls the
+      -- original to obtain outputs.
+      let postAssume := if info.hasPostCondition
+        then [mkWithMd (.Assume (mkCall info.postName args))] else []
+      preAssert ++ postAssume ++ [e]
+    | none => [e]
+  | .StaticCall callee args =>
+    match contractInfoMap.get? callee.text with
+    | some info =>
+      let preAssert := if info.hasPreCondition
+        then [mkWithMdSummary (.Assert (mkCall info.preName args)) (info.preSummary.getD "precondition")] else []
+      preAssert ++ [e]
+    | none => [e]
+  | _ => [e]
+
+/-- Rewrite call sites in a statement/expression tree. Processes Block children
+    at the statement level to avoid interfering with expression-level calls.
+    For each statement-level call to a contracted procedure, inserts
+    `assert pre(args)` before and `assume post(args)` after. -/
+private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
+    (expr : StmtExprMd) : StmtExprMd :=
+  let result := mapStmtExpr (fun e =>
+    match e.val with
+    | .Block stmts label =>
+      let stmts' := stmts.flatMap (rewriteStmt contractInfoMap)
+      if stmts'.length == stmts.length then e
+      else ⟨.Block stmts' label, e.source, e.md⟩
+    | _ => e) expr
+  -- Handle top-level non-Block statements (e.g., bare Assign or StaticCall)
+  let expanded := rewriteStmt contractInfoMap result
+  match expanded with
+  | [single] => single
+  | many => mkMd (.Block many none)
+
+/-- Rewrite call sites in all bodies of a procedure. -/
+private def rewriteCallSitesInProc (contractInfoMap : Std.HashMap String ContractInfo)
+    (proc : Procedure) : Procedure :=
+  let rw := rewriteCallSites contractInfoMap
+  match proc.body with
+  | .Transparent body =>
+    { proc with body := .Transparent (rw body) }
+  | .Opaque posts impl mods =>
+    let body := Body.Opaque (posts.map rw) (impl.map rw) (mods.map rw)
+    { proc with body := body }
+  | _ => proc
+
+/-- Build an axiom expression from `invokeOn` trigger and ensures clauses.
+    Produces `∀ p1, ∀ p2, ..., ∀ pn :: { trigger } (ensures1 && ensures2 && ...)`. -/
+private def mkInvokeOnAxiom (params : List Parameter) (trigger : StmtExprMd)
+    (postconds : List StmtExprMd) : StmtExprMd :=
+  let body := conjoin postconds
+  -- Wrap in nested Forall from last param (innermost) to first (outermost).
+  -- The trigger is placed on the innermost quantifier.
+  params.foldr (init := (body, true)) (fun p (acc, isInnermost) =>
+    let trig := if isInnermost then some trigger else none
+    (mkMd (.Forall p trig acc), false)) |>.1
+
+/-- Run the contract pass on a Laurel program.
+    All procedures with contracts are transformed. -/
+def contractPass (program : Program) : Program :=
+  let contractInfoMap := collectContractInfo program.staticProcedures
+
+  -- Generate helper procedures for all procedures with contracts
+  let helperProcs := program.staticProcedures.flatMap fun proc =>
+    let postconds := getPostconditions proc.body
+    let preProc :=
+      if proc.preconditions.isEmpty then []
+      else [mkConditionProc (preCondProcName proc.name.text) proc.inputs proc.preconditions]
+    let postProc :=
+      if postconds.isEmpty then []
+      else [mkPostConditionProc (postCondProcName proc.name.text) proc.name.text
+              proc.inputs proc.outputs postconds]
+    preProc ++ postProc
+
+  -- Transform procedures: strip contracts, add assume/assert, rewrite call sites
+  let transformedProcs := program.staticProcedures.map fun proc =>
+    -- Build axioms from invokeOn + ensures BEFORE transforming the body
+    -- (transformProcBody strips postconditions from the body)
+    let proc := match proc.invokeOn with
+      | some trigger =>
+        let postconds := getPostconditions proc.body
+        if postconds.isEmpty then { proc with invokeOn := none }
+        else { proc with
+          axioms := [mkInvokeOnAxiom proc.inputs trigger postconds]
+          invokeOn := none }
+      | none => proc
+    let proc := match contractInfoMap.get? proc.name.text with
+      | some info =>
+        { proc with
+          preconditions := []
+          body := transformProcBody proc info }
+      | none => proc
+    -- Rewrite call sites in the procedure body
+    rewriteCallSitesInProc contractInfoMap proc
+
+  { program with staticProcedures := helperProcs ++ transformedProcs }
+
+end -- public section
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
index 1d8596235a..815dd8794e 100644
--- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
+++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
@@ -5,9 +5,10 @@
 -/
 
 module
-public import Strata.Languages.Laurel.Laurel
+public import Strata.Languages.Laurel.FunctionsAndProofs
 import Strata.DL.Lambda.LExpr
 import Strata.DDM.Util.Graph.Tarjan
+import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 
 /-!
 ## Grouping and Ordering for Core Translation
@@ -15,8 +16,6 @@ import Strata.DDM.Util.Graph.Tarjan
 Utilities for computing the grouping and topological ordering of Laurel
 declarations before they are emitted as Strata Core declarations.
 
-- `groupDatatypesByScc` — groups mutually recursive datatypes into SCC groups
-  using Tarjan's SCC algorithm.
 - `computeSccDecls` — builds the procedure call graph, runs Tarjan's SCC
   algorithm, and returns each SCC as a list of procedures paired with a flag
   indicating whether the SCC is recursive. The result is in reverse topological
@@ -65,7 +64,7 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
   | .Assign targets v =>
       targets.flatMap (fun t => collectStaticCallNames t) ++
       collectStaticCallNames v
-  | .LocalVariable _ _ initOption =>
+  | .LocalVariable _ initOption =>
       match initOption with
       | some init => collectStaticCallNames init
       | none => []
@@ -108,27 +107,24 @@ Build the procedure call graph, run Tarjan's SCC algorithm, and return each SCC
 as a list of procedures paired with a flag indicating whether the SCC is recursive.
 Results are in reverse topological order: dependencies before dependents.
 
-Procedures with an `invokeOn` trigger are placed as early as possible — before
-unrelated procedures without one — by stably partitioning them first before building
+Procedures with axioms are placed as early as possible — before
+unrelated procedures without them — by stably partitioning them first before building
 the graph. Tarjan then naturally assigns them lower indices, causing them to appear
 earlier in the output.
-
-External procedures are excluded.
 -/
-public def computeSccDecls (program : Program) : List (List Procedure × Bool) :=
-  -- External procedures are completely ignored (not translated to Core).
-  -- Stable partition: procedures with invokeOn come first, preserving relative
+public def computeSccDecls (program : FunctionsAndProofsProgram) : List (List Procedure × Bool) :=
+  -- Stable partition: procedures with axioms come first, preserving relative
   -- order within each group. Tarjan then places them earlier in the topological output.
-  let (withInvokeOn, withoutInvokeOn) :=
-    (program.staticProcedures.filter (fun p => !p.body.isExternal))
-    |>.partition (fun p => p.invokeOn.isSome)
-  let nonExternal : List Procedure := withInvokeOn ++ withoutInvokeOn
+  let allProcs := program.functions ++ program.proofs
+  let (withAxioms, withoutAxioms) :=
+    allProcs.partition (fun p => !p.axioms.isEmpty)
+  let orderedProcs : List Procedure := withAxioms ++ withoutAxioms
 
-  -- Build a call-graph over all non-external procedures.
+  -- Build a call-graph over all procedures.
   -- An edge proc → callee means proc's body/contracts contain a StaticCall to callee.
-  let nonExternalArr : Array Procedure := nonExternal.toArray
+  let procsArr : Array Procedure := orderedProcs.toArray
   let nameToIdx : Std.HashMap String Nat :=
-    nonExternalArr.foldl (fun (acc : Std.HashMap String Nat × Nat) proc =>
+    procsArr.foldl (fun (acc : Std.HashMap String Nat × Nat) proc =>
       (acc.1.insert proc.name.text acc.2, acc.2 + 1)) ({}, 0) |>.1
 
   -- Collect all callee names from a procedure's body and contracts.
@@ -140,13 +136,13 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) :
       | _ => []
     let contractExprs : List StmtExprMd :=
       proc.preconditions ++
-      proc.invokeOn.toList
+      proc.axioms
     (bodyExprs ++ contractExprs).flatMap collectStaticCallNames
 
   -- Build the OutGraph for Tarjan.
-  let n := nonExternalArr.size
+  let n := procsArr.size
   let graph : Strata.OutGraph n :=
-    nonExternalArr.foldl (fun (acc : Strata.OutGraph n × Nat) proc =>
+    procsArr.foldl (fun (acc : Strata.OutGraph n × Nat) proc =>
       let callerIdx := acc.2
       let g := acc.1
       let callees := procCallees proc
@@ -162,7 +158,7 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) :
 
   sccs.toList.filterMap fun scc =>
     let procs := scc.toList.filterMap fun idx =>
-      nonExternalArr[idx.val]?
+      procsArr[idx.val]?
     if procs.isEmpty then none else
     let isRecursive := procs.length > 1 ||
       (match scc.toList.head? with
@@ -171,60 +167,85 @@ public def computeSccDecls (program : Program) : List (List Procedure × Bool) :
     some (procs, isRecursive)
 
 /--
-A single declaration in an ordered Laurel program. Declarations are in
+A single declaration in a CoreWithLaurelTypes program. Declarations are in
 dependency order (dependencies before dependents).
 -/
 public inductive OrderedDecl where
-  /-- A group of functions (single non-recursive, or mutually recursive). -/
-  | procs (procs : List Procedure) (isRecursive : Bool)
+  /-- A group of functions (single non-recursive, or mutually recursive).
+      Invariant: `funcs.length > 1 → isRecursive = true`. -/
+  | funcs (funcs : List Procedure) (isRecursive : Bool)
+  /-- A single (non-functional) procedure. -/
+  | procedure (procedure : Procedure)
   /-- A group of (possibly mutually recursive) datatypes. -/
   | datatypes (dts : List DatatypeDefinition)
   /-- A named constant. -/
   | constant (c : Constant)
 
 /--
-A Laurel program whose declarations have been grouped and topologically ordered.
-Produced by `orderProgram` from a `Program`.
+A program whose declarations have been grouped and topologically ordered,
+using Laurel types. Produced by `orderFunctionsAndProofs` from a
+`FunctionsAndProofsProgram`.
 -/
-public structure OrderedLaurel where
+public structure CoreWithLaurelTypes where
   decls : List OrderedDecl
 
-/--
-Group mutually recursive datatypes into SCC groups using Tarjan's SCC algorithm.
-Returns groups in topological order (dependencies before dependents).
--/
-public def groupDatatypesByScc (program : Program) : List (List DatatypeDefinition) :=
-  let laurelDatatypes := program.types.filterMap fun td => match td with
-    | .Datatype dt => some dt
-    | _ => none
-  let n := laurelDatatypes.length
-  if n == 0 then [] else
-  let nameToIdx : Std.HashMap String Nat :=
-    laurelDatatypes.foldlIdx (fun m i dt => m.insert dt.name.text i) {}
-  let edges : List (Nat × Nat) :=
-    laurelDatatypes.foldlIdx (fun acc i dt =>
-      (datatypeRefs dt).filterMap nameToIdx.get? |>.foldl (fun acc j => (j, i) :: acc) acc) []
-  let g := OutGraph.ofEdges! n edges
-  let dtsArr := laurelDatatypes.toArray
-  OutGraph.tarjan g |>.toList.filterMap fun comp =>
-    let members := comp.toList.filterMap fun idx => dtsArr[idx]?
-    if members.isEmpty then none else some members
+open Std (Format ToFormat)
 
-/--
-Group procedures into SCC groups and wrap them as `OrderedDecl.procs`.
--/
-public def groupProcsByScc (program : Program) : List OrderedDecl :=
-  (computeSccDecls program).map fun (procs, isRecursive) =>
-    OrderedDecl.procs procs isRecursive
+public section
+
+def formatOrderedDecl : OrderedDecl → Format
+  | .funcs funcs _ => Format.joinSep (funcs.map ToFormat.format) "\n\n"
+  | .procedure proc => ToFormat.format proc
+  | .datatypes dts => Format.joinSep (dts.map ToFormat.format) "\n\n"
+  | .constant c => ToFormat.format c
+
+instance : ToFormat OrderedDecl where
+  format := formatOrderedDecl
+
+def formatCoreWithLaurelTypes (p : CoreWithLaurelTypes) : Format :=
+  Format.joinSep (p.decls.map formatOrderedDecl) "\n\n"
+
+instance : ToFormat CoreWithLaurelTypes where
+  format := formatCoreWithLaurelTypes
+
+end -- public section
 
 /--
-Produce an `OrderedLaurel` from a `Program` by grouping and ordering
-procedures via SCC, collecting datatypes, and constants.
+Produce a `CoreWithLaurelTypes` from a `FunctionsAndProofsProgram` by
+computing a combined ordering of functions and proofs using the call graph,
+then collecting datatypes and constants.
+
+Functions are grouped into SCCs (for mutual recursion). Proofs are emitted
+as individual `procedure` decls. Both participate in the topological ordering
+so that axioms are available to functions that need them.
 -/
-public def orderProgram (program : Program) : OrderedLaurel :=
-  let datatypeDecls := (groupDatatypesByScc program).map OrderedDecl.datatypes
+public def orderFunctionsAndProofs (program : FunctionsAndProofsProgram) : CoreWithLaurelTypes :=
+  let datatypeDecls := (groupDatatypesByScc' program).map OrderedDecl.datatypes
   let constantDecls := program.constants.map OrderedDecl.constant
-  let procDecls := groupProcsByScc program
-  { decls := datatypeDecls ++ constantDecls ++ procDecls }
+  let funcNames : Std.HashSet String :=
+    program.functions.foldl (fun s p => s.insert p.name.text) {}
+  let orderedDecls := (computeSccDecls program).flatMap fun (procs, isRecursive) =>
+    -- Split the SCC into functions and proofs
+    let (funcs, proofs) := procs.partition (fun p => funcNames.contains p.name.text)
+    let funcDecl := if funcs.isEmpty then [] else [OrderedDecl.funcs funcs isRecursive]
+    let proofDecls := proofs.map OrderedDecl.procedure
+    funcDecl ++ proofDecls
+  { decls := datatypeDecls ++ constantDecls ++ orderedDecls }
+where
+  /-- Group datatypes from a FunctionsAndProofsProgram by SCC. -/
+  groupDatatypesByScc' (program : FunctionsAndProofsProgram) : List (List DatatypeDefinition) :=
+    let laurelDatatypes := program.datatypes
+    let n := laurelDatatypes.length
+    if n == 0 then [] else
+    let nameToIdx : Std.HashMap String Nat :=
+      laurelDatatypes.foldlIdx (fun m i dt => m.insert dt.name.text i) {}
+    let edges : List (Nat × Nat) :=
+      laurelDatatypes.foldlIdx (fun acc i dt =>
+        (datatypeRefs dt).filterMap nameToIdx.get? |>.foldl (fun acc j => (j, i) :: acc) acc) []
+    let g := OutGraph.ofEdges! n edges
+    let dtsArr := laurelDatatypes.toArray
+    OutGraph.tarjan g |>.toList.filterMap fun comp =>
+      let members := comp.toList.filterMap fun idx => dtsArr[idx]?
+      if members.isEmpty then none else some members
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateMultipleOutputs.lean b/Strata/Languages/Laurel/EliminateMultipleOutputs.lean
new file mode 100644
index 0000000000..f5ff111fea
--- /dev/null
+++ b/Strata/Languages/Laurel/EliminateMultipleOutputs.lean
@@ -0,0 +1,182 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.FunctionsAndProofs
+
+/-!
+# Eliminate Multiple Outputs
+
+Transforms bodiless functions with multiple outputs into functions that return
+a single synthesized result datatype. Call sites are rewritten to destructure
+the result using the generated accessors.
+
+This pass operates on `FunctionsAndProofsProgram → FunctionsAndProofsProgram`.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+private def emptyMd : MetaData := .empty
+private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none }
+private def mkTy (t : HighType) : HighTypeMd := { val := t, source := none }
+
+/-- Info about a function whose multiple outputs have been collapsed into a result datatype. -/
+private structure MultiOutInfo where
+  funcName : String
+  resultTypeName : String
+  constructorName : String
+  /-- Original output parameters (name, type). -/
+  outputs : List Parameter
+
+/-- Identify bodiless functions with multiple outputs and build info records. -/
+private def collectMultiOutFunctions (funcs : List Procedure) : List MultiOutInfo :=
+  funcs.filterMap fun f =>
+    if f.outputs.length > 1 && !f.body.isTransparent then
+      some {
+        funcName := f.name.text
+        resultTypeName := s!"{f.name.text}$result"
+        constructorName := s!"{f.name.text}$result$mk"
+        outputs := f.outputs
+      }
+    else none
+
+/-- Generate a result datatype for a multi-output function. -/
+private def mkResultDatatype (info : MultiOutInfo) : DatatypeDefinition :=
+  let args := info.outputs.zipIdx.map fun (p, i) =>
+    { name := mkId s!"out{i}", type := p.type : Parameter }
+  { name := mkId info.resultTypeName
+    typeArgs := []
+    constructors := [{ name := mkId info.constructorName, args := args }] }
+
+/-- Transform a multi-output function to return the result datatype. -/
+private def transformFunction (info : MultiOutInfo) (proc : Procedure) : Procedure :=
+  let resultOutput : Parameter :=
+    { name := mkId "$result", type := mkTy (.UserDefined (mkId info.resultTypeName)) }
+  { proc with outputs := [resultOutput] }
+
+/-- Destructor name for field `outN` of the result datatype. -/
+private def destructorName (info : MultiOutInfo) (idx : Nat) : String :=
+  s!"{info.resultTypeName}..out{idx}"
+
+/-- Check whether a statement is an Assume node. -/
+private def isAssume (stmt : StmtExprMd) : Bool :=
+  match stmt.val with
+  | .Assume _ => true
+  | _ => false
+
+/-- Rewrite a single multi-output Assign into a temp declaration + destructuring
+    assignments. Any `Assume` statements from `following` that appear immediately
+    after the call are collected and placed between the temp declaration and the
+    destructuring assignments, so they observe the pre-call variable values.
+    Returns the rewritten statements and the number of consumed following statements. -/
+private def rewriteAssign (infoMap : Std.HashMap String MultiOutInfo)
+    (targets : List StmtExprMd) (callee : Identifier) (args : List StmtExprMd)
+    (callSrc : Option FileRange) (callMd : MetaData)
+    (following : List StmtExprMd) : Option (List StmtExprMd × Nat) :=
+  match infoMap.get? callee.text with
+  | some info =>
+    if targets.length == info.outputs.length then
+      let tempName := s!"${callee.text}$temp"
+      let tempParam : Parameter := { name := mkId tempName, type := mkTy (.UserDefined (mkId info.resultTypeName)) }
+      let tempDecl := mkMd (.LocalVariable [tempParam]
+        (some ⟨.StaticCall callee args, callSrc, callMd⟩))
+      let assigns := targets.zipIdx.map fun (tgt, i) =>
+        mkMd (.Assign [tgt]
+          (mkMd (.StaticCall (mkId (destructorName info i))
+            [mkMd (.Identifier (mkId tempName))])))
+      -- Collect any Assume statements that immediately follow the call.
+      -- These must be placed before the destructuring assignments so they
+      -- observe the pre-call values of variables like $heap.
+      let assumes := following.takeWhile isAssume
+      let consumed := assumes.length
+      some (tempDecl :: assumes ++ assigns, consumed)
+    else none
+  | none => none
+
+/-- Rewrite a statement list, replacing multi-output call patterns.
+    When a multi-output Assign is followed by Assume statements (inserted by
+    the contract pass), the Assumes are hoisted before the destructuring
+    assignments so they reference pre-call variable values. -/
+private def rewriteStmts (infoMap : Std.HashMap String MultiOutInfo)
+    (stmts : List StmtExprMd) : List StmtExprMd :=
+  let rec go (remaining : List StmtExprMd) (acc : List StmtExprMd) : List StmtExprMd :=
+    match remaining with
+    | [] => acc.reverse
+    | stmt :: rest =>
+      match stmt.val with
+      | .Assign targets ⟨.StaticCall callee args, callSrc, callMd⟩ =>
+        match rewriteAssign infoMap targets callee args callSrc callMd rest with
+        | some (expanded, consumed) => go (rest.drop consumed) (expanded.reverse ++ acc)
+        | none => go rest (stmt :: acc)
+      | .LocalVariable params (some ⟨.StaticCall callee args, callSrc, callMd⟩) =>
+        match infoMap.get? callee.text with
+        | some info =>
+          if info.outputs.length > 1 then
+            let tempName := s!"${callee.text}$temp"
+            let tempParam : Parameter := { name := mkId tempName, type := mkTy (.UserDefined (mkId info.resultTypeName)) }
+            let tempDecl := mkMd (.LocalVariable [tempParam]
+              (some ⟨.StaticCall callee args, callSrc, callMd⟩))
+            -- Collect any Assume statements that immediately follow the call.
+            let assumes := rest.takeWhile isAssume
+            let consumed := assumes.length
+            -- Declare each original output parameter as a local variable initialized
+            -- from the corresponding destructor of the result datatype.
+            let localDecls := params.zipIdx.map fun (p, i) =>
+              mkMd (.LocalVariable [p]
+                (some (mkMd (.StaticCall (mkId (destructorName info i))
+                  [mkMd (.Identifier (mkId tempName))]))))
+            go (rest.drop consumed) ((assumes ++ localDecls).reverse ++ (tempDecl :: acc))
+          else go rest (stmt :: acc)
+        | none => go rest (stmt :: acc)
+      | _ => go rest (stmt :: acc)
+  termination_by remaining.length
+  go stmts []
+
+/-- Rewrite blocks in a StmtExprMd tree to handle multi-output calls. -/
+private def rewriteExpr (infoMap : Std.HashMap String MultiOutInfo)
+    (expr : StmtExprMd) : StmtExprMd :=
+  mapStmtExpr (fun e =>
+    match e.val with
+    | .Block stmts label => ⟨.Block (rewriteStmts infoMap stmts) label, e.source, e.md⟩
+    | _ => e) expr
+
+/-- Rewrite all procedure bodies. -/
+private def rewriteProcedure (infoMap : Std.HashMap String MultiOutInfo)
+    (proc : Procedure) : Procedure :=
+  match proc.body with
+  | .Transparent b =>
+    -- Wrap in a block so rewriteStmts can process top-level statements
+    let wrapped := mkMd (.Block [b] none)
+    let rewritten := rewriteExpr infoMap wrapped
+    { proc with body := .Transparent rewritten }
+  | .Opaque posts (some impl) mods =>
+    let wrapped := mkMd (.Block [impl] none)
+    let rewritten := rewriteExpr infoMap wrapped
+    { proc with body := .Opaque posts (some rewritten) mods }
+  | _ => proc
+
+/-- Eliminate multiple outputs from a FunctionsAndProofsProgram. -/
+def eliminateMultipleOutputs (program : FunctionsAndProofsProgram)
+    : FunctionsAndProofsProgram :=
+  let infos := collectMultiOutFunctions program.functions
+  if infos.isEmpty then program else
+  let infoMap : Std.HashMap String MultiOutInfo :=
+    infos.foldl (fun m info => m.insert info.funcName info) {}
+  let newDatatypes := infos.map mkResultDatatype
+  let functions := program.functions.map fun f =>
+    match infoMap.get? f.name.text with
+    | some info => rewriteProcedure infoMap (transformFunction info f)
+    | none => rewriteProcedure infoMap f
+  let proofs := program.proofs.map (rewriteProcedure infoMap)
+  { program with
+    functions := functions
+    proofs := proofs
+    datatypes := program.datatypes ++ newDatatypes }
+
+end -- public section
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateReturnStatements.lean b/Strata/Languages/Laurel/EliminateReturnStatements.lean
new file mode 100644
index 0000000000..c457970a81
--- /dev/null
+++ b/Strata/Languages/Laurel/EliminateReturnStatements.lean
@@ -0,0 +1,66 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+
+/-!
+# Eliminate Return Statements
+
+Replaces `return` statements in imperative procedure bodies with assignments
+to the output parameters followed by an `exit` to a labelled block that wraps
+the entire body. This ensures that code placed after the body block (e.g.,
+postcondition assertions inserted by the contract pass) is always reached.
+
+This pass should run after `EliminateReturnsInExpression` (which handles
+functional/expression-position returns) and before the contract pass.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+private def returnLabel : String := "$return"
+
+private def emptyMd : MetaData := .empty
+
+private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none }
+
+/-- Replace `Return val` with `output := val; exit "$return"` (or just `exit`
+    for valueless returns). Uses `mapStmtExpr` for bottom-up traversal. -/
+private def replaceReturn (outputs : List Parameter) (expr : StmtExprMd) : StmtExprMd :=
+  mapStmtExpr (fun e =>
+    match e.val with
+    | .Return (some val) =>
+      match outputs with
+      | [out] =>
+        let assign := mkMd (.Assign [mkMd (.Identifier out.name)] val)
+        let exit := mkMd (.Exit returnLabel)
+        ⟨.Block [assign, exit] none, e.source, e.md⟩
+      | _ => mkMd (.Exit returnLabel)
+    | .Return none => mkMd (.Exit returnLabel)
+    | _ => e) expr
+
+/-- Transform a single procedure: wrap body in a labelled block and replace returns. -/
+private def eliminateReturnStmts (proc : Procedure) : Procedure :=
+  match proc.body with
+  | .Opaque postconds (some impl) mods =>
+    let impl' := replaceReturn proc.outputs impl
+    let wrapped := mkMd (.Block [impl'] (some returnLabel))
+    { proc with body := .Opaque postconds (some wrapped) mods }
+  | .Transparent body =>
+    let body' := replaceReturn proc.outputs body
+    let wrapped := mkMd (.Block [body'] (some returnLabel))
+    { proc with body := .Transparent wrapped }
+  | _ => proc
+
+/-- Transform a program by eliminating return statements in all procedure bodies. -/
+def eliminateReturnStatements (program : Program) : Program :=
+  { program with staticProcedures := program.staticProcedures.map eliminateReturnStmts }
+
+end -- public section
+
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean
index ce7c6a3656..2bf7f8c459 100644
--- a/Strata/Languages/Laurel/FilterPrelude.lean
+++ b/Strata/Languages/Laurel/FilterPrelude.lean
@@ -92,8 +92,8 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
     collectExprNames cond; collectExprNames thenB
     elseB.forM collectExprNames
   | .Block stmts _ => stmts.forM collectExprNames
-  | .LocalVariable _ ty init =>
-    collectHighTypeNames ty
+  | .LocalVariable params init =>
+    params.forM fun p => collectHighTypeNames p.type
     init.forM collectExprNames
   | .While cond invs dec body =>
     collectExprNames cond; invs.forM collectExprNames
diff --git a/Strata/Languages/Laurel/FunctionsAndProofs.lean b/Strata/Languages/Laurel/FunctionsAndProofs.lean
new file mode 100644
index 0000000000..2daec60b6e
--- /dev/null
+++ b/Strata/Languages/Laurel/FunctionsAndProofs.lean
@@ -0,0 +1,82 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+public import Strata.Languages.Laurel.Laurel
+
+/-!
+## FunctionsAndProofs IR
+
+An intermediate representation that separates Laurel procedures into
+functions (pure, used for computation) and proofs (used for verification).
+
+This IR sits between Laurel and CoreWithLaurelTypes in the pipeline:
+  Laurel → FunctionsAndProofs → CoreWithLaurelTypes → Core
+-/
+
+namespace Strata.Laurel
+
+public section
+
+/--
+A program in the FunctionsAndProofs IR. Functions are pure computational
+procedures; proofs are verification-only procedures.
+Both reuse `Laurel.Procedure` as their representation.
+-/
+public structure FunctionsAndProofsProgram where
+  functions : List Procedure
+  proofs : List Procedure
+  datatypes : List DatatypeDefinition
+  constants : List Constant
+
+/-- Deep traversal that strips all Assert and Assume nodes from a StmtExpr tree.
+    Assert/Assume nodes are replaced with `LiteralBool true`, and Block nodes
+    are collapsed by filtering out trivial `LiteralBool true` leftovers. -/
+def stripAssertAssume (expr : StmtExprMd) : StmtExprMd :=
+  mapStmtExpr (fun e =>
+    match e.val with
+    | .Assert _ | .Assume _ => ⟨.LiteralBool true, e.source, e.md⟩
+    | .Block stmts label =>
+      let stmts' := stmts.filter fun s =>
+        match s.val with | .LiteralBool true => false | _ => true
+      match stmts' with
+      | [] => ⟨.LiteralBool true, e.source, e.md⟩
+      | [s] => if label.isNone then s else ⟨.Block [s] label, e.source, e.md⟩
+      | _ => ⟨.Block stmts' label, e.source, e.md⟩
+    | _ => e) expr
+
+/-- Create the function copy of a procedure. The function body is included only
+    when the procedure was originally functional and has a transparent body;
+    non-functional procedures get opaque function copies since their bodies
+    contain imperative constructs that cannot be translated as pure functions.
+    Assert/Assume nodes are stripped from function bodies. -/
+private def mkFunctionCopy (proc : Procedure) : Procedure :=
+  let body := match proc.body with
+      | .Transparent b => .Transparent (stripAssertAssume b)
+      | .Opaque _ _ _ => .Opaque [] none []
+      | x => x
+  { proc with isFunctional := true, body := body }
+
+/--
+Proof pass: translate a Laurel program to the FunctionsAndProofs IR.
+
+Partitions procedures by `isFunctional`: functional procedures become
+functions, non-functional become proofs.
+-/
+def laurelToFunctionsAndProofs (program : Program) : FunctionsAndProofsProgram :=
+  let nonExternal := program.staticProcedures.filter (fun p => !p.body.isExternal)
+  let functions := program.staticProcedures.map mkFunctionCopy
+  let proofs := nonExternal.map fun p =>
+    { p with isFunctional := false,
+             name := { p.name with text := p.name.text ++ "$proof", uniqueId := none } }
+  let datatypes := program.types.filterMap fun td => match td with
+    | .Datatype dt => some dt
+    | _ => none
+  { functions, proofs, datatypes, constants := program.constants }
+
+end -- public section
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
index 44012f3960..7158bd67bd 100644
--- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
@@ -9,6 +9,7 @@ public import Strata.DDM.AST
 public import Strata.DDM.Format
 public import Strata.Languages.Laurel.Grammar.LaurelGrammar
 public import Strata.Languages.Laurel.Laurel
+public import Strata.Languages.Laurel.FunctionsAndProofs
 
 namespace Strata
 namespace Laurel
@@ -95,10 +96,14 @@ where
       match label with
       | none => laurelOp "block" #[semicolonSep stmtArgs]
       | some l => laurelOp "labelledBlock" #[semicolonSep stmtArgs, ident l]
-    | .LocalVariable name ty init =>
+    | .LocalVariable params init =>
+      -- Grammar only supports single-target varDecl; use first parameter or placeholder
+      let (nameText, ty) := match params with
+        | p :: _ => (p.name.text, p.type)
+        | [] => ("_", ⟨.TVoid, none, #[]⟩)
       let typeOpt := optionArg (some (laurelOp "typeAnnotation" #[highTypeToArg ty]))
       let initOpt := optionArg (init.map fun e => laurelOp "initializer" #[stmtExprToArg e])
-      laurelOp "varDecl" #[ident name.text, typeOpt, initOpt]
+      laurelOp "varDecl" #[ident nameText, typeOpt, initOpt]
     | .Assign targets value =>
       -- Grammar only supports single-target assign; use first target or placeholder
       let targetArg := match targets with
@@ -187,8 +192,11 @@ private def ensuresClauseToArg (e : StmtExprMd) : Arg :=
   laurelOp "ensuresClause" #[stmtExprToArg e, errOpt]
 
 private def modifiesClauseToArg (modifies : List StmtExprMd) : Arg :=
-  let refs := modifies.map stmtExprToArg |>.toArray
-  laurelOp "modifiesClause" #[commaSep refs]
+  if modifies.any (fun e => match e.val with | .All => true | _ => false) then
+    laurelOp "modifiesWildcard" #[]
+  else
+    let refs := modifies.map stmtExprToArg |>.toArray
+    laurelOp "modifiesClause" #[commaSep refs]
 
 private def procedureToOp (proc : Procedure) : Strata.Operation :=
   let opName := if proc.isFunctional then "function" else "procedure"
@@ -212,19 +220,21 @@ private def procedureToOp (proc : Procedure) : Strata.Operation :=
   let requiresArgs := proc.preconditions.map requiresClauseToArg |>.toArray
   let invokeOnArg := optionArg (proc.invokeOn.map fun e =>
     laurelOp "invokeOnClause" #[stmtExprToArg e])
-  let (ensuresArgs, modifiesArgs, bodyArg) := match proc.body with
+  let (opaqueSpecArg, bodyArg) := match proc.body with
     | .Transparent body =>
-      (#[], #[], optionArg (some (laurelOp "body" #[stmtExprToArg body])))
+      (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg body])))
     | .Opaque postconds impl modifies =>
       let ens := postconds.map ensuresClauseToArg |>.toArray
       let mods := if modifies.isEmpty then #[] else #[modifiesClauseToArg modifies]
+      let opaqueOp := laurelOp "opaqueSpec" #[seqArg ens, seqArg mods]
       let body := optionArg (impl.map fun e => laurelOp "body" #[stmtExprToArg e])
-      (ens, mods, body)
+      (optionArg (some opaqueOp), body)
     | .Abstract postconds =>
       let ens := postconds.map ensuresClauseToArg |>.toArray
-      (ens, #[], optionArg none)
+      let opaqueOp := laurelOp "opaqueSpec" #[seqArg ens, seqArg #[]]
+      (optionArg (some opaqueOp), optionArg none)
     | .External =>
-      (#[], #[], optionArg (some (laurelOp "externalBody")))
+      (optionArg none, optionArg (some (laurelOp "externalBody")))
   { ann := sr
     name := { dialect := "Laurel", name := opName }
     args := #[
@@ -234,8 +244,7 @@ private def procedureToOp (proc : Procedure) : Strata.Operation :=
       returnParamsArg,
       seqArg requiresArgs,
       invokeOnArg,
-      seqArg ensuresArgs,
-      seqArg modifiesArgs,
+      opaqueSpecArg,
       bodyArg
     ] }
 
@@ -372,6 +381,17 @@ instance : Std.ToFormat Constant where format := formatConstant
 instance : Std.ToFormat TypeDefinition where format := formatTypeDefinition
 instance : Std.ToFormat Program where format := formatProgram
 
+def formatFunctionsAndProofsProgram (p : FunctionsAndProofsProgram) : Format :=
+  let sections : List Format :=
+    (p.datatypes.map formatDatatypeDefinition) ++
+    (p.constants.map formatConstant) ++
+    (p.functions.map formatProcedure) ++
+    (p.proofs.map formatProcedure)
+  Std.Format.joinSep sections "\n\n"
+
+instance : Std.ToFormat FunctionsAndProofsProgram where
+  format := formatFunctionsAndProofsProgram
+
 instance : Repr StmtExpr where
   reprPrec r _ := s!"{Std.format r}"
 
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index 77f223a66c..3c01d01743 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -240,7 +240,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
           | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
         | .option _ none => pure none
         | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
-      return mkStmtExprMd (.LocalVariable name varType value) src
+      return mkStmtExprMd (.LocalVariable [{ name := name, type := varType }] value) src
     | q`Laurel.identifier, #[arg0] =>
       let name ← translateIdent arg0
       return mkStmtExprMd (.Identifier name) src
@@ -378,6 +378,8 @@ def translateModifiesClauses (arg : Arg) : TransM (List StmtExprMd) := do
         | q`Laurel.modifiesClause, #[refsArg] =>
           let refs ← translateModifiesExprs refsArg
           allModifies := allModifies ++ refs
+        | q`Laurel.modifiesWildcard, #[] =>
+          allModifies := allModifies ++ [{ val := .All, source := none }]
         | _, _ => TransM.error s!"Expected modifiesClause operation, got {repr clauseOp.name}"
       | _ => TransM.error s!"Expected modifiesClause operation in modifies sequence"
     pure allModifies
@@ -433,9 +435,9 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
 
   match op.name, op.args with
   | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, invokeOnArg, ensuresArg, modifiesArg, bodyArg]
+      requiresArg, invokeOnArg, opaqueSpecArg, bodyArg]
   | q`Laurel.function, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, invokeOnArg, ensuresArg, modifiesArg, bodyArg] =>
+      requiresArg, invokeOnArg, opaqueSpecArg, bodyArg] =>
     let name ← translateIdent nameArg
     let parameters ← translateParameters paramArg
     -- Either returnTypeArg or returnParamsArg may have a value, not both
@@ -465,10 +467,16 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
         | _, _ => TransM.error s!"Expected invokeOnClause operation, got {repr invokeOnOp.name}"
       | .option _ none => pure none
       | _ => pure none
-    -- Parse postconditions (ensures clauses - zero or more)
-    let postconditions ← translateEnsuresClauses ensuresArg
-    -- Parse modifies clauses (zero or more)
-    let modifies ← translateModifiesClauses modifiesArg
+    -- Parse optional opaqueSpec (contains ensures and modifies)
+    let (isOpaque, postconditions, modifies) ← match opaqueSpecArg with
+      | .option _ (some (.op opaqueSpecOp)) => match opaqueSpecOp.name, opaqueSpecOp.args with
+        | q`Laurel.opaqueSpec, #[ensuresArg, modifiesArg] =>
+          let postconditions ← translateEnsuresClauses ensuresArg
+          let modifies ← translateModifiesClauses modifiesArg
+          pure (true, postconditions, modifies)
+        | _, _ => TransM.error s!"Expected opaqueSpec operation, got {repr opaqueSpecOp.name}"
+      | .option _ none => pure (false, [], [])
+      | _ => pure (false, [], [])
     -- Parse optional body
     let isExternal ← match bodyArg with
       | .option _ (some (.op bodyOp)) => match bodyOp.name, bodyOp.args with
@@ -485,10 +493,10 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
     -- Determine procedure body kind
     let procBody :=
       if isExternal then Body.External
-      else match postconditions, body with
-      | _ :: _, bodyOpt => Body.Opaque postconditions bodyOpt modifies
-      | [], some b => Body.Transparent b
-      | [], none => Body.Opaque [] none modifies
+      else if isOpaque then Body.Opaque postconditions body modifies
+      else match body with
+      | some b => Body.Transparent b
+      | none => Body.Opaque [] none modifies
     return {
       name := name
       inputs := parameters
@@ -501,7 +509,7 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
     }
   | q`Laurel.procedure, args
   | q`Laurel.function, args =>
-    TransM.error s!"parseProcedure expects 9 arguments, got {args.size}"
+    TransM.error s!"parseProcedure expects 8 arguments, got {args.size}"
   | _, _ =>
     TransM.error s!"parseProcedure expects procedure or function, got {repr op.name}"
 
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index fa35ae23fc..af7c43b711 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: parameterized bvType with arbitrary width
+-- Last grammar change: added modifiesWildcard op for wildcard modifies clauses.
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index 3dec015888..cc2cc46083 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -157,10 +157,15 @@ op ensuresClause(cond: StmtExpr, errorMessage: Option ErrorSummary): EnsuresClau
 
 category ModifiesClause;
 op modifiesClause(refs: CommaSepBy StmtExpr): ModifiesClause => "\n  modifies " refs;
+op modifiesWildcard: ModifiesClause => "\n  modifies *";
 
 category ReturnParameters;
 op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "\n  returns " "(" parameters ")";
 
+category OpaqueSpec;
+op opaqueSpec(ensures: Seq EnsuresClause, modifies: Seq ModifiesClause): OpaqueSpec =>
+  "\n  opaque" ensures modifies;
+
 category Body;
 op body(body: StmtExpr): Body => "\n" body:0;
 op externalBody: Body => "external";
@@ -171,20 +176,18 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
   invokeOn: Option InvokeOnClause,
-  ensures: Seq EnsuresClause,
-  modifies: Seq ModifiesClause,
+  opaqueSpec: Option OpaqueSpec,
   body : Option Body) : Procedure =>
-  "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn ensures modifies body ";";
+  "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn opaqueSpec body ";";
 
 op function (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option ReturnType,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
   invokeOn: Option InvokeOnClause,
-  ensures: Seq EnsuresClause,
-  modifies: Seq ModifiesClause,
+  opaqueSpec: Option OpaqueSpec,
   body : Option Body) : Procedure =>
-  "function " name "(" parameters ")" returnType returnParameters requires invokeOn ensures modifies body ";";
+  "function " name "(" parameters ")" returnType returnParameters requires invokeOn opaqueSpec body ";";
 
 op composite (name: Ident, extending: Option Extends, fields: Seq Field, procedures: Seq Procedure): Composite => "composite " name extending " {" fields procedures " }";
 
diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
index 0a3b9bf029..5e472fb978 100644
--- a/Strata/Languages/Laurel/HeapParameterization.lean
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -63,7 +63,7 @@ def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do
   | .StaticCall callee args => modify fun s => { s with callees := callee :: s.callees }; for a in args do collectExprMd a
   | .IfThenElse c t e => collectExprMd c; collectExprMd t; if let some x := e then collectExprMd x
   | .Block stmts _ => for s in stmts do collectExprMd s
-  | .LocalVariable _ _ i => if let some x := i then collectExprMd x
+  | .LocalVariable _ i => if let some x := i then collectExprMd x
   | .While c invs d b => collectExprMd c; collectExprMd b; for inv in invs do collectExprMd inv; if let some x := d then collectExprMd x
   | .Return v => if let some x := v then collectExprMd x
   | .Assign assignTargets v =>
@@ -99,9 +99,12 @@ def analyzeProc (proc : Procedure) : AnalysisResult :=
   let bodyResult := match proc.body with
     | .Transparent b => (collectExprMd b).run {} |>.2
     | .Opaque postconds impl modif =>
-        -- A non-empty modifies clause implies the procedure reads and writes the heap;
-        -- no need to inspect the body further in that case.
-        if !modif.isEmpty then
+        -- A non-empty modifies clause (excluding wildcard `*`) implies the procedure
+        -- reads and writes the heap; no need to inspect the body further in that case.
+        -- Wildcard modifies does not imply heap access — it only suppresses the frame condition.
+        let isWildcard (e : StmtExprMd) : Bool := match e.1 with | .All => true | _ => false
+        let concreteModifies := modif.filter (fun e => !isWildcard e)
+        if !concreteModifies.isEmpty then
           { readsHeapDirectly := true, writesHeapDirectly := true, callees := [] }
         else
           let r1 := postconds.foldl (fun (acc : AnalysisResult) pc =>
@@ -277,7 +280,7 @@ where
         if calleeWritesHeap then
           if valueUsed then
             let freshVar ← freshVarName
-            let varDecl := mkMd (.LocalVariable freshVar (computeExprType model exprMd) none)
+            let varDecl := mkMd (.LocalVariable [{ name := freshVar, type := computeExprType model exprMd }] none)
             let callWithHeap := ⟨ .Assign
               [mkMd (.Identifier heapVar), mkMd (.Identifier freshVar)]
               (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source, md ⟩), source, md ⟩
@@ -308,9 +311,9 @@ where
           termination_by sizeOf remaining
         let stmts' ← processStmts 0 stmts
         return ⟨ .Block stmts' label, source, md ⟩
-    | .LocalVariable n ty i =>
+    | .LocalVariable params i =>
         let i' ← match i with | some x => some <$> recurse x | none => pure none
-        return ⟨ .LocalVariable n ty i', source, md ⟩
+        return ⟨ .LocalVariable params i', source, md ⟩
     | .While c invs d b =>
         let invs' ← invs.mapM (recurse ·)
         return ⟨ .While (← recurse c) invs' d (← recurse b false), source, md ⟩
diff --git a/Strata/Languages/Laurel/InferHoleTypes.lean b/Strata/Languages/Laurel/InferHoleTypes.lean
index 7070e991a2..064c76482f 100644
--- a/Strata/Languages/Laurel/InferHoleTypes.lean
+++ b/Strata/Languages/Laurel/InferHoleTypes.lean
@@ -47,6 +47,7 @@ private def calleeParamTypes (model : SemanticModel) (callee : Identifier) : Opt
 structure InferHoleState where
   model : SemanticModel
   currentOutputType : HighTypeMd := ⟨.Unknown, none, #[]⟩
+  diagnostics : List DiagnosticModel := []
 
 private abbrev InferHoleM := StateM InferHoleState
 
@@ -80,6 +81,8 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol
   match val with
   | .Hole det _ =>
       if expectedType.val == .Unknown then
+        let diag := (fileRangeToCoreMd source md).toDiagnostic "could not infer type"
+        modify fun s => { s with diagnostics := s.diagnostics ++ [diag] }
         return expr
       else
         return ⟨.Hole det (some expectedType), source, md⟩
@@ -117,9 +120,10 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol
         | target :: _ => computeExprType model target
         | _ => defaultHoleType
       return ⟨.Assign targets (← inferExpr value targetType), source, md⟩
-  | .LocalVariable name ty init =>
+  | .LocalVariable params init =>
+      let ty := match params with | p :: _ => p.type | [] => defaultHoleType
       match init with
-      | some initExpr => return ⟨.LocalVariable name ty (some (← inferExpr initExpr ty)), source, md⟩
+      | some initExpr => return ⟨.LocalVariable params (some (← inferExpr initExpr ty)), source, md⟩
       | none => return expr
   | .While cond invs dec body =>
       let dec' ← match dec with
@@ -161,11 +165,12 @@ private def inferProcedure (proc : Procedure) : InferHoleM Procedure := do
 
 /--
 Annotate every `.Hole` in the program with a type inferred from context.
+Returns the updated program and any diagnostics (e.g. holes whose type could not be inferred).
 -/
-def inferHoleTypes (model : SemanticModel) (program : Program) : Program :=
+def inferHoleTypes (model : SemanticModel) (program : Program) : Program × List DiagnosticModel :=
   let initState : InferHoleState := { model := model }
-  let (procs, _) := (program.staticProcedures.mapM inferProcedure).run initState
-  { program with staticProcedures := procs }
+  let (procs, finalState) := (program.staticProcedures.mapM inferProcedure).run initState
+  ({ program with staticProcedures := procs }, finalState.diagnostics)
 
 end -- public section
 end Laurel
diff --git a/Strata/Languages/Laurel/InlineLocalVariablesInExpressions.lean b/Strata/Languages/Laurel/InlineLocalVariablesInExpressions.lean
new file mode 100644
index 0000000000..46f9a7f022
--- /dev/null
+++ b/Strata/Languages/Laurel/InlineLocalVariablesInExpressions.lean
@@ -0,0 +1,83 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+public import Strata.Languages.Laurel.FunctionsAndProofs
+import Strata.Util.Tactics
+
+/-!
+# Inline Local Variables in Expression Position
+
+Replaces local variable declarations in functional procedure bodies with
+direct substitution of the initializer into the remaining statements of
+the block. This eliminates `LocalVariable` nodes from expression contexts
+so the Core translator does not need to handle let-bindings in expressions.
+
+Example:
+```
+function f() returns (r: int) {
+  var x: int := 1;
+  var y: int := x + 1;
+  y
+}
+```
+becomes:
+```
+function f() returns (r: int) {
+  0 + 1
+}
+```
+-/
+
+namespace Strata.Laurel
+
+public section
+
+/-- Substitute all occurrences of identifier `name` with `replacement` in `expr`. -/
+private def substIdentifier (name : Identifier) (replacement : StmtExprMd) (expr : StmtExprMd)
+    : StmtExprMd :=
+  mapStmtExpr (fun e =>
+    match e.val with
+    | .Identifier n => if n == name then replacement else e
+    | _ => e) expr
+
+/-- Inline initialized local variables in a block, substituting their
+    initializers into the remaining statements. Non-LocalVariable
+    statements are kept as-is. -/
+private def inlineLocalsInStmts (stmts : List StmtExprMd) : List StmtExprMd :=
+  match stmts with
+  | [] => []
+  | ⟨.LocalVariable [parameter] (some initializer), _, _⟩ :: rest =>
+    let rest' := rest.map (substIdentifier parameter.name initializer)
+    inlineLocalsInStmts rest'
+  | s :: rest => s :: inlineLocalsInStmts rest
+termination_by stmts.length
+
+/-- Rewrite a single node: if it is a Block, inline any LocalVariable
+    declarations. Recursion into children is handled by `mapStmtExpr`. -/
+private def inlineLocalsNode (expr : StmtExprMd) : StmtExprMd :=
+  match expr.val with
+  | .Block stmts label =>
+    let stmts' := inlineLocalsInStmts stmts
+    match stmts' with
+    | [single] => single
+    | _ => ⟨.Block stmts' label, expr.source, expr.md⟩
+  | _ => expr
+
+/-- Apply local-variable inlining to all functional procedure bodies. -/
+def inlineLocalVariablesInExpressions (program : FunctionsAndProofsProgram) : FunctionsAndProofsProgram :=
+  { program with functions := program.functions.map fun proc =>
+      match proc.body with
+      | .Transparent body =>
+        { proc with body := .Transparent (mapStmtExpr inlineLocalsNode body) }
+      | .Opaque postconds (some impl) modif =>
+        { proc with body := .Opaque postconds (some (mapStmtExpr inlineLocalsNode impl)) modif }
+      | _ => proc
+  }
+
+end -- public section
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index f7f8129322..dc1ae0b8ef 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -197,6 +197,9 @@ structure Procedure : Type where
       whose body is the ensures clause universally quantified over the procedure's inputs,
       with this expression as the SMT trigger. -/
   invokeOn : Option (AstNode StmtExpr) := none
+  /-- Axioms to emit alongside this procedure. Populated by the contract pass from
+      `invokeOn` and ensures clauses. -/
+  axioms : List (AstNode StmtExpr) := []
 
 /--
 A typed parameter for a procedure.
@@ -238,8 +241,8 @@ inductive StmtExpr : Type where
   | IfThenElse (cond : AstNode StmtExpr) (thenBranch : AstNode StmtExpr) (elseBranch : Option (AstNode StmtExpr))
   /-- A sequence of statements with an optional label for `Exit`. -/
   | Block (statements : List (AstNode StmtExpr)) (label : Option String)
-  /-- A local variable declaration with a type and optional initializer. The initializer must be set if this `StmtExpr` is pure. -/
-  | LocalVariable (name : Identifier) (type : AstNode HighType) (initializer : Option (AstNode StmtExpr))
+  /-- A local variable declaration with typed parameters and optional initializer. The initializer must be set if this `StmtExpr` is pure. Multiple parameters are only allowed when the initializer is a `StaticCall` to a procedure with multiple outputs. -/
+  | LocalVariable (parameters : List Parameter) (initializer : Option (AstNode StmtExpr))
   /-- A while loop with a condition, invariants, optional termination measure, and body. Only allowed in impure contexts. -/
   | While (cond : AstNode StmtExpr) (invariants : List (AstNode StmtExpr))
     (decreases : Option (AstNode StmtExpr))
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index 81d34ba1d6..6dfbed3612 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -8,8 +8,12 @@ module
 public import Strata.Languages.Laurel.LaurelToCoreTranslator
 import Strata.Languages.Laurel.DesugarShortCircuit
 import Strata.Languages.Laurel.EliminateReturnsInExpression
+import Strata.Languages.Laurel.EliminateReturnStatements
 import Strata.Languages.Laurel.EliminateValueReturns
+import Strata.Languages.Laurel.InlineLocalVariablesInExpressions
 import Strata.Languages.Laurel.ConstrainedTypeElim
+import Strata.Languages.Laurel.ContractPass
+import Strata.Languages.Laurel.EliminateMultipleOutputs
 import Strata.Languages.Core.Verifier
 
 /-!
@@ -21,9 +25,10 @@ to Strata Core. The pipeline is:
 1. Prepend core definitions for Laurel.
 2. Run a sequence of Laurel-to-Laurel lowering passes (resolution, heap
    parameterization, type hierarchy, modifies clauses, hole inference,
-   desugaring, lifting, constrained type elimination).
-3. Group and order declarations into an `OrderedLaurel`.
-4. Translate the `OrderedLaurel` to a `Core.Program`.
+   desugaring, lifting, constrained type elimination, contract pass).
+3. Run the proof pass to produce a `FunctionsAndProofsProgram`.
+4. Group and order declarations into a `CoreWithLaurelTypes`.
+5. Translate the `CoreWithLaurelTypes` to a `Core.Program`.
 -/
 
 open Core (VCResult VCResults VerifyOptions)
@@ -92,7 +97,7 @@ private def runLaurelPasses (options : LaurelTranslateOptions) (program : Progra
   let result := resolve program (some model)
   let (program, model) := (result.program, result.model)
   emit "ModifiesClausesTransform" program
-  let program := inferHoleTypes model program
+  let (program, inferHoleDiags) := inferHoleTypes model program
   emit "InferHoleTypes" program
   let program := eliminateHoles program
   emit "EliminateHoles" program
@@ -105,13 +110,32 @@ private def runLaurelPasses (options : LaurelTranslateOptions) (program : Progra
   let (program, model) := (result.program, result.model)
   emit "EliminateReturns" program
 
+  let program := eliminateReturnStatements program
+  emit "EliminateReturnStatements" program
+
   let (program, constrainedTypeDiags) := constrainedTypeElim model program
   let result := resolve program (some model)
   let (program, model) := (result.program, result.model)
   emit "ConstrainedTypeElim" program
 
+  let program := contractPass program
+
+  -- Check if the pipeline introduced new resolution errors that weren't present initially.
+  -- This catches bugs where a pass produces unresolvable names, which would silently
+  -- cause coreProgramHasSuperfluousErrors to be set with no user-visible diagnostic.
+  let finalResolutionErrors := (resolve program (some model)).errors
+  let newResolutionErrors : List DiagnosticModel :=
+    if finalResolutionErrors.size > resolutionErrors.length then
+      let newCount := finalResolutionErrors.size - resolutionErrors.length
+      let firstNew := finalResolutionErrors.toList.drop resolutionErrors.length
+        |>.head?.map (·.message) |>.getD "unknown"
+      [DiagnosticModel.fromMessage
+        s!"Strata bug: {newCount} new resolution error(s) introduced by pipeline passes. First new error: {firstNew}"
+        DiagnosticType.StrataBug]
+    else []
+
   let allDiags := resolutionErrors ++ diamondErrors ++ nonCompositeDiags ++
-    valueReturnDiags.toList ++ modifiesDiags ++ constrainedTypeDiags
+    valueReturnDiags.toList ++ modifiesDiags ++ inferHoleDiags ++ constrainedTypeDiags ++ newResolutionErrors
   return (program, model, allDiags)
 
 /--
@@ -124,14 +148,54 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
     (keepAllFilesPrefix : Option String := none)
     : IO TranslateResultWithLaurel := do
   let (program, model, passDiags) ← runLaurelPasses options program keepAllFilesPrefix
-  let ordered := orderProgram program
-  let initState : TranslateState := { model := model, overflowChecks := options.overflowChecks }
-  let (coreProgramOption, translateState) :=
-    runTranslateM initState (translateLaurelToCore options program ordered)
-  let allDiagnostics := passDiags ++ translateState.diagnostics
-  let coreProgramOption :=
-    if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption
-  return (coreProgramOption, allDiagnostics, program)
+  let functionsAndProofs := laurelToFunctionsAndProofs program
+  let functionsAndProofs := eliminateMultipleOutputs functionsAndProofs
+  let functionsAndProofs := inlineLocalVariablesInExpressions functionsAndProofs
+
+  let fnProgram : Program := {
+    staticProcedures := functionsAndProofs.functions ++ functionsAndProofs.proofs,
+    staticFields := [],
+    types := functionsAndProofs.datatypes.map TypeDefinition.Datatype ++
+    -- Hack to compensate for references to composite types not having been updated yet.
+      program.types.filter (fun t => match t with | .Composite _ => true | _ => false),
+    constants := program.constants
+  }
+  let fnResolveResult := resolve fnProgram (some model)
+  let fnModel := fnResolveResult.model
+
+  -- Reconstruct FunctionsAndProofsProgram from the resolved fnProgram so that
+  -- identifiers introduced by eliminateMultipleOutputs have their uniqueId set.
+  let resolvedProcs := fnResolveResult.program.staticProcedures
+  let resolvedDatatypes := fnResolveResult.program.types.filterMap fun td =>
+    match td with | .Datatype dt => some dt | _ => none
+  let functionsAndProofs : FunctionsAndProofsProgram := {
+    functions := resolvedProcs.filter (·.isFunctional)
+    proofs := resolvedProcs.filter (!·.isFunctional)
+    datatypes := resolvedDatatypes
+    constants := fnResolveResult.program.constants
+  }
+
+  let coreWithLaurelTypes := orderFunctionsAndProofs functionsAndProofs
+  if ! passDiags.isEmpty then
+    return (none, passDiags, program)
+  else
+    let initState : TranslateState := { model := fnModel, overflowChecks := options.overflowChecks }
+    let (coreProgramOption, translateState) :=
+      runTranslateM initState (translateLaurelToCore options program coreWithLaurelTypes)
+    -- Because of the duplication between functions and proofs, this translation is liable to create duplicate diagnostics
+    -- User errors should be checked in an earlier phase, and all dumb translation errors are Strata bugs
+    let allDiagnostics := translateState.diagnostics.eraseDups
+    let allDiagnostics :=
+      if translateState.coreProgramHasSuperfluousErrors && allDiagnostics.isEmpty then
+        -- The program was suppressed but no diagnostics explain why — that's a bug.
+        allDiagnostics ++ [DiagnosticModel.fromMessage
+          "Core program was suppressed due to superfluous errors, but no diagnostics were emitted. This is a bug."
+          DiagnosticType.StrataBug]
+      else allDiagnostics
+
+    let coreProgramOption :=
+      if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption
+    return (coreProgramOption, allDiagnostics, program)
 
 /--
 Translate Laurel Program to Core Program.
@@ -145,8 +209,9 @@ Verify a Laurel program using an SMT solver.
 -/
 def verifyToVcResults (program : Program)
     (options : VerifyOptions := .default)
+    (laurelOptions : LaurelTranslateOptions)
     : IO (Option VCResults × List DiagnosticModel) := do
-  let (coreProgramOption, translateDiags) ← translate {} program
+  let (coreProgramOption, translateDiags) ← translate laurelOptions program
 
   match coreProgramOption with
   | some coreProgram =>
@@ -166,13 +231,15 @@ duplicated assertions merged at the VCOutcome level.
 -/
 def verifyToMergedResults (program : Program)
     (options : VerifyOptions := .default)
+    (laurelOptions : LaurelTranslateOptions)
     : IO (Option VCResults × List DiagnosticModel) := do
-  let (vcOpt, diags) ← verifyToVcResults program options
+  let (vcOpt, diags) ← verifyToVcResults program options laurelOptions
   return (vcOpt.map (·.mergeByAssertion), diags)
 
 def verifyToDiagnostics (files : Map Strata.Uri Lean.FileMap) (program : Program)
-    (options : VerifyOptions := .default) : IO (Array Diagnostic) := do
-  let results ← verifyToMergedResults program options
+    (options : VerifyOptions := .default)
+    (laurelOptions : LaurelTranslateOptions := {}) : IO (Array Diagnostic) := do
+  let results ← verifyToMergedResults program options laurelOptions
   let phases := Core.coreAbstractedPhases
   let translationDiags := results.snd.map (fun dm => dm.toDiagnostic files)
   let vcDiags := match results.fst with
@@ -182,7 +249,7 @@ def verifyToDiagnostics (files : Map Strata.Uri Lean.FileMap) (program : Program
 
 def verifyToDiagnosticModels (program : Program) (options : VerifyOptions := .default)
     : IO (Array DiagnosticModel) := do
-  let results ← verifyToMergedResults program options
+  let results ← verifyToMergedResults program options {}
   let phases := Core.coreAbstractedPhases
   let vcDiags := match results.fst with
   | none => []
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index f916dce425..d6a6e70665 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -32,7 +32,7 @@ import Strata.Languages.Laurel.ConstrainedTypeElim
 import Strata.Util.Tactics
 
 open Core (VCResult VCResults VerifyOptions)
-open Core (intAddOp intSubOp intMulOp intSafeDivOp intSafeModOp intSafeDivTOp intSafeModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp)
+open Core (intAddOp intSubOp intMulOp intDivOp intSafeDivOp intModOp intSafeModOp intDivTOp intSafeDivTOp intModTOp intSafeModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp)
 open Core (realAddOp realSubOp realMulOp realDivOp realNegOp realLtOp realLeOp realGtOp realGeOp)
 
 namespace Strata.Laurel
@@ -64,6 +64,11 @@ structure TranslateState where
   overflowChecks : Core.OverflowChecks := {}
   /-- Do not process the produces Core program, since it has superfluous errors -/
   coreProgramHasSuperfluousErrors: Bool := false
+  /-- When `true`, use safe division (`intSafeDivOp`) and safe datatype selectors
+      (with preconditions). When `false`, use unsafe division (`intDivOp`) and
+      unsafe datatype selectors (without preconditions).
+      Set to `true` for proof procedures and `false` for functions. -/
+  proof : Bool := false
 
 /-- The translation monad: state over Except, allowing both accumulated diagnostics and hard failures -/
 @[expose] abbrev TranslateM := OptionT (StateM TranslateState)
@@ -72,6 +77,25 @@ structure TranslateState where
 def emitDiagnostic (d : DiagnosticModel) : TranslateM Unit :=
   modify fun s => { s with diagnostics := s.diagnostics ++ [d] }
 
+/-- Adjust a datatype selector (destructor) name based on the `proof` flag.
+    Destructor names contain `..` (e.g. `IntList..head`, `IntList..head!`).
+    Tester names also contain `..` but start with `is` after the separator.
+    - `proof = true` → use safe selectors (strip `!` suffix)
+    - `proof = false` → use unsafe selectors (add `!` suffix) -/
+private def adjustSelectorName (name : String) (proof : Bool) : String :=
+  -- Only adjust destructor names (contain ".." but are not testers)
+  match name.splitOn ".." with
+  | [_, suffix] =>
+    if suffix.startsWith "is" then name  -- tester, leave unchanged
+    else if proof then
+      name
+      -- Safe: strip trailing "!"
+      -- if name.endsWith "!" then (name.dropEnd 1).toString else name
+    else
+      -- Unsafe: add trailing "!" if not already present
+      if name.endsWith "!" then name else name ++ "!"
+  | _ => name  -- not a destructor name, leave unchanged
+
 /-- Abort the Core program by setting the superfluous-errors flag and returning a dummy type. -/
 private def throwTypeDiagnostic (ty : HighTypeMd) (msg : String) : TranslateM LMonoTy := do
   emitDiagnostic ((astNodeToCoreMd ty).toDiagnostic msg)
@@ -88,7 +112,7 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do
   | .TBool => return LMonoTy.bool
   | .TString => return LMonoTy.string
   | .TBv n => return LMonoTy.bitvec n
-  | .TVoid => return LMonoTy.bool -- Using bool as placeholder for void
+  | .TVoid => return .tcons "errorVoid" []
   | .THeap => return .tcons "Heap" []
   | .TTypedField _ => return .tcons "Field" []
   | .TSet elementType => return Core.mapTy (← translateType elementType) LMonoTy.bool
@@ -100,7 +124,7 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do
     | some (.datatypeConstructor typeName _) => return .tcons typeName.text []
     | _ => do -- resolution should have already emitted a diagnostic
       modify fun s => { s with coreProgramHasSuperfluousErrors := true }
-      return .tcons "Composite" []
+      return .tcons "errorUserDefined" []
   | .TCore s => return .tcons s []
   | .TReal => return LMonoTy.real
   | .Unknown => throwTypeDiagnostic ty "could not infer type"
@@ -115,9 +139,6 @@ def lookupType (name : Identifier) : TranslateM LMonoTy := do
 def runTranslateM (s : TranslateState) (m : TranslateM α) : (Option α × TranslateState) :=
   m s
 
-def returnNone: TranslateM α :=
-  StateT.pure none
-
 /-- Allocate a fresh unique ID. -/
 private def freshId : TranslateM Nat := do
   let s ← get
@@ -129,8 +150,7 @@ private def freshId : TranslateM Nat := do
 def throwExprDiagnostic (d : DiagnosticModel): TranslateM Core.Expression.Expr := do
   emitDiagnostic d
   modify fun s => { s with coreProgramHasSuperfluousErrors := true }
-  let id ← freshId
-  return LExpr.fvar () (⟨s!"DUMMY_VAR_{id}", ()⟩) none
+  return default
 
 /--
 Translate Laurel StmtExpr to Core Expression using the `TranslateM` monad.
@@ -151,11 +171,9 @@ def translateExpr (expr : StmtExprMd)
   let s ← get
   let model := s.model
   let md := astNodeToCoreMd expr
+  let proof := (← get).proof
   let disallowed (md : MetaData) (msg : String) : TranslateM Core.Expression.Expr := do
-    if isPureContext then
-      throwExprDiagnostic $ md.toDiagnostic msg
-    else
-      throwExprDiagnostic $ md.toDiagnostic s!"{msg} (should have been lifted)" DiagnosticType.StrataBug
+    throwExprDiagnostic $ md.toDiagnostic msg DiagnosticType.StrataBug
 
   match h: expr.val with
   | .LiteralBool b => return .const () (.boolConst b)
@@ -205,10 +223,10 @@ def translateExpr (expr : StmtExprMd)
     | .Add => return binOp (if isReal then realAddOp else intAddOp)
     | .Sub => return binOp (if isReal then realSubOp else intSubOp)
     | .Mul => return binOp (if isReal then realMulOp else intMulOp)
-    | .Div => return binOp (if isReal then realDivOp else intSafeDivOp)
-    | .Mod => return binOp intSafeModOp
-    | .DivT => return binOp intSafeDivTOp
-    | .ModT => return binOp intSafeModTOp
+    | .Div => return binOp (if isReal then realDivOp else if proof then intSafeDivOp else intDivOp)
+    | .Mod => return binOp (if (← get).proof then intSafeModOp else intModOp)
+    | .DivT => return binOp (if (← get).proof then intSafeDivTOp else intDivTOp)
+    | .ModT => return binOp (if (← get).proof then intSafeModTOp else intModTOp)
     | .Lt => return binOp (if isReal then realLtOp else intLtOp)
     | .Leq => return binOp (if isReal then realLeOp else intLeOp)
     | .Gt => return binOp (if isReal then realGtOp else intGtOp)
@@ -235,7 +253,8 @@ def translateExpr (expr : StmtExprMd)
       if isPureContext && !model.isFunction callee then
         disallowed md "calls to procedures are not supported in functions or contracts"
       else
-        let fnOp : Core.Expression.Expr := .op () ⟨callee.text, ()⟩ none
+        let calleeName := adjustSelectorName callee.text (← get).proof
+        let fnOp : Core.Expression.Expr := .op () ⟨calleeName, ()⟩ none
         args.attach.foldlM (fun acc ⟨arg, _⟩ => do
           let re ← translateExpr arg boundVars isPureContext
           return .app () acc re) fnOp
@@ -277,15 +296,20 @@ def translateExpr (expr : StmtExprMd)
   | .Block (⟨ .Assume _, innerSrc, innerMd⟩ :: rest) label =>
     _ ← disallowed (fileRangeToCoreMd innerSrc innerMd) "assumes are not YET supported in functions or contracts"
     translateExpr { val := StmtExpr.Block rest label, source := innerSrc, md := innerMd } boundVars isPureContext
-  | .Block (⟨ .LocalVariable name ty (some initializer), innerSrc, innerMd⟩ :: rest) label => do
-      let valueExpr ← translateExpr  initializer boundVars isPureContext
+  | .Block (⟨ .LocalVariable [] (some initializer), innerSrc, innerMd⟩ :: rest) label =>
+    -- If a local variables has no targets, it can be ignored.
+    translateExpr { val := StmtExpr.Block rest label, source := innerSrc, md := innerMd } boundVars isPureContext
+  | .Block (⟨ .LocalVariable [⟨ name, ty ⟩] (some initializer), innerSrc, innerMd⟩ :: rest) label => do
+      let valueExpr ← translateExpr initializer boundVars isPureContext
       let bodyExpr ← translateExpr { val := StmtExpr.Block rest label, source := innerSrc, md := innerMd } (name :: boundVars) isPureContext
       disallowed (fileRangeToCoreMd innerSrc innerMd) "local variables in functions are not YET supported"
       -- This doesn't work because of a limitation in Core.
-      -- let coreMonoType := translateType ty
-      -- return .app () (.abs () (some coreMonoType) bodyExpr) valueExpr
-  | .Block (⟨ .LocalVariable name ty none, innerSrc, innerMd⟩ :: rest) label =>
+      -- let coreMonoType ← translateType ty
+      -- return .app () (.abs () "" (some coreMonoType) bodyExpr) valueExpr
+  | .Block (⟨ .LocalVariable _params none, innerSrc, innerMd⟩ :: rest) label =>
     disallowed (fileRangeToCoreMd innerSrc innerMd) "local variables in functions must have initializers"
+  | .Block (⟨ .LocalVariable (x::xs) _, innerSrc, innerMd⟩ :: rest) label =>
+    disallowed (fileRangeToCoreMd innerSrc innerMd) "local variables in functions may only have one target"
   | .Block (⟨ .IfThenElse cond thenBranch (some elseBranch), innerSrc, innerMd⟩ :: rest) label =>
     disallowed (fileRangeToCoreMd innerSrc innerMd) "if-then-else only supported as the last statement in a block"
 
@@ -298,7 +322,7 @@ def translateExpr (expr : StmtExprMd)
       throwExprDiagnostic $ md.toDiagnostic s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldId.text}" DiagnosticType.StrataBug
   | .Block _ _ =>
       throwExprDiagnostic $ md.toDiagnostic "block expression should have been lowered in a separate pass" DiagnosticType.StrataBug
-  | .LocalVariable _ _ _ =>
+  | .LocalVariable _ _ =>
       throwExprDiagnostic $ md.toDiagnostic "local variable expression should be lowered in a separate pass" DiagnosticType.StrataBug
   | .Return _ => disallowed md "return expression should be lowered in a separate pass"
 
@@ -370,37 +394,51 @@ def translateStmt (stmt : StmtExprMd)
       match label with
       | some l => return [Imperative.Stmt.block l innerStmts md]
       | none   => return innerStmts
-  | .LocalVariable id ty initializer =>
-      let coreMonoType ← translateType ty
-      let coreType := LTy.forAll [] coreMonoType
-      let ident := ⟨id.text, ()⟩
+  | .LocalVariable params initializer =>
       match initializer with
       | some (⟨ .StaticCall callee args, callSrc, callMd⟩) =>
           -- Check if this is a function or a procedure call
           if model.isFunction callee then
             -- Translate as expression (function application)
             let coreExpr ← translateExpr { val := .StaticCall callee args, source := callSrc, md := callMd }
-            return [Core.Statement.init ident coreType (.det coreExpr) md]
+            let stmts ← params.mapM fun p => do
+              let coreType := LTy.forAll [] (← translateType p.type)
+              pure (Core.Statement.init ⟨p.name.text, ()⟩ coreType (.det coreExpr) md)
+            return stmts
           else
             -- Translate as: var name; call name := callee(args)
             let coreArgs ← args.mapM (fun a => translateExpr a)
-            let defaultExpr ← defaultExprForType ty
-            let initStmt := Core.Statement.init ident coreType (.det defaultExpr) md
-            let callStmt := Core.Statement.call [ident] callee.text coreArgs md
-            return [initStmt, callStmt]
+            let initStmts ← params.mapM fun p => do
+              let coreType := LTy.forAll [] (← translateType p.type)
+              let defaultExpr ← defaultExprForType p.type
+              pure (Core.Statement.init ⟨p.name.text, ()⟩ coreType (.det defaultExpr) md)
+            let idents := params.map fun p => ⟨p.name.text, ()⟩
+            let callStmt := Core.Statement.call idents callee.text coreArgs md
+            return initStmts ++ [callStmt]
       | some (⟨ .InstanceCall .., _, _⟩) =>
           -- Instance method call as initializer: var name := target.method(args)
           -- Havoc the result since instance methods may be on unmodeled types
-          let initStmt := Core.Statement.init ident coreType .nondet md
-          return [initStmt]
+          let stmts ← params.mapM fun p => do
+            let coreType := LTy.forAll [] (← translateType p.type)
+            pure (Core.Statement.init ⟨p.name.text, ()⟩ coreType .nondet md)
+          return stmts
       | some (⟨ .Hole _ _, _, _⟩) =>
           -- Hole initializer: treat as havoc (init without value)
-          return [Core.Statement.init ident coreType .nondet md]
+          let stmts ← params.mapM fun p => do
+            let coreType := LTy.forAll [] (← translateType p.type)
+            pure (Core.Statement.init ⟨p.name.text, ()⟩ coreType .nondet md)
+          return stmts
       | some initExpr =>
           let coreExpr ← translateExpr initExpr
-          return [Core.Statement.init ident coreType (.det coreExpr) md]
+          let stmts ← params.mapM fun p => do
+            let coreType := LTy.forAll [] (← translateType p.type)
+            pure (Core.Statement.init ⟨p.name.text, ()⟩ coreType (.det coreExpr) md)
+          return stmts
       | none =>
-          return [Core.Statement.init ident coreType .nondet md]
+          let stmts ← params.mapM fun p => do
+            let coreType := LTy.forAll [] (← translateType p.type)
+            pure (Core.Statement.init ⟨p.name.text, ()⟩ coreType .nondet md)
+          return stmts
   | .Assign targets value =>
       match targets with
       | [⟨ .Identifier targetId, _, _ ⟩] =>
@@ -456,7 +494,7 @@ def translateStmt (stmt : StmtExprMd)
               return (havocStmts)
           | _ =>
               emitDiagnostic $ md.toDiagnostic "Assignments with multiple target but without a RHS call should not be constructed"
-              returnNone
+              return []
   | .IfThenElse cond thenBranch elseBranch =>
       let bcond ← translateExpr cond
       let bthen ← translateStmt thenBranch
@@ -574,42 +612,6 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do
   let spec : Core.Procedure.Spec := { modifies, preconditions, postconditions }
   return { header, spec, body }
 
-def translateInvokeOnAxiom (proc : Procedure) (trigger : StmtExprMd)
-    : TranslateM (Option Core.Decl) := do
-  let postconds := match proc.body with
-    | .Opaque postconds _ _ | .Abstract postconds => postconds
-    | _ => []
-  if postconds.isEmpty then return none
-  -- All input param names become bound variables.
-  -- buildQuants nests ∀ p1, ∀ p2, ..., ∀ pn :: body, so inside body the innermost
-  -- binder (pn) is de Bruijn index 0, and the outermost (p1) is index n-1.
-  -- translateExpr uses findIdx? on boundVars, so we must list params innermost-first
-  -- (i.e. reversed) so that pn → 0, ..., p1 → n-1.
-  let boundVars := proc.inputs.reverse.map (·.name)
-  -- Translate postconditions and trigger with the full bound-var context
-  let postcondExprs ← postconds.mapM (fun pc => translateExpr pc boundVars (isPureContext := true))
-  let bodyExpr : Core.Expression.Expr := match postcondExprs with
-    | [] => .const () (.boolConst true)
-    | [e] => e
-    | e :: rest => rest.foldl (fun acc x => LExpr.mkApp () boolAndOp [acc, x]) e
-  let triggerExpr ← translateExpr trigger boundVars (isPureContext := true)
-  -- Wrap in ∀ from outermost (first param) to innermost (last param).
-  -- The trigger is placed on the innermost quantifier.
-  let quantified ← buildQuants proc.inputs bodyExpr triggerExpr
-  return some (.ax { name := s!"invokeOn_{proc.name.text}", e := quantified } proc.name.md)
-where
-  /-- Build `∀ p1 ... pn :: { trigger } body`. The trigger is on the innermost quantifier. -/
-  buildQuants (params : List Parameter)
-      (body : Core.Expression.Expr) (trigger : Core.Expression.Expr)
-      : TranslateM Core.Expression.Expr := do
-    match params with
-    | [] => return body
-    | [p] =>
-      return LExpr.allTr () p.name.text (some (← translateType p.type)) trigger body
-    | p :: rest => do
-      let inner ← buildQuants rest body trigger
-      return LExpr.all () p.name.text (some (← translateType p.type)) inner
-
 structure LaurelTranslateOptions where
   emitResolutionErrors : Bool := true
   inlineFunctionsWhenPossible : Bool := false
@@ -694,35 +696,31 @@ def translateDatatypeDefinition (dt : DatatypeDefinition)
 abbrev TranslateResult := (Option Core.Program) × (List DiagnosticModel)
 
 /--
-Translate an `OrderedLaurel` program to a `Core.Program`.
+Translate a `CoreWithLaurelTypes` program to a `Core.Program`.
 The `program` parameter is the lowered Laurel program, used for type definitions.
 -/
-def translateLaurelToCore (options: LaurelTranslateOptions) (program : Program) (ordered : OrderedLaurel): TranslateM Core.Program := do
+def translateLaurelToCore (options: LaurelTranslateOptions) (_program : Program) (ordered : CoreWithLaurelTypes): TranslateM Core.Program := do
 
   let coreDecls ← ordered.decls.flatMapM fun
-    | .procs procs isRecursive => do
-      -- For each SCC, determine if it is purely functional or contains procedures.
-      let isFuncSCC := procs.all (·.isFunctional)
-      if isFuncSCC then
-        let funcs ← procs.mapM (translateProcedureToFunction options isRecursive)
-        if isRecursive then
-          let coreFuncs := funcs.filterMap (fun d => match d with
-            | .func f _ => some f
-            | _ => none)
-          return [Core.Decl.recFuncBlock coreFuncs mdWithUnknownLoc]
-        else
-          return funcs
+    | .funcs funcs isRecursive => do
+      modify fun s => { s with proof := false }
+      let nonExternal := funcs.filter (fun p => !p.body.isExternal)
+      let coreFuncs ← nonExternal.mapM (translateProcedureToFunction options isRecursive)
+      if isRecursive then
+        let coreFuncValues := coreFuncs.filterMap (fun d => match d with
+          | .func f _ => some f
+          | _ => none)
+        return [Core.Decl.recFuncBlock coreFuncValues mdWithUnknownLoc]
       else
-        let procDecls ← procs.flatMapM fun proc => do
-          let procDecl ← translateProcedure proc
-          -- Turn free postconditions into axioms placed right behind the related procedure
-          let axiomDecls : List Core.Decl ← match proc.invokeOn with
-            | none => pure []
-            | some trigger => do
-              let axDecl? ← translateInvokeOnAxiom proc trigger
-              pure axDecl?.toList
-          return [Core.Decl.proc procDecl proc.name.md] ++ axiomDecls
-        return procDecls
+        return coreFuncs
+    | .procedure proc => do
+      modify fun s => { s with proof := true }
+      let procDecl ← translateProcedure proc
+      -- Translate axioms (populated by the contract pass from invokeOn + ensures)
+      let axiomDecls ← proc.axioms.mapM fun ax => do
+        let coreExpr ← translateExpr ax [] (isPureContext := true)
+        return Core.Decl.ax { name := s!"invokeOn_{proc.name.text}", e := coreExpr } proc.name.md
+      return [Core.Decl.proc procDecl proc.name.md] ++ axiomDecls
     | .datatypes dts => do
       let ldatatypes ← dts.mapM translateDatatypeDefinition
       return [Core.Decl.type (.data ldatatypes) mdWithUnknownLoc]
@@ -737,14 +735,6 @@ def translateLaurelToCore (options: LaurelTranslateOptions) (program : Program)
         body := body
       } mdWithUnknownLoc]
 
-
-  -- Emit diagnostics for composite types with instance procedures.
-  for td in program.types do
-    if let .Composite ct := td then
-      for proc in ct.instanceProcedures do
-        emitDiagnostic $ proc.name.md.toDiagnostic
-          s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' is not yet supported"
-          DiagnosticType.NotYetImplemented
   pure { decls := coreDecls }
 
 end -- public section
diff --git a/Strata/Languages/Laurel/LaurelTypes.lean b/Strata/Languages/Laurel/LaurelTypes.lean
index 0abc0cdcc2..7530fc8888 100644
--- a/Strata/Languages/Laurel/LaurelTypes.lean
+++ b/Strata/Languages/Laurel/LaurelTypes.lean
@@ -75,7 +75,7 @@ def computeExprType (model : SemanticModel) (expr : StmtExprMd) : HighTypeMd :=
         computeExprType model last
     | none => ⟨ .TVoid, source, md ⟩
   -- Statements
-  | .LocalVariable _ _ _ => ⟨ .TVoid, source, md ⟩
+  | .LocalVariable _ _ => ⟨ .TVoid, source, md ⟩
   | .While _ _ _ _ => ⟨ .TVoid, source, md ⟩
   | .Exit _ => ⟨ .TVoid, source, md ⟩
   | .Return _ => ⟨ .TVoid, source, md ⟩
diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 9aa9045606..0fcb4304a8 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -102,7 +102,7 @@ private def freshTempFor (varName : Identifier) : LiftM Identifier := do
 private def freshCondVar : LiftM Identifier := do
   let n := (← get).condCounter
   modify fun s => { s with condCounter := n + 1 }
-  return s!"$c_{n}"
+  return s!"$cndtn_{n}"
 
 private def prepend (stmt : StmtExprMd) : LiftM Unit :=
   modify fun s => { s with prependedStmts := stmt :: s.prependedStmts }
@@ -212,7 +212,7 @@ private def liftAssignExpr (targets : List StmtExprMd) (seqValue : StmtExprMd)
         let snapshotName ← freshTempFor varName
         let varType ← computeType target
         -- Snapshot goes before the assignment (cons pushes to front)
-        prepend (⟨.LocalVariable snapshotName varType (some (⟨.Identifier varName, source, md⟩)), source, md⟩)
+        prepend (⟨.LocalVariable [{ name := snapshotName, type := varType }] (some (⟨.Identifier varName, source, md⟩)), source, md⟩)
         setSubst varName snapshotName
     | _ => pure ()
 
@@ -233,7 +233,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
   | .Hole false (some holeType) =>
       -- Nondeterministic typed hole: lift to a fresh variable with no initializer (havoc)
       let holeVar ← freshCondVar
-      prepend (bare (.LocalVariable holeVar holeType none))
+      prepend ⟨ .LocalVariable [{ name := holeVar, type := holeType }] none, source, md⟩
       return bare (.Identifier holeVar)
 
   | .Assign targets value =>
@@ -271,7 +271,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       let callResultVar ← freshCondVar
       let callResultType ← computeType expr
       let liftedCall := [
-        ⟨ (.LocalVariable callResultVar callResultType none), source, md ⟩,
+        ⟨ (.LocalVariable [{ name := callResultVar, type := callResultType }] none), source, md ⟩,
         ⟨.Assign [bare (.Identifier callResultVar)] seqCall, source, md⟩
       ]
       modify fun s => { s with prependedStmts := s.prependedStmts ++ liftedCall}
@@ -312,7 +312,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
         -- IfThenElse added first (cons puts it deeper), then declaration (cons puts it on top)
         -- Output order: declaration, then if-then-else
         prepend (⟨.IfThenElse seqCond thenBlock seqElse, source, md⟩)
-        prepend (bare (.LocalVariable condVar condType none))
+        prepend ⟨ .LocalVariable [{ name := condVar, type := condType }] none, source, md ⟩
         return bare (.Identifier condVar)
       else
         -- No assignments in branches — recurse normally
@@ -327,19 +327,23 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       let newStmts := (← stmts.reverse.mapM transformExpr).reverse
       return ⟨ .Block (← onlyKeepSideEffectStmtsAndLast newStmts) labelOption, source, md ⟩
 
-  | .LocalVariable name ty initializer =>
-      -- If the substitution map has an entry for this variable, it was
+  | .LocalVariable params initializer =>
+      -- If the substitution map has an entry for any of these variables, it was
       -- assigned to the right and we need to lift this declaration so it
       -- appears before the snapshot that references it.
-      let hasSubst := (← get).subst.lookup name |>.isSome
+      let subst := (← get).subst
+      let hasSubst := params.any fun p => subst.lookup p.name |>.isSome
       if hasSubst then
         match initializer with
         | some initExpr =>
             let seqInit ← transformExpr initExpr
-            prepend (⟨.LocalVariable name ty (some seqInit), expr.source, expr.md⟩)
+            prepend (⟨.LocalVariable params (some seqInit), expr.source, expr.md⟩)
         | none =>
-            prepend (⟨.LocalVariable name ty none, expr.source, expr.md⟩)
-        return ⟨.Identifier (← getSubst name), expr.source, expr.md⟩
+            prepend (⟨.LocalVariable params none, expr.source, expr.md⟩)
+        -- Return substitution for the first name
+        match params with
+        | p :: _ => return ⟨.Identifier (← getSubst p.name), expr.source, expr.md⟩
+        | [] => return expr
       else
         return expr
 
@@ -380,7 +384,7 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
       let seqStmts ← stmts.mapM transformStmt
       return [bare (.Block seqStmts.flatten metadata)]
 
-  | .LocalVariable name ty initializer =>
+  | .LocalVariable params initializer =>
       match _ : initializer with
       | some initExprMd =>
          -- If the initializer is a direct imperative StaticCall, don't lift it —
@@ -394,18 +398,18 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
                 let seqInit ← transformExpr initExprMd
                 let prepends ← takePrepends
                 modify fun s => { s with subst := [] }
-                return prepends ++ [⟨.LocalVariable name ty (some seqInit), source, md⟩]
+                return prepends ++ [⟨.LocalVariable params (some seqInit), source, md⟩]
               else
                 -- Pass through as-is; translateStmt will emit init + call
                 let seqArgs ← args.mapM transformExpr
                 let argPrepends ← takePrepends
                 modify fun s => { s with subst := [] }
-                return argPrepends ++ [⟨.LocalVariable name ty (some ⟨.StaticCall callee seqArgs, initExprMd.source, initExprMd.md⟩), source, md⟩]
+                return argPrepends ++ [⟨.LocalVariable params (some ⟨.StaticCall callee seqArgs, initExprMd.source, initExprMd.md⟩), source, md⟩]
           | _ =>
               let seqInit ← transformExpr initExprMd
               let prepends ← takePrepends
               modify fun s => { s with subst := [] }
-              return prepends ++ [⟨.LocalVariable name ty (some seqInit), source, md⟩]
+              return prepends ++ [⟨.LocalVariable params (some seqInit), source, md⟩]
       | none =>
           return [stmt]
 
@@ -473,6 +477,10 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
       modify fun s => { s with subst := [] }
       return prepends ++ [⟨.Return (some seqRet), source, md⟩]
 
+  | .PrimitiveOp name args =>
+      let seqArgs ← args.mapM transformExpr
+      let prepends ← takePrepends
+      return prepends ++ [⟨.PrimitiveOp name seqArgs, source, md⟩]
   | _ =>
       return [stmt]
   termination_by (sizeOf stmt, 0)
diff --git a/Strata/Languages/Laurel/MapStmtExpr.lean b/Strata/Languages/Laurel/MapStmtExpr.lean
index 3ca5fd7beb..3a354e6845 100644
--- a/Strata/Languages/Laurel/MapStmtExpr.lean
+++ b/Strata/Languages/Laurel/MapStmtExpr.lean
@@ -39,8 +39,8 @@ def mapStmtExprM [Monad m] (f : StmtExprMd → m StmtExprMd) (expr : StmtExprMd)
       (← el.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e), source, md⟩
   | .Block stmts label =>
     pure ⟨.Block (← stmts.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e) label, source, md⟩
-  | .LocalVariable name ty init =>
-    pure ⟨.LocalVariable name ty (← init.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e), source, md⟩
+  | .LocalVariable params init =>
+    pure ⟨.LocalVariable params (← init.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e), source, md⟩
   | .While cond invs dec body =>
     pure ⟨.While (← mapStmtExprM f cond)
       (← invs.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e)
@@ -115,13 +115,14 @@ def mapProcedureBodiesM [Monad m] (f : StmtExprMd → m StmtExprMd) (proc : Proc
   | .External => return proc
 
 /-- Apply a monadic transformation to all `StmtExprMd` nodes in a procedure
-    (preconditions, decreases, body, and invokeOn). -/
+    (preconditions, decreases, body, invokeOn, and axioms). -/
 def mapProcedureM [Monad m] (f : StmtExprMd → m StmtExprMd) (proc : Procedure) : m Procedure := do
   let proc ← mapProcedureBodiesM f proc
   return { proc with
     preconditions := ← proc.preconditions.mapM f
     decreases := ← proc.decreases.mapM f
-    invokeOn := ← proc.invokeOn.mapM f }
+    invokeOn := ← proc.invokeOn.mapM f
+    axioms := ← proc.axioms.mapM f }
 
 /-- Apply a monadic transformation to procedure bodies in a program.
     Does **not** traverse preconditions, decreases, or invokeOn — use
diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean
index 78dfade9cd..f1d582e098 100644
--- a/Strata/Languages/Laurel/ModifiesClauses.lean
+++ b/Strata/Languages/Laurel/ModifiesClauses.lean
@@ -136,6 +136,12 @@ indicating it mutates the heap.
 def hasHeapOut (proc : Procedure) : Bool :=
   proc.outputs.any (fun p => p.name.text == "$heap")
 
+/--
+Check whether a modifies list contains a wildcard (`All`), meaning anything can be modified.
+-/
+def hasWildcardModifies (modifiesExprs : List StmtExprMd) : Bool :=
+  modifiesExprs.any (fun e => match e.val with | .All => true | _ => false)
+
 /--
 Transform a single procedure: if it has modifies clauses, generate the frame
 condition and conjoin it with the postcondition, then clear the modifies list.
@@ -143,13 +149,18 @@ condition and conjoin it with the postcondition, then clear the modifies list.
 If the procedure has a `$heap` but no modifies clause, adds a postcondition
 that all allocated objects are preserved between heaps:
   `forall $obj: Composite, $fld: Field => $obj < $heap_in.nextReference ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld)`
+
+If the modifies clause uses a wildcard (`*`), the frame condition is skipped
+entirely — the procedure may modify anything.
 -/
 def transformModifiesClauses (model: SemanticModel)
     (proc : Procedure) : Except (Array DiagnosticModel) Procedure :=
   match proc.body with
   | .External => .ok proc
   | .Opaque postconds impl modifiesExprs =>
-      if hasHeapOut proc then
+      if hasWildcardModifies modifiesExprs then
+        .ok { proc with body := .Opaque postconds impl [] }
+      else if hasHeapOut proc then
         let heapInName : Identifier := "$heap_in"
         let heapName : Identifier := "$heap"
         let frameCondition := buildModifiesEnsures proc model modifiesExprs heapInName heapName
@@ -172,10 +183,13 @@ def filterBodyNonCompositeModifies (model : SemanticModel) (body : Body)
   match body with
   | .Opaque posts impl mods =>
     let (kept, diags) := mods.foldl (fun (acc, ds) e =>
-      let ty := (computeExprType model e).val
-      if isHeapRelevantType ty then (acc ++ [e], ds)
-      else
-        (acc, ds ++ [(fileRangeToCoreMd e.source e.md).toDiagnostic s!"modifies clause entry has non-composite type '{formatHighTypeVal ty}' and will be ignored"])
+      match e.val with
+      | .All => (acc ++ [e], ds)
+      | _ =>
+        let ty := (computeExprType model e).val
+        if isHeapRelevantType ty then (acc ++ [e], ds)
+        else
+          (acc, ds ++ [(fileRangeToCoreMd e.source e.md).toDiagnostic s!"modifies clause entry has non-composite type '{formatHighTypeVal ty}' and will be ignored"])
     ) ([], [])
     (.Opaque posts impl kept, diags)
   | other => (other, [])
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 4b0b1217e9..ab1e9d9e43 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -101,8 +101,10 @@ def ResolvedNode.getType (node: ResolvedNode): HighTypeMd := match node with
  | .constant c => c.type
  | .quantifierVar _ type => type
  | .unresolved =>
-    -- The Python through Laurel pipeline does not resolve yet
-    ⟨ .UserDefined "dummyName", none, default ⟩
+   -- Expected when a reference failed to resolve (a diagnostic was already emitted
+   -- by resolveRef or defineNameCheckDup). Returning Unknown propagates the error
+   -- gracefully through type translation.
+   ⟨ .Unknown, none, default ⟩
  | _ => dbg_trace s!"SOUND BUG: getType called on {repr node}"; ⟨ HighType.Unknown, none, default ⟩
 
 /-! ## Resolution result -/
@@ -115,8 +117,15 @@ structure SemanticModel where
 
 def SemanticModel.get (model: SemanticModel) (iden: Identifier): ResolvedNode :=
   match iden.uniqueId with
-  | some key => (model.refToDef.get? key).getD default
-  | none => default
+  | some key =>
+    match model.refToDef.get? key with
+    | some node => node
+    | none =>
+      -- An ID was assigned during Phase 1 but the reference was never registered in
+      -- Phase 2 (buildRefToDef). This is a bug in the resolution pass itself.
+      dbg_trace s!"SOUND BUG: identifier '{iden.text}' (id={key}) has a uniqueId but is missing from refToDef"
+      .unresolved
+  | none => .unresolved
 
 def SemanticModel.isFunction (model: SemanticModel) (id: Identifier): Bool :=
   match model.get id with
@@ -307,11 +316,13 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do
     withScope do
       let stmts' ← stmts.mapM resolveStmtExpr
       pure (.Block stmts' label)
-  | .LocalVariable name ty init =>
-    let ty' ← resolveHighType ty
+  | .LocalVariable params init =>
     let init' ← init.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val)
-    let name' ← defineNameCheckDup name (.var name ty')
-    pure (.LocalVariable name' ty' init')
+    let params' ← params.mapM fun p => do
+      let ty' ← resolveHighType p.type
+      let name' ← defineNameCheckDup p.name (.var p.name ty')
+      pure { name := name', type := ty' }
+    pure (.LocalVariable params' init')
   | .While cond invs dec body =>
     let cond' ← resolveStmtExpr cond
     let invs' ← invs.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val)
@@ -449,10 +460,12 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
     let dec' ← proc.decreases.mapM resolveStmtExpr
     let body' ← resolveBody proc.body
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
+    let axioms' ← proc.axioms.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
              isFunctional := proc.isFunctional,
              preconditions := pres', decreases := dec',
              invokeOn := invokeOn',
+             axioms := axioms',
              body := body' }
 
 /-- Resolve a field: define its name under the qualified key (OwnerType.fieldName) and resolve its type. -/
@@ -473,12 +486,18 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     let pres' ← proc.preconditions.mapM resolveStmtExpr
     let dec' ← proc.decreases.mapM resolveStmtExpr
     let body' ← resolveBody proc.body
+    if !proc.isFunctional && body'.isTransparent then
+      let diag := proc.name.md.toDiagnostic
+        s!"transparent statement bodies are not supported. Add 'opaque' to make the procedure opaque"
+      modify fun s => { s with errors := s.errors.push diag }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     modify fun s => { s with instanceTypeName := savedInstType }
+    let axioms' ← proc.axioms.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
              isFunctional := proc.isFunctional,
              preconditions := pres', decreases := dec',
              invokeOn := invokeOn',
+             axioms := axioms',
              body := body' }
 
 /-- Resolve a type definition. -/
@@ -579,9 +598,8 @@ private def collectStmtExpr (map : Std.HashMap Nat ResolvedNode) (expr : StmtExp
     | some e => collectStmtExpr map e
     | none => map
   | .Block stmts _ => stmts.foldl collectStmtExpr map
-  | .LocalVariable name ty init =>
-    let map := register map name (.var name ty)
-    let map := collectHighType map ty
+  | .LocalVariable params init =>
+    let map := params.foldl (fun m p => register (collectHighType m p.type) p.name (.var p.name p.type)) map
     match init with
     | some i => collectStmtExpr map i
     | none => map
@@ -744,8 +762,18 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do
 
 /-- Run the full resolution pass on a Laurel program. -/
 def resolve (program : Program) (existingModel: Option SemanticModel := none) : ResolutionResult :=
+
   -- Phase 1: pre-register all top-level names, then assign IDs and resolve references
   let phase1 : ResolveM Program := do
+
+    for td in program.types do
+      if let .Composite ct := td then
+        for proc in ct.instanceProcedures do
+          let diag := proc.name.md.toDiagnostic
+            s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' is not yet supported"
+            DiagnosticType.NotYetImplemented
+          modify fun s => { s with errors := s.errors.push diag }
+
     preRegisterTopLevel program
     let types' ← program.types.mapM resolveTypeDefinition
     let constants' ← program.constants.mapM resolveConstant
diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean
index 30c3602393..5d972263fe 100644
--- a/Strata/Languages/Laurel/TypeHierarchy.lean
+++ b/Strata/Languages/Laurel/TypeHierarchy.lean
@@ -143,7 +143,7 @@ def validateDiamondFieldAccessesForStmtExpr (model : SemanticModel)
     match e with
     | some eb => errs ++ validateDiamondFieldAccessesForStmtExpr model eb
     | none => errs
-  | .LocalVariable _ _ (some init) =>
+  | .LocalVariable _ (some init) =>
     validateDiamondFieldAccessesForStmtExpr model init
   | .While c invs _ b =>
     let errs := validateDiamondFieldAccessesForStmtExpr model c ++
@@ -214,7 +214,7 @@ def lowerNew (name : Identifier) (source : Option FileRange) (md : Imperative.Me
   let heapVar : Identifier := "$heap"
   let freshVar ← freshVarName
   let getCounter := mkMd (.StaticCall "Heap..nextReference!" [mkMd (.Identifier heapVar)])
-  let saveCounter := mkMd (.LocalVariable freshVar ⟨.TInt, none, #[]⟩ (some getCounter))
+  let saveCounter := mkMd (.LocalVariable [{ name := freshVar, type := ⟨.TInt, none, #[]⟩ }] (some getCounter))
   let newHeap := mkMd (.StaticCall "increment" [mkMd (.Identifier heapVar)])
   let updateHeap := mkMd (.Assign [mkMd (.Identifier heapVar)] newHeap)
   let compositeResult := mkMd (.StaticCall "MkComposite" [mkMd (.Identifier freshVar), mkMd (.StaticCall (name.text ++ "_TypeTag") [])])
diff --git a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean
index 9041269200..ff8d50a785 100644
--- a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean
+++ b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean
@@ -330,6 +330,7 @@ function List_len (l : ListAny) : int
 
 procedure List_len_pos(l : ListAny)
   invokeOn List_len(l)
+  opaque
   ensures List_len(l) >= 0;
 
 function List_contains (l : ListAny, x: Any) : bool
@@ -368,6 +369,7 @@ function List_take (l : ListAny, i: int) : ListAny
 
 procedure List_take_len(l : ListAny, i: int)
   invokeOn List_len(List_take(l,i))
+  opaque
   ensures i >= 0 && i <= List_len(l) ==> List_len(List_take(l,i)) == i;
 
 function List_drop (l : ListAny, i: int) : ListAny
@@ -380,6 +382,7 @@ function List_drop (l : ListAny, i: int) : ListAny
 
 procedure List_drop_len(l : ListAny, i: int)
   invokeOn List_len(List_drop(l,i))
+  opaque
   ensures i >= 0 && i <= List_len(l) ==> List_len(List_drop(l,i)) == List_len(l) - i;
 
 function int_max (i1: int, i2: int) : int
@@ -1013,10 +1016,12 @@ function datetime_strptime(dtstring: Any, format: Any) : Any;
 
 procedure datetime_tostring_cancel(dt: Any)
   invokeOn datetime_strptime(to_string_any(dt), from_str ("%Y-%m-%d"))
+  opaque
   ensures datetime_strptime(to_string_any(dt), from_str ("%Y-%m-%d")) == dt;
 
 procedure datetime_date(d: Any) returns (ret: Any, error: Error)
   requires Any..isfrom_datetime(d) summary "(Origin_datetime_date_Requires)d_type"
+  opaque
   ensures Any..isfrom_datetime(ret) && Any..as_datetime!(ret) <= Any..as_datetime!(d) summary "ret_type"
 {
   var timedt: int;
@@ -1033,6 +1038,7 @@ procedure datetime_date(d: Any) returns (ret: Any, error: Error)
 };
 
 procedure datetime_now(tz: Any) returns (ret: Any)
+  opaque
   ensures Any..isfrom_datetime(ret) summary "ret_type"
 {
   var d: int;
@@ -1044,6 +1050,7 @@ procedure timedelta_func(days: Any, hours: Any) returns (delta : Any, maybe_exce
   requires Any..isfrom_None(hours) || Any..isfrom_int(hours) summary "(Origin_timedelta_Requires)hours_type"
   requires Any..isfrom_int(days) ==> Any..as_int!(days)>=0 summary "(Origin_timedelta_Requires)days_pos"
   requires Any..isfrom_int(hours) ==> Any..as_int!(hours)>=0 summary "(Origin_timedelta_Requires)hours_pos"
+  opaque
   ensures Any..isfrom_int(delta) && Any..as_int!(delta)>=0 summary "ret_pos"
 {
   var days_i : int := 0;
@@ -1065,6 +1072,7 @@ procedure test_helper_procedure(req_name : Any, opt_name : Any) returns (ret: An
   requires req_name == from_str("foo") summary "(Origin_test_helper_procedure_Requires)req_name_is_foo"
   requires (Any..isfrom_None(opt_name)) || (Any..isfrom_str(opt_name)) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_str"
   requires (opt_name == from_None()) || (opt_name == from_str("bar")) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar"
+  opaque
   ensures (Error..isNoError(maybe_except)) summary "ensures_maybe_except_none"
 {
   assert req_name == from_str("foo") summary "assert_name_is_foo";
diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index 7cb878359f..90295eb65f 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -178,6 +178,9 @@ def mkCoreType (s: String): HighTypeMd :=
 def mkStmtExprMd (expr : StmtExpr) : StmtExprMd :=
   { val := expr, source := none }
 
+/-- A wildcard modifies list, meaning the procedure may modify anything. -/
+def wildcardModifies : List StmtExprMd := [mkStmtExprMd .All]
+
 /-- Create a StmtExprMd with source location metadata.
     NOTE: stores location in `md` (legacy); a follow-up should migrate to `source`. -/
 def mkStmtExprMdWithLoc (expr : StmtExpr) (md : Imperative.MetaData Core.Expression) : StmtExprMd :=
@@ -1153,7 +1156,7 @@ partial def translateAssign  (ctx : TranslationContext)
           | some _ =>
             throw (.userPythonError lhs.ann s!"'{annType}' is not a type")
           | _ => pure (AnyTy, "Any")
-        let initStmt := mkStmtExprMd (StmtExpr.LocalVariable n.val varTy (mkStmtExprMd .Hole))
+        let initStmt := mkStmtExprMd (StmtExpr.LocalVariable [{ name := n.val, type := varTy }] (mkStmtExprMd .Hole))
         let newctx := {ctx with variableTypes:=(n.val, trackType)::ctx.variableTypes}
         return (newctx, [initStmt] ++ exceptHavoc, true)
     | _ => return (ctx, [mkStmtExprMd .Hole] ++ exceptHavoc, false)
@@ -1174,7 +1177,7 @@ partial def translateAssign  (ctx : TranslationContext)
                 let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] newExpr) md
                 [assignStmt, initStmt]
               else
-                let newStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable n.val varType (some newExpr)) md
+                let newStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable [{ name := n.val, type := varType }] (some newExpr)) md
                 [newStmt, initStmt]
             else if withException ctx fnname.text then
               [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr, maybeExceptVar] rhs_trans) md]
@@ -1185,7 +1188,7 @@ partial def translateAssign  (ctx : TranslationContext)
               [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md]
             else
               let varType := mkHighTypeMd (.UserDefined className)
-              let newStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable n.val varType (some rhs_trans)) md
+              let newStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable [{ name := n.val, type := varType }] (some rhs_trans)) md
               [newStmt]
         | _ => [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md]
         newctx := match rhs_trans.val with
@@ -1207,7 +1210,7 @@ partial def translateAssign  (ctx : TranslationContext)
                -- If the annotation isn't a recognized type, prefer the
                -- inferred type from the RHS (e.g., overload dispatch).
                if isKnownType ctx annStr then annStr else inferType
-          let initStmt := mkStmtExprMd (StmtExpr.LocalVariable n.val AnyTy AnyNone)
+          let initStmt := mkStmtExprMd (StmtExpr.LocalVariable [{ name := n.val, type := AnyTy }] AnyNone)
           newctx := {ctx with variableTypes:=(n.val, type)::ctx.variableTypes}
           return (newctx, initStmt :: assignStmts, true)
     | .Subscript _ _ _ _ =>
@@ -1311,7 +1314,7 @@ def createVarDeclStmtsAndCtx (ctx : TranslationContext) (newDecls : List (String
       then acc else acc ++ [(n, ty)]) []
   let hoistedDecls : List StmtExprMd ←  newDecls.mapM fun (name, tyStr) => do
       let ty ← translateType ctx tyStr
-      pure $ mkStmtExprMd (StmtExpr.LocalVariable (name : String) ty (some (mkStmtExprMd .Hole)))
+      pure $ mkStmtExprMd (StmtExpr.LocalVariable [{ name := (name : String), type := ty }] (some (mkStmtExprMd .Hole)))
   let hoistedCtx := { ctx with variableTypes := ctx.variableTypes ++
       (newDecls.map fun (n, ty) =>
         if isCompositeType ctx ty then (n, ty) else (n, PyLauType.Any)) }
@@ -1405,7 +1408,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
           return (ctx, [])
       let newctx := {ctx with variableTypes:=(varName, varType)::ctx.variableTypes}
       let varType ← translateType ctx varType
-      let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName varType AnyNone)
+      let declStmt := mkStmtExprMd (StmtExpr.LocalVariable [{ name := varName, type := varType }] AnyNone)
       return (newctx, [declStmt])
 
   -- If statement
@@ -1462,7 +1465,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
       | .Hole =>
         let freshVar := s!"assert_cond_{test.toAst.ann.start.byteIdx}"
         let varType := mkHighTypeMd .TBool
-        let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr))
+        let varDecl := mkStmtExprMd (StmtExpr.LocalVariable [{ name := freshVar, type := varType }] (some condExpr))
         let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar)
         ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] })
       | _ => ([], condExpr, ctx)
@@ -1565,7 +1568,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
         let mgrExpr ← translateExpr currentCtx ctxExpr
         let mgrTy ← inferExprType currentCtx ctxExpr
         let mgrLauTy ← translateType currentCtx mgrTy
-        let mgrDecl := mkStmtExprMd (StmtExpr.LocalVariable mgrName mgrLauTy (some mgrExpr))
+        let mgrDecl := mkStmtExprMd (StmtExpr.LocalVariable [{ name := mgrName, type := mgrLauTy }] (some mgrExpr))
         let mgrRef := mkStmtExprMd (StmtExpr.Identifier mgrName)
         currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(mgrName, mgrTy)]}
         let enterCall := mkInstanceMethodCall mgrTy "__enter__" mgrRef [] md
@@ -1579,7 +1582,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
             setupStmts := setupStmts ++ [mgrDecl, assignStmt]
           else
             -- New variable — declare outside the block so it's visible after
-            let varDecl := mkStmtExprMd (StmtExpr.LocalVariable varName AnyTy (some enterCall))
+            let varDecl := mkStmtExprMd (StmtExpr.LocalVariable [{ name := varName, type := AnyTy }] (some enterCall))
             currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(varName, PyLauType.Any)]}
             setupStmts := setupStmts ++ [mgrDecl, varDecl]
         | none =>
@@ -1665,7 +1668,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
       | _ => (target, [], [])
     let slices ← slices.mapM (translateExpr ctx)
     let tempVarDecls := (tempVars.zip slices).map λ (var, slice) =>
-              mkStmtExprMd (.LocalVariable { text := var, md := default } AnyTy slice)
+              mkStmtExprMd (.LocalVariable [{ name := { text := var, md := default }, type := AnyTy }] slice)
     let rhs : Python.expr SourceRange := .BinOp sr target op value
     let pyNormalAssign : Python.stmt SourceRange :=
           .Assign sr {val:= #[target], ann:= target.ann} rhs {val:= none, ann:= sr}
@@ -1687,7 +1690,7 @@ partial def translateStmtList (ctx : TranslationContext) (stmts : List (Python.s
 end
 
 def prependExceptHandlingHelper (l: List StmtExprMd) : List StmtExprMd :=
-  mkStmtExprMd (.LocalVariable "maybe_except" (mkCoreType "Error") (some NoError)) :: l
+  mkStmtExprMd (.LocalVariable [{ name := "maybe_except", type := mkCoreType "Error" }] (some NoError)) :: l
 
 partial def getNestedSubscripts (expr:  Python.expr SourceRange) : List ( Python.expr SourceRange) :=
   match expr with
@@ -1825,7 +1828,7 @@ def translateFunctionBody (ctx : TranslationContext) (inputTypes : List (String
     let (varDecls, ctx) ←  createVarDeclStmtsAndCtx ctx newDecls
     let (newctx, bodyStmts) ← translateStmtList ctx body
     let bodyStmts := prependExceptHandlingHelper (varDecls ++ bodyStmts)
-    let bodyStmts := (mkStmtExprMd (.LocalVariable "nullcall_ret" AnyTy (some AnyNone))) :: bodyStmts
+    let bodyStmts := (mkStmtExprMd (.LocalVariable [{ name := "nullcall_ret", type := AnyTy }] (some AnyNone))) :: bodyStmts
     return (mkStmtExprMd (StmtExpr.Block bodyStmts none), newctx)
 
 /-- Translate Python function to Laurel Procedure -/
@@ -1864,14 +1867,14 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun
     | .Block bodyStmts label => {bodyBlock with val:= .Block (noneReturn::bodyStmts) label}
     | _ => bodyBlock
 
-    -- Create procedure with transparent body (no contracts for now)
+    -- Create procedure
     let proc : Procedure := {
       name := { text := funcDecl.name, md := sourceRangeToMetaData ctx.filePath sourceRange }
       inputs := inputs
       outputs := outputs
       preconditions := typeConstraintPreconditions
       decreases := none
-      body := Body.Opaque typeConstraintPostcondition bodyBlock []
+      body := Body.Opaque typeConstraintPostcondition bodyBlock wildcardModifies
       isFunctional := false
     }
 
@@ -2000,7 +2003,7 @@ def translateMethod (ctx : TranslationContext) (className : String)
     let paramCopies := nonSelfParams.map fun p =>
       let origName := p.name.text
       let renamedName := "$in_" ++ origName
-      mkStmtExprMd (StmtExpr.LocalVariable origName p.type
+      mkStmtExprMd (StmtExpr.LocalVariable [{ name := origName, type := p.type }]
         (some (mkStmtExprMd (StmtExpr.Identifier renamedName))))
     let bodyStmts := paramCopies ++ bodyStmts
     let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts none)
@@ -2013,7 +2016,7 @@ def translateMethod (ctx : TranslationContext) (className : String)
       preconditions := [mkStmtExprMd (StmtExpr.LiteralBool true)]
       isFunctional := false
       decreases := none
-      body := .Transparent bodyBlock
+      body := .Opaque [] (some bodyBlock) wildcardModifies
     }
   | _ => throw (.internalError "Expected FunctionDef for method")
 
@@ -2063,7 +2066,7 @@ def mkDefaultInitDecl (className : String) : PythonFunctionDecl × Procedure :=
     preconditions := [mkStmtExprMd (StmtExpr.LiteralBool true)]
     isFunctional := false
     decreases := none
-    body := .Opaque [] .none []
+    body := .Opaque [] .none wildcardModifies
   }
   (decl, proc)
 
@@ -2121,7 +2124,7 @@ def translateClass (ctx : TranslationContext) (classStmt : Python.stmt SourceRan
       if let .FunctionDef .. := stmt then
         let proc ← translateMethod ctx className stmt
         if inHierarchy then
-          instanceProcedures := instanceProcedures.push { proc with body := .Opaque [] .none [] }
+          instanceProcedures := instanceProcedures.push { proc with body := .Opaque [] .none wildcardModifies }
         else
           instanceProcedures := instanceProcedures.push proc
     -- Add synthesized default __init__ if needed
@@ -2185,7 +2188,7 @@ structure PreludeInfo where
   maybeExceptionFunctions : List String := []
   /-- Procedure names (non-function callables) -/
   procedureNames : List String := []
-  /-- Names of procedures with transparent bodies (can be inlined). -/
+  /-- Names of procedures that should generate calls (have transparent bodies or preconditions). -/
   inlinableProcedures : Std.HashSet String := {}
   /-- Maps Python-visible names to their structured symbol info.
       Includes both canonical Laurel names and unprefixed aliases. -/
@@ -2271,7 +2274,10 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
       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
+      match p.body with
+      | .Transparent _ => s.insert p.name.text
+      | .Opaque _ (some _) _ => s.insert p.name.text
+      | _ => if !p.preconditions.isEmpty then s.insert p.name.text else s
 
 /-- Merge two `PreludeInfo` values by concatenating each field. -/
 def PreludeInfo.merge (a b : PreludeInfo) : PreludeInfo where
@@ -2418,7 +2424,7 @@ def pythonToLaurel' (info : PreludeInfo)
     outputs := [],
     preconditions := [],
     decreases := none,
-    body := .Transparent bodyBlock
+    body := .Opaque [] (some bodyBlock) wildcardModifies
     isFunctional := false
   }
 
@@ -2434,7 +2440,7 @@ def pythonToLaurel' (info : PreludeInfo)
         outputs := [{ name := "result", type := mkHighTypeMd .TString }]
         preconditions := []
         decreases := none
-        body := .Opaque [] none []
+        body := .Opaque [] none wildcardModifies
         isFunctional := false }
     procedures := procedures.push
       { name := { text := compositeToStringAnyName ct.name.text, md := .empty }
@@ -2442,7 +2448,7 @@ def pythonToLaurel' (info : PreludeInfo)
         outputs := [{ name := "result", type := AnyTy }]
         preconditions := []
         decreases := none
-        body := .Opaque [] none []
+        body := .Opaque [] none wildcardModifies
         isFunctional := false }
 
   let program : Laurel.Program := {
diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean
index 78c6e28ff4..bf3556d3d7 100644
--- a/Strata/Languages/Python/Specs/ToLaurel.lean
+++ b/Strata/Languages/Python/Specs/ToLaurel.lean
@@ -557,7 +557,7 @@ def buildSpecBody (preconditions : Array Assertion)
       source := none,
       md := fileMd
   }
-  return .Transparent body
+  return .Opaque [] (some body) [{ val := .All, source := none }]
 
 /-! ## Declaration Translation -/
 
@@ -617,7 +617,7 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl)
           if a.default.isNone then some a.name else none)
       pure (anyInputs, anyOutputs, body)
     else
-      pure (inputs, outputs, Body.Opaque [] none [])
+      pure (inputs, outputs, Body.Opaque [] none [{ val := .All, source := none }])
   let md ← mkMdWithFileRange func.loc
   return {
     name := { text := procName, md := md }
diff --git a/Strata/SimpleAPI.lean b/Strata/SimpleAPI.lean
index 9364e2b927..bcbf6ce455 100644
--- a/Strata/SimpleAPI.lean
+++ b/Strata/SimpleAPI.lean
@@ -349,7 +349,7 @@ def Laurel.verifyProgram
     (program : Laurel.Program)
     (options : Core.VerifyOptions := .default)
     : IO (Option Core.VCResults × List DiagnosticModel) :=
-  Strata.Laurel.verifyToVcResults program options
+  Strata.Laurel.verifyToVcResults program options {}
 
 /--
 Analyze a Laurel program and return structured diagnostic models
diff --git a/StrataTest/Backends/CBMC/contracts/test_contract.lr.st b/StrataTest/Backends/CBMC/contracts/test_contract.lr.st
index c0023ba105..20505c2cbc 100644
--- a/StrataTest/Backends/CBMC/contracts/test_contract.lr.st
+++ b/StrataTest/Backends/CBMC/contracts/test_contract.lr.st
@@ -1,11 +1,14 @@
 procedure add(x: int, y: int) returns (r: int)
   requires x >= 0
+  opaque
   ensures r >= x
 {
   r := x + y;
 };
 
-procedure main() {
+procedure main()
+  opaque
+{
   var a: int := 42;
   assert a > 0;
 };
diff --git a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
index ab077ee42c..c5ffbd5f02 100644
--- a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
+++ b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
@@ -58,24 +58,31 @@ private def roundtrip (input : String) : IO String := do
 
 /--
 info: procedure foo()
+  opaque
 { assert true; assert false };
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure foo() { assert true; assert false };")
+#eval do IO.println (← roundtrip r"procedure foo()
+  opaque
+{ assert true; assert false };")
 
 /--
 info: procedure add(x: int, y: int): int
+  opaque
 { x + y };
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int { x + y };")
+#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int
+  opaque
+{ x + y };")
 
 /--
 info: function aFunction(x: int): int
 { x };
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"function aFunction(x: int): int { x };")
+#eval do IO.println (← roundtrip r"function aFunction(x: int): int
+{ x };")
 
 /--
 info: composite Point { var x: int var y: int }
@@ -90,14 +97,18 @@ composite Point {
 
 /--
 info: procedure test(x: int): int
+  opaque
 { if x > 0 then x else 0 - x };
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure test(x: int): int { if x > 0 then x else 0 - x };")
+#eval do IO.println (← roundtrip r"procedure test(x: int): int
+  opaque
+{ if x > 0 then x else 0 - x };")
 
 /--
 info: procedure divide(x: int, y: int): int
   requires y != 0
+  opaque
   ensures result >= 0
 { x / y };
 -/
@@ -105,17 +116,21 @@ info: procedure divide(x: int, y: int): int
 #eval do IO.println (← roundtrip r"
 procedure divide(x: int, y: int): int
   requires y != 0
+  opaque
   ensures result >= 0
 { x / y };
 ")
 
 /--
 info: procedure test()
+  opaque
 { assert forall(x: int) => x == x; assert exists(y: int) => y > 0 };
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
-procedure test() {
+procedure test()
+  opaque
+{
     assert forall(x: int) => x == x;
     assert exists(y: int) => y > 0
 };
@@ -125,6 +140,7 @@ procedure test() {
 info: composite Point { var x: int var y: int }
 
 procedure test(): int
+  opaque
 { var p: Point := new Point; p#x := 5; p#x };
 -/
 #guard_msgs in
@@ -133,7 +149,9 @@ composite Point {
   var x: int
   var y: int
 }
-procedure test(): int {
+procedure test(): int
+  opaque
+{
     var p: Point := new Point;
     p#x := 5;
     p#x
@@ -158,25 +176,31 @@ info: composite Animal { }
 composite Dog extends Animal { }
 
 procedure test(a: Animal): bool
+  opaque
 { a is Dog };
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
 composite Animal {}
 composite Dog extends Animal {}
-procedure test(a: Animal): bool { a is Dog };
+procedure test(a: Animal): bool
+  opaque
+{ a is Dog };
 ")
 
 -- Additional coverage: while loops
 
 /--
 info: procedure test()
+  opaque
 { var x: int := 0; while(x < 10)
   invariant x >= 0 { x := x + 1 } };
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
-procedure test() {
+procedure test()
+  opaque
+{
     var x: int := 0;
     while(x < 10)
       invariant x >= 0
@@ -198,6 +222,7 @@ info: constrained Positive = v: int where v > 0 witness 1
 info: composite Container { var value: int }
 
 procedure modify(c: Container)
+  opaque
   ensures true
   modifies c
 { c#value := c#value + 1; true };
@@ -206,6 +231,7 @@ procedure modify(c: Container)
 #eval do IO.println (← roundtrip r"
 composite Container { var value: int }
 procedure modify(c: Container)
+  opaque
   ensures true
   modifies c
 { c#value := c#value + 1; true };
@@ -215,9 +241,12 @@ procedure modify(c: Container)
 
 /--
 info: procedure test(): int
+  opaque
 { <??> };
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure test(): int { <??> };")
+#eval do IO.println (← roundtrip r"procedure test(): int
+  opaque
+{ <??> };")
 
 end Strata.Laurel
diff --git a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
index a809805989..53d3d97d42 100644
--- a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
+++ b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
@@ -23,7 +23,9 @@ namespace Strata.Laurel
 
 def testProgram : String := r"
 constrained nat = x: int where x >= 0 witness 0
-procedure test(n: nat) returns (r: nat) {
+procedure test(n: nat) returns (r: nat)
+  opaque
+{
   assert r >= 0;
   var y: nat := n;
   return y
@@ -48,9 +50,11 @@ info: function nat$constraint(x: int): bool
 procedure test(n: int)
   returns (r: int)
   requires nat$constraint(n)
+  opaque
   ensures nat$constraint(r)
 { assert r >= 0; var y: int := n; assert nat$constraint(y); return y };
 procedure $witness_nat()
+  opaque
 { var $witness: int := 0; assert nat$constraint($witness) };
 -/
 #guard_msgs in
@@ -62,7 +66,9 @@ procedure $witness_nat()
 -- Scope management: constrained variable in if-branch must not leak into sibling block
 def scopeProgram : String := r"
 constrained pos = v: int where v > 0 witness 1
-procedure test(b: bool) {
+procedure test(b: bool)
+  opaque
+{
   if b then {
     var x: pos := 1
   };
@@ -77,8 +83,10 @@ procedure test(b: bool) {
 info: function pos$constraint(v: int): bool
 { v > 0 };
 procedure test(b: bool)
+  opaque
 { if b then { var x: int := 1; assert pos$constraint(x) }; { var x: int := -5; x := -10 } };
 procedure $witness_pos()
+  opaque
 { var $witness: int := 1; assert pos$constraint($witness) };
 -/
 #guard_msgs in
@@ -91,7 +99,9 @@ procedure $witness_pos()
 -- The variable has no known value, only the type constraint is assumed.
 def uninitProgram : String := r"
 constrained posint = x: int where x > 0 witness 1
-procedure f() {
+procedure f()
+  opaque
+{
   var x: posint;
   assert x == 1
 };
@@ -101,8 +111,10 @@ procedure f() {
 info: function posint$constraint(x: int): bool
 { x > 0 };
 procedure f()
+  opaque
 { var x: int; assume posint$constraint(x); assert x == 1 };
 procedure $witness_posint()
+  opaque
 { var $witness: int := 1; assert posint$constraint($witness) };
 -/
 #guard_msgs in
diff --git a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
index de6cf5a807..8237b96f98 100644
--- a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
+++ b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
@@ -19,7 +19,9 @@ generates verification conditions for these preconditions.
 -/
 
 def e2eProgram := r"
-procedure safeDivision() {
+procedure safeDivision()
+  opaque
+{
   var x: int := 10;
   var y: int := 2;
   var z: int := x / y;
@@ -27,7 +29,9 @@ procedure safeDivision() {
 };
 
 // Error ranges are too wide because Core does not use expression locations
-procedure unsafeDivision(x: int) {
+procedure unsafeDivision(x: int)
+  opaque
+{
   var z: int := 10 / x
 //^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
 // Error ranges are too wide because Core does not use expression locations
@@ -39,19 +43,23 @@ function pureDiv(x: int, y: int): int
   x / y
 };
 
-procedure callPureDivSafe() {
+procedure callPureDivSafe()
+  opaque
+{
   var z: int := pureDiv(10, 2);
   assert z == 5
 };
 
-procedure callPureDivUnsafe(x: int) {
+procedure callPureDivUnsafe(x: int)
+  opaque
+{
   var z: int := pureDiv(10, x)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
 // Error ranges are too wide because Core does not use expression locations
 };
 "
 
 #guard_msgs(drop info, error) in
-#eval testInputWithOffset "DivByZeroE2E" e2eProgram 22 processLaurelFile
+#eval testInputWithOffset "DivByZeroE2E" e2eProgram 20 processLaurelFile
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/DuplicateNameTests.lean b/StrataTest/Languages/Laurel/DuplicateNameTests.lean
index b948859925..08c5085dea 100644
--- a/StrataTest/Languages/Laurel/DuplicateNameTests.lean
+++ b/StrataTest/Languages/Laurel/DuplicateNameTests.lean
@@ -37,8 +37,8 @@ private def processResolution (input : Lean.Parser.InputContext) : IO (Array Dia
 /-! ## Duplicate static procedure names -/
 
 def dupProcedures := r"
-procedure foo() { };
-procedure foo() { };
+procedure foo() opaque { };
+procedure foo() opaque { };
 //        ^^^ error: Duplicate definition 'foo' is already defined in this scope
 "
 
@@ -72,30 +72,38 @@ composite Foo {
 /-! ## Duplicate parameter names in a procedure -/
 
 def dupParams := r"
-procedure foo(x: int, x: bool) { };
+procedure foo(x: int, x: bool)
 //                    ^ error: Duplicate definition 'x' is already defined in this scope
+  opaque
+{ };
 "
 
 #guard_msgs (error, drop all) in
-#eval testInputWithOffset "DupParams" dupParams 61 processResolution
+#eval testInputWithOffset "DupParams" dupParams 77 processResolution
 
 /-! ## Duplicate instance procedure names in a composite type -/
 
 def dupInstanceProcs := r"
 composite Foo {
-  procedure bar() { };
-  procedure bar() { };
+  procedure bar()
+//          ^^^ error: Instance procedure 'bar' on composite type 'Foo' is not yet supported
+    opaque
+  { };
+  procedure bar()
+//          ^^^ error: Instance procedure 'bar' on composite type 'Foo' is not yet supported
 //          ^^^ error: Duplicate definition 'bar' is already defined in this scope
+    opaque
+  { };
 }
 "
 
 #guard_msgs (error, drop all) in
-#eval testInputWithOffset "DupInstanceProcs" dupInstanceProcs 71 processResolution
+#eval testInputWithOffset "DupInstanceProcs" dupInstanceProcs 89 processResolution
 
 /-! ## Duplicate local variable names in the same block -/
 
 def dupLocals := r"
-procedure foo() {
+procedure foo() opaque {
   var x: int := 1;
   var x: int := 2
 //    ^ error: Duplicate definition 'x' is already defined in this scope
@@ -109,7 +117,7 @@ procedure foo() {
 
 def dupProcType := r"
 composite Foo { }
-procedure Foo() { };
+procedure Foo() opaque { };
 //        ^^^ error: Duplicate definition 'Foo' is already defined in this scope
 "
 
@@ -119,7 +127,7 @@ procedure Foo() { };
 /-! ## Shadowing quantifier variables in nested scopes is OK (no error expected) -/
 
 def shadowQuantifierVars := r"
-procedure test() {
+procedure test() opaque {
   assert forall(x: int) => forall(x: int) => x > 0
 };
 "
@@ -130,7 +138,7 @@ procedure test() {
 /-! ## Shadowing in nested blocks is OK (no error expected) -/
 
 def shadowingOk := r"
-procedure foo() {
+procedure foo() opaque {
   var x: int := 1;
   {
     var x: int := 2
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
index 291f669064..f7c0d45829 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
@@ -17,56 +17,76 @@ constrained nat = x: int where x >= 0 witness 0
 constrained posnat = x: nat where x != 0 witness 1
 
 // Input constraint becomes requires — body can rely on it
-procedure inputAssumed(n: nat) {
+procedure inputAssumed(n: nat)
+  opaque
+{
   assert n >= 0
 };
 
 // Output constraint — valid return passes
-procedure outputValid(): nat {
+procedure outputValid(): nat
+  opaque
+{
   return 3
 };
 
 // Output constraint — invalid return fails
-procedure outputInvalid(): nat {
-//                         ^^^ error: assertion does not hold
+procedure outputInvalid(): nat
+//                         ^^^ error: postcondition does not hold
+  opaque
+{
   return -1
 };
 
 // Return value of constrained type — caller gets ensures via call elimination
 procedure opaqueNat(): nat;
-procedure callerAssumes() returns (r: int) {
+procedure callerAssumes() returns (r: int)
+  opaque
+{
   var x: int := opaqueNat();
   assert x >= 0;
   return x
 };
 
 // Assignment to constrained-typed variable — valid
-procedure assignValid() {
+procedure assignValid()
+  opaque
+{
   var y: nat := 5
 };
 
 // Assignment to constrained-typed variable — invalid
-procedure assignInvalid() {
+procedure assignInvalid()
+  opaque
+{
   var y: nat := -1
 //^^^^^^^^^^^^^^^^ error: assertion does not hold
 };
 
 // Reassignment to constrained-typed variable — invalid
-procedure reassignInvalid() {
+procedure reassignInvalid()
+  opaque
+{
   var y: nat := 5;
   y := -1
 //^^^^^^^ error: assertion does not hold
 };
 
 // Argument to constrained-typed parameter — valid
-procedure takesNat(n: nat) returns (r: int) { return n };
-procedure argValid() returns (r: int) {
+procedure takesNat(n: nat) returns (r: int)
+  opaque
+{ return n };
+procedure argValid() returns (r: int)
+  opaque
+{
   var x: int := takesNat(3);
   return x
 };
 
 // Argument to constrained-typed parameter — invalid (requires violation)
-procedure argInvalid() returns (r: int) {
+procedure argInvalid() returns (r: int)
+  opaque
+{
   var x: int := takesNat(-1);
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
   return x
@@ -75,26 +95,34 @@ procedure argInvalid() returns (r: int) {
 // Nested constrained type — independent constraints require transitive collection
 constrained even = x: int where x % 2 == 0 witness 0
 constrained evenpos = x: even where x > 0 witness 2
-procedure nestedInput(x: evenpos) {
+procedure nestedInput(x: evenpos)
+  opaque
+{
   assert x > 0;
   assert x % 2 == 0
 };
 
 // Multiple constrained-typed parameters
-procedure multiParam(a: nat, b: nat) {
+procedure multiParam(a: nat, b: nat)
+  opaque
+{
   assert a >= 0;
   assert b >= 0
 };
 
 // Two calls to same procedure — no temp var collision
-procedure twoCalls() returns (r: int) {
+procedure twoCalls() returns (r: int)
+  opaque
+{
   var a: int := takesNat(1);
   var b: int := takesNat(2);
   return a + b
 };
 
 // Constrained type in expression position must be resolved
-procedure constrainedInExpr() {
+procedure constrainedInExpr()
+  opaque
+{
   var b: bool := forall(n: nat) => n + 1 > n;
   assert b
 };
@@ -104,42 +132,34 @@ constrained bad = x: int where x > 0 witness -1
 //                                           ^^ error: assertion does not hold
 
 // Uninitialized constrained variable — havoc + assume constraint
-procedure uninitNat() {
+procedure uninitNat()
+  opaque
+{
   var y: nat;
   assert y >= 0
 };
 
 // Uninitialized nested constrained variable — havoc + assume constraint
-procedure uninitPosnat() {
+procedure uninitPosnat()
+  opaque
+{
   var y: posnat;
   assert y != 0;
   assert y >= 0
 };
 
 // Uninitialized constrained variable — witness value is not provable
-procedure uninitNotWitness() {
+procedure uninitNotWitness()
+  opaque
+{
   var y: posnat;
   assert y == 1
 //^^^^^^^^^^^^^ error: assertion does not hold
 };
 
-// Function with valid constrained return — constraint not checked (not yet supported)
-function goodFunc(): nat { 3 };
-//       ^^^^^^^^ error: constrained return types on functions are not yet supported
-
-// Function with invalid constrained return — constraint not checked (not yet supported)
-function badFunc(): nat { -1 };
-//       ^^^^^^^ error: constrained return types on functions are not yet supported
-
-// Caller of constrained function — body is inlined, caller sees actual value
-procedure callerGood() {
-  var x: int := goodFunc();
-  assert x >= 0
-};
-
 // Quantifier constraint injection — forall
 // n + 1 > 0 is only provable with n >= 0 injected; false for all int
-procedure forallNat() {
+procedure forallNat() opaque {
   var b: bool := forall(n: nat) => n + 1 > 0;
   assert b
 };
@@ -147,14 +167,16 @@ procedure forallNat() {
 // Quantifier constraint injection — exists
 // n == -1 is satisfiable for int, but not when n >= 0 is required
 // n == 42 works because 42 >= 0
-procedure existsNat() {
+procedure existsNat() opaque {
   var b: bool := exists(n: nat) => n == 42;
   assert b
 };
 
 // Quantifier constraint injection — nested constrained type
 // n - 1 >= 0 is only provable with n > 0 injected
-procedure forallPosnat() {
+procedure forallPosnat()
+  opaque
+{
   var b: bool := forall(n: posnat) => n - 1 >= 0;
   assert b
 };
@@ -162,7 +184,9 @@ procedure forallPosnat() {
 // Capture avoidance — bound var y in constraint must not collide with parameter y
 // Without capture avoidance, requires becomes exists(y) => y > y (false), making body vacuously true
 constrained haslarger = x: int where (exists(y: int) => y > x) witness 0
-procedure captureTest(y: haslarger) {
+procedure captureTest(y: haslarger)
+  opaque
+{
   assert false
 //^^^^^^^^^^^^ error: assertion does not hold
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean
new file mode 100644
index 0000000000..342b6b144d
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean
@@ -0,0 +1,39 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+
+namespace Strata
+namespace Laurel
+
+def program := r"
+constrained nat = x: int where x >= 0 witness 0
+
+// Function with valid constrained return — constraint not checked (not yet supported)
+function goodFunc(): nat { 3 };
+//       ^^^^^^^^ error: constrained return types on functions are not yet supported
+
+// Function with invalid constrained return — constraint not checked (not yet supported)
+function badFunc(): nat { -1 };
+//       ^^^^^^^ error: constrained return types on functions are not yet supported
+
+// Caller of constrained function — body is inlined, caller sees actual value
+procedure callerGood()
+  opaque
+{
+  var x: int := goodFunc();
+  assert x >= 0
+};
+"
+
+#guard_msgs(drop info, error) in
+#eval testInputWithOffset "ConstrainedTypes" program 14 processLaurelFile
+
+end Laurel
+end Strata
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
index d8a2e9374f..b33450c145 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def operatorsProgram := r"
-procedure testArithmetic() {
+procedure testArithmetic()
+  opaque
+{
     var a: int := 10;
     var b: int := 3;
     var x: int := a - b;
@@ -26,7 +28,9 @@ procedure testArithmetic() {
     assert r == 2
 };
 
-procedure testLogical() {
+procedure testLogical()
+  opaque
+{
     var t: bool := true;
     var f: bool := false;
     var a: bool := t && f;
@@ -39,13 +43,17 @@ procedure testLogical() {
     assert f ==> t
 };
 
-procedure testUnary() {
+procedure testUnary()
+  opaque
+{
     var x: int := 5;
     var y: int := -x;
     assert y == 0 - 5
 };
 
-procedure testTruncatingDiv() {
+procedure testTruncatingDiv()
+  opaque
+{
     assert 7 /t 3 == 2;
     assert 7 %t 3 == 1;
     assert (0 - 7) /t 3 == 0 - 2;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
index 9e6b2d195e..b6b0b2e178 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def whileLoopsProgram := r"
-procedure countDown() {
+procedure countDown()
+  opaque
+{
     var i: int := 3;
     while(i > 0)
       invariant i >= 0
@@ -23,7 +25,9 @@ procedure countDown() {
     assert i == 0
 };
 
-procedure countUp() {
+procedure countUp()
+  opaque
+{
     var n: int := 5;
     var i: int := 0;
     while(i < n)
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
index f0f8ee554a..50ae574f18 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
@@ -13,23 +13,30 @@ namespace Strata
 namespace Laurel
 
 def quantifiersProgram := r"
-procedure testForall() {
+procedure testForall()
+  opaque
+{
     assert forall(x: int) => x + 0 == x
 };
 
-procedure testExists() {
+procedure testExists()
+  opaque
+{
     assert exists(x: int) => x == 42
 };
 
 procedure testQuantifierInContract(n: int)
   requires n > 0
+  opaque
   ensures forall(i: int) => i >= 0 ==> i < n ==> i < n + 1
 {
 };
 
 function P(x: int): int;
 function Q(): int;
-procedure triggers() {
+procedure triggers()
+  opaque
+{
   assert forall(i: int) { P(i) } => P(i) == i + 1;
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
   assert forall(i: int) => true;
@@ -42,7 +49,7 @@ procedure triggers() {
 
 "
 
-#guard_msgs(drop info, error) in
+#guard_msgs (drop info, error) in
 #eval testInputWithOffset "Quantifiers" quantifiersProgram 14 processLaurelFile
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
index 2559e95b2d..2e5b46a8ab 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
@@ -19,54 +19,73 @@ function mustNotCallFunc(x: int): int
 
 procedure mustNotCallProc(): int
   requires false
+  opaque
 {
   return 0
 };
 
 // Pure path: function with requires false
 
-procedure testAndThenFunc() {
+procedure testAndThenFunc()
+  opaque
+{
   var b: bool := false && mustNotCallFunc(0) > 0;
   assert !b
 };
 
-procedure testOrElseFunc() {
+procedure testOrElseFunc()
+  opaque
+{
   var b: bool := true || mustNotCallFunc(0) > 0;
   assert b
 };
 
-procedure testImpliesFunc() {
+procedure testImpliesFunc()
+  opaque
+{
   var b: bool := false ==> mustNotCallFunc(0) > 0;
   assert b
 };
 
 // Pure path: division by zero
 
-procedure testAndThenDivByZero() {
+procedure testAndThenDivByZero()
+  opaque
+{
   assert !(false && 1 / 0 > 0)
 };
 
-procedure testOrElseDivByZero() {
+procedure testOrElseDivByZero()
+  opaque
+{
   assert true || 1 / 0 > 0
 };
 
-procedure testImpliesDivByZero() {
+procedure testImpliesDivByZero()
+  opaque
+{
   assert false ==> 1 / 0 > 0
 };
 
 // Imperative path: procedure with requires false
 
-procedure testAndThenProc() {
+procedure testAndThenProc()
+  opaque
+{
   var b: bool := false && mustNotCallProc() > 0;
   assert !b
 };
 
-procedure testOrElseProc() {
+procedure testOrElseProc()
+  opaque
+{
   var b: bool := true || mustNotCallProc() > 0;
   assert b
 };
 
-procedure testImpliesProc() {
+procedure testImpliesProc()
+  opaque
+{
   var b: bool := false ==> mustNotCallProc() > 0;
   assert b
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
index 67d2f109d3..b9d25ce265 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
@@ -16,13 +16,16 @@ def program := r#"
 procedure divide(x: int, y: int) returns (result: int)
   requires y != 0 summary "divisor is non-zero"
 // Call elimination reports precondition errors at the call site.
+  opaque
 {
   assert y == 0 summary "divisor is zero";
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: divisor is zero does not hold
   return x
 };
 
-procedure checkPositive(n: int) returns (ok: bool) {
+procedure checkPositive(n: int) returns (ok: bool)
+  opaque
+{
   var x: int := divide(3, 0)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: divisor is non-zero does not hold
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
index 9710af32c7..9e0276a960 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def forLoopProgram := r"
-procedure sumToThree() {
+procedure sumToThree()
+  opaque
+{
   var sum: int := 0;
   for (var i: int := 0; i < 3; i := i + 1)
     invariant sum >= 0
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
index a0325e7c1b..7257ec2df3 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
@@ -22,28 +22,35 @@ datatype IntList {
   Cons(head: int, tail: IntList)
 }
 
-function listLen(xs: IntList): int {
+function listLen(xs: IntList): int
+{
   if IntList..isNil(xs) then 0
   else 1 + listLen(IntList..tail!(xs))
 };
 
-procedure testListLen() {
+procedure testListLen()
+  opaque
+{
   var xs: IntList := Cons(1, Cons(2, Nil()));
   assert listLen(xs) == 2
 };
 
 // Mutual recursion
-function listLenEven(xs: IntList): bool {
+function listLenEven(xs: IntList): bool
+{
   if IntList..isNil(xs) then true
   else listLenOdd(IntList..tail!(xs))
 };
 
-function listLenOdd(xs: IntList): bool {
+function listLenOdd(xs: IntList): bool
+{
   if IntList..isNil(xs) then false
   else listLenEven(IntList..tail!(xs))
 };
 
-procedure testMutualRecursion() {
+procedure testMutualRecursion()
+  opaque
+{
   var xs: IntList := Cons(1, Cons(2, Nil()));
   assert listLenEven(xs) == true
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
index 1e814bd74f..dec53e08a4 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
@@ -16,28 +16,38 @@ def bvProgram := r"
 // Bitvector types in procedure signatures and variable declarations.
 
 // Parameters and return types
-procedure identity32(x: bv 32) returns (r: bv 32) {
+procedure identity32(x: bv 32) returns (r: bv 32)
+  opaque
+{
   r := x
 };
 
-procedure identity8(x: bv 8) returns (r: bv 8) {
+procedure identity8(x: bv 8) returns (r: bv 8)
+  opaque
+{
   r := x
 };
 
 // Local variable with bv type
-procedure localBv() returns (r: bv 16) {
+procedure localBv() returns (r: bv 16)
+  opaque
+{
   var x: bv 16 := r;
   r := x
 };
 
 // Opaque procedure returning bv64 — caller gets typed result
 procedure opaqueBv64() returns (r: bv 64);
-procedure callOpaque() returns (r: bv 64) {
+procedure callOpaque() returns (r: bv 64)
+  opaque
+{
   r := opaqueBv64()
 };
 
 // Mixed bv and int parameters
-procedure mixedTypes(a: bv 32, b: int) returns (r: int) {
+procedure mixedTypes(a: bv 32, b: int) returns (r: int)
+  opaque
+{
   r := b
 };
 "
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
index b1ade4f39e..d4937969b0 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
@@ -23,6 +23,7 @@ function needsPAndQsInvoke1(): int {
 
 procedure PAndQ(x: int)
   invokeOn P(x)
+  opaque
   ensures P(x) && Q(x);
 
 function needsPAndQsInvoke2(): int {
@@ -30,11 +31,15 @@ function needsPAndQsInvoke2(): int {
 };
 
 // The axiom fires because P(x) appears in the goal.
-procedure fireAxiomUsingPattern(x: int) {
+procedure fireAxiomUsingPattern(x: int)
+  opaque
+{
   assert P(x)
 };
 
-procedure axiomDoesNotFireBecauseOfPattern(x: int) {
+procedure axiomDoesNotFireBecauseOfPattern(x: int)
+  opaque
+{
   assert Q(x)
 //^^^^^^^^^^^ error: assertion could not be proved
 };
@@ -43,13 +48,18 @@ function A(x: int, y: real): bool;
 function B(x: real): bool;
 procedure AAndB(x: int, y: real)
   invokeOn A(x, y)
+  opaque
   ensures A(x, y) && B(y);
 
-procedure invokeA(x: int, y :real) {
+procedure invokeA(x: int, y :real)
+  opaque
+{
   assert A(x, y)
 };
 
-procedure invokeB(x: int, y :real) {
+procedure invokeB(x: int, y :real)
+  opaque
+{
   assert B(y)
 //^^^^^^^^^^^ error: assertion could not be proved
 };
@@ -57,8 +67,9 @@ procedure invokeB(x: int, y :real) {
 function R(x: int): bool;
 procedure badPostcondition(x: int)
   invokeOn R(x)
+  opaque
   ensures R(x)
-//        ^^^^ error: assertion does not hold
+//        ^^^^ error: postcondition does not hold
 {
 };
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
index 7baf038299..7a913ad921 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def program := r"
-procedure foo() {
+procedure foo()
+  opaque
+{
     assert true;
     assert false;
 //  ^^^^^^^^^^^^ error: assertion does not hold
@@ -21,7 +23,9 @@ procedure foo() {
 //  ^^^^^^^^^^^^ error: assertion does not hold
 };
 
-procedure bar() {
+procedure bar()
+  opaque
+{
     assume false;
     assert false
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_InferTypeError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_InferTypeError.lean
index d8f352f716..f8a149f6da 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_InferTypeError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_InferTypeError.lean
@@ -13,7 +13,8 @@ namespace Strata
 namespace Laurel
 
 def inferTypeErrorProgram := r"
-procedure foo() {
+procedure foo()
+{
   <?>
 //^^^ error: could not infer type
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
index d9d4b0988e..97db999027 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
@@ -12,7 +12,9 @@ open StrataTest.Util
 namespace Strata.Laurel
 
 def exitMultiPathProgram := r"
-procedure foo(x: int) {
+procedure foo(x: int)
+  opaque
+{
   {
     if x == 0 then {
       exit myBlock
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index 3c94933f5d..efb9340b8b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -13,7 +13,9 @@ open Strata
 namespace Strata.Laurel
 
 def program: String := r"
-procedure nestedImpureStatements() {
+procedure nestedImpureStatements()
+  opaque
+{
   var y: int := 0;
   var x: int := y;
   var z: int := y := y + 1;
@@ -22,13 +24,17 @@ procedure nestedImpureStatements() {
   assert z == y
 };
 
-procedure multipleAssignments() {
+procedure multipleAssignments()
+  opaque
+{
   var x: int := 1;
   var y: int := x + ((x := 2) + x) + (x := 3);
   assert y == 8
 };
 
-procedure conditionalAssignmentInExpression(x: int) {
+procedure conditionalAssignmentInExpression(x: int)
+  opaque
+{
   var y: int := 0;
   var z: int := (if x > 0 then { y := y + 1 } else { 0 }) + y;
   if x > 0 then {
@@ -40,14 +46,18 @@ procedure conditionalAssignmentInExpression(x: int) {
   }
 };
 
-procedure anotherConditionAssignmentInExpression(c: bool) {
+procedure anotherConditionAssignmentInExpression(c: bool)
+  opaque
+{
   var b: bool := c;
   var z: bool := (if b then { b := false } else (b := true)) || b;
   assert z
 //^^^^^^^^ error: assertion does not hold
 };
 
-procedure blockWithTwoAssignmentsInExpression() {
+procedure blockWithTwoAssignmentsInExpression()
+  opaque
+{
   var x: int := 0;
   var y: int := 0;
   var z: int := { x := 1; y := 2 };
@@ -57,7 +67,7 @@ procedure blockWithTwoAssignmentsInExpression() {
 };
 
 procedure nestedImpureStatementsAndOpaque()
-  ensures true
+  opaque
 {
   var y: int := 0;
   var x: int := y;
@@ -70,14 +80,16 @@ procedure nestedImpureStatementsAndOpaque()
 // An imperative procedure call in expression position is lifted before the
 // surrounding expression is evaluated.
 procedure imperativeProc(x: int) returns (r: int)
-   // ensures clause required because Core's symbolic verification does not support transparent proceduces yet
+  opaque
   ensures r == x + 1
 {
   r := x + 1;
   r
 };
 
-procedure imperativeCallInExpressionPosition() {
+procedure imperativeCallInExpressionPosition()
+  opaque
+{
   var x: int := 0;
   // imperativeProc(x) is lifted out; its argument is evaluated before the call,
   // so the result is 1 (imperativeProc(0)), and x is still 0 afterwards.
@@ -87,7 +99,9 @@ procedure imperativeCallInExpressionPosition() {
 };
 
 // An imperative call inside a conditional expression is also lifted.
-procedure imperativeCallInConditionalExpression(b: bool) {
+procedure imperativeCallInConditionalExpression(b: bool)
+  opaque
+{
   var counter: int := 0;
   // The imperative call in the then-branch is lifted out of the expression.
   var result: int := (if b then { imperativeProc(counter) } else { 0 }) + counter;
@@ -103,7 +117,9 @@ function add(x: int, y: int): int
   x + y
 };
 
-procedure repeatedBlockExpressions() {
+procedure repeatedBlockExpressions()
+  opaque
+{
   var x: int := 2;
   var y: int := { x := 1; x } + { x := x + 10; x };
   var z: int := add({ x := 1; x }, { x := x + 10; x });
@@ -112,11 +128,14 @@ procedure repeatedBlockExpressions() {
 };
 
 procedure addProc(a: int, b: int) returns (r: int)
+  opaque
   ensures r == a + b {
   return a + b
 };
 
-procedure addProcCaller(): int {
+procedure addProcCaller(): int
+  opaque
+{
   var x: int := 0;
   var y: int := addProc({x := 1; x}, {x := x + 10; x});
   assert y == 11
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
index 379701d566..5eb598de7f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
@@ -13,7 +13,9 @@ open Strata
 namespace Strata.Laurel
 
 def program: String := r"
-procedure impure(): int {
+procedure impure(): int
+  opaque
+{
   var x: int := 0;
   x := x + 1;
   x
@@ -33,20 +35,19 @@ function impureFunction2(x: int): int
 function impureFunction3(x: int): int
 {
   impure()
-//^^^^^^^^ error: calls to procedures are not supported in functions or contracts
 };
 
 procedure impureContractIsNotLegal1(x: int)
   requires x == impure()
-//              ^^^^^^^^ error: calls to procedures are not supported in functions or contracts
+  opaque
 {
   assert impure() == 1
-//       ^^^^^^^^ error: calls to procedures are not supported in functions or contracts
 };
 
 procedure impureContractIsNotLegal2(x: int)
   requires (x := 2) == 2
 //          ^^^^^^ error: destructive assignments are not supported in functions or contracts
+  opaque
 {
   assert (x := 2) == 2
 //        ^^^^^^ error: destructive assignments are not supported in functions or contracts
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
index 150ee55f50..3839b44afa 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
@@ -13,7 +13,16 @@ open Strata
 namespace Strata.Laurel
 
 def program := r"
-function returnAtEnd(x: int) returns (r: int) {
+function assertAndAssumeInFunctions(a: int) returns (r: int)
+{
+  assert 2 == 3;
+//^^^^^^^^^^^^^ error: assertion does not hold
+  assume true;
+  a
+};
+
+function returnAtEnd(x: int) returns (r: int)
+{
   if x > 0 then {
     if x == 1 then {
       return 1
@@ -25,11 +34,13 @@ function returnAtEnd(x: int) returns (r: int) {
   }
 };
 
-function elseWithCall(): int {
+function elseWithCall(): int
+{
   if true then 3 else returnAtEnd(3)
 };
 
-function guardInFunction(x: int) returns (r: int) {
+function guardInFunction(x: int) returns (r: int)
+{
   if x > 0 then {
     if x == 1 then {
       return 1
@@ -41,7 +52,9 @@ function guardInFunction(x: int) returns (r: int) {
   return 3
 };
 
-procedure testFunctions() {
+procedure testFunctions()
+  opaque
+{
   assert returnAtEnd(1) == 1;
   assert returnAtEnd(1) == 2;
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
@@ -52,6 +65,7 @@ procedure testFunctions() {
 };
 
 procedure guards(a: int) returns (r: int)
+  opaque
 {
   var b: int := a + 2;
   if b > 2 then {
@@ -70,6 +84,7 @@ procedure guards(a: int) returns (r: int)
 };
 
 procedure dag(a: int) returns (r: int)
+  opaque
 {
   var b: int;
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
index b336119eae..1408b84fa1 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
@@ -16,21 +16,15 @@ def program := r"
 function assertAndAssumeInFunctions(a: int) returns (r: int)
 {
   assert 2 == 3;
-//^^^^^^^^^^^^^ error: asserts are not YET supported in functions or contracts
   assume true;
-//^^^^^^^^^^^ error: assumes are not YET supported in functions or contracts
   a
 };
 
-// Lettish bindings in functions not yet supported
-// because Core expressions do not support let bindings
+// Lettish bindings in functions now supported via inlining
 function letsInFunction() returns (r: int) {
   var x: int := 0;
-//^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported
   var y: int := x + 1;
-//^^^^^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported
   var z: int := y + 1;
-//^^^^^^^^^^^^^^^^^^^ error: local variables in functions are not YET supported
   z
 };
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
index 040bf3a186..6fa2eaab2e 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
@@ -13,7 +13,9 @@ open Strata
 namespace Laurel
 
 def program := r"
-procedure whileWithBreakAndContinue(steps: int, continueSteps: int, exitSteps: int): int {
+procedure whileWithBreakAndContinue(steps: int, continueSteps: int, exitSteps: int): int
+  opaque
+{
   var counter = 0
   {
     while(steps > 0)
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
index c321315684..ce3868af8f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
@@ -12,7 +12,9 @@ open StrataTest.Util
 namespace Strata.Laurel
 
 def exitProgram := r"
-procedure exitSkipsRest() {
+procedure exitSkipsRest()
+  opaque
+{
     var x: int := 0;
     {
         x := 1;
@@ -21,7 +23,9 @@ procedure exitSkipsRest() {
     assert x == 1
 };
 
-procedure exitFromNestedBlock() {
+procedure exitFromNestedBlock()
+  opaque
+{
     var x: int := 0;
     {
         {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
index adb08b2aaf..36a73d6b17 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
@@ -13,7 +13,9 @@ open Strata
 namespace Strata.Laurel
 
 def program := r"
-procedure fooReassign(): int {
+procedure fooReassign(): int
+  opaque
+{
   var x: int := 0;
   x := x + 1;
   assert x == 1;
@@ -21,27 +23,33 @@ procedure fooReassign(): int {
   x
 };
 
-procedure fooSingleAssign(): int {
+procedure fooSingleAssign(): int
+  opaque
+{
   var x: int := 0;
   var x2: int := x + 1;
   var x3: int := x2 + 1;
   x3
 };
 
-procedure fooProof() {
+procedure fooProof()
+  opaque
+{
   var x: int := fooReassign();
   var y: int := fooSingleAssign()
 // The following assertions fails while it should succeed,
-// because Core does not yet support transparent procedures
+// because Core does not yet support transparent statement bodies
 //  assert x == y;
 };
 
-function aFunction(x: int): int
+procedure aFunction(x: int): int
 {
   x
 };
 
-procedure aFunctionCaller() {
+procedure aFunctionCaller()
+  opaque
+{
   var x: int := aFunction(3);
   assert x == 3
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
index c22d91c671..0387a6af7b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
@@ -18,6 +18,7 @@ procedure hasRequires(x: int) returns (r: int)
 // Call elimination reports precondition errors at the call site,
 // not at the requires clause definition.
 //
+  opaque
 {
   assert x > 0;
   assert x > 3;
@@ -25,7 +26,9 @@ procedure hasRequires(x: int) returns (r: int)
   x + 1
 };
 
-procedure caller() {
+procedure caller()
+  opaque
+{
   var x: int := hasRequires(1);
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
   var y: int := hasRequires(3)
@@ -37,20 +40,25 @@ function aFunctionWithPrecondition(x: int): int
   x
 };
 
-procedure aFunctionWithPreconditionCaller() {
+procedure aFunctionWithPreconditionCaller()
+  opaque
+{
   var x: int := aFunctionWithPrecondition(0)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
 // Error ranges are too wide because Core does not use expression locations
 };
 
 procedure multipleRequires(x: int, y: int) returns (r: int)
   requires x > 0
   requires y > 0
+  opaque
 {
   x + y
 };
 
-procedure multipleRequiresCaller() {
+procedure multipleRequiresCaller()
+  opaque
+{
   var a: int := multipleRequires(1, 2);
   var b: int := multipleRequires(-1, 2)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
@@ -63,10 +71,12 @@ function funcMultipleRequires(x: int, y: int): int
   x + y
 };
 
-procedure funcMultipleRequiresCaller() {
+procedure funcMultipleRequiresCaller()
+  opaque
+{
   var a: int := funcMultipleRequires(1, 2);
   var b: int := funcMultipleRequires(1, -1)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
 };
 "
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
index ee5cfc149d..9167c54f51 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
@@ -19,26 +19,33 @@ A procedure with a decreases clause may be called in an erased context.
 
 def program := r"
 procedure noDecreases(x: int): boolean;
+  opaque
 procedure caller(x: int)
   requires noDecreases(x)
 //                    ^ error: noDecreases can not be called from a pure context, because it is not proven to terminate
+  opaque
 ;
 
 procedure noCyclicCalls()
+  opaque
   decreases []
 {
   leaf();
 };
 
-procedure leaf() decreases [1] { };
+procedure leaf() decreases [1]
+  opaque
+{ };
 
 procedure mutualRecursionA(x: nat)
+  opaque
   decreases [x, 1]
 {
   mutualRecursionB(x);
 };
 
 procedure mutualRecursionB(x: nat)
+  opaque
   decreases [x, 0]
 {
   if x != 0 { mutualRecursionA(x-1); }
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
index 9fa92af45a..44a27be2eb 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
@@ -14,23 +14,26 @@ namespace Strata.Laurel
 
 def program := r"
 procedure opaqueBody(x: int) returns (r: int)
-// the presence of the ensures make the body opaque. we can consider more explicit syntax.
+  opaque
   ensures r > 0
 {
   if x > 0 then { r := x }
   else { r := 1 }
 };
 
-procedure callerOfOpaqueProcedure() {
+procedure callerOfOpaqueProcedure()
+  opaque
+{
   var x: int := opaqueBody(3);
   assert x > 0;
   assert x == 3
-//^^^^^^^^^^^^^ error: assertion could not be proved
+//^^^^^^^^^^^^^ error: assertion does not hold
 };
 
 procedure invalidPostcondition(x: int)
-    ensures false
-//          ^^^^^ error: assertion does not hold
+  opaque
+  ensures false
+//        ^^^^^ error: postcondition does not hold
 {
 };
 "
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
deleted file mode 100644
index 539049e793..0000000000
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
-import StrataTest.Util.TestDiagnostics
-import StrataTest.Languages.Laurel.TestExamples
-
-open StrataTest.Util
-open Strata
-
-namespace Strata.Laurel
-
-def program := r"
-
-function opaqueFunction(x: int) returns (r: int)
-//       ^^^^^^^^^^^^^^ error: functions with postconditions are not yet supported
-// The above limitation is because Core does not yet support functions with postconditions
-  requires x > 0
-  ensures r > 0
-// The above limitation is because functions in Core do not support postconditions
-{
-  x
-};
-
-procedure callerOfOpaqueFunction() {
-  var x: int := opaqueFunction(3);
-  assert x > 0;
-// The following assertion should fail but does not
-// Because Core does not support opaque functions
-  assert x == 3
-};
-"
-
-#guard_msgs (drop info, error) in
-#eval testInputWithOffset "Postconditions" program 14 processLaurelFile
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
index 2795f28a21..f8f4b8089b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
@@ -14,6 +14,7 @@ namespace Strata.Laurel
 
 def program := r"
 procedure earlyReturnCorrect(x: int) returns (r: int)
+  opaque
   ensures r >= 0
 {
   if x < 0 then {
@@ -23,8 +24,9 @@ procedure earlyReturnCorrect(x: int) returns (r: int)
 };
 
 procedure earlyReturnBuggy(x: int) returns (r: int)
+  opaque
   ensures r >= 0
-//        ^^^^^^ error: assertion does not hold
+//        ^^^^^^ error: postcondition does not hold
 {
   if x < 0 then {
     return x
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean
index bb04673c81..1c99869d5e 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean
@@ -5,6 +5,8 @@
 -/
 
 import Strata.SimpleAPI
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
 
 /-! # Bodiless Procedure Inlining Test
 
@@ -16,41 +18,27 @@ the inlined call is correctly rejected. -/
 
 namespace Strata.Laurel.BodilessInliningTest
 
+open StrataTest.Util
+open Strata
+
 private def laurelSource := "
 procedure bodilessProcedure() returns (r: int)
+  opaque
   ensures r > 0
 ;
 
-procedure caller() {
+procedure caller()
+  opaque
+{
   var x: int := bodilessProcedure();
   assert x > 0;
   assert false
+//^^^^^^^^^^^^ error: assertion does not hold
 };
 "
 
-/-- info: "assert(143): ❌ fail" -/
-#guard_msgs in
-#eval show IO String from do
-  let laurelProg ← Strata.parseLaurelText "test.laurel" laurelSource
-  let coreProg ← match ← Strata.laurelToCore laurelProg with
-    | .ok p => pure p
-    | .error e => throw (IO.userError s!"Translation failed: {e}")
-  let inlined ← match Strata.Core.inlineProcedures coreProg {} with
-    | .ok p => pure p
-    | .error e => throw (IO.userError s!"Inlining failed: {e}")
-  let vcResults ←
-    EIO.toIO (fun e => IO.Error.userError e)
-      (Strata.Core.verifyProgram inlined
-        { Core.VerifyOptions.default with verbose := .quiet }
-        (proceduresToVerify := some ["caller"]))
-  -- Collect only failing results
-  let failures := vcResults.filter fun vcr =>
-    match vcr.outcome with
-    | .ok o => o.validityProperty != .unsat
-    | .error _ => true
-  let mut output := ""
-  for vcr in failures do
-    output := output ++ s!"{vcr.obligation.label}: {vcr.formatOutcome}"
-  return output
+#guard_msgs (drop info, error) in
+#eval testInputWithOffset "Postconditions" laurelSource 23
+  (fun p => processLaurelFileWithOptions default {inlineFunctionsWhenPossible := true} p)
 
 end Strata.Laurel.BodilessInliningTest
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean
index c0bfe80044..0e2a397570 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean
@@ -18,6 +18,7 @@ composite Container {
 }
 
 procedure setAndReturn(c: Container, x: int) returns (r: int)
+  opaque
   ensures r == x
   modifies c
 {
@@ -26,8 +27,9 @@ procedure setAndReturn(c: Container, x: int) returns (r: int)
 };
 
 procedure setAndReturnBuggy(c: Container, x: int) returns (r: int)
+  opaque
   ensures r == x + 1
-//        ^^^^^^^^^^ error: assertion does not hold
+//        ^^^^^^^^^^ error: postcondition could not be proved
   modifies c
 {
   c#value := x;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
index 99d4bed09f..545bf8830b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
@@ -14,12 +14,15 @@ namespace Laurel
 
 def program := r"
 nondet procedure nonDeterministic(x: int): (r: int)
+  opaque
   ensures r > 0
 {
   assumed
 };
 
-procedure caller() {
+procedure caller()
+  opaque
+{
   var x = nonDeterministic(1)
   assert x > 0;
   var y = nonDeterministic(1)
@@ -28,11 +31,13 @@ procedure caller() {
 };
 
 nondet procedure nonDeterminsticTransparant(x: int): (r: int)
+  opaque
 {
   nonDeterministic(x + 1)
 };
 
 procedure nonDeterministicCaller(x: int): int
+  opaque
 {
   nonDeterministic(x)
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
index 832b8633c9..a4d032c3d2 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
@@ -20,13 +20,17 @@ composite Container {
   var stringValue: string
 }
 
-procedure newsAreNotEqual() {
+procedure newsAreNotEqual()
+  opaque
+{
   var c: Container := new Container;
   var d: Container := new Container;
   assert c != d
 };
 
-procedure simpleAssign() {
+procedure simpleAssign()
+  opaque
+{
   var c: Container := new Container;
   var iv: int := c#intValue;
   var rv: real := c#realValue;
@@ -45,6 +49,7 @@ procedure simpleAssign() {
 };
 
 procedure updatesAndAliasing()
+  opaque
 {
   var c: Container := new Container;
   var d: Container := new Container;
@@ -62,13 +67,17 @@ procedure updatesAndAliasing()
   assert dAlias#intValue == d#intValue
 };
 
-procedure subsequentHeapMutations(c: Container) {
+procedure subsequentHeapMutations() opaque {
+  var c: Container := new Container;
+
   // The additional parenthesis on the next line are needed to let the parser succeed. Joe, any idea why this is needed?
   var sum: int := ((c#intValue := 1) + c#intValue) + (c#intValue := 2);
   assert sum == 4
 };
 
-procedure implicitEquality(c: Container, d: Container) {
+procedure implicitEquality() opaque {
+  var c: Container := new Container;
+  var d: Container := new Container;
   c#intValue := 1;
   d#intValue := 2;
   if c#intValue == d#intValue then {
@@ -79,7 +88,9 @@ procedure implicitEquality(c: Container, d: Container) {
   }
 };
 
-procedure useBool(c: Container) returns (r: bool) {
+procedure useBool(c: Container) returns (r: bool)
+  opaque
+{
   r := c#boolValue
 };
 
@@ -87,7 +98,9 @@ composite SameFieldName {
   var intValue: bool
 }
 
-procedure sameFieldNameDifferentType(a: Container, b: SameFieldName) {
+procedure sameFieldNameDifferentType() opaque {
+  var a: Container := new Container;
+  var b: SameFieldName := new SameFieldName;
   a#intValue := 1;
   b#intValue := true;
 
@@ -106,7 +119,7 @@ composite Pixel {
   var color: Color
 }
 
-procedure datatypeField() {
+procedure datatypeField() opaque {
   var p: Pixel := new Pixel;
   p#color := Red();
   assert Color..isRed(p#color);
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
index f7b718e57b..91ec0fc9a0 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
@@ -28,20 +28,16 @@ composite Container {
 }
 
 procedure modifyContainerOpaque(c: Container) returns (b: bool)
-  ensures true // makes this procedure opaque. Maybe we should use explicit syntax
+  opaque
   modifies c
 {
   c#value := c#value + 1;
   true
 };
 
-procedure modifyContainerTransparant(c: Container) returns (i: int)
+procedure caller()
+  opaque
 {
-  c#value := c#value + 1;
-  7
-};
-
-procedure caller() {
   var c: Container := new Container;
   var d: Container := new Container;
   var x: int := d#value;
@@ -49,8 +45,13 @@ procedure caller() {
   assert x == d#value // pass
 };
 
-// This test-case does not work yet.
-// Because Core procedures never have transparent bodies
+// Commented out because
+// Transparent assignments are not supported yet
+// procedure modifyContainerTransparant(c: Container) returns (i: int)
+//{
+//  c#value := c#value + 1;
+//  7
+//};
 //procedure modifyContainerWithPermission1(c: Container, d: Container)
 //   ensures true
 //   modifies c
@@ -58,38 +59,46 @@ procedure caller() {
 //    var i: int := modifyContainerTransparant(c);
 //}
 
+procedure modifyContainerWildcard(c: Container) returns (i: int)
+  opaque
+  modifies *
+{
+  c#value := c#value + 1;
+  7
+};
+
 procedure modifyContainerWithoutPermission1(c: Container, d: Container)
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
-// the above error is because the body does not satisfy the empty modifies clause. error needs to be improved
-   ensures true
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: postcondition does not hold
+  opaque
 {
-    var i: int := modifyContainerTransparant(c)
+    var i: int := modifyContainerWildcard(c)
 };
 
 procedure modifyContainerWithoutPermission2(c: Container, d: Container)
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
-// the above error is because the body does not satisfy the modifies clause. error needs to be improved
-  ensures true
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: postcondition could not be proved
+  opaque
   modifies d
 {
     c#value := 2
 };
 
 procedure modifyContainerWithoutPermission3(c: Container, d: Container)
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
-// the above error is because the body does not satisfy the modifies clause. error needs to be improved
-  ensures true
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: postcondition could not be proved
+  opaque
   modifies d
 {
-    var i: int := modifyContainerTransparant(c)
+    var i: bool := modifyContainerOpaque(c)
 };
 
 procedure multipleModifiesClauses(c: Container, d: Container, e: Container)
+  opaque
   modifies c
   modifies d
 ;
 
-procedure multipleModifiesClausesCaller() {
+procedure multipleModifiesClausesCaller()
+  opaque
+{
   var c: Container := new Container;
   var d: Container := new Container;
   var e: Container := new Container;
@@ -99,7 +108,7 @@ procedure multipleModifiesClausesCaller() {
 };
 
 procedure newObjectDoNotCountForModifies()
-  ensures true
+  opaque
 {
   var c: Container := new Container;
   c#value := 1
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st
index d95606784d..210a95c155 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st
@@ -16,10 +16,11 @@ composite Container {
 
 procedure opaqueProcedure(c: Container): int
   reads c
-  ensures true
+  opaque
 ;
 
 procedure foo(c: Container, d: Container) 
+  opaque
 {
   var x = opaqueProcedure(c);
   d.value = 1;
@@ -33,6 +34,7 @@ procedure foo(c: Container, d: Container)
 
 procedure permissionLessReader(c: Container): int
   reads {}
+  opaque
   { c.value }
 //  ^^^^^^^ error: enclosing procedure 'permissionLessReader' does not have permission to read 'c.value'
 ;
@@ -44,7 +46,8 @@ type Composite;
 type Field;
 val value: Field;
 
-function opaqueProcedure_ensures(heap: Heap, c: Container, r: int): boolean {
+function opaqueProcedure_ensures(heap: Heap, c: Container, r: int): boolean
+{
   true
 }
 
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T4_ImmutableFields.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/T4_ImmutableFields.lr.st
index d92a44c6bd..f287c7f84d 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T4_ImmutableFields.lr.st
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T4_ImmutableFields.lr.st
@@ -9,6 +9,7 @@ composite ImmutableContainer {
 }
 
 procedure valueReader(c: ImmutableContainer): int
+  opaque
   { c.value } // no reads clause needed because value is immutable
 ;
 
@@ -18,7 +19,8 @@ Translation towards SMT:
 type Composite;
 function ImmutableContainer_value(c: Composite): int
 
-function valueReader(c: Composite): int {
+function valueReader(c: Composite): int
+{
   ImmutableContainer_value(c)
 }
 
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
index d9cb4dbde4..440e3f833e 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
@@ -25,7 +25,10 @@ composite Extender extends Base, Base2 {
   var zValue: int
 }
 
-procedure inheritedFields(a: Extender) {
+procedure inheritedFields(a: Extender)
+  opaque
+  modifies a
+{
   a#xValue := 1;
   a#yValue := 2;
   a#zValue := 3;
@@ -35,7 +38,9 @@ procedure inheritedFields(a: Extender) {
   assert a#zValue == 3
 };
 
-procedure typeCheckingAndCasting() {
+procedure typeCheckingAndCasting()
+  opaque
+{
   var a: Base := new Base;
   assert a is Base;
   assert !(a is Extender);
@@ -64,7 +69,9 @@ composite Bottom extends Left, Right {
   var bValue: int
 }
 
-procedure diamondInheritance() {
+procedure diamondInheritance()
+  opaque
+{
   var b: Bottom := new Bottom;
   b#lValue := 1;
   b#rValue := 2;
@@ -82,7 +89,7 @@ procedure diamondInheritance() {
 };
 
 // Currently does not pass. Implementation needs b type invariant mechanism that we have yet to add.
-//procedure typedParameter(b: Bottom) {
+//procedure typedParameter(b: Bottom) opaque {
 //  var b: Bottom := b;
 //  assert b is Left;
 //  assert b is Right;
@@ -91,5 +98,5 @@ procedure diamondInheritance() {
 //}
 "
 
-#guard_msgs (drop info) in
+#guard_msgs (drop info, error) in
 #eval testInputWithOffset "Inheritance" program 14 processLaurelFile
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritanceErrors.lean b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritanceErrors.lean
index 0b6d471b6c..af1b8ee5eb 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritanceErrors.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritanceErrors.lean
@@ -21,7 +21,10 @@ composite Left extends Top {}
 composite Right extends Top {}
 composite Bottom extends Left, Right {}
 
-procedure diamondField(b: Bottom) {
+procedure diamondField(b: Bottom)
+  opaque
+  modifies b
+{
   b#xValue := 1
 //  ^^^^^^ error: fields that are inherited multiple times can not be accessed.
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean b/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
index 00be7c2c8f..56b1f673b7 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
@@ -19,13 +19,17 @@ datatype IntList {
 }
 
 // Construction and destructor access
-procedure testConstruction() {
+procedure testConstruction()
+  opaque
+{
   var xs: IntList := Cons(42, Nil());
   assert IntList..head(xs) == 42
 };
 
 // Constructor testing
-procedure testConstructorTest() {
+procedure testConstructorTest()
+  opaque
+{
   var xs: IntList := Cons(1, Nil());
   assert IntList..isCons(xs);
   assert !IntList..isNil(xs);
@@ -36,7 +40,9 @@ procedure testConstructorTest() {
 };
 
 // Nested construction and deconstruction
-procedure testNested() {
+procedure testNested()
+  opaque
+{
   var xs: IntList := Cons(1, Cons(2, Nil()));
   assert IntList..isCons(xs);
   assert IntList..head(xs) == 1;
@@ -45,7 +51,9 @@ procedure testNested() {
   assert IntList..isNil(IntList..tail(IntList..tail(xs)))
 };
 
-procedure unsafeDestructor() {
+procedure unsafeDestructor()
+  opaque
+{
   var nil: IntList := Nil();
   var noError: int := IntList..head!(nil);
   var error: int := IntList..head(nil)
@@ -59,14 +67,18 @@ function listHead(xs: IntList): int
   IntList..head(xs)
 };
 
-procedure testFunction() {
+procedure testFunction()
+  opaque
+{
   var xs: IntList := Cons(10, Nil());
   var h: int := listHead(xs);
   assert h == 10
 };
 
 // Failing assertion
-procedure testFailing() {
+procedure testFailing()
+  opaque
+{
   var xs: IntList := Nil();
   assert IntList..isCons(xs)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
@@ -82,7 +94,9 @@ datatype OddList {
   OCons(head: int, tail: EvenList)
 }
 
-procedure testMutualConstruction() {
+procedure testMutualConstruction()
+  opaque
+{
   var even: EvenList := ENil();
   assert EvenList..isENil(even);
   var odd: OddList := OCons(1, ENil());
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
index 069c33cd4f..4451893acf 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
@@ -15,12 +15,14 @@ namespace Strata.Laurel
 def instanceProcedureProgram := r"
 composite Counter {
   var count: int
-  procedure increment(self: Counter) {
-//          ^^^^^^^^^ error: Instance procedure 'increment' on composite type 'Counter' is not yet supported
+  procedure increment2(self: Counter) opaque {
+//          ^^^^^^^^^^ error: Instance procedure 'increment2' on composite type 'Counter' is not yet supported
     self#count := self#count + 1
   };
-  procedure reset(self: Counter) {
+  procedure reset(self: Counter)
 //          ^^^^^ error: Instance procedure 'reset' on composite type 'Counter' is not yet supported
+    opaque
+  {
     self#count := 0
   };
 }
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean b/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean
index 904a43006f..cb0a8c69a1 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean
@@ -25,18 +25,18 @@ composite Container {
 }
 
 procedure incWithPrimitiveModifies(x: int) returns (r: int)
-  ensures true
+  opaque
   modifies x
-//         ^ error: non-composite type
+//         ^ error: modifies clause entry has non-composite type 'int' and will be ignored
 {
   r := x + 1
 };
 
 procedure modifyContainerAndPrimitive(c: Container, x: int)
-  ensures true
+  opaque
   modifies c
   modifies x
-//         ^ error: non-composite type
+//         ^ error: modifies clause entry has non-composite type 'int' and will be ignored
 {
   c#value := 1
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st
index cc0377ee27..9ce2bd2f05 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st	
@@ -13,6 +13,7 @@ composite Immutable {
   invariant x + y >= 5
 
   procedure construct()
+    opaque
     constructor
     requires contructing == {this}
     ensures constructing == {}
@@ -23,7 +24,9 @@ composite Immutable {
   };
 }
 
-procedure foo() {
+procedure foo()
+  opaque
+{
   val immutable = Immutable.construct(); // constructor instance method can be called as a static.
 };
 
@@ -34,6 +37,7 @@ composite ImmutableChainOfTwo {
   invariant other.other == this // reading other.other is allowed because the field is immutable
 
   procedure construct() 
+    opaque
     constructor
     requires contructing == {this}
     ensures constructing == {}
@@ -49,13 +53,16 @@ composite ImmutableChainOfTwo {
 
   // only used privately
   procedure allocate()
+    opaque
     constructor
     ensures constructing = {this} {    
     // empty body
   };
 }
 
-procedure foo2() {
+procedure foo2()
+  opaque
+{
   val immutable = ImmutableChainOfTwo.construct();
   val same = immutable.other.other;
   assert immutable =&= same;
@@ -67,6 +74,7 @@ composite UsesHelperConstructor {
   val y: int
 
   procedure setXhelper() 
+    opaque
     constructor
     requires constructing == {this}
     ensures constructing == {this} && assigned(this.x)
@@ -75,6 +83,7 @@ composite UsesHelperConstructor {
   };
 
   procedure construct() 
+    opaque
     constructor
     requires contructing == {this}
     ensures constructing == {}
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st
index 5d2c02cfd5..fd1c136e1b 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st	
@@ -18,6 +18,7 @@ composite Immutable {
   // fields of Immutable are considered mutable inside this procedure
   // and invariants of Immutable are not visible
   // can only call procedures that are also constructing Immutable
+    opaque
     constructs Immutable
     modifies this
   {
@@ -27,13 +28,16 @@ composite Immutable {
   };
 
   procedure assignToY() 
+    opaque
     constructs Immutable
   {
     this.y = 3;
   };
 }
 
-procedure foo() {
+procedure foo()
+  opaque
+{
   var c = new Immutable.construct();
   var temp = c.x;
   c.z = 1;
@@ -41,7 +45,9 @@ procedure foo() {
   assert temp == c.x; // pass
 };
 
-procedure pureCompositeAllocator(): boolean {
+procedure pureCompositeAllocator(): boolean
+  opaque
+{
   // can be called in a determinstic context
   var i: Immutable = Immutable.construct(); 
   var j: Immutable = Immutable.construct();
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st
index 6d94f9a08d..2b067c7f2a 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st	
@@ -19,7 +19,9 @@ composite Extended2 extends Base {
   var z: int
 }
 
-procedure typeTests(e: Extended1) {
+procedure typeTests(e: Extended1)
+  opaque
+{
   var b: Base = e as Base; // even upcasts are not implicit, but they pass statically
   var e2 = e as Extended2;
 //           ^^ error: could not prove 'e' is of type 'Extended2'
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/7. InstanceCallables.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/7. InstanceCallables.lr.st
index fe4c5756d6..95cf829196 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/7. InstanceCallables.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/7. InstanceCallables.lr.st	
@@ -5,12 +5,14 @@
 */
 composite Base {
   procedure foo(): int
+    opaque
     ensures result > 3
     { abstract };
 }
 
 composite Extender1 extends Base {
   procedure foo(): int
+    opaque
     ensures result > 4
 //  ^^^^^^^ error: could not prove ensures clause guarantees that of extended method 'Base.foo'
     { abstract };
@@ -19,6 +21,7 @@ composite Extender1 extends Base {
 composite Extender2 extends Base {
   value: int
   procedure foo(): int
+    opaque
     ensures result > 2
   {
     this.value + 2 // 'this' is an implicit variable inside instance callables
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st
index 73a72a4738..bd3932322d 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st	
@@ -87,6 +87,7 @@ so in affect there no longer are any variables captured by a closure.
 
 // Option A: first class procedures
 procedure hasClosure() returns (r: int)
+  opaque
   ensures r == 7
 {
   var x = 3;
@@ -100,17 +101,21 @@ procedure hasClosure() returns (r: int)
 
 // Option B: type closures
 composite ATrait {
-  procedure foo() returns (r: int) ensures r > 0 {
+  procedure foo() returns (r: int) ensures r > 0
+    opaque
+  {
     abstract
   };
 }
 
 procedure hasClosure() returns (r: int)
+  opaque
   ensures r == 7
 {
   var x = 3;
   var aClosure := closure extends ATrait {
     procedure foo() returns (r: int) 
+      opaque
     {
       r = x + 4;
     };
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
index 417c1ec77f..98d3908d77 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def decimalsProgram := r"
-procedure testDecimalLiterals() {
+procedure testDecimalLiterals()
+  opaque
+{
     var a: real := 1.5;
     var b: real := 2.5;
     assert a == 1.5;
@@ -21,7 +23,9 @@ procedure testDecimalLiterals() {
     assert a != b
 };
 
-procedure testDecimalArithmetic() {
+procedure testDecimalArithmetic()
+  opaque
+{
     var a: real := 1.5;
     var b: real := 2.5;
     var sum: real := a + b;
@@ -34,13 +38,17 @@ procedure testDecimalArithmetic() {
     assert quot == 5.0 / 3.0
 };
 
-procedure testDecimalNeg() {
+procedure testDecimalNeg()
+  opaque
+{
     var a: real := 1.5;
     var neg: real := -a;
     assert neg == 0.0 - 1.5
 };
 
-procedure testDecimalComparisons() {
+procedure testDecimalComparisons()
+  opaque
+{
     var a: real := 1.5;
     var b: real := 2.5;
     assert a < b;
@@ -51,7 +59,9 @@ procedure testDecimalComparisons() {
     assert a >= a
 };
 
-procedure testDecimalAssertFails() {
+procedure testDecimalAssertFails()
+  opaque
+{
     var a: real := 1.5;
     var b: real := 2.5;
     assert a == b
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
index bfb32714e0..c5f150cb95 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
@@ -15,8 +15,8 @@ namespace Laurel
 
 def program := r#"
 procedure testStringKO()
-returns (result: string)
-requires true
+  returns (result: string)
+  opaque
 {
   var message: string := "Hello";
   assert(message == "Hell");
@@ -27,7 +27,7 @@ requires true
 
 procedure testStringOK()
 returns (result: string)
-requires true
+  opaque
 {
   var message: string := "Hello";
   assert(message == "Hello");
@@ -36,14 +36,14 @@ requires true
 };
 
 procedure testStringLiteralConcatOK()
-requires true
+  opaque
 {
   var result: string := "a" ++ "b";
   assert(result == "ab")
 };
 
 procedure testStringLiteralConcatKO()
-requires true
+  opaque
 {
   var result: string := "a" ++ "b";
   assert(result == "cd")
@@ -51,7 +51,7 @@ requires true
 };
 
 procedure testStringVarConcatOK()
-requires true
+  opaque
 {
   var x: string := "Hello";
   var result: string := x ++ " World";
@@ -59,7 +59,7 @@ requires true
 };
 
 procedure testStringVarConcatKO()
-requires true
+  opaque
 {
   var x: string := "Hello";
   var result: string := x ++ " World";
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
index 482dd20d0c..6f0b2a01a7 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
@@ -14,7 +14,7 @@ namespace Strata.Laurel
 
 def stringConcatLiftingProgram := r#"
 procedure stringConcatWithAssignment()
-requires true
+  opaque
 {
   var x: string := "Hello";
   var y: string := x ++ (x := " World");
@@ -23,7 +23,7 @@ requires true
 };
 
 procedure stringConcatOK()
-requires true
+  opaque
 {
   var a: string := "Hello";
   var b: string := " World";
@@ -32,7 +32,7 @@ requires true
 };
 
 procedure stringConcatKO()
-requires true
+  opaque
 {
   var a: string := "Hello";
   var b: string := " World";
diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
index f3a3acbd6f..5512cb50bc 100644
--- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
+++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
@@ -23,6 +23,7 @@ namespace Strata.Laurel
 
 def blockStmtLiftingProgram : String := r"
 procedure assertInBlockExpr()
+  opaque
 {
   var x: int := 0;
   var y: int := { assert x == 0; x := 1; x };
@@ -44,6 +45,7 @@ def parseLaurelAndLift (input : String) : IO Program := do
 
 /--
 info: procedure assertInBlockExpr()
+  opaque
 { var x: int := 0; assert x == 0; var $x_0: int := x; x := 1; var y: int := { x }; assert y == 1 };
 -/
 #guard_msgs in
diff --git a/StrataTest/Languages/Laurel/LiftHolesTest.lean b/StrataTest/Languages/Laurel/LiftHolesTest.lean
index fe4ceb18ca..5fc1c83fbc 100644
--- a/StrataTest/Languages/Laurel/LiftHolesTest.lean
+++ b/StrataTest/Languages/Laurel/LiftHolesTest.lean
@@ -33,7 +33,7 @@ private def parseElimAndPrint (input : String) : IO Unit := do
   | .ok program =>
     let result := resolve program
     let (program, model) := (result.program, result.model)
-    let program := inferHoleTypes model program
+    let (program, _inferDiags) := inferHoleTypes model program
     let program := eliminateHoles program
     for proc in program.staticProcedures do
       IO.println (toString (Std.Format.pretty (Std.ToFormat.format proc)))
@@ -43,110 +43,146 @@ private def parseElimAndPrint (input : String) : IO Unit := do
 -- Hole in Add arg inside typed local variable → int.
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test()
+  opaque
 { var x: int := 1 + $hole_0() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := 1 + <?> };
+procedure test()
+  opaque
+{ var x: int := 1 + <?> };
 "
 
 -- Bare Hole as LocalVariable initializer → replaced with call (no longer preserved as havoc).
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test()
+  opaque
 { var x: int := $hole_0() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?> };
+procedure test()
+  opaque
+{ var x: int := <?> };
 "
 
 -- Hole in comparison arg inside assert → int (inferred from sibling literal).
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test()
+  opaque
 { assert $hole_0() > 0 };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <?> > 0 };
+procedure test()
+  opaque
+{ assert <?> > 0 };
 "
 
 -- Hole directly as assert condition → bool.
 /--
 info: function $hole_0()
-  returns ($result: bool);
+  returns ($result: bool)
+  opaque;
 procedure test()
+  opaque
 { assert $hole_0() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <?> };
+procedure test()
+  opaque
+{ assert <?> };
 "
 
 -- Hole directly as assume condition → bool.
 /--
 info: function $hole_0()
-  returns ($result: bool);
+  returns ($result: bool)
+  opaque;
 procedure test()
+  opaque
 { assume $hole_0() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assume <?> };
+procedure test()
+  opaque
+{ assume <?> };
 "
 
 -- Hole as if-then-else condition → bool.
 /--
 info: function $hole_0()
-  returns ($result: bool);
+  returns ($result: bool)
+  opaque;
 procedure test()
+  opaque
 { if $hole_0() then { assert true } };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { if <?> then { assert true } };
+procedure test()
+  opaque
+{ if <?> then { assert true } };
 "
 
 -- Hole in then-branch of if-then-else inside typed local variable → int.
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test()
+  opaque
 { var x: int := if true then $hole_0() else 0 };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := if true then <?> else 0 };
+procedure test()
+  opaque
+{ var x: int := if true then <?> else 0 };
 "
 
 -- Hole as while-loop condition → bool.
 /--
 info: function $hole_0()
-  returns ($result: bool);
+  returns ($result: bool)
+  opaque;
 procedure test()
+  opaque
 { while($hole_0()) {  } };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { while(<?>) {} };
+procedure test()
+  opaque
+{ while(<?>) {} };
 "
 
 -- Hole as while-loop invariant → bool.
 /--
 info: function $hole_0()
-  returns ($result: bool);
+  returns ($result: bool)
+  opaque;
 procedure test()
+  opaque
 { while(true)
   invariant $hole_0() {  } };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { while(true) invariant <?> {} };
+procedure test()
+  opaque
+{ while(true) invariant <?> {} };
 "
 
 /-! ## Operators -/
@@ -154,31 +190,40 @@ procedure test() { while(true) invariant <?> {} };
 -- Hole in And arg inside assert → bool.
 /--
 info: function $hole_0()
-  returns ($result: bool);
+  returns ($result: bool)
+  opaque;
 procedure test()
+  opaque
 { assert true && $hole_0() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert true && <?> };
+procedure test()
+  opaque
+{ assert true && <?> };
 "
 
 -- Hole in Neg inside typed local variable → int.
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test()
+  opaque
 { var x: int := -$hole_0() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := -<?> };
+procedure test()
+  opaque
+{ var x: int := -<?> };
 "
 
 -- Hole in StrConcat inside typed local variable → string.
 /--
 info: function $hole_0()
-  returns ($result: string);
+  returns ($result: string)
+  opaque;
 procedure test()
 { var s: string := "hello" ++ $hole_0() };
 -/
@@ -191,29 +236,39 @@ procedure test()
 -- Two holes in Add → both int, separate functions.
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 function $hole_1()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test()
+  opaque
 { var x: int := $hole_0() + $hole_1() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?> + <?> };
+procedure test()
+  opaque
+{ var x: int := <?> + <?> };
 "
 
 -- Holes across statements: Mul arg (int) then assert condition (bool).
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 function $hole_1()
-  returns ($result: bool);
+  returns ($result: bool)
+  opaque;
 procedure test()
+  opaque
 { var x: int := 2 * $hole_0(); assert $hole_1() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := 2 * <?>; assert <?> };
+procedure test()
+  opaque
+{ var x: int := 2 * <?>; assert <?> };
 "
 
 /-! ## Combinations: holes in nested contexts -/
@@ -221,38 +276,50 @@ procedure test() { var x: int := 2 * <?>; assert <?> };
 -- Hole in Add inside Gt inside if condition → int (inferred from sibling literal 0).
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test()
+  opaque
 { if 1 + $hole_0() > 0 then { assert true } };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { if 1 + <?> > 0 then { assert true } };
+procedure test()
+  opaque
+{ if 1 + <?> > 0 then { assert true } };
 "
 
 -- Hole in Implies inside while invariant → bool.
 /--
 info: function $hole_0()
-  returns ($result: bool);
+  returns ($result: bool)
+  opaque;
 procedure test()
+  opaque
 { var p: bool; while(true)
   invariant p ==> $hole_0() {  } };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var p: bool; while(true) invariant p ==> <?> {} };
+procedure test()
+  opaque
+{ var p: bool; while(true) invariant p ==> <?> {} };
 "
 
 -- Hole in Mul inside typed local variable with real type → real.
 /--
 info: function $hole_0()
-  returns ($result: real);
+  returns ($result: real)
+  opaque;
 procedure test()
+  opaque
 { var r: real := 3.14 * $hole_0() };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var r: real := 3.14 * <?> };
+procedure test()
+  opaque
+{ var r: real := 3.14 * <?> };
 "
 
 /-! ## Call argument and return type inference -/
@@ -260,13 +327,17 @@ procedure test() { var r: real := 3.14 * <?> };
 -- Hole in comparison with variable sibling → hole function takes the procedure's params.
 /--
 info: function $hole_0(n: int)
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test(n: int)
+  opaque
 { assert n > $hole_0(n) };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test(n: int) { assert n > <?> };
+procedure test(n: int)
+  opaque
+{ assert n > <?> };
 "
 
 /-! ## Holes in functions -/
@@ -274,13 +345,17 @@ procedure test(n: int) { assert n > <?> };
 -- Hole in function body → same treatment as procedures.
 /--
 info: function $hole_0(x: int)
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 function test(x: int): int
+  opaque
 { $hole_0(x) };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-function test(x: int): int { <?> };
+function test(x: int): int
+  opaque
+{ <?> };
 "
 
 /-! ## Nondeterministic holes (<??>) -/
@@ -288,23 +363,30 @@ function test(x: int): int { <?> };
 -- Nondet hole in procedure → preserved after eliminateHoles (lifted by liftExpressionAssignments).
 /--
 info: procedure test()
+  opaque
 { assert <??> };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <??> };
+procedure test()
+  opaque
+{ assert <??> };
 "
 
 -- Mixed: det hole eliminated, nondet hole preserved.
 /--
 info: function $hole_0()
-  returns ($result: int);
+  returns ($result: int)
+  opaque;
 procedure test()
+  opaque
 { var x: int := $hole_0(); assert <??> };
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?>; assert <??> };
+procedure test()
+  opaque
+{ var x: int := <?>; assert <??> };
 "
 
 -- Nondet hole in function → should be rejected (not tested here since
diff --git a/StrataTest/Languages/Laurel/MapStmtExprTest.lean b/StrataTest/Languages/Laurel/MapStmtExprTest.lean
index 1b2926a613..b1406daf31 100644
--- a/StrataTest/Languages/Laurel/MapStmtExprTest.lean
+++ b/StrataTest/Languages/Laurel/MapStmtExprTest.lean
@@ -55,6 +55,7 @@ private def testMapStmtExprId (input : String) : IO Unit := do
 def testProgram : String := r"
 procedure test(x: int, b: bool) returns (r: int)
   requires x > 0
+  opaque
   ensures r >= 0
 {
   var y: int := x;
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index 36f970736a..3fbb312f80 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -19,7 +19,7 @@ open Lean.Parser (InputContext)
 
 namespace Strata.Laurel
 
-def processLaurelFileWithOptions (options : Core.VerifyOptions) (input : InputContext) : IO (Array Diagnostic) := do
+def processLaurelFileWithOptions (options : Core.VerifyOptions) (laurelOptions : LaurelTranslateOptions := {}) (input : InputContext) : IO (Array Diagnostic) := do
   let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
   let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name input
 
@@ -29,11 +29,11 @@ def processLaurelFileWithOptions (options : Core.VerifyOptions) (input : InputCo
   | .error transErrors => throw (IO.userError s!"Translation errors: {transErrors}")
   | .ok laurelProgram =>
     let files := Map.insert Map.empty uri input.fileMap
-    let diagnostics ← Laurel.verifyToDiagnostics files laurelProgram options
+    let diagnostics ← Laurel.verifyToDiagnostics files laurelProgram options laurelOptions
 
     pure diagnostics
 
-def processLaurelFile (input : InputContext) : IO (Array Diagnostic) :=
-  processLaurelFileWithOptions Core.VerifyOptions.default input
+def processLaurelFile (input : InputContext): IO (Array Diagnostic) :=
+  processLaurelFileWithOptions Core.VerifyOptions.default {} input
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/tests/test_arithmetic.lr.st b/StrataTest/Languages/Laurel/tests/test_arithmetic.lr.st
index 679d116441..7b5da7f2d3 100644
--- a/StrataTest/Languages/Laurel/tests/test_arithmetic.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_arithmetic.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var x: int := 5;
     var y: int := 3;
 
diff --git a/StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st b/StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st
index 9e83f61157..6c98d6fc40 100644
--- a/StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st
@@ -1,14 +1,20 @@
 // Bitvector types through the GOTO/CBMC pipeline.
 
-procedure identity32(x: bv 32) returns (r: bv 32) {
+procedure identity32(x: bv 32) returns (r: bv 32)
+  opaque
+{
   r := x
 };
 
-procedure identity8(x: bv 8) returns (r: bv 8) {
+procedure identity8(x: bv 8) returns (r: bv 8)
+  opaque
+{
   r := x
 };
 
-procedure localBv() returns (r: bv 16) {
+procedure localBv() returns (r: bv 16)
+  opaque
+{
   var x: bv 16 := r;
   r := x
 };
diff --git a/StrataTest/Languages/Laurel/tests/test_comparisons.lr.st b/StrataTest/Languages/Laurel/tests/test_comparisons.lr.st
index 6b67b797e0..1b0dc4d6b1 100644
--- a/StrataTest/Languages/Laurel/tests/test_comparisons.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_comparisons.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var a: int := 10;
     var b: int := 10;
     assert a == b;
diff --git a/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st b/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
index b255bd7b3a..84fba11963 100644
--- a/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var x: int := 5;
     var result: int := 0;
 
diff --git a/StrataTest/Languages/Laurel/tests/test_failing_assert.lr.st b/StrataTest/Languages/Laurel/tests/test_failing_assert.lr.st
index 9a6248151b..3cf0ace618 100644
--- a/StrataTest/Languages/Laurel/tests/test_failing_assert.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_failing_assert.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var x: int := 5;
     assert x == 10
 };
diff --git a/StrataTest/Languages/Laurel/tests/test_operators.lr.st b/StrataTest/Languages/Laurel/tests/test_operators.lr.st
index e38dfa7d9e..392414ad11 100644
--- a/StrataTest/Languages/Laurel/tests/test_operators.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_operators.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var a: int := 10;
     var b: int := 3;
     var x: int := a - b;
diff --git a/StrataTest/Languages/Laurel/tests/test_strings.lr.st b/StrataTest/Languages/Laurel/tests/test_strings.lr.st
index 35c643a9e2..f9a84a5b3e 100644
--- a/StrataTest/Languages/Laurel/tests/test_strings.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_strings.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var s1: string := "hello";
     var s2: string := " world";
     var result: string := s1 ++ s2;
diff --git a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
index e0441ae3dc..246f792f81 100644
--- a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
+++ b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
@@ -298,10 +298,9 @@ Expected output (when Python + z3 available):
     | .ok vcResults =>
       let mut foundAlwaysFalse := false
       for r in vcResults do
-        if r.obligation.label.startsWith "servicelib_Storage_" then
-          let line := r.formatOutcome
-          if (line.splitOn "✖️").length != 1 then
-            foundAlwaysFalse := true
+        let line := r.formatOutcome
+        if (line.splitOn "✖️").length != 1 then
+          foundAlwaysFalse := true
       if !foundAlwaysFalse then
         throw <| IO.userError
           "Expected ✖️ always false for regex violation"
@@ -323,10 +322,9 @@ assertion. This exercises the full pipeline with type alias resolution.
     | .ok vcResults =>
       let mut foundAlwaysFalse := false
       for r in vcResults do
-        if r.obligation.label.startsWith "servicelib_Storage_" then
-          let line := r.formatOutcome
-          if (line.splitOn "✖️").length != 1 then
-            foundAlwaysFalse := true
+        let line := r.formatOutcome
+        if (line.splitOn "✖️").length != 1 then
+          foundAlwaysFalse := true
       if !foundAlwaysFalse then
         throw <| IO.userError
           "Expected ✖️ always false for empty bucket violation"
diff --git a/StrataTest/Languages/Python/VerifyPythonTest.lean b/StrataTest/Languages/Python/VerifyPythonTest.lean
index e07d743898..e2d83cf05e 100644
--- a/StrataTest/Languages/Python/VerifyPythonTest.lean
+++ b/StrataTest/Languages/Python/VerifyPythonTest.lean
@@ -255,7 +255,7 @@ def main() -> None:
 "
   let (laurel, output) ← toLaurel pythonCmd program
   let calcAdd := manglePythonMethod "Calculator" "add"
-  assertTransparent laurel calcAdd
+  assertOpaque laurel calcAdd
   unless containsSubstr output s!"{calcAdd}(" do
     throw <| IO.userError s!"Expected '{calcAdd}(' in Laurel output but not found"
 
diff --git a/StrataTest/Util/TestDiagnostics.lean b/StrataTest/Util/TestDiagnostics.lean
index ebfb9f8ecb..3a23a20c4b 100644
--- a/StrataTest/Util/TestDiagnostics.lean
+++ b/StrataTest/Util/TestDiagnostics.lean
@@ -137,6 +137,10 @@ def testInputWithOffset (filename: String) (input : String) (lineOffset : Nat)
       IO.println s!"\nUnexpected diagnostics:"
       for diag in unmatchedDiagnostics do
         IO.println s!"  - Line {diag.start.line}, Col {diag.start.column}-{diag.ending.column}: {diag.message}"
+
+    if unmatchedExpectations.length == 0 && unmatchedDiagnostics.length == 0 then
+      IO.println s!"Duplicate diagnostics: {repr diagnostics}"
+
     throw (IO.userError "Test failed")
 
 def testInput (filename: String) (input : String) (process : Lean.Parser.InputContext -> IO (Array Diagnostic)) : IO Unit :=