diff --git a/Specimen/DeriveConstrainedProducer.lean b/Specimen/DeriveConstrainedProducer.lean
index 4455630..df4b3e9 100644
--- a/Specimen/DeriveConstrainedProducer.lean
+++ b/Specimen/DeriveConstrainedProducer.lean
@@ -896,21 +896,25 @@ def deriveConstrainedProducer
     constrainingInductive inductiveLevels freshArgIdents freshenedOutputNames.toList
     outputTypes.toList producerSort localCtx
 
-/-- Compile a schedule to a weighted sub-producer term. Handles the common pattern of:
-    schedule → MExp → TSyntax, then wrapping with the weight function for the backtracking
-    combinator. Returns the compiled term and whether it should go in the recursive bucket. -/
-private def compileWeightedProducer
+/-- Compile a schedule to a sub-producer term (no weight wrapper).
+    Returns the compiled generator/enumerator/checker body. -/
+private def compileSubProducer
     (schedule : List ScheduleStep × ScheduleSort)
     (outputType : Expr) (deriveSort : DeriveSort)
-    (fuelPrimeName sizePrimeName targetInductive : Name)
-    (weightFnIdent : Ident) (modifierIdent : Option Ident)
-    (ctorName : Name) (outputIndices : List Nat)
-    (badness : Float) (isRecursive : Bool)
-    (freshSize' numBaseLit numRecLit : TSyntax `term) : TermElabM (TSyntax `term) := do
+    (fuelPrimeName sizePrimeName targetInductive : Name) : TermElabM (TSyntax `term) := do
   let (subProducer, _) ← StateT.run (s := #[]) (do
     let mexp ← MExp.scheduleToMExp schedule (.MId `size) (.MId `initSize) outputType
       (fuelPrimeName := fuelPrimeName) (sizePrimeName := sizePrimeName) (targetInductive := targetInductive)
     MExp.mexpToTSyntax mexp deriveSort)
+  return subProducer
+
+/-- Wrap a compiled sub-producer with a weight annotation for the backtracking combinator. -/
+private def wrapWithWeight
+    (subProducer : TSyntax `term) (deriveSort : DeriveSort)
+    (weightFnIdent : Ident) (modifierIdent : Option Ident)
+    (ctorName : Name) (outputIndices : List Nat)
+    (badness : Float) (isRecursive : Bool)
+    (sizeTerm numBaseLit numRecLit : TSyntax `term) : TermElabM (TSyntax `term) := do
   let badnessLit := Syntax.mkScientificLit (toString badness)
   let ctorNameLit := Lean.quote ctorName
   let outputIndicesLit := Lean.quote outputIndices
@@ -921,22 +925,30 @@ private def compileWeightedProducer
     | .Theorem => `(Schedules.DeriveSort.Theorem)
   match deriveSort with
   | .Generator =>
-    let baseWeight ←
-      if isRecursive then
-        `($weightFnIdent $ctorNameLit $outputIndicesLit $deriveSortLit $badnessLit true $freshSize' $numBaseLit $numRecLit)
-      else
-        `($weightFnIdent $ctorNameLit $outputIndicesLit $deriveSortLit $badnessLit false 0 $numBaseLit $numRecLit)
+    let isRecLit := Lean.quote isRecursive
+    let baseWeight ← `($weightFnIdent $ctorNameLit $outputIndicesLit $deriveSortLit $badnessLit $isRecLit $sizeTerm $numBaseLit $numRecLit)
     let finalWeight ← match modifierIdent with
       | none => pure baseWeight
       | some modIdent =>
-        if isRecursive then
-          `($modIdent $baseWeight $ctorNameLit $outputIndicesLit $deriveSortLit $badnessLit true $freshSize' $numBaseLit $numRecLit)
-        else
-          `($modIdent $baseWeight $ctorNameLit $outputIndicesLit $deriveSortLit $badnessLit false 0 $numBaseLit $numRecLit)
+        `($modIdent $baseWeight $ctorNameLit $outputIndicesLit $deriveSortLit $badnessLit $isRecLit $sizeTerm $numBaseLit $numRecLit)
     `( ($finalWeight, $subProducer) )
   | .Enumerator => pure subProducer
   | .Checker | .Theorem => `(fun (_ : Unit) => $subProducer)
 
+/-- Compile a schedule to a weighted sub-producer term. Handles the common pattern of:
+    schedule → MExp → TSyntax, then wrapping with the weight function for the backtracking
+    combinator. Returns the compiled term and whether it should go in the recursive bucket. -/
+private def compileWeightedProducer
+    (schedule : List ScheduleStep × ScheduleSort)
+    (outputType : Expr) (deriveSort : DeriveSort)
+    (fuelPrimeName sizePrimeName targetInductive : Name)
+    (weightFnIdent : Ident) (modifierIdent : Option Ident)
+    (ctorName : Name) (outputIndices : List Nat)
+    (badness : Float) (isRecursive : Bool)
+    (freshSize' numBaseLit numRecLit : TSyntax `term) : TermElabM (TSyntax `term) := do
+  let subProducer ← compileSubProducer schedule outputType deriveSort fuelPrimeName sizePrimeName targetInductive
+  wrapWithWeight subProducer deriveSort weightFnIdent modifierIdent ctorName outputIndices badness isRecursive freshSize' numBaseLit numRecLit
+
 /-- Walk a ConstructorExpr tree and collect which type params it references. -/
 def extractTypeParamRefs (typeParams : Std.HashSet Name) : ConstructorExpr → Std.HashSet Name
   | .Unknown n => if typeParams.contains n then Std.HashSet.ofList [n] else {}
@@ -1283,15 +1295,30 @@ def compileInductiveSchedule (indSched : InductiveSchedule)
     let numRec := indSched.recSchedules.length + numBaseMutual.length
     let numBaseLit := Syntax.mkNumLit (toString numBase)
     let numRecLit := Syntax.mkNumLit (toString numRec)
+    -- Non-recursive producers get different weight terms in the two size branches:
+    -- - size=0 branch (baseProducers): size' is unbound, use literal 0
+    -- - size>0 branch (inductiveProducers): size' is bound, pass it through
+    -- The sub-producer body is compiled once and wrapped with weights for each branch.
+    let mut nonRecProducersForBase : Array (TSyntax `term) := #[]
+    let freshSizeZero ← `((0 : Nat))
     for (ctorName, schedule) in indSched.baseSchedules do
       let (steps, sort) := schedule
       let rewrittenSteps := rewriteSchedule steps
       let isRec := scheduleUsesMutualCall rewrittenSteps
-      let term ← compileWeightedProducer (rewrittenSteps, sort) outputType key.deriveSort
-        freshFuelPrimeName freshSizePrimeName key.inductiveName
-        weightFnIdent modifierIdent ctorName key.outputIndices (lookupCtorBadness ctorName) isRec freshSize' numBaseLit numRecLit
-      if isRec then recursiveProducers := recursiveProducers.push term
-      else nonRecursiveProducers := nonRecursiveProducers.push term
+      if isRec then
+        let term ← compileWeightedProducer (rewrittenSteps, sort) outputType key.deriveSort
+          freshFuelPrimeName freshSizePrimeName key.inductiveName
+          weightFnIdent modifierIdent ctorName key.outputIndices (lookupCtorBadness ctorName) true freshSize' numBaseLit numRecLit
+        recursiveProducers := recursiveProducers.push term
+      else
+        let subProducer ← compileSubProducer (rewrittenSteps, sort) outputType key.deriveSort
+          freshFuelPrimeName freshSizePrimeName key.inductiveName
+        let termInductive ← wrapWithWeight subProducer key.deriveSort
+          weightFnIdent modifierIdent ctorName key.outputIndices (lookupCtorBadness ctorName) false freshSize' numBaseLit numRecLit
+        nonRecursiveProducers := nonRecursiveProducers.push termInductive
+        let termBase ← wrapWithWeight subProducer key.deriveSort
+          weightFnIdent modifierIdent ctorName key.outputIndices (lookupCtorBadness ctorName) false freshSizeZero numBaseLit numRecLit
+        nonRecProducersForBase := nonRecProducersForBase.push termBase
     for (ctorName, schedule) in indSched.recSchedules do
       let (steps, sort) := schedule
       let term ← compileWeightedProducer (rewriteSchedule steps, sort) outputType key.deriveSort
@@ -1306,13 +1333,13 @@ def compileInductiveSchedule (indSched : InductiveSchedule)
         match key.deriveSort with
         | .Checker | .Theorem =>
           let failsafe ← `((fun (_ : Unit) => $failFn $genericFailure))
-          pure (nonRecursiveProducers.push failsafe)
+          pure (nonRecProducersForBase.push failsafe)
         | .Enumerator =>
           let failsafe ← `($failFn $genericFailure)
-          pure (nonRecursiveProducers.push failsafe)
-        | .Generator => pure nonRecursiveProducers
+          pure (nonRecProducersForBase.push failsafe)
+        | .Generator => pure nonRecProducersForBase
       else
-        pure nonRecursiveProducers
+        pure nonRecProducersForBase
     let baseProducers ← `([$baseProducersWithFailsafe,*])
     let allProducers := nonRecursiveProducers ++ recursiveProducers
     let inductiveProducers ← `([$allProducers,*])
diff --git a/Specimen/Scoring.lean b/Specimen/Scoring.lean
index b5ab297..2615ab4 100644
--- a/Specimen/Scoring.lean
+++ b/Specimen/Scoring.lean
@@ -1454,4 +1454,157 @@ initialize do
   registerScoringBundle { base with wholeScheduleScorer := some sourceQualityWholeScheduleScorer }
 
 
+----------------------------------------------
+-- Built-in: RecAwareGradedScore
+-- Like GradedUniformDensityScore but with a RecursionKind axis that
+-- distinguishes direct recursion (Source.Rec) from same-inductive
+-- cross-mode calls (Source.NonRec targeting the same inductive with
+-- different output indices or derive sort). Direct recursion is
+-- preferred as the simpler pattern when both are available.
+----------------------------------------------
+
+inductive RecursionKind
+  | None
+  | Direct
+  | Mutual
+  deriving Repr, BEq, Inhabited
+
+namespace RecursionKind
+
+def toNat : RecursionKind → Nat
+  | .None => 0
+  | .Direct => 1
+  | .Mutual => 2
+
+instance : Ord RecursionKind where
+  compare a b := compare a.toNat b.toNat
+
+def max (a b : RecursionKind) : RecursionKind :=
+  if a.toNat ≥ b.toNat then a else b
+
+end RecursionKind
+
+structure RecAwareGradedScore where
+  density        : Density := .Total
+  recursionKind  : RecursionKind := .None
+  checkSpeed     : CheckSpeed := .NotACheck
+  passLikelihood : PassLikelihood := .Certain
+  varDeps        : Nat := 0
+  deriving Repr, BEq, Inhabited
+
+deriving instance TypeName for RecAwareGradedScore
+
+instance : Ord RecAwareGradedScore where
+  compare a b :=
+    match compare a.density.toNat b.density.toNat with
+    | .eq => match compare a.recursionKind.toNat b.recursionKind.toNat with
+      | .eq => match compare a.checkSpeed.toNat b.checkSpeed.toNat with
+        | .eq => match compare a.passLikelihood.toNat b.passLikelihood.toNat with
+          | .eq => compare a.varDeps b.varDeps
+          | r => r
+        | r => r
+      | r => r
+    | r => r
+
+instance : LT RecAwareGradedScore := ltOfOrd
+
+instance : Scorable RecAwareGradedScore where
+  empty := {}
+  combine a b :=
+    { density := Density.max a.density b.density
+      recursionKind := RecursionKind.max a.recursionKind b.recursionKind
+      checkSpeed := CheckSpeed.max a.checkSpeed b.checkSpeed
+      passLikelihood := PassLikelihood.max a.passLikelihood b.passLikelihood
+      varDeps := a.varDeps + b.varDeps }
+  isBetter a b := a < b
+  bestOf scores := scores.foldl (fun acc s => if s < acc then s else acc) (scores.headD {})
+  uncoveredPenalty := { density := .Partial, varDeps := 0 }
+  worst := { density := .Checking, recursionKind := .Mutual, checkSpeed := .Recursive, passLikelihood := .Desperate, varDeps := 1000 }
+  badness s :=
+    let varDepPenalty := min 0.05 (s.varDeps.toFloat * 0.01)
+    let recPenalty := s.recursionKind.toNat.toFloat * 0.15
+    if s.density != .Checking then
+      let level := s.density.toNat.toFloat / 4.0
+      min 1.0 (level + recPenalty + varDepPenalty)
+    else
+      let speedVal := match s.checkSpeed with
+        | .NotACheck => 0.0 | .Decidable => 0.0 | .Moderate => 0.33
+        | .Expensive => 0.66 | .Recursive => 1.0
+      let likelVal := match s.passLikelihood with
+        | .Certain => 0.0 | .Likely => 0.0 | .Moderate => 0.33
+        | .Unlikely => 0.66 | .Desperate => 1.0
+      let severity := max speedVal likelVal * 0.7 + min speedVal likelVal * 0.3
+      min 1.0 (0.75 + severity * 0.25 + recPenalty + varDepPenalty)
+
+private def classifyRecursionKind (key : SpecKey)
+    (src : Source) (outputs : List (Name × Option ConstructorExpr)) (prodSort : ProducerSort) : RecursionKind :=
+  match src with
+  | .Rec .. => .Direct
+  | .MutRec .. => .Mutual
+  | .NonRec (indName, args) =>
+    if indName != key.inductiveName then .None
+    else
+      let outputIdxs := outputs.filterMap fun (n, _) =>
+        args.findIdx? fun a => match a with | .Unknown v => v == n | _ => false
+      let depDeriveSort := match prodSort with
+        | .Enumerator => DeriveSort.Enumerator
+        | .Generator => DeriveSort.Generator
+      let depKey : SpecKey := { inductiveName := indName, outputIndices := outputIdxs, deriveSort := depDeriveSort }
+      if depKey == key then .Direct
+      else .Mutual
+
+private def classifyRecursionKindCheck (key : SpecKey) (src : Source) : RecursionKind :=
+  match src with
+  | .Rec .. => .Direct
+  | .MutRec .. => .Mutual
+  | .NonRec (indName, _args) =>
+    if indName != key.inductiveName then .None
+    else
+      if key.deriveSort == .Checker && key.outputIndices.isEmpty then .Direct
+      else .Mutual
+
+def recAwareStepScorer : StepScorer RecAwareGradedScore := fun key memo inputVars step => do
+  match step with
+  | .Unconstrained .. => return { density := .Total }
+  | .Match .. => return { density := .Backtracking }
+  | .Check src polarity =>
+    let varDeps := countGeneratedVarDeps inputVars src
+    let speed := classifyCheckSpeed memo key src varDeps
+    let likelihood ← classifyPassLikelihood inputVars key src polarity varDeps
+    let recKind := classifyRecursionKindCheck key src
+    return { density := .Checking, recursionKind := recKind, checkSpeed := speed, passLikelihood := likelihood, varDeps := varDeps }
+  | .SuchThat outputs src prodSort =>
+    let outputNames := Std.HashSet.ofList (outputs.map (·.1))
+    let varDeps := countGeneratedVarDeps (inputVars.union outputNames) src
+    let recKind := classifyRecursionKind key src outputs prodSort
+    let depDensity : Density := match src with
+      | .Rec .. => .Partial
+      | .MutRec .. => .Partial
+      | .NonRec (indName, args) =>
+        let outputIdxs := outputs.filterMap fun (n, _) =>
+          args.findIdx? fun a => match a with | .Unknown v => v == n | _ => false
+        let depDeriveSort := match prodSort with
+          | .Enumerator => DeriveSort.Enumerator
+          | .Generator => DeriveSort.Generator
+        let depKey : SpecKey := { inductiveName := indName, outputIndices := outputIdxs, deriveSort := depDeriveSort }
+        if depKey == key then .Partial
+        else match memo[depKey]? with
+          | some (.done depSched) => (Score.unwrap RecAwareGradedScore depSched.score).density
+          | _ => .Partial
+    return { density := depDensity, recursionKind := recKind, varDeps := varDeps }
+
+def recAwareScheduleScorer : ScheduleScorer RecAwareGradedScore := fun stepScores =>
+  stepScores.foldl Scorable.combine Scorable.empty
+
+def recAwareLeafAggregator : LeafAggregator RecAwareGradedScore := fun ctors =>
+  match ctors with
+  | [] => Scorable.uncoveredPenalty
+  | _ => Scorable.bestOf (ctors.map Prod.snd)
+
+def recAwareInductiveAggregator : InductiveAggregator RecAwareGradedScore := fun leafScores =>
+  leafScores.foldl Scorable.combine Scorable.empty
+
+initialize registerScoringBundle (mkScorerBundle `Scoring.RecAwareGradedScore
+  recAwareStepScorer recAwareScheduleScorer recAwareLeafAggregator recAwareInductiveAggregator)
+
 end Scoring
