diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index d6cbbd7c98..5a2e9f8f5f 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -1736,18 +1736,26 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     let summary := match msg.val with
       | some (.Constant _ (.ConString _ str) _) => some str.val
       | _ => none
-    -- Check if condition contains a Hole - if so, hoist to variable
-    let (condStmts, finalCondExpr, condCtx) :=
+    -- Hoist unmodelled conditions (e.g. isinstance(...)) into a fresh
+    -- bool-typed variable. The `alreadyBool` flag records, at the point of
+    -- construction, whether `finalCondExpr` is statically known to have type
+    -- bool -- avoiding a fragile round-trip through `variableTypes` later.
+    -- See #1102.
+    let (condStmts, finalCondExpr, condCtx, alreadyBool) :=
       match condExpr.val with
       | .Hole =>
         let freshVar := s!"assert_cond_{test.toAst.ann.start.byteIdx}"
         let varType := mkHighTypeMd .TBool
         let varDecl := mkVarDeclInit freshVar varType condExpr
         let varRef := mkStmtExprMd (StmtExpr.Var (.Local freshVar))
-        ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] })
-      | _ => ([], condExpr, ctx)
-
-    let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := Any_to_bool finalCondExpr, summary }) md
+        ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, PyLauType.Bool)] }, true)
+      | _ => ([], condExpr, ctx, false)
+
+    -- Skip Any_to_bool when the condition is already a bool-typed local;
+    -- wrapping it would produce ill-typed Any_to_bool(bool). See #1102.
+    let coercedCond :=
+      if alreadyBool then finalCondExpr else Any_to_bool finalCondExpr
+    let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert { condition := coercedCond, summary }) md
 
     -- Wrap in block if we hoisted condition
     let result := if condStmts.isEmpty then
diff --git a/StrataTestExtra/Languages/Python/Issue1102/isinstance_if.py b/StrataTestExtra/Languages/Python/Issue1102/isinstance_if.py
new file mode 100644
index 0000000000..08877c0321
--- /dev/null
+++ b/StrataTestExtra/Languages/Python/Issue1102/isinstance_if.py
@@ -0,0 +1,6 @@
+def main():
+    x: int = 5
+    if isinstance(x, int):
+        assert x > 0
+
+main()
diff --git a/StrataTestExtra/Languages/Python/Issue1102/isinstance_int.py b/StrataTestExtra/Languages/Python/Issue1102/isinstance_int.py
new file mode 100644
index 0000000000..224d6f3f83
--- /dev/null
+++ b/StrataTestExtra/Languages/Python/Issue1102/isinstance_int.py
@@ -0,0 +1,4 @@
+def main():
+    assert isinstance(5, int)
+
+main()
diff --git a/StrataTestExtra/Languages/Python/Issue1102/isinstance_list.py b/StrataTestExtra/Languages/Python/Issue1102/isinstance_list.py
new file mode 100644
index 0000000000..19d5959fd2
--- /dev/null
+++ b/StrataTestExtra/Languages/Python/Issue1102/isinstance_list.py
@@ -0,0 +1,4 @@
+def main():
+    assert isinstance([1], list)
+
+main()
diff --git a/StrataTestExtra/Languages/Python/Issue1102Test.lean b/StrataTestExtra/Languages/Python/Issue1102Test.lean
new file mode 100644
index 0000000000..942444ec75
--- /dev/null
+++ b/StrataTestExtra/Languages/Python/Issue1102Test.lean
@@ -0,0 +1,77 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Languages.Python.TestExamples
+import StrataTest.Util.TestDiagnostics
+
+open StrataTest.Util
+open Strata.Python (processPythonFile withPython)
+open Strata.Parser (stringInputContext)
+open Strata
+
+namespace Strata.Python.Issue1102
+
+/-! Regression test for #1102: `isinstance(...)` inside `assert` must not
+crash the Python-to-Laurel-to-Core translation pipeline. Before the fix
+these programs failed in Laurel type checking with
+"Impossible to unify (arrow Any bool) with (arrow bool $__ty…)".
+
+Each fixture snapshots both the diagnostic `type` and the full rendered
+message, so a silent-drop regression (translating the assert to a no-op)
+or a message reword would also fail. Fixtures live in `Issue1102/`.
+
+Note: compound assert conditions such as `isinstance(x, T) and x > 0` or
+`not isinstance(x, T)` currently trip a *separate* StrataBug ("block
+expression should have been lowered in a separate pass") that is
+independent of #1102 and should be tracked in its own issue. -/
+
+private meta def fixtureDir : System.FilePath :=
+  "StrataTestExtra/Languages/Python/Issue1102"
+
+/-- Render a diagnostic as a single deterministic line:
+"type @ line:colStart-colEnd :: message". -/
+private def renderDiag (d : Diagnostic) : String :=
+  s!"{repr d.type} @ {d.start.line}:{d.start.column}-{d.ending.column} :: {d.message}"
+
+/-- Load a fixture and print each diagnostic on its own line, prefixed
+with the fixture name. Prefer this over ad-hoc prose filters: it asserts
+structurally on `type` and keeps the full message in the snapshot. -/
+private def snapshotDiags (pythonCmd : System.FilePath) (pyFile : String) : IO Unit := do
+  let path := fixtureDir / pyFile
+  let source ← IO.FS.readFile path
+  let diags ← processPythonFile pythonCmd (stringInputContext pyFile source)
+  for d in diags do
+    IO.println s!"{pyFile}: {renderDiag d}"
+  -- Belt-and-braces structural check: any StrataBug is a regression.
+  if diags.any (fun d => d.type == Strata.DiagnosticType.StrataBug) then
+    throw <| .userError s!"{pyFile}: unexpected StrataBug diagnostic"
+
+-- `assert isinstance(5, int)` — the minimal fuzz reproduction. Before
+-- the fix this raised a Laurel type error; after the fix the pipeline
+-- completes and the verifier reports the assertion as unprovable
+-- (expected, since `isinstance` is unmodelled).
+/--
+info: isinstance_int.py: Strata.DiagnosticType.UserError @ 2:4-29 :: assertion could not be proved
+-/
+#guard_msgs in
+#eval withPython fun pythonCmd => snapshotDiags pythonCmd "isinstance_int.py"
+
+-- `assert isinstance([1], list)` — the original fuzz_semantic_0004 shape.
+/--
+info: isinstance_list.py: Strata.DiagnosticType.UserError @ 2:4-32 :: assertion could not be proved
+-/
+#guard_msgs in
+#eval withPython fun pythonCmd => snapshotDiags pythonCmd "isinstance_list.py"
+
+-- `if isinstance(x, int): assert x > 0` — the non-hoisting .If path,
+-- included to show the fix does not affect the path that already worked.
+/--
+info: isinstance_if.py: Strata.DiagnosticType.UserError @ 4:8-20 :: assertion could not be proved
+-/
+#guard_msgs in
+#eval withPython fun pythonCmd => snapshotDiags pythonCmd "isinstance_if.py"
+
+end Strata.Python.Issue1102