The undo has to exist before the write does

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).

Not released.