diff --git a/SpecimenTest/DeriveArbitrarySuchThat/BoundedBuffer.lean b/SpecimenTest/DeriveArbitrarySuchThat/BoundedBuffer.lean
index edb0a41..3486ee9 100644
--- a/SpecimenTest/DeriveArbitrarySuchThat/BoundedBuffer.lean
+++ b/SpecimenTest/DeriveArbitrarySuchThat/BoundedBuffer.lean
@@ -57,10 +57,6 @@ inductive SafeBBTrace : BB -> BBTrace -> BB -> Prop where
 
 -- Generating safe traces (no ErrResult ever generated)
 
-set_option specimen.multiOutput true
-set_option specimen.autoDeriveDeps true
-set_option match.ignoreUnusedAlts true
-
 instance (s : List String) (c : Nat) : DecOpt (WithinCapacity s c) where
   decOpt _ := if s.length ≤ c then .ok true else .ok false
 
@@ -76,29 +72,17 @@ instance instArbitraryString : Arbitrary String where
 -- generates a command freely and then checks `¬ CanStep`.
 deriving instance Arbitrary for BBCmd
 
-derive_mutual
-  (fun i => ∃ t s, SafeBBTrace i t s),
-  (fun s => ∃ t i, SafeBBTrace i t s)
+set_option specimen.multiOutput true
+set_option specimen.autoDeriveDeps true
+set_option match.ignoreUnusedAlts true
+-- set_option specimen.scoreType "Scoring.BoundedGradedScore"
+set_option specimen.scoreType "Scoring.RecAwareGradedScore"
+instance : ArbitrarySizedSuchThat Nat (fun b => a <= b) where
+  arbitrarySizedST _ := do
+    let n ← Gen.choose _ 0 5 (by omega)
+    return (n.1 + a)
 
