diff --git a/Strata/Languages/Python/Approximation.lean b/Strata/Languages/Python/Approximation.lean
new file mode 100644
index 0000000000..ca169f5d59
--- /dev/null
+++ b/Strata/Languages/Python/Approximation.lean
@@ -0,0 +1,50 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+/-!
+# Approximation diagnostics
+
+Single source of truth for the wording and `[approximation]` prefix used by
+both the Python→Laurel translator and the PySpec parser when an unsupported
+Python construct is approximated (or silently dropped) under lax mode and
+would be rejected as an error under `--reject-approximations`. Keeping the
+prefix in one place lets downstream tooling filter on it reliably.
+-/
+
+public section
+
+namespace Strata.Python.Approximation
+
+/-- Kind of approximation site. -/
+inductive Kind where
+  /-- The translator emits a havoc'd `Hole` instead of a faithful translation. -/
+  | hole
+  /-- The translator silently drops the construct from the lowered program. -/
+  | drop
+  /-- The PySpec parser fell back to `.placeholder` and emitted a warning;
+      strict mode promotes that warning to an error. -/
+  | warningPromotion
+  deriving DecidableEq, Repr
+
+/-- The `[approximation] ` prefix that downstream tooling filters on. Must
+    not change without coordinating with consumers. -/
+def prefixTag : String := "[approximation] "
+
+/-- Render a strict-mode approximation diagnostic. The `construct` argument
+    names the surface form (e.g. `"BinOp Div"`) for `.hole` and `.drop`; for
+    `.warningPromotion`, it carries the original warning message verbatim. -/
+def render : Kind → (construct : String) → String
+  | .hole, c =>
+    s!"{prefixTag}{c} is approximated as Hole; not in the sound subset"
+  | .drop, c =>
+    s!"{prefixTag}{c} is silently dropped by current translation; not in the sound subset"
+  | .warningPromotion, msg =>
+    s!"{prefixTag}{msg}"
+
+end Strata.Python.Approximation
+
+end
diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean
index 5c05cfc37a..e13c72abf2 100644
--- a/Strata/Languages/Python/PySpecPipeline.lean
+++ b/Strata/Languages/Python/PySpecPipeline.lean
@@ -134,7 +134,8 @@ private def mergeOverloads (old new : OverloadTable) : OverloadTable :=
     to namespace all generated Laurel names (e.g., `"servicelib_Storage"` for
     module `servicelib.Storage`). -/
 private def buildPySpecLaurelM (pyspecEntries : Array (Python.ModuleName × String))
-    (overloads : OverloadTable) : Pipeline.PipelineM PySpecLaurelResult := do
+    (overloads : OverloadTable) (rejectApproximations : Bool := false)
+    : Pipeline.PipelineM PySpecLaurelResult := do
   let mut combinedProcedures : Array (Laurel.Procedure × String) := #[]
   let mut combinedTypes : Array (Laurel.TypeDefinition × String) := #[]
   let mut allOverloads := overloads
