Detection statistics¶

DST's claims about itself are measured, not asserted. The harness is exercised against a contract-misuse corpus — hand-authored known-bug twins of correct Forze workloads (a dropped rev guard, an outbox write outside its transaction, a retry without its idempotency key), each paired with a known-correct control — so every number below has ground truth behind it: the defect is known to be there, and for every transferable mutant its manifestation is verified against real Postgres, not only the mock.

Detection time is survival analysis: a campaign runs seeds until the first detection or a censoring ceiling, and the results are quantiles and exact intervals — never means over heavy-tailed, censored data. The full protocol runs 300 independent campaigns per (mutant, strategy); the whole dataset reproduces from one master seed.

How fast is a bug found?¶

The corpus's deepest bug — a double torn window, where a reader must catch both halves of a two-transaction provision mid-flight, which no single scheduler overtake can arrange — is where exploration strategies genuinely separate:

Random detects in a median of 6 seeds; the PCT strategies take 77–118 — an inversion of the ladder their parameters suggest, and a measured finding rather than a surprise left unexplained: this bug wants fine-grained alternation between writer and reader, which is closer to the random scheduler's baseline than to PCT's run-to-priority stalls. On depth-1 bugs the three strategies are statistically comparable (PCT's depth parameter buys nothing when a bug needs zero ordering constraints), and on the lease-release race the ladder points the other way — PCT detects at 0.92–0.95 per seed versus random's 0.74. Which strategy is "better" is a per-bug-shape fact, and the corpus is what makes that measurable. Every campaign above detects well before the 2000-seed ceiling.

Per-seed detection probability, per mutant¶

The spread is the corpus design, not noise: collision-pool workloads deliberately make the trigger rare (p̂ ≈ 1/16) so strategies have something to discriminate; crash-fault mutants sit at the crash-point lottery's rate; deterministic-manifestation mutants (a dropped tenant filter leaks on essentially every seed) sit at 1. Known-correct controls produced zero false positives across every strategy at 400 runs per cell — reported with its exact upper bound, never as a bare zero.

The canonical data views, regenerated by just dst-campaign and the analysis script, are the campaign results page — including the p̂-versus-PCT-bound analysis, where the measured detection rates respect the published guarantee in every applicable cell. The per-run schedule profiles (measured task counts and ordering-choice ticks) decompose the bound's conservatism honestly: at depth 3 the formal floor is ~100× below the measurement, but restated at the measured schedule length it is only 2× below — most of the slack is the draw-range parameter, not the theorem.

The method¶

Every number above comes from one measurement protocol, built so its own errors would surface:

• Ground truth by construction. The corpus is 20 hand-authored mutants — each a correct Forze workload with exactly one seeded contract misuse — beside 18 known-correct controls, several of them adversarial: shaped like the misuse, differing only in the one line that makes it correct. A detection is right or wrong by construction, never by judgment; whether the mock's verdicts hold on a real engine is the fidelity page's claim, and every transferable mutant here carries that verification.
• Detection time is survival analysis. A campaign runs independent seeds until the first detection or a 2000-seed censoring ceiling. A campaign that hits the ceiling is censored — it stays in the estimate as "survived 2000 seeds", never discarded — and the results are Kaplan–Meier quantiles, never means: detection times are heavy-tailed and censored, and a mean over such data is not a statistic, it is an artifact of the ceiling.
• Exact intervals everywhere. Rates carry exact Clopper–Pearson intervals, so zero observed events still reports a bound, never a bare zero. The kernel is ~300 lines of stdlib implementing exactly the statistics cited here, pinned to published worked examples (the Gehan 6-MP survival data; the textbook Clopper–Pearson intervals) rather than to itself.
• One integer reproduces everything. Every trial seed derives from one master seed via a keyed hash, so the full 18,054-record dataset — and any single campaign in it — replays bit-identically.
• Depth labels are derived, not asserted. Each mutant's depth is extracted mechanically: a violating interleaving found by systematic search, minimized to the schedule choices the bug genuinely needs, with the minimal vector recorded so a reviewer can re-derive it.
• The bound comparison conditions on the trigger. PCT's guarantee p ≥ 1/(n·k^(d−1)) speaks about schedules, but a measured per-seed rate is a product — p(the workload carries the trigger) × p(the schedule realizes it) — so the comparison divides out the recorded workload structure first; the first, unconditioned draft of this analysis produced false "violations", and keeping that correction visible is part of the method. n and k are measured per run (distinct contending tasks; real ordering-choice ticks), and mutants whose trigger is a crash lottery or an uninstrumented workload-order lottery are excluded by name, never silently.
• The scan states how far its own assumptions can be wrong. Dividing by the trigger introduces one input carrying no interval, so every cell publishes the exact factor by which that constant would have to be mis-derived for its verdict to flip. Cells where the flip would need a probability above 1 read as unreachable; the tightest real cells sit around 2.3×, and knowing which is which is the point. n and k are left without intervals deliberately — they are per-cell maxima, biased toward the most conservative floor, which is the direction that cannot manufacture a violation.

What the bound divides by¶

A clean sweep prints an exclusion bound: 0 violations in S seeds licenses "the per-seed detection probability is below 1 − 0.05^(1/S)". Read closely, that sentence is a claim about a denominator — it says there were S independent chances at the thing being bounded. Most of the ways this number can be wrong are ways S is not what it looks like, so each is named on the surface that prints it rather than left to the reader:

• S must be fixed before the runs exist. Clopper–Pearson's exactness is a fixed-design guarantee. A plateau-stopped coverage() sweep chooses its seed count from the runs it is summarizing, which is a different, unstated design — not a conservative one — so it states its stop reason and prints no bound at all. audit() is unaffected: it disables the early stop, so every configured seed runs. A confidence sequence would make peeking safe, and was priced rather than dismissed — it costs 2.3–5.1× width, against an alternative (run the pool you already configured) that costs nothing.
• Each invariant has its own S. The scope clause names the witnessed invariants, but "witnessed" is a static status: it says a falsifiability witness exists, not how many runs put that invariant at risk. An invariant exposed on 50 of 1000 runs is bounded at 5.82%, not the 0.30% the aggregate quotes. The verdict now counts exposure per invariant and prints the weakest member beside the aggregate, with its own number.
• S counts seeds, not distinct trials. Every bound treats S seeds as S independent chances. Measured across the corpus's controls, 200 seeds explore anywhere from 1 to 170 distinct execution shapes — six of eighteen produced exactly one. That gap is reported as a confidence warning and never folded into the denominator: the execution-shape fingerprint erases entity ids, and entity collision is exactly what the collision-pool regimes vary, so distinct-shape count is a coarse lower proxy. Substituting it would trade a known overstatement for an unknown understatement.
• Many bounds at 95% each are not one claim at 95%. The bound-comparison scan checks every applicable cell and reports one violation count; at 15 cells, a spurious flag under the null is likelier than not. Each cell's interval is corrected to the number of cells actually scanned — by the union bound, which needs no independence assumption these cells have not been shown to satisfy — and both levels are stated. The pytest plugin corrects the other way: it never aggregates per-sweep bounds by default, and offers one opt-in line that holds across every sweep at once.
• "Saturated" is not "explored". The coverage sweep's plateau flag is a boolean over the behavioural alphabet, which settles early — at the shipped coverage_plateau=8, a sweep still discovering on 10% of its seeds declares saturation 43% of the time. Beside it the report prints a measured deficit over the finer execution-shape alphabet: Good–Turing unseen mass and a Chao1 richness estimate, which is a lower bound and so under-promises how much is left.

What these numbers license — and what they don't¶

• A detection rate is scoped to its workload regime × strategy × oracle set. The collision pools prove the point deliberately: the same bug moves from p̂ ≈ 1 to p̂ ≈ 1/16 when the workload changes, so a rate quoted without its regime is meaningless.
• The false-positive zero is a bound, not an absolute: at 400 runs per cell it licenses "the per-seed false-positive rate is below ~0.9% per cell (95%, exact)" — for these controls, these strategies, and nothing stronger.
• A sweep-wide bound is not a per-invariant bound. The aggregate is the number that gets quoted, so it stays — but it divides by the whole sweep for every invariant it names, and each was only at risk in some of those runs. Read the weakest-member line beside it before quoting the aggregate for any single invariant, and treat an invariant reported with unmeasured exposure (an opaque read footprint) as outside the aggregate entirely.
• Seeds are the unit, not independent trials. Where a sweep's seeds collapse onto a handful of execution shapes the bound is optimistic by an unquantified factor, and the confidence report says so rather than repricing it. A redundancy warning means the number is worth less than it reads — not that a corrected number is available.
• There is no best strategy, and this data refuses to name one. Random beats PCT by ~20× on the depth-3 bug; PCT beats random on the lease-release race; they tie on depth-1 exactly as theory predicts. Which scheduler finds your bug faster is a property of the bug's shape.
• Depth is model-relative above d=2. The mechanical labels count deviations from the cooperative round-robin baseline; PCT's parameter counts priority stalls. The two provably coincide up to d=2 and measurably diverge at d=3 — bound comparisons stay valid in the conservative direction, but "what PCT-d buys" on a deep bug is an empirical, per-shape question, not a corollary of the label.
• The corpus bounds every claim: five misuse families, depths 1–3, document-plane workloads. These numbers say nothing about defect classes outside it — and growing the corpus, not extrapolating from it, is the only honest way to widen them.