--- The backward generator (fun s => ∃ t i, SafeBBTrace i t s) is poor quality:
--- it relies on guess-and-check for GetOp and PutOp (randomly generating lists
--- and hoping they satisfy WithinCapacity), so in practice it only produces
--- SizeOp operations. When the target final state is already at capacity, GetOp
--- and PutOp both require generating valid pre-states that the scheduler can't
--- efficiently construct.
-def backwardOnlySizeOps : IO Unit := do
-  for i in List.range 100 do
-    let (_, trace) ← Gen.run
-      (ArbitrarySizedSuchThat.arbitrarySizedST
-        (fun (s, t) => SafeBBTrace s t (["A", "B", "C"], 3)) 10) (i + 5)
-    let allSize := trace.all fun
-      | (.Size, _) => true
-      | _ => false
-    if !allSize then
-      throw <| IO.userError s!"Expected only SizeOp in backward trace, got: {repr trace}"
 
-#guard_msgs in
-#eval backwardOnlySizeOps
 
 -- Generating traces that admit errors (via `BBStep` / `EveryBBTrace`).
 
@@ -125,8 +109,64 @@ inductive EveryBBTrace : BB -> BBTrace -> BB -> Prop where
     EveryBBTrace s' ps s'' ->
     EveryBBTrace s ((cmd, res)::ps) s''
 