@@ -150,6 +151,7 @@ private def buildPySpecLaurelM (pyspecEntries : Array (Python.ModuleName × Stri
         emitMessageAndAbort .pySpecReadError msg (file := ionFile)
     let { program, errors, overloads, typeAliases, exhaustiveClasses } :=
       Python.Specs.ToLaurel.signaturesToLaurel ionPath sigs moduleName
+        (rejectApproximations := rejectApproximations)
     for msg in errors do
       Pipeline.addMessage msg
       if msg.kind.impact.isFatal then throw ()
@@ -207,8 +209,9 @@ private def buildPySpecLaurelM (pyspecEntries : Array (Python.ModuleName × Stri
 public def buildPySpecLaurel
     (ctx : Pipeline.PipelineContext)
     (pyspecEntries : Array (Python.ModuleName × String))
-    (overloads : OverloadTable) : EIO Unit PySpecLaurelResult :=
-  buildPySpecLaurelM pyspecEntries overloads |>.run ctx
+    (overloads : OverloadTable) (rejectApproximations : Bool := false)
+    : EIO Unit PySpecLaurelResult :=
+  buildPySpecLaurelM pyspecEntries overloads (rejectApproximations := rejectApproximations) |>.run ctx
 
 /-- Read dispatch Ion files and merge their overload tables. -/
 private def readDispatchOverloadsM
@@ -278,6 +281,7 @@ public def resolveAndBuildLaurelPrelude
     (pyspecModules : Array String)
     (stmts : Array (Python.stmt SourceRange))
     (specDir : System.FilePath := ".")
+    (rejectApproximations : Bool := false)
     : Pipeline.PipelineM PySpecLaurelResult := do
   -- Dispatch modules (fatal on invalid name or missing file)
   let dispatchEntries ← resolveModules dispatchModules specDir
@@ -296,6 +300,7 @@ public def resolveAndBuildLaurelPrelude
   -- Explicit pyspec modules (fatal on invalid name or missing file)
   let explicitEntries ← resolveModules pyspecModules specDir
   buildPySpecLaurelM (autoSpecEntries ++ explicitEntries) dispatchOverloads
+    (rejectApproximations := rejectApproximations)
 
 /-! ### Pipeline Steps -/
 
@@ -427,6 +432,7 @@ public def pythonAndSpecToLaurel
     (pyspecModules : Array String := #[])
     (sourcePath : Option String := none)
     (specDir : System.FilePath := ".")
+    (rejectApproximations : Bool := false)
     : Pipeline.PipelineM Laurel.Program := do
   let stmts ← Pipeline.withPhase "readPythonIon" do
     match ← Python.readPythonStrata pythonIonPath |>.toBaseIO with
@@ -436,12 +442,14 @@ public def pythonAndSpecToLaurel
 
   let result ← Pipeline.withPhase "resolveAndBuildPrelude" do
     resolveAndBuildLaurelPrelude dispatchModules pyspecModules stmts specDir
+      (rejectApproximations := rejectApproximations)
 
   let preludeInfo := buildPreludeInfo result
   let metadataPath := sourcePath.getD pythonIonPath
 
   let (laurelProgram, _ctx) ←
-    match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads with
+    match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads
+            (rejectApproximations := rejectApproximations) with
     | .error (.userPythonError range msg) =>
       emitMessageAndAbort (file := sourcePath.getD pythonIonPath) (loc := range)
         .laurelLoweringUserError msg
diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index 0c1a030899..bc1b988c71 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -9,6 +9,7 @@ public import Strata.Languages.Core.Program
 public import Strata.Languages.Laurel.Laurel
 public import Strata.Languages.Python.OverloadTable
 public import Strata.Languages.Python.PythonDialect
+import Strata.Languages.Python.Approximation
 import Strata.Languages.Python.PythonRuntimeLaurelPart
 import Strata.Util.DecideProp
 
@@ -129,6 +130,11 @@ structure TranslationContext where
   classesInHierarchy : Std.HashSet String := {}
   loopBreakLabel : Option String := none
   loopContinueLabel : Option String := none
+  /-- When `true`, every site that would silently emit a `Hole` for a
+      Python construct outside the precise sound subset raises a hard
+      `unsupportedConstruct` error instead. Default is `false` for
+      back-compat; the `--reject-approximations` CLI flag turns it on. -/
+  rejectApproximations : Bool := false
 deriving Inhabited
 
 /-! ## Error Handling -/
@@ -211,6 +217,47 @@ def wildcardModifies : List StmtExprMd := [mkStmtExprMd .All]
 def mkStmtExprMdWithLoc (expr : StmtExpr) (source : Option FileRange) : StmtExprMd :=
   { val := expr, source := source }
 
+/-- Build the `pyAst` payload for an approximation diagnostic.
+    Prefers the source location (cheap, useful) when available; otherwise
+    falls back to a capped AST string so user-facing errors don't grow to
+    multi-kilobyte sizes for deeply nested expressions. -/
+private def approximationAstPayload (source : Option FileRange) (astRepr : String) : String :=
+  match source with
+  | some fr => toString (Std.format fr)
+  | none =>
+    if astRepr.length ≤ 200 then astRepr
+    else (astRepr.toRawSubstring.take 200).toString ++ "…"
+
+/-- Emit a `Hole` (the lax behavior) or raise `unsupportedConstruct`
+    under `--reject-approximations`. Used at every site that would
+    otherwise approximate an unsupported Python construct as a havoc'd
+    Hole. The `construct` argument names the surface form (e.g.,
+    `"BinOp Div"`) for the error message. The optional `source` is
+    stamped on the resulting `Hole` and used to render a short
+    `file:line:col` payload on the rejection error. -/
+def rejectableHole (rejectApproximations : Bool) (construct : String)
+    (source : Option FileRange := none) (astRepr : String := "")
+    : Except TranslationError StmtExprMd :=
+  if rejectApproximations then
+    throw (.unsupportedConstruct
+      (Strata.Python.Approximation.render .hole construct)
+      (approximationAstPayload source astRepr))
+  else
+    pure (mkStmtExprMdWithLoc .Hole source)
+
+/-- Same as `rejectableHole` but for sites that silently drop a Python
+    statement (e.g., `raise`, `try…else`, `for…else`) under lax mode.
+    The error message names the dropped construct. -/
+def rejectableDrop (rejectApproximations : Bool) (construct : String)
+    (source : Option FileRange := none) (astRepr : String := "")
+    : Except TranslationError Unit :=
+  if rejectApproximations then
+    throw (.unsupportedConstruct
+      (Strata.Python.Approximation.render .drop construct)
+      (approximationAstPayload source astRepr))
+  else
+    pure ()
+
 /-- Create a local variable declaration with initializer. -/
 def mkVarDeclInit (name : Identifier) (ty : AstNode HighType) (init : StmtExprMd) : StmtExprMd :=
   mkStmtExprMd (.Assign [mkVariableMd (.Declare ⟨name, ty⟩)] init)
@@ -224,12 +271,17 @@ def manglePythonMethod (className : String) (methodName : String) : String :=
   className ++ "@" ++ methodName
 
 /-- Build a StaticCall for an instance method: ClassName@methodName(self, args...).
-    For Any-typed receivers (no model available), returns a Hole instead. -/
-def mkInstanceMethodCall (className : String) (methodName : String)
+    For Any-typed receivers (no model available), returns a Hole under lax
+    mode, or raises `unsupportedConstruct` under `--reject-approximations`. -/
+def mkInstanceMethodCall (ctx : TranslationContext) (className : String) (methodName : String)
     (self : StmtExprMd) (args : List StmtExprMd)
-    (source : Option FileRange := none) : StmtExprMd :=
-  if className == "Any" then mkStmtExprMdWithLoc .Hole source
-  else mkStmtExprMdWithLoc (StmtExpr.StaticCall (manglePythonMethod className methodName) (self :: args)) source
+    (source : Option FileRange := none) : Except TranslationError StmtExprMd :=
+  if className == "Any" then
+    rejectableHole ctx.rejectApproximations
+      s!"instance method call '{methodName}' on Any-typed receiver"
+      (source := source)
+  else
+    pure (mkStmtExprMdWithLoc (StmtExpr.StaticCall (manglePythonMethod className methodName) (self :: args)) source)
 
 /-- Extract string representation from Python expression (for type annotations) -/
 partial def pyExprToString (e : Python.expr SourceRange) : String :=
@@ -572,21 +624,25 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
 
   -- Bytes literal
   | .Constant _ (.ConBytes _ _) _ =>
-    return mkStmtExprMd .Hole
+    rejectableHole ctx.rejectApproximations
+      "bytes literal" (source := md)
 
   -- Float literal
   | .Constant _ (.ConFloat _ f) _ =>
     match parseFloatString f.val with
     | some d => return floatToAny d
-    | none => return mkStmtExprMd .Hole
+    | none => rejectableHole ctx.rejectApproximations
+                "unparseable float literal" (source := md)
 
   -- Complex literal
   | .Constant _ (.ConComplex _ _ _) _ =>
-    return mkStmtExprMd .Hole
+    rejectableHole ctx.rejectApproximations
+      "complex literal" (source := md)
 
   -- Ellipsis literal
   | .Constant _ (.ConEllipsis _) _ =>
-    return mkStmtExprMd .Hole
+    rejectableHole ctx.rejectApproximations
+      "ellipsis (...) as expression" (source := md)
 
   -- Variable references
   | .Name _ name _ =>
@@ -601,15 +657,19 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       | .Add _ => .ok "PAdd"
       | .Sub _ => .ok "PSub"
       | .Mult _ => .ok "PMul"
-      | .Div _ => return mkStmtExprMd .Hole -- Floating-point are not supported yet
+      | .Div _ => return ← rejectableHole ctx.rejectApproximations
+                              "BinOp Div (true division)" (source := md)
       | .FloorDiv _ => .ok "PFloorDiv"  -- Python // maps to Laurel Div
       | .Mod _ => .ok "PMod"
       | .Pow _ => .ok "PPow"
       | .LShift _ => .ok "PLShift"
       | .RShift _ => .ok "PRShift"
-      | .BitAnd _ => return mkStmtExprMd .Hole --TODO: Adding BitVector subtype in Any type, then the related operations
-      | .BitOr _ => return mkStmtExprMd .Hole
-      | .BitXor _ => return mkStmtExprMd .Hole
+      | .BitAnd _ => return ← rejectableHole ctx.rejectApproximations
+                                "BinOp BitAnd" (source := md)
+      | .BitOr _ => return ← rejectableHole ctx.rejectApproximations
+                               "BinOp BitOr" (source := md)
+      | .BitXor _ => return ← rejectableHole ctx.rejectApproximations
+                                "BinOp BitXor" (source := md)
       -- Unsupported for now
       | _ => throw (.unsupportedConstruct s!"Binary operator not yet supported: {repr op}" (toString (repr e)))
     return mkStmtExprMdWithLoc (StmtExpr.StaticCall preludeOpnames [leftExpr, rightExpr]) md
@@ -764,8 +824,12 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       return mkStmtExprMd (.StaticCall "from_str" [concat])
 
   -- Interpolation / TemplateStr (Python 3.14+ t-strings) - not yet supported
-  | .Interpolation .. => return mkStmtExprMd .Hole
-  | .TemplateStr .. => return mkStmtExprMd .Hole
+  | .Interpolation .. =>
+    rejectableHole ctx.rejectApproximations
+      "string interpolation (t-string)" (source := md)
+  | .TemplateStr .. =>
+    rejectableHole ctx.rejectApproximations
+      "template string (t-string)" (source := md)
 
   | .IfExp _ cond thenb elseb =>
     let condExpr ← translateExpr ctx cond
@@ -833,7 +897,8 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
           -- so standalone reads like `x = self.field` are not silently lost.
           let hasDispatch := ctx.dispatchFieldTypes[className]?.any (·.contains attr.val)
           if hasDispatch then
-            return mkStmtExprMd .Hole
+            rejectableHole ctx.rejectApproximations
+              s!"dispatch field read (self.{attr.val})" (source := md)
           else
             return fieldExpr
         | _ =>
@@ -841,7 +906,8 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       else if isPackage ctx obj then
         -- FIXME: Module attribute (e.g., sys.argv): modules are not modeled as
         -- Laurel values, so return Hole like we do for unmodeled package calls.
-        return mkStmtExprMd .Hole
+        rejectableHole ctx.rejectApproximations
+          "module attribute access" (source := md)
       else
         -- Regular object.field access
         let objExpr ← translateExpr ctx obj
@@ -867,24 +933,34 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
 
   -- Set literal: {1, 2, 3}
   -- Abstract: return havoc'd set (sound abstraction)
-  | .Set .. => return mkStmtExprMd .Hole
+  | .Set .. =>
+    rejectableHole ctx.rejectApproximations
+      "Set literal" (source := md)
 
   -- Tuple literal: (1, 2)
   | .Tuple _ elems _ => translateList ctx elems.val.toList
 
   -- List comprehension: [x for x in items]
   -- Abstract: return havoc'd list (sound abstraction)
-  | .ListComp .. => return mkStmtExprMd .Hole
+  | .ListComp .. =>
+    rejectableHole ctx.rejectApproximations
+      "list comprehension" (source := md)
 
   -- Set comprehension: {x for x in items}
   -- Abstract: return havoc'd set (sound abstraction)
-  | .SetComp .. => return mkStmtExprMd .Hole
+  | .SetComp .. =>
+    rejectableHole ctx.rejectApproximations
+      "set comprehension" (source := md)
 
   -- Dict comprehension: {k: v for k, v in items}
-  | .DictComp .. => return mkStmtExprMd .Hole
+  | .DictComp .. =>
+    rejectableHole ctx.rejectApproximations
+      "dict comprehension" (source := md)
 
   -- Generator expression: (x for x in items)
-  | .GeneratorExp .. => return mkStmtExprMd .Hole
+  | .GeneratorExp .. =>
+    rejectableHole ctx.rejectApproximations
+      "generator expression" (source := md)
 
   | _ => throw (.unsupportedConstruct "Expression type not yet supported" (toString (repr e)))
 
@@ -978,12 +1054,15 @@ The following function return a tuple (translated function name, first argument,
 /-- Coerce an expression to Any if its inferred type is a Composite class.
     Composite values are replaced with a Hole (unconstrained Any value)
     since Composite→Any coercion is not yet modeled. This limits
-    bug-finding ability but avoids type unification errors. -/
+    bug-finding ability but avoids type unification errors.
+    Under `--reject-approximations`, refuse to lower the coercion. -/
 partial def coerceToAny (ctx : TranslationContext) (expr : Python.expr SourceRange)
     (translated : StmtExprMd) : Except TranslationError StmtExprMd := do
   let ty ← inferExprType ctx expr
   if isCompositeType ctx ty then
-    pure <| mkStmtExprMd (.Hole)
+    rejectableHole ctx.rejectApproximations
+      s!"Composite-to-Any coercion ({ty})"
+      (source := sourceRangeToSource ctx.filePath expr.toAst.ann)
   else pure translated
 
 partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr SourceRange) :
@@ -1197,10 +1276,13 @@ partial def translateCall (ctx : TranslationContext)
         | _ => []
       else []
     let havocStmts := receiverHavoc ++ argHavoc
+    let h ← rejectableHole ctx.rejectApproximations
+              s!"unmodeled call to '{funcName}'"
+              (source := sourceRangeToSource ctx.filePath f.toAst.ann)
     if havocStmts.isEmpty then
-      return mkStmtExprMd .Hole
+      return h
     else
-      return mkStmtExprMd (.Block (havocStmts ++ [mkStmtExprMd .Hole]) none)
+      return mkStmtExprMd (.Block (havocStmts ++ [h]) none)
   -- Step 3: translate the resolved call
   let methodName := match f with
     | .Attribute _ _ attr _ => attr.val
@@ -1250,12 +1332,17 @@ partial def translateCall (ctx : TranslationContext)
             -- so the static resolution may be wrong. Emit a Hole in that case.
             let classPrefix := funcName.splitOn "@" |>.head!
             if ctx.classesInHierarchy.contains classPrefix then
-              return mkStmtExprMdWithLoc (.Hole) callMd
-            let callWithSelf := mkStmtExprMdWithLoc
-              (StmtExpr.StaticCall funcName (target_trans :: callArgs)) callMd
-            return callWithSelf
+              rejectableHole ctx.rejectApproximations
+                s!"method call '{funcName}' with uncertain inheritance dispatch"
+                (source := callMd)
+            else
+              let callWithSelf := mkStmtExprMdWithLoc
+                (StmtExpr.StaticCall funcName (target_trans :: callArgs)) callMd
+              return callWithSelf
           else
-            return mkStmtExprMdWithLoc (.Hole) callMd
+            rejectableHole ctx.rejectApproximations
+              s!"method call '{funcName}' on receiver of unknown type"
+              (source := callMd)
         else return mkCall funcName
     | _ => throw (.unsupportedConstruct "Invalid call construct" (toString (repr f)))
   -- When ** is used at the call site and we have a known function signature,
@@ -1489,7 +1576,12 @@ partial def translateAssign  (ctx : TranslationContext)
               let newExpr := mkStmtExprMd (StmtExpr.New resolvedId)
               let varType := mkHighTypeMd (.UserDefined resolvedId)
               let selfRef := mkStmtExprMd (StmtExpr.Var (.Local n.val))
-              let initStmt := mkInstanceMethodCall laurelName "__init__" selfRef args source
+              -- `laurelName` came from `ImportedSymbol.compositeType` so it
+              -- is a concrete class name, never `"Any"`.
+              let initStmt := mkStmtExprMdWithLoc
+                (StmtExpr.StaticCall
+                  (manglePythonMethod laurelName "__init__")
+                  (selfRef :: args)) source
               if n.val ∈ ctx.variableTypes.unzip.1 then
                 let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [target] newExpr) source
                 [assignStmt, initStmt]
@@ -1800,8 +1892,11 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     return (bodyCtx, preamble ++ [ifStmt])
 
   -- While loop
-  | .While _ test body _orelse => do
+  | .While _ test body orelse => do
     -- Note: Python while-else not supported yet
+    if !orelse.val.isEmpty then
+      rejectableDrop ctx.rejectApproximations
+        "while…else clause" (source := md)
     let condExpr ← translateExpr ctx test
     let breakLabel := s!"loop_break_{test.toAst.ann.start.byteIdx}"
     let continueLabel := s!"loop_continue_{test.toAst.ann.start.byteIdx}"
@@ -1892,7 +1987,13 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   | .Import _ _ | .ImportFrom _ _ _ _ |.Pass _ => return (ctx, [])
 
   -- Try/except - wrap body with exception checks and handlers
-  | .Try _ body handlers _ _ => do
+  | .Try _ body handlers orelse finalbody => do
+    if !orelse.val.isEmpty then
+      rejectableDrop ctx.rejectApproximations
+        "try…else clause" (source := md)
+    if !finalbody.val.isEmpty then
+      rejectableDrop ctx.rejectApproximations
+        "try…finally clause" (source := md)
     let tryLabel := s!"try_end_{s.toAst.ann.start.byteIdx}"
     let catchersLabel := s!"exception_handlers_{s.toAst.ann.start.byteIdx}"
     let (bodyCtx, bodyStmts) ← translateStmtList ctx body.val.toList
@@ -1951,7 +2052,9 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
 
   -- FIXME: Placeholder — `raise` is dropped so the Hole type inferrer doesn't
   -- produce Unknown types. Must be replaced to correctly model exceptions later.
-  | .Raise _ _ _ => return (ctx, [])
+  | .Raise _ _ _ => do
+    rejectableDrop ctx.rejectApproximations "raise" (source := md)
+    return (ctx, [])
 
   -- With statement: with EXPR as VAR: BODY
   -- Desugars to: mgr = EXPR; VAR = mgr.__enter__(); BODY; mgr.__exit__()
@@ -1969,8 +2072,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
         let mgrDecl := mkVarDeclInit mgrName mgrLauTy mgrExpr
         let mgrRef := mkStmtExprMd (StmtExpr.Var (.Local mgrName))
         currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(mgrName, mgrTy)]}
-        let enterCall := mkInstanceMethodCall mgrTy "__enter__" mgrRef [] md
-        let exitCall := mkInstanceMethodCall mgrTy "__exit__" mgrRef [] md
+        let enterCall ← mkInstanceMethodCall ctx mgrTy "__enter__" mgrRef [] md
+        let exitCall ← mkInstanceMethodCall ctx mgrTy "__exit__" mgrRef [] md
         match optVars.val with
         | some varExpr =>
           let varName := pyExprToString varExpr
@@ -2004,7 +2107,10 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   -- Note that Any_iter_index(iter, index) should not return an exception when 0 <= index < Any_len(iter)
   -- and Any_iter_index is only called inside the loop body where that condition is satisfied,
   -- so it is sound to not put it inside AnyMaybeExceptionList
-  | .For _ target iter body _orelse _ => do
+  | .For _ target iter body orelse _ => do
+    if !orelse.val.isEmpty then
+      rejectableDrop ctx.rejectApproximations
+        "for…else clause" (source := md)
     -- The iterator expression (we abstract it away).
     -- When the expression contains side-effect statements (e.g. a block with
     -- receiver havoc from an unmodeled method call), bind it to a temporary
@@ -2082,11 +2188,17 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   | .Break _ =>
     match ctx.loopBreakLabel with
     | some lbl => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Exit lbl) md])
