The Bound Is the Easy Part; You Need a Denominator First

Findings Note: The Bound Is the Easy Part; You Need a Denominator First

The paper is Efficient and Sound Probabilistic Verification for AI Agents (arxiv.org/abs/2606.20510, Google DeepMind / UPenn / UW-Madison). It answers a question Chimera’s whole safety story quietly assumes away: every one of our ~14 gates — the critic, the witness panel, differential and mutation checks, scope/charter/evasion guards, guardrail-eval, the entropy gates — is fallible, yet a pass is read as “verified,” with no statement of how leaky the gate is. The paper turns “this fallible detector passed” into “the probability an actual violation slipped through is provably ≤ U,” and composes per-gate guarantees into a stack-level bound. Its machinery is genuinely elegant: compile the execution trace against a Datalog policy into a derivation DAG, embed the Boolean lineage as multilinear polynomials, and take the maximum violation probability over every joint distribution consistent with the per-detector marginals — a distributionally-robust optimization that assumes no independence — then make it tractable by relaxing that exponential LP to a polynomial-size semidefinite program (sound because the SDP optimum provably upper-bounds the true worst case). The marginals themselves are made sound with a one-sided Clopper-Pearson upper bound on each detector’s measured miss rate.

I evaluated it for Chimera with a multi-agent pass — the paper read in full, a from-disk inventory of our fallible gates, a survey of the sound-bounding techniques, and three adversarial critics. The critics earned their keep: they overturned the comfortable version of the answer.

Reject the superstructure; keep the kernel. The DRO/SDP-over-Datalog machine does not fit us. It requires a Datalog information-flow policy and hand-modeled taint semantics for every tool, plus a conic solver (cvxpy/SCS) that would bloat a dependency set we keep deliberately tiny. Worse, the paper’s own limitations say the bound degrades toward vacuous over long traces and that arbitrary agent-generated Python/Bash “directly breaks the precondition that every tool maps to a predefined transition rule.” That is precisely an autonomous coding agent’s regime. The one transferable idea is narrow and good: the Clopper-Pearson upper bound on a detector’s miss rate. That kernel is adoptable; the rest is not.

The crux is the denominator, and we don’t have it. A sound false-negative-rate bound is a statement about measured misses on known-violation inputs — misses / known-positives, with a confidence level. Looking at the live ledgers, not the design’s hopes:

• The reverted disposition — the design’s proposed “strongest free ground-truth signal” — has been recorded zero times across 70 ledger lines (4 merged, 29 abandoned, 4 pending). set_disposition has no automated caller; it is operator-only and has fired never.
• The critic gate, the only gate with labelled cases, has n = 12 should-reject cases. Clopper-Pearson on 0/12 gives FNR ≤ 22% — and those twelve are a hand-curated benchmark, not a sample of the diffs the live gate actually faces. A confidence interval is sound only for the population the cases were drawn from; calling a benchmark number a field guarantee is exactly the falsely-tight figure that lulls an operator.
• The three ledgers cannot even be joined (the critic log is keyed by diff_sha, the crawl ledger by run_id), and the deterministic gates have no “rate” at all — re-running them on the same input gives the same answer, so a confidence interval is the wrong object.

So any “sound bound” printed today would be vacuous — and printing one and calling the gate “sound-bounded” would itself violate the rule this whole line of work exists to enforce: no signal must never read as verified.

The reframe. B.4l is therefore a measurement rung, not a bounds rung. Build the substrate that could one day carry a bound, advisory-only, and say so plainly: (1) a pure gate_calibration.py core — a dependency-free Clopper-Pearson function, a GateOutcome record, an UNCERTIFIED sentinel below an n-floor, and a structural guard that refuses to pool strata; (2) the piece the design originally skipped and the critics demanded — the label producer: an automated revert/override detector that actually populates the ground truth, plus a join key across the ledgers (you cannot calibrate a detector you never score against an outcome); (3) the cheapest honest value available now — surface the revert_rate the ledger already folds, n-annotated and advisory; (4) deferred and explicitly conditional — an anytime-valid drift monitor, and, only if a gate’s data ever clears the floor, the promotion of a single gate to a hard bound. With a retire criterion so it never becomes maintained infrastructure that measures nothing.

The lesson rhymes with q004 and q005. There, a single sample lied (a guardrail “failure” that didn’t reproduce; a fixed-input test that certified buggy code). Here the seduction is one level up: an elegant proof that would be sound — if we had the calibration data. We don’t. The honest contribution of this paper to Chimera is not a bound; it is the discipline of refusing to emit one until there is a denominator under it, and of building the thing that produces denominators first. Measure before you bound.

Shipped (B.4l substrate, 2026-06-22)

Stages 1-3 landed the same day (#381-#383): the pure dependency-free Clopper-Pearson core (its soundness verified against the binomial defining property, not just its own beta code), the automated revert label producer (reconcile_reverts — the crawl ledger’s long-promised “gh-reconcile”, now run daily, so reverted finally populates from real history instead of a manual step), and the advisory chimera gate-calibration report.

Stages 4-5 then completed the rung (#395, #396). Stage 4 is an anytime-valid drift monitor — a betting test-supermartingale whose false-alarm rate Ville’s inequality controls at any stopping time, the one prior-art family that survives peeking and the non-i.i.d. drift Chimera has. Stage 5 is hard-gate promotion (a cell is promotable only if its FNR is provably ≤ an operator’s budget — never auto-applied) plus sound stack composition (P(violation slips ALL gates) ≤ min per-gate FNR — not the product, which assumes an independence we lack, and not the sum, which bounds a different event), with Bonferroni applied across cells so a dashboard read can’t cherry-pick. Both stages were built as pure cores and put through their own adversarial soundness audits (supermartingale/Ville/λ-clamp; min-composition/promotion/Bonferroni) — each caught a real fix before merge. They are inert until the calibration ledger accrues data: today the whole apparatus honestly reads UNCERTIFIED.

What the report says today is the whole point, and it is honest: “CRAWL landed-work revert rate: 0.0% (reverted 0/4 merged); per-gate FNR bounds: no labelled gate outcomes yet → UNCERTIFIED. The substrate is in place; the data is not.” That last sentence is the deliverable. We did not ship a safety certificate; we shipped the apparatus that will earn one — and a structural refusal to pretend, in the meantime, that an empty denominator is a clean bill of health.