+
+
+def inverseScaleBase (baseWeight : Nat) (_ctorName : Name) (_outputIndices : List Nat)
+    (_deriveSort : Schedules.DeriveSort) (_scoreBadness : Float) (isRec : Bool) (size : Nat)
+    (_numBase _numRec : Nat) : Nat :=
+  if isRec then baseWeight
+  else max 1 (baseWeight / (size + 1))
+
+section
+set_option specimen.multiOutput true
+set_option specimen.autoDeriveDeps true
+set_option match.ignoreUnusedAlts true
+set_option specimen.weightModifier "BoundedBuffer.inverseScaleBase"
+
+-- Every stage is listed explicitly as an entry of this one `derive_mutual`,
+-- rather than as a bare `derive_mutual (fun i => ∃ t s, EveryBBTrace i t s)`
+-- (letting `autoDeriveDeps` discover every dependency). The reason was that
+-- experiments showed that doing so produced a worse generator.
+
+-- The stages:
+--   1. Enumerator for the `BBSafeStep` witnesses `(r, bb')` — used to decide `CanStep`.
+--   2. Checker `DecOpt (CanStep bb c)` — enumerate-and-check (backed by the
+--      enumerator above); negated via `DecOpt.negOpt` for `ErrStep`.
+--   3a. Generator for the `BBSafeStep` witnesses given a command — used by `SafeStep`
+--       when the command is an input.
+--   3b. Forward `BBSafeStep` generator (command generated too) — used by the forward
+--       `BBStep` generator.
+--   3c. Forward `BBStep` generator — one step of `EveryBBTrace`, generating the
+--       command, result, and next state from the current state.
+--   4. Generator for `EveryBBTrace`, via `derive_mutual` so the recursive instance
+--      is registered and the scheduler can step forward and recurse.
+
+#guard_msgs(drop info, error) in
 derive_mutual