-    | none => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := mkStmtExprMd .Hole }) md])
+    | none =>
+      let h ← rejectableHole ctx.rejectApproximations
+        "break outside enclosing loop" (source := md)
+      return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := h }) md])
   | .Continue _ =>
     match ctx.loopContinueLabel with
     | some lbl => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Exit lbl) md])
-    | none => return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := mkStmtExprMd .Hole }) md])
+    | none =>
+      let h ← rejectableHole ctx.rejectApproximations
+        "continue outside enclosing loop" (source := md)
+      return (ctx, [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := h }) md])
 
   -- Augmented assignment: x += expr  →  x = x op expr
   | .AugAssign sr target op value => do
@@ -2811,6 +2923,7 @@ def pythonToLaurel (info : PreludeInfo)
     (body : Array (stmt SourceRange))
     (filePath : String := "")
     (overloadTable : OverloadTable := {})
+    (rejectApproximations : Bool := false)
     : Except TranslationError (Laurel.Program × TranslationContext) := do
   -- Collect user function names (top-level and class methods)
   let userFunctions := body.toList.flatMap fun stmt =>
@@ -2916,7 +3029,8 @@ def pythonToLaurel (info : PreludeInfo)
     compositeTypeReverse := compositeTypeReverse,
     exhaustiveClasses := exhaustiveClasses,
     classesInHierarchy := classesInHierarchy,
