diff --git a/StrataMain.lean b/StrataMain.lean
index 179d04a6c0..5ffcf348a8 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -656,7 +656,21 @@ def pyAnalyzeLaurelCommand : Command where
     let coreProgram ←
       match coreProgramOption with
       | none =>
-        exitPyAnalyzeInternalError s!"Laurel to Core translation failed: {laurelTranslateErrors}"
+        let msg := s!"Laurel to Core translation failed: {laurelTranslateErrors}"
+        -- Classify by worst-severity diagnostic: StrataBug (tool bug) outranks
+        -- UserError (user-actionable) outranks NotYetImplemented (wait-for-support).
+        -- An empty list or warnings-only failure with `coreProgramOption = none`
+        -- is itself a tool bug (translation should not silently fail).
+        if laurelTranslateErrors.isEmpty
+            ∨ laurelTranslateErrors.any (·.type == .StrataBug) then
+          exitPyAnalyzeInternalError msg
+        else if laurelTranslateErrors.any (·.type == .UserError) then
+          exitPyAnalyzeUserError msg
+        else if laurelTranslateErrors.any (·.type == .NotYetImplemented) then
+          exitPyAnalyzeKnownLimitation msg
+        else
+          -- Only warnings, but translation failed → unexpected.
+          exitPyAnalyzeInternalError msg
       | some core => pure core
 
     if verbose then