The undo has to exist before the write does

An agent that changes something runs in the order decide, act, report. Verification, where there is any, reads what already happened. That's a fine shape for a log. As a control it's empty: by the time the check fails, the effect is already on disk, and what's left is describing the damage, attempting a repair nobody verified, or restoring from a backup whose age nobody measured.

For the last few months I've been building the other order, not for one tool but for the whole path a change takes. A proposed change gets a canonical identity. Its inverse is constructed, checked, and stored before anything is applied. A gate rules on it and returns one of three verdicts. The outcome, refusals included, becomes a signed record that a third party can re-check offline with no trust in me.

There's a longer draft paper behind this, deposited at doi.org/10.5281/zenodo.22168558. It's a draft, not peer reviewed, and not a specification. This post is the part that fits in a coffee break.

What I'd have to be wrong about

Putting this first, because a claim that only becomes checkable after you already agree with it isn't checkable.

Inverse availability. The escrow design assumes a useful fraction of write-capable tools expose something you can build an inverse from. A first census of public MCP tools put that at about 13.8% of the tools that write anything at all (census v2 stage 1, public MCP servers only, not production deployments). If the real number in production is at or under that, this is mostly a refusal machine, and "reversibility as a property" degrades into "refusal as a property", which is a much smaller and much less interesting thing to have built. That's the most dangerous fact in the project and it's mine, not a critic's.

Offline re-verification. If a signed receipt can't be re-checked with networking off and no trust in the issuer, meaning signature, log inclusion and identifier consistency, then the provenance layer is a log and not a proof. This one is runnable today: point the verifier at a frozen receipt corpus with the network down.

The model and the code. The Lean model and the Rust implementation are related by a differential test over 1,500 conformance vectors, not by a refinement theorem. No refinement theorem exists. If someone finds a divergence the vectors don't catch, then "machine-checked" was carrying more weight in your head than the evidence supports.

Four more are in the paper. Two of the seven are blocked on something I don't have, which is an operator population. Zero external users so far, so I can't tell you whether the third verdict ever fires in real hands.

The hash is a name, not the thing

This is the part that decides the architecture, and it's easy to get backwards.

Canonical identity is a projection. Take the space of concrete presentations of a value (encodings, field ordering) and quotient it by canonicalisation equivalence. Two different byte sequences that mean the same thing land on one identity. The map is surjective and not injective, so it has no left inverse. You cannot get the bytes back out of the identity.

So a system that keeps only identities can prove that a value was the one that got decided about, and cannot produce the value. Reversibility isn't a feature you bolt on afterwards, then. It forces a pair into the ledger: the canonical identity, plus whatever material you'd need to invert, stored separately, before the change lands.

In the code that second half isn't one tidy struct. It's three receipt fields: the canonical identifier of the change, the identifier of the stored inverse delta, and the recorded read set. The read set is the one that turns "restorable" into "attributable", and it's the field most often absent elsewhere.

An earlier internal draft of this material called the identity hash SHA-256. Wrong. The primary body is canonical DAG-CBOR and the digest over it is BLAKE3. There's a JSON-compatible route with an RFC 8785 digest under SHA-256 for interop with ecosystems that speak JSON, and that digest explicitly does not constitute identity. I'd rather print the correction next to the right answer than quietly patch it.

Three verdicts, and "couldn't evaluate" isn't one of them

The gate returns:

Verdict ::= Admit(proof) | Deny(reasons) | Escalate(ticket)

Three arms, no fourth. The design decision worth arguing about is what's excluded: an evaluation that could not be performed is not an arm. It's an error, returned outside the verdict type altogether.

The usual formulation is "three-valued logic, ALLOW / DENY / UNKNOWN", and it quietly merges two different unknowns. We evaluated and couldn't decide is a decision. We couldn't evaluate is the absence of one. Fold the second into the first and a caller reading an error as a denial has made a policy choice on the engine's behalf. Fail-closed belongs in the caller's policy, not in the type.

I care about this more than about the rest of the design, because I broke it myself. My own audit tooling collapsed "couldn't measure" into "measured false" and misreported 18 of 65 items on 2026-08-29. Loosening the probe made it under-report, tightening it made it over-report, and the threshold was never the answer; the third value was. Loading "couldn't measure" into "measured false" is a measurement failure being reported as a property of the subject, and it's the same defect whichever direction it points.

Two evaluation systems run, a policy evaluator and an invariant registry, and their results meet with Deny absorbing across all four quadrants. Reasons are held in a canonical order, so two evaluations refusing for the same reasons produce the same proof digest regardless of which system got consulted first.

