tracefold

It asks before the changes it can't put back.

Tracefold holds a checked inverse for an agent's change before it lands, in Rust. When the
inverse is in hand the change goes through and you are never asked; when one cannot be built, the
agent stops and the question comes to you. Every verdict also becomes a receipt that verifies
offline, without trusting whoever issued it.

Try it ·
Limits ·
The whole chain ·
Where it stands ·
What it does ·
Report ·
Contributing ·
Glovrex

Flip one byte, and the verifier says no

Three files are on that terminal: a receipt, a signed checkpoint, a public key. No project
directory, no account, no network call. The receipt verifies and exits 0. One byte of its
payload is flipped in place, cmp -l prints the single line proving exactly one byte moved,
and the same command exits 7.

Real terminal, captured with script(1) against a fresh anonymous clone at commit 177141e3
on 26 August 2026, WSL2 Ubuntu 24.04. Nothing retyped or staged. Outside the recording on
purpose: cargo build --workspace, 64 seconds on that run. Also published as
asciicast v2.

Try it yourself

Not released. There is nothing to install from a registry, so this starts from a clone.

What that costs you today, stated plainly. You need a Rust toolchain (stable, pinned in
rust-toolchain.toml) and roughly a minute of compile time. On Windows the documented path is
WSL, and a WSL install is not free: the virtual disk grows with the build tree, and on this
project's own machine it reached hundreds of gigabytes. If that is more than you want to spend
to check one receipt, that is a reasonable place to stop, and it is the honest state today.

Two routes out of that requirement are being built, and neither is finished, so treat both as
in progress rather than as a plan you can use. sdk/wasm-verify/ is the verifier compiled to
WebAssembly, which is what browser-side checking with no toolchain at all would be built on.
Prebuilt binaries per platform would remove the compile step. When they land, verification
becomes the thing you do without installing a compiler; until then it is not, and this page
will not pretend otherwise.

Signing, when binaries exist. macOS builds are intended to be codesigned and notarized, so
a Mac user gets a double-clickable binary and no unidentified-developer dialog; the developer
account for it is in hand. Windows is not the same story. An EV certificate is a real recurring
cost that is not being paid yet, so a Windows binary would raise a SmartScreen warning, and the
honest options there are to document that warning and how to proceed past it, or to build from
source. No Windows signing is being promised.

git clone https://github.com/TraceFold/tracefold
cd tracefold
cargo build --workspace          # about a minute, and the slowest step here
export PATH="$PWD/target/debug:$PATH"

Make one change the way an agent would, through the gate, so there is a receipt to check:

mkdir -p walk && cd walk
echo "before any agent touched it" > notes.md
gx key gen --json > pub.json
KEY_ID=$(python3 -c 'import json;print(json.load(open("pub.json"))["key_id"])')

printf 'after an agent wrote through gx\n' > intent.txt
gx --project . submit --substrate fs --locator "$PWD/notes.md" \
  --intent intent.txt --context Substrate --actor-key "$KEY_ID" \
  --actor-kind agent --actor-model "readme/1" > submit.json
IID=$(python3 -c 'import json;print(json.load(open("submit.json"))["intent_id"])')

gx --project . plan "$IID" > plan.json
TID=$(python3 -c 'import json;print(json.load(open("plan.json"))["transformation"]["id"])')
gx --project . verify "$TID" > verify.json
gx --project . commit "$TID" > commit.json

RECEIPT=$(python3 -c 'import json;print(json.load(open("commit.json"))["stored_at"])')
gx --project . log checkpoint --key ~/.gx/keys/"$KEY_ID".key --out head.json

Now check it the way a stranger would, with no workspace and no network:

gx receipt verify "$RECEIPT" --offline \
  --checkpoint head.json --checkpoint-key pub.json --key pub.json

Exit 0. Then flip one byte of the receipt and run the identical command against the copy:

python3 - "$RECEIPT" <<'EOF'
import re, sys
raw = open(sys.argv[1], "rb").read()
m = re.search(rb'"payload": ?"([A-Za-z0-9+/=]+)"', raw)
i = m.start(1) + 40
b = raw[i:i+1]
open("tampered.json", "wb").write(raw[:i] + (b"A" if b != b"A" else b"B") + raw[i+1:])
EOF
cmp -l "$RECEIPT" tampered.json          # exactly one line
gx receipt verify tampered.json --offline \
  --checkpoint head.json --checkpoint-key pub.json --key pub.json

