Six weeks later, the record still had to match

A refund was approved above the limit an automated agent could act on alone, so a human supervisor stepped in, reviewed the case, and committed the decision. That is an ordinary event. What makes it useful later is that the moment it happened, the whole of it, who approved it, under what authority, on what evidence, what outcome they expected, and the confirmation that a person actually signed off, was written into a single record and sealed.

Weeks pass. Someone asks the question that logs are bad at answering: not whether the refund ran, but whether the account of it can still be trusted. A log will say an event occurred. It will not say who was allowed to allow it, what they knew, or whether the story has been edited since. The sealed record is built to answer exactly those questions, and to answer one more: has this record been changed since it was committed.

The seal is a fingerprint computed over the record’s contents in a canonical form. Recomputing it and comparing to the stored value is a check anyone can run, in a browser, without trusting the party that produced it. If the record is untouched, the recomputed fingerprint matches. Edit any field, raise the approval limit, soften the evidence, change the expected outcome, and the recomputed fingerprint no longer matches. The edit is not prevented; it is made undeniable.

A careful adversary sees the obvious next move: change the field, then re-seal the record so its own fingerprint matches again. That works against a record standing alone. It stops working once each record is chained to the one before it, because re-sealing the edited record breaks the link the following record carries. Re-seal the whole chain to repair the links, and the mismatch moves outward to an anchor held outside the store, where the attacker cannot reach it. Each escalation of the tamper is caught one step further out. The figure below traces the three attacks and the point at which each recompute stops matching.

The programme’s contribution is not the demo but the proof behind it. In Lean, the canonical encoding is shown injective, the chain append-only, and tampering that survives the check shown to force a hash collision, established without assuming the hash is collision-resistant as an axiom, and without claiming the opaque hash is any particular function. What the record establishes is narrow and stated as such: it is intact and can be reconstructed. It does not establish that the decision was right, or that the reasoning recorded is the reasoning that actually occurred. Those are different properties, and conflating them is its own kind of failure.

This case is the assurance-architecture corner of a programme about whether claims about AI systems can be independently checked. Read where it fits in the programme.