-  generator (fun i => ∃ t s, EveryBBTrace i t s)
+  generator (fun i => ∃ t s, EveryBBTrace i t s),
+  generator (fun i => ∃ t s, SafeBBTrace i t s),
+  generator (fun s => ∃ t i, SafeBBTrace i t s)
+end
+
+-- The backward generator (fun s => ∃ t i, SafeBBTrace i t s) is poor quality:
+-- it relies on guess-and-check for GetOp and PutOp (randomly generating lists
+-- and hoping they satisfy WithinCapacity), so in practice it only produces
+-- SizeOp operations. When the target final state is already at capacity, GetOp
+-- and PutOp both require generating valid pre-states that the scheduler can't
+-- efficiently construct.
+def backwardOnlySizeOps : IO Unit := do
+  for i in List.range 100 do
+    let (_, trace) ← Gen.run
+      (ArbitrarySizedSuchThat.arbitrarySizedST
+        (fun (s, t) => SafeBBTrace s t (["A", "B", "C"], 3)) 10) (i + 5)
+    let allSize := trace.all fun
+      | (.Size, _) => true
+      | _ => false
+    if !allSize then
+      throw <| IO.userError s!"Expected only SizeOp in backward trace, got: {repr trace}"
+
+#guard_msgs in
+#eval backwardOnlySizeOps
 
 -----
 -- DIFFERENTIAL TESTING USING TRACES
