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. Correction 2026-09-01: still not released as a package, but the v0.1.0-alpha tag now carries one Linux x86_64 tarball, uploaded 2026-08-31 and built outside CI. The sentence that used to sit here went stale the day the binary landed.
Top comments (9)
The limit I would look for is that the inverse is itself a write, while the receipt covers only the forward change. If applying a stored inverse does not re-enter the gate with its own canonical identity, its own precondition and its own receipt, then the undo is the one write in the system running in the decide, act, report order the opening rejects, and it is the write that runs during an incident with the least attention on it. The read set makes that checkable rather than rhetorical: an inverse constructed and checked against the read set at apply time only restores at undo time if nothing in that set moved since, so without a compare-and-swap at replay the escrow can overwrite a later legitimate write and still report a clean restoration.
That’s a very good catch. I think you’ve identified a real boundary in the current design.
I agree that the inverse cannot be treated as a privileged “undo path.” If it mutates state, it should itself re-enter the same discipline: canonical identity, precondition/read-set check, gate, and its own receipt.
The CAS point is especially important. An inverse being valid when it was constructed is not enough; replay has to establish that the state it is about to overwrite is still the state the inverse was constructed against. Otherwise a successful “undo” could actually erase a later legitimate write.
I’m going to treat this as a design gap rather than hand-wave it away. The interesting question now is whether the inverse receipt should be a normal effect receipt linked to the original receipt, or a distinct replay/compensation relation in the receipt graph.
Thanks. this is exactly the kind of limit I wanted people to find.
I'd make it a normal effect receipt carrying a
compensatesfield, and the reason is the argument you already make about the third verdict. A compensation relation is boolean — the edge is there or it isn't — so an inverse that gates to Deny or Escalate has nowhere to live: draw the edge and you've asserted a restore that never applied, leave it out and it reads the same as never having tried. That is "couldn't evaluate" folded into "measured false" again, one level up in the graph. The receipt form also has somewhere to put the replay read set, which the CAS check needs and an edge has no room for. What it costs you is "is X compensated?" as a lookup, since that becomes a scan over receipts naming X plus a reduce over their verdicts — but you need that reduce for correctness either way, so the relation was hiding the cost rather than removing it.You argued for the normal effect receipt, and that is what shipped.
The third-verdict argument is what decided it. An edge is boolean, so an inverse that gates to Deny or Escalate has nowhere to live, and folding "couldn't evaluate" into "measured false" is the same mistake one level up in the graph. So the receipt carries one key rather than two: a disposition that is either attested, or unobservable with the reason it was unobservable. Two fields can be assembled into contradictory states and one cannot.
github.com/TraceFold/tracefold/blo...
The property you were actually asking about has a test named after it,
checked_and_restored_is_distinguishable_from_fired_without_checking. Two forgery probes hold it down, one that moves the disposition under a kept signature and one that repoints which transformation was undone. Both refused.github.com/TraceFold/tracefold/blo...
On the CAS itself I measured before building anything. It was already there: a disturbed read set exits 3, and over HTTP it comes back as a 409 PRECONDITION_CHANGED. But I had only ever tested that against a third-party write, so I re-ran it with the disturbance being a legitimate commit made through our own CLI, and it refused that too. Worth saying plainly that this used to be broken. The old behaviour was RC 0, "Committed", and the file back at its pre-image with the other write silently gone.
You did not just name the cost, you dissolved it. "Is X compensated?" becomes a scan plus a reduce over verdicts, but the reduce is needed for correctness either way, so the lookup was hiding that cost rather than removing it. That is what made the trade easy to take.
Where it is still weak, since you would find these anyway.
The replay read set has somewhere to live in the receipt form, as you said, but I have not put it there. Read set staying inside the CAS scope is currently a property of the five shipped adapters rather than a check. That is the gap I am least comfortable with.
Two defects are filed against my own change. Some CLI paths report "no postcondition" when the truth is "could not read the world", so the visibility I just added now signs a wrong reason in those arms. And a re-undo of something already in the table returns early before the journal append, so the receipt names the first plan's disposition rather than the last call's. That one is fail-closed, it under-claims rather than over-claims, but it is still wrong.
The attestation is exercised on fs only. git, mcp, postgres and mysql are zero.
One acceptance criterion I wrote turned out to be false and I corrected it. I had claimed the receipt-derived and journal-derived edge sets would match exactly. They do not. Receipt edges equal superseded edges and are a strict subset of planned parents, because an undo you never settle still writes a parent.
Falsifier, up front: all of this folds into one claim, that a third party holding only the receipt can verify the undo was sound. The read set gap above is the most likely place to break it. If you can construct a case that does not fold into that shape, then the classification is wrong.
Taking the falsifier seriously, I think the edge-set correction you just made is itself a case that does not fold into the read set. Receipt edges equal superseded edges and are a strict subset of planned parents, so a third party holding only the receipt sees the parents that settled and has no way to separate "nothing else was planned" from "something was planned and never settled". That does not threaten soundness of the undo that did happen. It threatens the scope word, because sound-for-this-edge is verifiable from the receipt and complete-over-what-was-planned is not, and both look the same in the receipt form.
Your re-undo defect is a second one, and it is not a concurrency problem either. If the early return skips the journal append, two calls hand back a receipt naming the first plan's disposition, so a receipt-only verifier cannot order them or say which call it is holding. Fail-closed stops it over-claiming, agreed, but the identity of the call being attested is what goes missing there, and no read set is involved.
Both points survive contact with the code. I checked before answering rather than arguing from memory, so here is what is actually there.
On the edge set: you're right, and it turns out the code already knew. The receipt-borne edges are exactly the undos that committed, which is the journal's Superseded set, and a test asserts that set sits strictly inside Planned.parents (
the_receipt_dag_equals_the_superseded_dag_and_sits_strictly_inside_the_planned_dag, incrates/gx-engine/tests/r973_undo_attestation.rs). So "planned but never settled" is invisible to a receipt-only verifier by construction, and the two readings you name really do look identical in receipt form. What doesn't survive is where that scope statement lives. It's a doc comment above the emitter, not a line on the limits page, so the one person who needed it, someone holding only a receipt, is the one person who'd never see it. That's the gap your comment exposes: the containment belongs on the public limits page as a declared non-claim, and it isn't there today. Completeness over the planned set needs the journal, and the receipt should say so instead of leaving the scope word doing quiet double duty.On the re-undo: also correct, and already filed. The early return sits before the Planned append, so a second call hands back the first call's disposition. It's an open defect with an id (DR-46-47, filed 2026-08-31, the comment block sits right on the return in
crates/gx-engine/src/pipeline.rs) and a release condition: either the second call updates the seat, or the re-plan is refused when its witness differs, with a probe driving both orders. One thing worth being precise about, since you were: the CAS runs on both calls before that return, so the failure direction is under-claiming only. A later call that compared clean can still be reported Unobservable. Nothing can be reported Attested without having compared. Fail-closed held, the call identity didn't.Your last sentence is the one I can't repair inside the receipt, though. TransformationId is content-derived, so a repeat mints the same id, and issued_at is deliberately unsigned and outside the ledger digest. Even after DR-46-47 lands, a receipt names a transformation, not a call. Ordering two calls is journal work, and whether call identity belongs in the signed bytes at all is a real design question, because a per-call nonce would cost the deterministic identity the dedup depends on. I don't have a clean answer yet.
Pinned to the current public head if you want the actual lines: receipt.rs and pipeline.rs.
The ordering might already be sitting in the log, without touching the identity preimage. Two receipts naming the same
TransformationIdstill land on distinct leaves, and an inclusion proof against a signed tree head orders them, so dedup keeps keying on the content-derived id while ordering keys on the log instead.What blocks that today is that the one per-call field you have,
issued_at, is deliberately outside the ledger digest, so two calls produce byte-identical envelopes and, Ed25519 being deterministic, identical signatures. The log can hold both leaves, but no inclusion proof attributes to a call. Putting a call id inside the signed envelope and leaving it out of the identity preimage costs the dedup nothing, and it only buys you ordering within one log and one issuer.You’re right that, with
issued_atoutside the digest and Ed25519 being deterministic, two identical calls collapse into a single attributable leaf.I checked the [witness receipt construction path] before answering: the envelope currently carries no per-call identifier inside the signed bytes. Your placement—putting the call ID inside the envelope but outside the identity preimage—survives our deduplication by construction, so I’ve filed it as a candidate wire change.
The one cost you didn’t mention: replay verifiers that byte-compare envelopes will now see two receipts where they previously saw one, so the change needs to ship with a version bump.
Following up since you've been asking the sharpest questions in this thread: the crates shipped today. 13 crates on crates.io as of today (docs.rs green on all 13), including the receipt code we've been going back and forth about -- gx-witness/src/receipt.rs, ac_070, if you want to read it directly instead of my paraphrasing it back to you. Still alpha (v0.1.2), still one maintainer, still no users but me. Posting mostly because the source's now one
cargo addaway instead of a git clone.