-    filePath := filePath
+    filePath := filePath,
+    rejectApproximations := rejectApproximations
   }
 
   -- Separate functions from other statements
diff --git a/Strata/Languages/Python/Specs.lean b/Strata/Languages/Python/Specs.lean
index 92663d1706..8699ee68f2 100644
--- a/Strata/Languages/Python/Specs.lean
+++ b/Strata/Languages/Python/Specs.lean
@@ -7,6 +7,7 @@ module
 
 import        Strata.DDM.Format
 import all    Strata.DDM.Util.Fin
+import        Strata.Languages.Python.Approximation
 import        Strata.Languages.Python.ReadPython
 import        Strata.Languages.Python.Specs.DDM
 public import Strata.Languages.Python.Specs.Decls
@@ -225,6 +226,11 @@ structure PySpecContext where
   /-- Python module name for the current file (e.g., "boto3.dynamodb").
       Used as `pythonModule` for locally-defined classes. -/
   currentModule : ModuleName
+  /-- When `true`, any `specWarning` or `specError` reported during
+      icontract decorator parsing (which today silently falls back to
+      `.placeholder` for unrecognized patterns) is treated as a fatal
+      error by the downstream pipeline. Off by default. -/
+  rejectApproximations : Bool := false
 
 /-- Resolve a module name to a file path, registering the file's FileMap
     for source-location error reporting.  Returns `(filePath, isInit)`
