diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 8c8f02ab14..be167466a4 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -1069,6 +1069,18 @@ def label (o : VCOutcome) (property : Imperative.PropertyType)
         | .unsat => "pass"
         | .sat _ => "fail"
         | .unknown _ | .err _ => "unknown"
+      else if checkMode == .bugFinding then
+        -- `bugFinding` runs the satisfiability check only (see the check
+        -- selection at `verifySingleEnv`), so matching on
+        -- `satisfiabilityProperty` had no case that could report a
+        -- non-bug: every goal came out `satisfiable` or `unknown` and was
+        -- then counted as failed. Classify with the mode-aware predicates
+        -- instead. `bugFindingAssumingCompleteSpec` runs both checks and
+        -- keeps its existing labels, because `bugFindingSuccess` encodes
+        -- only the `bugFinding` column of docs/VerificationModes.md.
+        if o.bugFindingFailure then "fail"
+        else if o.bugFindingSuccess then "no definite bug"
+        else "unknown"
       else
         match o.satisfiabilityProperty with
         | .sat _ => "satisfiable"
@@ -1105,6 +1117,11 @@ def emoji (o : VCOutcome) (property : Imperative.PropertyType)
         | .unsat => "✅"
         | .sat _ => "❌"
         | .unknown _ | .err _ => "❓"
+      else if checkMode == .bugFinding then
+        -- See the matching comment in `label` above.
+        if o.bugFindingFailure then "❌"
+        else if o.bugFindingSuccess then "✅"
+        else "❓"
       else
         match o.satisfiabilityProperty with
         | .sat _ => "❓"
diff --git a/StrataTest/Languages/Core/VCOutcomeTests.lean b/StrataTest/Languages/Core/VCOutcomeTests.lean
index fcbc62aa75..c7177ca747 100644
--- a/StrataTest/Languages/Core/VCOutcomeTests.lean
+++ b/StrataTest/Languages/Core/VCOutcomeTests.lean
@@ -146,6 +146,34 @@ Sat:unknown|Val:unknown ❓ unknown, Unknown (solver timeout or incomplete), SAR
 #guard outcomeToLevel .bugFindingAssumingCompleteSpec .assert (mkOutcome (.sat []) .unsat) = Strata.Sarif.Level.none
 #guard outcomeToLevel .bugFindingAssumingCompleteSpec .assert (mkOutcome .unknown (.sat [])) = Strata.Sarif.Level.error
 
+/-! ### `bugFinding` at the `minimal` check level
+
+`bugFinding` runs the satisfiability check only, so `validityProperty` is
+`unknown` on every goal. Classify with `bugFindingSuccess`/`bugFindingFailure`
+so a goal that is not a definite bug is not labelled a failure. -/
+
+#guard (mkOutcome (.sat []) .unknown).label .assert .minimal .bugFinding
+  = "no definite bug"
+#guard (mkOutcome (.sat []) .unknown).emoji .assert .minimal .bugFinding = "✅"
+#guard (mkOutcome .unsat .unknown).label .assert .minimal .bugFinding = "fail"
+#guard (mkOutcome .unsat .unknown).emoji .assert .minimal .bugFinding = "❌"
+#guard (mkOutcome .unknown .unknown).label .assert .minimal .bugFinding
+  = "unknown"
+#guard (mkOutcome .unknown .unknown).emoji .assert .minimal .bugFinding = "❓"
+
+/-! ### `minimal` labels for the other two modes are unchanged
+
+`bugFindingAssumingCompleteSpec` runs both checks and treats any
+counterexample as an error, so it keeps the satisfiability-based labels. -/
+
+#guard (mkOutcome (.sat []) (.sat [])).label .assert .minimal
+  .bugFindingAssumingCompleteSpec = "satisfiable"
+#guard (mkOutcome .unsat (.sat [])).label .assert .minimal
+  .bugFindingAssumingCompleteSpec = "fail"
+#guard (mkOutcome (.sat []) .unsat).label .assert .minimal .deductive = "pass"
+#guard (mkOutcome (.sat []) (.sat [])).label .assert .minimal .deductive
+  = "fail"
+
 /-! ### Outcome table verification -/
 
 private def printOutcomeRow (sat val : Imperative.SMT.Result (Ident := Core.Expression.Ident)) : IO Unit := do