Exit 7. Every command on this page was run in that order on a fresh clone before being
printed here.

Pass --checkpoint-key. Without it the check still exits 0, but the answer says
"anchor_authenticated":false: the checkpoint was read and not authenticated, so you
verified against a file you took on faith. Drop --checkpoint entirely and you get 7 with
"inclusion":"unanchored", the tool refusing to call a receipt verified when it cannot place
it in a log.

Exit codes are the contract a script branches on without parsing JSON: 0 valid, 7 does
not verify or is unanchored, 6 not found, 1 bad input, 2 refused by policy. Full table
in crates/gx-cli/src/exit.rs. The subcommands that exist today: submit, plan, verify,
commit, undo, cancel, escalation, receipt, replay, log, key, policy,
serve. gx limits prints the gaps below at a terminal.

Free forever for one person. Receipt generation, offline verification and self-hosting
are unlimited and unexpiring for a single person using this alone, which is a promise rather
than a price.

What you cannot take from this

Five classes of failure sit outside this by declaration rather than oversight. They are
above the features because reading them first can save you the afternoon.

The demonstration above has a limit worth saying in the same breath as the claim. Exit 7
proves the receipt you hold is not the receipt that was signed. It says nothing about whether
the change the receipt describes was the change anyone wanted.

One more thing worth knowing before you start rather than after. What you can later
select on is fixed at the moment of capture, not at the moment you ask. A field that was not
recorded when the change landed cannot be recovered as a filter afterwards, so the set of
questions you can put to the history only ever grows forward from the day you begin.

The full list ships in docs/LIMITS.md, and a test fails if it drifts from
the code that enforces it. These are not sentences someone remembered to update.

The whole chain

The atom above is one command against one file. This is why it matters: the receipt travels,
and it still holds in someone else's hands.

An agent changes a file through gx. The change is described, planned, judged and committed,
and leaves a signed receipt. Three files travel to somebody who was not there and does not
trust the sender: receipt, checkpoint, public key. They verify offline and get 0, tamper
with one byte, and get 7. Nothing else moved, and no service was asked to vouch for
anything. Same recording conditions as above.

[!IMPORTANT]
Not released. The names tracefold on npm and on crates.io are ours and are taken,
but what sits behind both is an empty 0.0.1 placeholder holding the name, published on
12 and 13 August 2026. Installing it gets you nothing. What you can actually run today is
a build from source, and nothing above should be read otherwise. The download counters on
those pages are mirrors and scanners fetching a new name once: 110 of the 125 npm
downloads landed on the day of publication, and the last two days are zero.

Who this is for. Someone who will later have to show a third party what an agent
did, and to whom "we checked our logs" is not an acceptable answer: an audit, a customer
contract, a regulator, an internal review. If you only want to undo a mistake, the
service you are already using probably keeps enough history, and you do not need this.

Two things your agent's own client cannot do for you, however good it gets. It cannot
see what left it: a rewind feature covers the conversation and the edits it made itself,
not what went out through a shell command or through someone else's tool server. And it
cannot be the independent check on its own work, because the party being audited grading
its own paper is not an audit, at any level of accuracy. Both are questions of position,
not of features, so they do not close when the client improves.

Implemented is a different word. The engine, the ledger, the policy gate, three
substrate adapters, the MCP wrapper, the CLI, the HTTP API, an SDK and a machine-checked
model are written and tested. Released is the one that is not yet true.

Where it stands

The commands that produce the first, second and fourth, all runnable in a clone:

# test floor, and the SDK line separately
bash tools/e2e.sh
cd sdk/typescript && npm ci && npm test
# theorems, then the one assumed statement; add up the per-file counts
grep -rcE '^theorem' lean/GxSpec.lean lean/GxSpec/*.lean
grep -rcE '^axiom' lean/GxSpec.lean lean/GxSpec/*.lean
# the unmeasured surfaces, declared rather than discovered
grep -n "Windows, OneDrive" docs/LIMITS.md

Those greps are anchored to the start of the line on purpose. Allowing leading whitespace
returns 119 theorems and 2 axioms, but the three extra hits are English sentences wrapped
inside doc comments, where a line happens to begin with the word:

lean/GxSpec/Attribution.lean:49:  theorem below asserts that gx's running implementation ...
lean/GxSpec/MinimalityF0.lean:41:  theorem here strengthens, weakens or restates any frozen ...
lean/GxSpec/MinimalityF0.lean:32:  axiom set stays `{propext, Quot.sound, GxSpec.composeId}` ...

None is a declaration. Counting the loose way would add a theorem the prover never saw and a
second unproved assumption that does not exist, so 117 and 1 are the numbers above.

The third row has no command, and that is not an oversight. An open-hole count is read off
the audit ledger, and no single invocation produces it. So that row says where the number
comes from and you are taking it on our word. A count that only ever falls is a count someone
is managing rather than measuring.

What would show this is wrong. Two things, and either one is enough. Produce a receipt
that gx receipt verify accepts while the inverse it names does not restore the state it
claims to restore. Or land a change through the gate that leaves no receipt. Both are
checkable by someone who does not trust us, which is the point; if you find either, open an
issue and it will be recorded here whatever it costs us.

Deliberately absent: no build badge, because continuous integration is switched off and a
green tick would be a lie. No download counts, no star totals; neither measures whether the
thing works.

What it does

Four behaviours, and they are not four settings you configure separately. One declaration
names an object and what may happen to it; the gate that runs before the action, the rule
enforced while it runs, and the fields attested after it all read out of that declaration.
That shape is not a discovery of ours and is being arrived at independently elsewhere. The
narrower difference: a receipt here carries an inverse constructed and checked before the
change landed, which is not a field reporting afterwards that an action was reversible.

Escrow before commit. Where an inverse can be constructed it is constructed, checked, and
stored durably before the change is applied. Undo is a checked property, not an assumption
made afterwards.

Measured, not self-reported. A fingerprint of the substrate is taken before and after a
change reaches the object a transformation names, so what happened is measured rather than
described by the same process that did it.

Offline-verifiable receipts. Every verdict, admit or deny or escalate, is signed and
anchored in an append-only log, and re-checks with no network and no trust in the issuer.

Declared coverage. What is not covered ships beside what is. A skip prints its name
rather than passing quietly.

Figures you can re-derive

Numbers about a project are worth what it costs you to check them, so the commands sit here
rather than the claims. Run them in a clone at any commit and you get whatever is true at
that commit, which may differ from what is printed below.

# implementation, excluding the test trees
find crates -name '*.rs' -not -path '*/tests/*' -print0 | xargs -0 cat | wc -l
# the test trees
find crates -path '*/tests/*' -name '*.rs' -print0 | xargs -0 cat | wc -l
# direct dependency surface, once the toolchain is installed
cargo tree --depth 1 -e normal

On 26 August 2026, at commit 177141e3, the first printed 80,647 and the second 139,966,
across 142 and 362 files in 13 crates. The tests are larger than the thing they test, and
that is the only claim these figures support. Our own ledger counts test lines a second way,
excluding files merely named for tests, and on 18 August the two rules disagreed by eight per
cent on the same tree on the same day. That is why the command sits above the number and the
date sits beside it.

The dependency surface is real: the third command lists it, and every entry is code you would
be trusting on our recommendation.

Read further

Two walkthroughs go slower than this page, with every command executed and printed:

• Flip one byte and the verifier exits 7, the
  full tamper table and every exit code from 0 to 7.
• Verifying an AI agent's actions offline,
  what an audit trail here contains and what it is blind to.

docs/TUTORIAL.md drives the same steps by hand against a real MCP
server. docs/TRACEFOLD_TR.md is the long form: the calculus, the
receipt format, what was measured and under which conditions, related work graded by how well
it was checked, and every non-claim this project makes about itself.
examples/ci/receipt-check.yml is a copy-pasteable GitHub
Actions job that fails a pull request when a delivery's receipt is missing or does not verify.

Contributing

Open an issue before a large change, and bring a measurement. The rules are short and are in
CONTRIBUTING.md; the shortest version is that a pull request
which lowers a count, skips a suite or narrows an assertion has to say so in its own
description. Silently bounded is the failure this project guards against hardest.

Good first things to pick up: a limit that is true but badly worded, a platform in the
"not measured" row above, or a self red-team probe that breaks something we believe holds.

Questions and half-formed ideas belong in an issue. There is no chat channel to point at that
will still be there next month, so this page does not point at one.

Sponsors

None, and none are being solicited yet. If this ends up load-bearing for your work and you
want it to keep being maintained,
say so; knowing who depends on it changes
what gets prioritised more than money would at this stage.

License

Apache-2.0 © Glovrex. See LICENSE and NOTICE for attribution of
incorporated work.