@@ -298,9 +304,15 @@ instance : PySpecMClass PySpecM where
   specError loc message := do
     specErrorAt (←read).pythonFile loc message
   specWarning loc message := do
-    let file := (←read).pythonFile
-    let w : PipelineMessage := { file, loc, phase := pySpecParsingPhase, kind := .pySpecParsingWarning, message }
-    modify fun s => { s with warnings := s.warnings.push w }
+    let ctx ← read
+    -- Under strict mode (`--reject-approximations`), every warning is an
+    -- error: the parser only emits warnings on patterns it falls back to
+    -- `.placeholder` for, which silently drops the user's spec.
+    if ctx.rejectApproximations then
+      specErrorAt ctx.pythonFile loc (Strata.Python.Approximation.render .warningPromotion message)
+    else
+      let w : PipelineMessage := { file := ctx.pythonFile, loc, phase := pySpecParsingPhase, kind := .pySpecParsingWarning, message }
+      modify fun s => { s with warnings := s.warnings.push w }
   runChecked act := do
     let cnt := (←get).errors.size
     let r ← act
@@ -1584,7 +1596,8 @@ def translateModule
     (pythonCmd : String := "python")
     (events : Std.HashSet EventType := {})
     (skipNames : Std.HashSet PythonIdent := {})
