Skip to content

Methodology

A tool that asks to be trusted about verification owes the same standard to its own claims. Every statistic on this site is held to that standard mechanically, not editorially. This page describes the machinery and publishes the ledger: what is validated, what was tested and falsified, and what remains open.

How a claim gets on this site

Every number renders from a single source file (src/lib/facts.ts), where each constant carries a pointer to the artifact it was measured from. Three gates run in CI on every push and pull request: a claims gate that fails the build if a correlation appears without its label basis or if a banned overclaim phrase appears anywhere in the source (the banned list is enforced to stay identical to the one in bulla’s own test suite); a facts gate that fails if a constant drifts from the bulla source it cites; and a dead-route gate for links. The site cannot state a claim the package does not back.

Validated

  • The mathematics. The coherence fee is a genuine coboundary-rank invariant with an exact additive decomposition over convention dimensions. The research-program ledger documents 56 theorems machine-checked in Lean 4 (0 sorry) backing the witness-geometry chain; the Per-Dimension Additivity Theorem is verified on all 703 corpus compositions. The PyPI package does not vendor Lean; it implements the measurement and receipt layers in Python.
  • The wire format. ActionReceipt v0.2 is verifiable from the spec alone: a zero-dependency checker (stdlib only, no bulla imports) reproduces all four hashes and the modality law, against 7 published golden vectors. A second implementer needs the spec, not our source.
  • The corpus and benchmark. The calibration corpus (38 servers, 703 compositions) is frozen at bulla 0.33.0; BABEL ships frozen dev/test/hidden splits with method-neutral ground truth.

Tested and falsified

Bulla was once described as if the coherence fee predicted execution failure — “catches this before execution.” We built a pre-registered, execution-labelled kill-test to check: a fee-vs-baselines battery scored by real Python round-trips the predictors never see. The fee’s fire was approximately independent of whether a break occurred — likelihood ratio ≈ 1.07, against 1.0 for no information. Two supporting negatives, kept distinct: a pre-registered result that on the real corpus a cheap depth-3 baseline recovers the full obstruction, and an execution-labelled probe in which fee=0 compositions breached under real file I/O (30 of 36 — on an authored tool set, so evidence the blind spot is broad, not a corpus estimate). The claim was retired; the full record is in FALSIFICATIONS.md.

What replaced it: the fee is a disclosure measure — how much convention two composed tools leave undisclosed at their seam — and one field a receipt can carry. The record and recourse layer (receipt, registry, coverage, retention asymmetry) never depended on the fee predicting anything. The falsification retired a product claim, not the mathematics and not the receipt.

Open

  • The log-inclusion rung. The verification ladder names three levels — digest, attestation, log inclusion. The published checker covers the digest rung; signature and inclusion verification require key distribution and a log, which the spec names rather than fakes.
  • A second, independently operated log. Today there is one registry, operated by us. The standing model (ADR-001) commits to any-log verification and records this as its named closing condition — until a second log exists, log plurality is a commitment, not a fact.
  • Evidence grounding classes. Spec v0.2 (NORMATIVE) adds per-evidence grounding — self_asserted, counterparty_signed, third_party_anchored, execution_verified — so a receipt’s displayed strength is the minimum over its necessary evidence. Drafted, not yet implemented.