Refusals get receipts too

A receipt is signed with Ed25519, wrapped in a DSSE envelope, and its leaf goes into a Merkle log with leaf and interior domains separated: H(0x00 || leaf) against H(0x01 || left || right), following the RFC 6962 section 2.1 construction with RFC 9162's numbered steps for inclusion and consistency proofs. The separation is what stops a leaf being presented as an interior node.

What a receipt asserts: this change was judged before it was applied; where an inverse could be constructed it was constructed, checked and stored first; the verdict was recorded, refusals included; the canonical identifier is consistent.

What it does not assert: that your predicate expresses anyone's intent, that a change satisfying it is safe, or that anybody can reconstruct the data that changed. Object bytes aren't stored. And a clean verdict count proves only that nothing was hidden from the counter. Weaken the policy until it admits everything and the count still reads clean.

The receipt also carries a field naming where replay-determinism stops: deterministic_replay, llm_originated, mixed, unknown. Mixed isn't an atomic fifth value, it carries two stage sub-fields drawn from a three-valued set of their own, so the unconstrained carrier is twelve inhabitants and four is just the count of top-level shapes. The combining function refuses to mint unknown over a stage that already has an established class. A stage nobody established can be said out loud. A stage that was established can't be laundered into silence. That node is the one place in the whole design where a written spec clause, a running implementation and a test that enforces it all exist at the same time, which is why I keep pointing at it.

What actually runs

Splitting this out, because everything above reads like a description of software and about a third of it isn't.

Nineteen of 27 components are running code, one of those partial. Three are designed with a written contract and not built. Five are targets with no contract at all. At layer granularity that's 6 of 9, and the two with zero implementation are the search layer and the evolution layer. Where the paper describes those, it's describing something I want.

Measured on 2026-08-29 unless noted: 17 workspace crates, of which 13 were shipped publicly as of 2026-08-25. Three refusal reason codes against a vision that names eight law classes. Eighteen receipt payload fields. A seven-method substrate contract with a conformance harness every adapter has to pass. Five substrate families, being filesystem, Git, tool-protocol proxy, PostgreSQL and MySQL, and the MySQL adapter has never been run against a live instance. The Lean model carries 117 theorems, 12 of them named counterexamples, 1 carried axiom, 0 sorry, re-counted on a fresh clone on 2026-08-26. Public test floor: 2,664 probes across 470 suites as of 2026-08-30, reconstructed from the tree rather than re-measured on a clean clone. That floor has moved more than forty times in a month, which tells you what a single reading of it is worth.

Then the condition that governs every number above. CI has run zero jobs on any push since 2026-08-15T17:25:29Z. Thirteen days, 2,245 commits, no machine signal, because the account is billing-blocked rather than because of a code defect. Failing runs show two to five seconds of "duration", which is the scheduler refusing the job before assignment, and there's no log for any of them because none of them ever ran. The workflow that cuts a release has never run at all. So every figure here is a local or hand-taken measurement, and "it compiles clean" is not the claim a green build would have been.

One more, since it's the kind of thing that usually gets found rather than disclosed. A frozen test in the repo reproduces a single signed receipt carrying inverse_delta = None while reversibility = Some(true). Two fields on one signed record disagreeing about whether the change could be put back. It's marked #[ignore], it isn't repaired, and whether the fix needs a fourth value in that vocabulary is still open.

Nothing here is new, and that's deliberate

Every part has a named ancestor. Leaf and interior domain separation in a Merkle tree is Certificate Transparency. The signed envelope is DSSE, out of in-toto. Content addressing over a canonical encoding is IPLD, and Git before it. Compare-and-swap on a precondition fingerprint is optimistic concurrency control. Pre-provisioned inverses are compensating transactions, which is Sagas, 1987. Deciding before applying, then applying exactly the thing that was decided about, is the plan/apply idiom. The policy engine is an unmodified third-party evaluator.

What's offered is the combination: those parts constraining each other in one pipeline, under one vocabulary that reaches from the substrate contract up to the drawn surface, with the coverage boundary published as a first-class artifact instead of an appendix. Where I say I didn't find something assembled this way, that's a statement about how I searched, carrying a date and a method. It isn't a statement about the world. No mechanism here gets called a first, the only one of its kind, or unique.

If you want to break it

Clone it, run the verifier against a frozen receipt with the network off, and tell me if it passes when it shouldn't. Or find a limit that isn't already on the limits page, which is honestly the reply I want, because that one turns into inventory.

Repo: github.com/TraceFold/tracefold (Rust, Apache-2.0). Paper: 10.5281/zenodo.22168558.

Not released.