-    (currentModulePrefix : Option ModuleName := none) :
+    (currentModulePrefix : Option ModuleName := none)
+    (rejectApproximations : Bool := false) :
     BaseIO (FileMaps × Array Signature × Array PipelineMessage × Array PipelineMessage) := do
   let fmm : FileMaps := {}
   let fmm := fmm.insert pythonFile fileMap
@@ -1600,6 +1613,7 @@ def translateModule
     strataDir := strataDir
     pythonFile := pythonFile
     currentModule := currentModule
+    rejectApproximations := rejectApproximations
   }
   let (res, s) ← translateModuleAux body |>.run ctx |>.run { warnings := #[], errors := #[] }
   let fmm ← fileMapsRef.get
@@ -1612,6 +1626,7 @@ public def translateFile
     (pythonCmd : String := "python")
     (events : Std.HashSet EventType := {})
     (skipNames : Std.HashSet PythonIdent := {})
+    (rejectApproximations : Bool := false)
     : EIO String (Array Signature × Array String) := do
   let mod := moduleName
   -- Compute the package prefix for relative import resolution.
@@ -1645,6 +1660,7 @@ public def translateFile
         (currentModulePrefix := modulePrefix)
         (strataDir := strataDir)
         (pythonFile := pythonFile)
+        (rejectApproximations := rejectApproximations)
         (.ofString contents)
         body
         mod
diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean
index 2f8f07897b..b33c6b4d72 100644
--- a/Strata/Languages/Python/Specs/ToLaurel.lean
+++ b/Strata/Languages/Python/Specs/ToLaurel.lean
@@ -76,6 +76,12 @@ structure ToLaurelContext where
   /-- Module prefix prepended to generated type and procedure names
       to avoid collisions when multiple PySpec files are combined. -/
   modulePrefix : String
+  /-- When `true`, every spec-level approximation (placeholder expression,
+      unsupported `isinstance` / `forall` / float literal, etc.) raises a
+      hard error rather than being silently skipped. The downstream
+      pipeline should fail the build when this flag is on and any errors
+      were reported. Off by default for back-compat. -/
+  rejectApproximations : Bool := false
 
 /-- State for PySpec to Laurel translation. -/
 structure ToLaurelState where
@@ -640,11 +646,12 @@ public structure TranslationResult where
 /-- Run the translation and return a Laurel Program, dispatch table,
     and any errors. -/
 public def signaturesToLaurel (filepath : System.FilePath) (sigs : Array Signature)
-    (moduleName : ModuleName)
+    (moduleName : ModuleName) (rejectApproximations : Bool := false)
     : TranslationResult :=
   let ctx : ToLaurelContext := {
     filepath,
     modulePrefix := moduleName.toString (sep := "_")
+    rejectApproximations
   }
   let ((), state) := (sigs.forM signatureToLaurel).run ctx |>.run {}
   let pgm : Laurel.Program := {
diff --git a/Strata/Pipeline/PyAnalyzeLaurel.lean b/Strata/Pipeline/PyAnalyzeLaurel.lean
index a03fe7d187..cfd8f1b0eb 100644
--- a/Strata/Pipeline/PyAnalyzeLaurel.lean
+++ b/Strata/Pipeline/PyAnalyzeLaurel.lean
@@ -37,6 +37,7 @@ public structure PyAnalyzeConfig where
   isBugFinding : Bool := true
   outputMode : OutputMode := .default
   skipVerification : Bool := false
+  rejectApproximations : Bool := false
   profilePipeline : Bool := true
   metricsHandle : Option IO.FS.Handle := none
 
@@ -45,6 +46,7 @@ private def runPipeline (config : PyAnalyzeConfig)
   let combinedLaurel ← withPhase "pythonAndSpecToLaurel" do
     Strata.pythonAndSpecToLaurel
       (specDir := config.specDir)
+      (rejectApproximations := config.rejectApproximations)
       config.filePath config.dispatchModules config.pyspecModules config.sourcePath
 
   if config.outputMode == .verbose then
diff --git a/Strata/SimpleAPI.lean b/Strata/SimpleAPI.lean
index 449b8e61f7..6de4b4c065 100644
--- a/Strata/SimpleAPI.lean
+++ b/Strata/SimpleAPI.lean
@@ -456,6 +456,7 @@ def pySpecsDir (sourceDir strataDir dialectFile : System.FilePath)
     (skipNames : Array String := #[])
     (warningOutput : WarningOutput := .detail)
     (pythonCmd : String := "python")
+    (rejectApproximations : Bool := false)
     : EIO String Unit := do
   -- Create output dir
   match ← IO.FS.createDirAll strataDir |>.toBaseIO with
@@ -513,7 +514,8 @@ def pySpecsDir (sourceDir strataDir dialectFile : System.FilePath)
     match ← Strata.Python.Specs.translateFile
         dialectFile strataDir pythonFile sourceDir mod
         (events := events) (skipNames := skipIdents)
-        (pythonCmd := pythonCmd) |>.toBaseIO with
+        (pythonCmd := pythonCmd)
+        (rejectApproximations := rejectApproximations) |>.toBaseIO with
     | .error msg =>
       Python.Specs.baseLogEvent events "import" s!"Failed {mod}: {msg}"
       failures := failures.push (toString mod, msg)
diff --git a/StrataMainLib.lean b/StrataMainLib.lean
index 2ca6c87ba2..76a52bab05 100644
--- a/StrataMainLib.lean
+++ b/StrataMainLib.lean
@@ -413,7 +413,9 @@ def pySpecsCommand : Command where
       takesArg := .repeat "name" },
     { name := "module",
       help := "Translate only the named module (dot-separated). May be repeated.",
-      takesArg := .repeat "module" }
+      takesArg := .repeat "module" },
+    { name := "reject-approximations",
+      help := "Reject every spec construct silently lowered to a placeholder or warning. Off by default." }
   ]
   help := "Translate Python specification files in a directory into Strata DDM Ion format. If --module is given, translates only those modules; otherwise translates all .py files. Creates subdirectories as needed. (Experimental)"
   callback := fun v pflags => do
