A receipt for every consequential agent action.

The record

One canonicalization rule and four hashes, each answering one question: recompute the verdict (content), which occurrence (event), who vouched (attestation), where logged (log leaf). The content hash is the receipt’s identity — identical on any machine, free of the clock and the signature, the field a bond’s slash condition recomputes.

A verifier reports the highest rung it reached — digest, attestation, log inclusion — never a lying boolean. The acceptance test for the whole format is a zero-dependency checker that reproduces every hash from the spec, with zero bulla imports.

The recourse

Every receipt carries an appeal path, and the spec enforces a modality law: a remedy must name a verifier and a stateful anchor — a remedy with neither is process theater, and the verifier rejects the receipt. The gate turns that into an enforcement point:

$ bulla gate --certificate coherent.json --registry log.jsonl
PROCEED   fee=0 · authentic · included under trusted root

$ bulla gate --certificate seam.json --registry log.jsonl
REFUSE    fee>0 (filesystem↔git path seam) · exit 1
CURE      disclose path_separator on the writing tool

A refusal ships with its cure. In the loop-closure demos the same gate catches a host serving an equivocated registry root — and the same convention disclosure that clears the fee fixes the real git execution.

The registry

Receipts append to an RFC 6962 Merkle log with inclusion and consistency proofs — the Certificate Transparency construction, not a database with an API. The trust rule is strict: a host’s bare claim about its own root is refused; an inclusion proof counts only against a root you obtained independently.

Standing recomputes from the public record — we never hold a score the record cannot reproduce, and records exit with their subjects. Agents meet the whole layer at runtime through the live MCP proxy, which fronts your servers and injects 8 bulla__* meta-tools the agent itself calls — from bulla__should_proceed to bulla__deed_emit.

Why trust the result

You don’t have to. The verdict is a deterministic function of pinned inputs — recompute it and you get the same answer, which is the whole difference between being told and being able to check.

Formal where exact. Explicit where not.

The mathematics behind the diagnostics is machine-checked: 56 theorems in Lean 4 against Mathlib, 0 sorry, with the per-dimension additivity theorem verified on all 703 corpus compositions.

Diagnostics, calibrated on real MCP compositions

One field a receipt can carry is the boundary fee: how much convention two composed tools leave undisclosed at their seam — date formats, unit scales, path roots that pass schema validation and still disagree. It has an exact additive decomposition per convention dimension, so a repair is a worklist, not a mystery.

The BABEL benchmark freezes 932 instances (public dev reference split: 514) across seven workflow families. On that dev split, the structural reference diagnostic achieves macro-averaged Spearman ρ ≥ 0.91 across families against the benchmark’s annotation-derived labels; plain schema validation correlates at 0.17.