@@ -237,6 +277,89 @@ def errorDifferentialTest (buggy : Bool := false) : IO Unit := do
 -- #guard_msgs(error, drop info) in
 -- #eval errorDifferentialTest (buggy := true)
 
+-----
+-- STATISTICS: comparing SafeBBTrace vs EveryBBTrace output distributions
+-----
+
+structure TraceStats where
+  samples     : Nat := 0
+  puts        : Nat := 0
+  gets        : Nat := 0
+  sizes       : Nat := 0
+  errors      : Nat := 0
+  created     : Nat := 0  -- successful Put count (keys added)
+  destroyed   : Nat := 0  -- successful Get count (keys removed)
+  finalBufLen : Nat := 0  -- sum of final buffer lengths
+  emptyTraces : Nat := 0
+  deriving Repr
+
+def classifyOp : BBCmd × BBResult → TraceStats → TraceStats
+  | (.Put _, .PutOk), s => { s with puts := s.puts + 1, created := s.created + 1 }
+  | (.Put _, .Error), s => { s with puts := s.puts + 1, errors := s.errors + 1 }
+  | (.Get, .GetOk _), s => { s with gets := s.gets + 1, destroyed := s.destroyed + 1 }
+  | (.Get, .Error), s => { s with gets := s.gets + 1, errors := s.errors + 1 }
+  | (.Size, .SizeOk _), s => { s with sizes := s.sizes + 1 }
+  | (.Size, .Error), s => { s with sizes := s.sizes + 1, errors := s.errors + 1 }
+  | _, s => s
+
+def collectStats (traces : List (BBTrace × BB)) : TraceStats :=
+  traces.foldl (fun acc (trace, (finalBuf, _)) =>
+    let s := trace.foldl (fun st op => classifyOp op st) acc
+    { s with
+      samples := s.samples + 1
+      finalBufLen := s.finalBufLen + finalBuf.length
+      emptyTraces := s.emptyTraces + if trace.isEmpty then 1 else 0 }
+  ) {}
+
+def printStats (name : String) (s : TraceStats) : IO Unit := do
+  IO.println s!"=== {name} ({s.samples} samples) ==="
+  let totalOps := s.puts + s.gets + s.sizes
+  IO.println s!"  Total ops: {totalOps}"
+  IO.println s!"  Put: {s.puts}, Get: {s.gets}, Size: {s.sizes}"
+  IO.println s!"  Errors: {s.errors}"
+  IO.println s!"  Created (successful puts): {s.created}"
+  IO.println s!"  Destroyed (successful gets): {s.destroyed}"
+  IO.println s!"  Avg final buffer length: {if s.samples > 0 then s.finalBufLen / s.samples else 0}"
+  IO.println s!"  Empty traces: {s.emptyTraces}"
+
+def generateTraces (gen : Nat → Plausible.Gen (BBTrace × BB)) (n : Nat := 1000) : IO (List (BBTrace × BB)) := do
+  let mut results : List (BBTrace × BB) := []
+  for i in List.range n do
+    let (trace, bb) ← Gen.run (gen 10) (i + 5)
+    results := (trace, bb) :: results
+  return results
+
+def assertGeneratorQuality (name : String) (stats : TraceStats)
+    (minOps : Nat) (maxEmptyPct : Nat) (minGets : Nat := 0) : IO Unit := do
+  let totalOps := stats.puts + stats.gets + stats.sizes
+  let emptyPct := stats.emptyTraces * 100 / stats.samples
+  if totalOps < minOps then
+    throw <| IO.userError s!"{name}: too few ops ({totalOps} < {minOps})"
+  if emptyPct > maxEmptyPct then
+    throw <| IO.userError s!"{name}: too many empty traces ({emptyPct}% > {maxEmptyPct}%)"
+  if stats.destroyed < minGets then
+    throw <| IO.userError s!"{name}: too few successful gets ({stats.destroyed} < {minGets})"
+
+def safeBBTraceQuality : IO Unit := do
+  let results ← generateTraces (ArbitrarySizedSuchThat.arbitrarySizedST
+    (fun (t, s) => SafeBBTrace ([], 3) t s))
+  let stats := collectStats results
+  assertGeneratorQuality "SafeBBTrace" stats
+    (minOps := 2000) (maxEmptyPct := 20) (minGets := 100)
+
+#guard_msgs in
+#eval safeBBTraceQuality
+
+def everyBBTraceQuality : IO Unit := do
+  let results ← generateTraces (ArbitrarySizedSuchThat.arbitrarySizedST
+    (fun (t, s) => EveryBBTrace ([], 3) t s))
+  let stats := collectStats results
+  assertGeneratorQuality "EveryBBTrace" stats
+    (minOps := 2000) (maxEmptyPct := 20) (minGets := 100)
+
+#guard_msgs in
+#eval everyBBTraceQuality
+
 end BoundedBuffer
 
 /-