@@ -427,6 +429,7 @@ def pySpecsCommand : Command where
     let modules := pflags.getRepeated "module"
     let warningOutput : Strata.WarningOutput :=
       if quiet then .none else .detail
+    let rejectApproximations := pflags.getBool "reject-approximations"
     -- Serialize embedded dialect for Python subprocess
     IO.FS.withTempFile fun _handle dialectFile => do
       IO.FS.writeBinFile dialectFile Strata.Python.Python.toIon
@@ -434,6 +437,7 @@ def pySpecsCommand : Command where
                 (skipNames := skipNames)
                 (modules := modules)
                 (warningOutput := warningOutput)
+                (rejectApproximations := rejectApproximations)
                 v[0] v[1] dialectFile |>.toBaseIO
       match r with
       | .ok () => pure ()
@@ -623,6 +627,9 @@ def pyAnalyzeLaurelCommand : Command where
               takesArg := .arg "file" },
             { name := "skip-verification",
               help := "Run Python-to-Laurel and Laurel-to-Core translation only (skip SMT verification).",
+              takesArg := .none },
+            { name := "reject-approximations",
+              help := "Reject every Python construct currently approximated as a havoc'd Hole or silently dropped. First error stops translation. Off by default.",
               takesArg := .none }]
   help := "Verify a Python Ion program via the Laurel pipeline. Translates Python to Laurel to Core, then runs SMT verification."
   callback := fun v pflags => do
@@ -685,6 +692,7 @@ def pyAnalyzeLaurelCommand : Command where
       else if quiet then .quiet
       else .default
     let skipVerification := pflags.getBool "skip-verification"
+    let rejectApproximations := pflags.getBool "reject-approximations"
 
     -- Run the pipeline
     let (outcome, laurelPassStats, pctx) ← Strata.Pipeline.runPyAnalyzePipeline {
@@ -693,7 +701,7 @@ def pyAnalyzeLaurelCommand : Command where
       keepAllFilesPrefix := keepPrefix
       verifyOptions := options
       entryPoint, isBugFinding
-      outputMode, skipVerification
+      outputMode, skipVerification, rejectApproximations
       metricsHandle
     }
 
