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 · Discord · Glovrex
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.
The CLI is not released. There is no gx binary to install from a registry, so running the tool
starts from a clone. Checking a receipt somebody hands you is a separate question with a shorter
answer, and that one installs nothing.
In a browser, with nothing installed: https://tracefold.github.io/tracefold/verify.html
Paste or drop in a receipt and the key it should verify against, plus a checkpoint if you were
given one. The check runs in your tab, on the same WebAssembly build of the same function
gx receipt verify --offline calls, so what comes back is the engine's answer rather than a
second opinion about it. If you have no receipt yet, four buttons load real files out of the test
suite. Nothing you paste leaves the page, and you are not asked to take that on trust: the page
wraps fetch, XMLHttpRequest, WebSocket and sendBeacon and prints the running count of
requests its own code has made, on screen, where it stays at zero. Save the file, disconnect and
reopen it if you would rather check it that way.
It answers in three values, not two. Verified, Refuted, and a third for a check that did
not conclude, meaning the signature held but no ledger claim was checked, or this build cannot read
that receipt. The third is the one worth having. A two-valued verifier must file "I could not read
this" as either a pass or an accusation, and the command line still collapses it: exit 7 covers
both a tampered receipt and one too new to parse, and the field that separates them sits in the
JSON body an exit code cannot carry. The page reads that body, so it does not call a document
forged when the truth is that it failed to read it.
What the page cannot do is make a receipt. It checks one. Producing one is still the clone below.
What the clone 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.
If you write JavaScript, there is a second shipped route. @mahirhir/tracefold is on npm under
Apache-2.0 and carries that same WebAssembly verifier, so checking a receipt costs a package
install and six lines, with no Rust toolchain and no WSL. It also talks to a running gx serve,
which the browser page does not.
npm i @mahirhir/tracefold
F=https://raw.githubusercontent.com/TraceFold/tracefold/main/crates/gx-cli/tests/fixtures/attach_face_frozen/issued_2026_08_22
curl -sO $F/commit_receipt.json -O $F/key.pub.json -O $F/checkpoint.jsonimport { readFileSync } from "node:fs";
import { verifyReceiptOffline } from "@mahirhir/tracefold";
const key = JSON.parse(readFileSync("key.pub.json", "utf8"));
const result = verifyReceiptOffline(
readFileSync("commit_receipt.json", "utf8"),
key.key_id,
key.public_key,
readFileSync("checkpoint.json", "utf8"),
key.key_id,
key.public_key,
);
console.log(result.valid, result.checks.inclusion, result.anchor_authenticated);
// true verified trueIt never throws. A bad signature, a wrong key, a malformed document and an argument that is not a
string all arrive as {valid: false, error: "..."}, because whether a receipt is good is an
answer, not an exception. Drop the last three arguments and you get valid: false with
inclusion: "unanchored", the CLI's own refusal to call a receipt verified when it cannot place
it in a log.
The module it loads declares exactly one host import, and that import is a table initialiser, so
there is no socket and no clock inside it. It is 423,910 bytes, sha256 8f7064b675cc89e5..., the
same bytes sdk/wasm-verify/ builds in this tree. Offline is a property of the artifact you can
check rather than a promise on this page.
One route is still unfinished: prebuilt binaries would remove the compile step for the CLI itself. That has not landed, so treat it as in progress rather than as a plan you can use, 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.jsonNow 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.jsonExit 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.jsonExit 7. Every command on this page was run in that order on a fresh clone before being
printed here.
If it exits 0 instead, that is a finding, and we would rather have it than not. The same
goes for anywhere the tool turns out to claim more than it actually checked. You are now
holding the three files a verification needs and the binary that reads them, which is
everything required to attack the claim: open an issue with what you ran, and it gets recorded
here whatever it costs us.
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.
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.
| out of scope | why it cannot be closed from the inside |
|---|---|
| Root or kernel-privileged writes | They bypass the tool entirely, and this build does not detect that |
| Writes into the tool's own state directory | A detector living in that directory cannot judge it. The defence is an artifact held elsewhere |
| A policy encoding the wrong intent | It is enforced faithfully. No verification reaches the question of whether the rule was right |
| Undoing one change and not another, across objects | Today the unit is a single transformation, and the check is a compare-and-set on the same object. If one change was made after reading another, nothing here records that it was read, so there is no way to ask for one back without the other |
| An issuer who cuts the tail off the chain | A hash chain proves that what you hold has not been edited. C970 It cannot prove that what you hold is all there was. An issuer who hands you a genuine but older checkpoint, with the last entries removed, produces something that verifies. Detecting that needs a newer checkpoint from somewhere the issuer does not control, which is what an external anchor is for, and we do not publish to one yet |
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 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, with one exception named here. The bare 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 either gets you nothing.
The exception is the scoped @mahirhir/tracefold 0.1.0, published 25 August 2026, which is
a real package and the one the JavaScript above installs: it verifies receipts and does not
contain the engine. There is no released gx binary anywhere, the tool itself is still a
build from source, and nothing above should be read otherwise. The download counters on the
two placeholder 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.
| measured | under what conditions | |
|---|---|---|
| Test floor | 2,602 | probes across 454 suites, plus the SDK's 36 passed / 0 failed / 7 skipped. Frozen harness, fresh clone, one machine, single run, 25 August 2026. This floor has moved more than forty times in a month; it moves with every repair round |
| Machine-checked | 117 | theorems in Lean, 12 of them counterexamples, out of 118 line-initial declarations. The remaining one is an axiom, a statement assumed rather than proved, and it is named in the report. No sorry, the keyword standing in for a proof nobody wrote, so there are none. Proof rather than bounded model checking: nothing here is true only up to a scope · re-counted on a fresh clone 26 August 2026 |
| Open holes | 0 | high severity, open as of 25 August 2026, counted as accepted findings whose repair has not been accepted. This number was 3, then 0, then 1, then 0 again inside a week, so read a zero here as the state of one afternoon rather than a property of the system. Forty-four adversarial rounds have landed, plus independent B-band and S(1) audits, all at zero as recorded |
| Not measured | 3 | Windows native, OneDrive, SMB. Zero runs out of the three, as of 25 August 2026 |
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.mdThose 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.
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.
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 normalOn 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.
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
0to7. - 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.
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, or in Discord if you would rather think out loud. The invite above is the one we intend to keep; if you find it expired, that is a bug in this page and an issue about it is welcome.
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.
Apache-2.0 © Glovrex. See LICENSE and NOTICE for attribution of incorporated work.