diff --git a/StrataTest/Languages/Python/RejectApproximationsTest.lean b/StrataTest/Languages/Python/RejectApproximationsTest.lean
new file mode 100644
index 0000000000..c114263aca
--- /dev/null
+++ b/StrataTest/Languages/Python/RejectApproximationsTest.lean
@@ -0,0 +1,130 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Python.Approximation
+import Strata.Languages.Python.PythonToLaurel
+
+/-! # `--reject-approximations` flag tests
+
+Unit tests for the `rejectableHole` / `rejectableDrop` helpers: with
+the flag off, they emit a `Hole` / no-op (lax behavior); with the flag
+on, they raise `unsupportedConstruct` with an `[approximation]` tag.
+-/
+
+namespace Strata.Python.RejectApproximationsTest
+
+open Strata.Python (rejectableHole rejectableDrop)
+open Strata.Python.TranslationError
+
+/-! ## Boolean dispatch lemmas
+
+Pin the bool branch of `rejectableHole` / `rejectableDrop` so a future
+refactor cannot accidentally reverse the strict/lax meaning. -/
+
+theorem rejectableHole_strict (c : String) (r : String) :
+    (rejectableHole (rejectApproximations := true) c (astRepr := r)).isOk = false := rfl
+
+theorem rejectableHole_lax (c : String) (r : String) :
+    (rejectableHole (rejectApproximations := false) c (astRepr := r)).isOk = true := rfl
+
+theorem rejectableDrop_strict (c : String) (r : String) :
+    (rejectableDrop (rejectApproximations := true) c (astRepr := r)).isOk = false := rfl
+
+theorem rejectableDrop_lax (c : String) (r : String) :
+    (rejectableDrop (rejectApproximations := false) c (astRepr := r)).isOk = true := rfl
+
+/-- Strict mode produces a `.unsupportedConstruct` whose message starts
+    with `Approximation.prefixTag`. Downstream tooling can rely on this. -/
+theorem rejectableHole_strict_message (c : String) (r : String) :
+    ∃ msg ast,
+      rejectableHole (rejectApproximations := true) c (astRepr := r)
+        = .error (.unsupportedConstruct msg ast)
+      ∧ msg = Strata.Python.Approximation.render .hole c :=
+  ⟨_, _, rfl, rfl⟩
+
+theorem rejectableDrop_strict_message (c : String) (r : String) :
+    ∃ msg ast,
+      rejectableDrop (rejectApproximations := true) c (astRepr := r)
+        = .error (.unsupportedConstruct msg ast)
+      ∧ msg = Strata.Python.Approximation.render .drop c :=
+  ⟨_, _, rfl, rfl⟩
+
+-- rejectableHole false -> emits a Hole (lax behavior preserved)
+#guard
+  match rejectableHole false "BinOp Div" (astRepr := "<ast>") with
+  | .ok ⟨.Hole, _⟩ => true
+  | _ => false
+
+-- rejectableHole true -> raises unsupportedConstruct with [approximation] tag
+#guard
+  match rejectableHole true "BinOp Div" (astRepr := "<ast>") with
+  | .error (.unsupportedConstruct msg _) =>
+      msg.startsWith "[approximation]" && (msg.splitOn "BinOp Div").length > 1
+  | _ => false
+
+-- rejectableDrop false -> no-op
+#guard
+  match rejectableDrop false "raise" (astRepr := "<ast>") with
+  | .ok () => true
+  | _ => false
+
+-- rejectableDrop true -> raises with "silently dropped" wording
+#guard
+  match rejectableDrop true "raise" (astRepr := "<ast>") with
+  | .error (.unsupportedConstruct msg _) =>
+      msg.startsWith "[approximation]"
+        && (msg.splitOn "silently dropped").length > 1
+  | _ => false
+
+-- astRepr longer than 200 chars is truncated with an ellipsis
+#guard
+  let big := String.ofList (List.replicate 500 'x')
+  match rejectableHole true "huge" (astRepr := big) with
+  | .error (.unsupportedConstruct _ payload) =>
+      payload.length < big.length && payload.endsWith "…"
+  | _ => false
+
+-- a `source` is preferred over the AST repr for the diagnostic payload
+#guard
+  let fr : Strata.FileRange := ⟨.file "f.py", ⟨⟨10⟩, ⟨20⟩⟩⟩
+  match rejectableHole true "x" (source := some fr) (astRepr := "huge") with
+  | .error (.unsupportedConstruct _ payload) =>
+      (payload.splitOn "huge").length == 1
+        && (payload.splitOn "f.py").length > 1
+  | _ => false
+
+/-! ## Shared `Approximation.render` format
+
+All three approximation sites — `rejectableHole`, `rejectableDrop`, and
+`Specs.lean`'s `specWarning` warning→error promotion — render through
+`Strata.Python.Approximation.render`. The guards below pin the prefix
+and per-kind wording so the three sites cannot drift apart. -/
+
+open Strata.Python.Approximation (render Kind prefixTag)
+
+#guard (render .hole "BinOp Div").startsWith prefixTag
+#guard (render .drop "raise").startsWith prefixTag
+#guard (render .warningPromotion "fallback to placeholder").startsWith prefixTag
+
+#guard prefixTag == "[approximation] "
+
+#guard ((render .hole "X").splitOn "approximated as Hole").length > 1
+#guard ((render .drop "X").splitOn "silently dropped").length > 1
+#guard render .warningPromotion "msg" == "[approximation] msg"
+
+-- The strict-mode arm of `rejectableHole` shares wording with `render .hole`.
+#guard
+  match rejectableHole true "X" with
+  | .error (.unsupportedConstruct msg _) => msg == render .hole "X"
+  | _ => false
+
+-- Likewise for `rejectableDrop`.
+#guard
+  match rejectableDrop true "X" with
+  | .error (.unsupportedConstruct msg _) => msg == render .drop "X"
+  | _ => false
+
+end Strata.Python.RejectApproximationsTest