The README for the thing I'm building puts the limits above the features. Not as a humility move. Reading them first can save you the afternoon, and a limits page that quietly rewrites its own history has no standing to be believed about the present.
So here's the list, written before anyone asked for it. The project is a verification layer for changes an agent wants to make: judge the change before it lands, store its inverse first, sign the outcome, let a stranger re-check the record offline. Everything below is a place where that sentence stops being true.
Things it structurally cannot do
A write running as root goes around the whole thing. There's no clever answer to this and I'm not going to pretend there is one.
If the policy encodes the wrong intent, the gate enforces the wrong intent faithfully. The system checks that a change matches a predicate you supplied. It has no opinion about whether your predicate is any good, and a signed receipt saying a change was admitted is not a statement that admitting it was wise.
An issuer who cuts the tail off their own chain still verifies clean. Inclusion proofs are internally consistent by construction, so consistency with an issuer's own log proves the issuer is consistent. You need an anchor outside them, and if you don't have one, you're trusting the party you were trying not to trust.
Coverage is bounded by declaration, not by ambition
Effects that reach a substrate by any route other than an adapter are not prevented, not detected, and not seen. That's a design decision rather than a gap I'll close later.
Concretely: an agent that starts its own tool server is outside the proxy. A call that only reads is outside it too. A server that maps one path onto another underneath the system is invisible to it, because the system sees the name it was given and not the inode it landed on. Five substrate families are covered as of 2026-08-29, being filesystem, Git, tool-protocol proxy, PostgreSQL and MySQL, and the MySQL adapter has never been run against a live instance. It passes the conformance harness's static shape checks and that is all it has ever done.
Counts prove less than they look like they prove
A verdict count proves that nothing was hidden from the counter. That's all it proves. Weaken the policy until it admits everything, run a thousand changes through, and the count reads perfectly clean.
Two verifiers can also legitimately be shown two different chains, which is a property of any log that doesn't gossip, not a defect I introduced.
Three surfaces have zero runs
Windows native, OneDrive, and SMB. Not "probably fine", not "should work". Zero runs, as of 2026-08-25, declared rather than discovered.
Related and worse: the filesystem adapter's fsync call isn't gated by platform. On Windows-native filesystems the persistence a receipt reports may not be the persistence the OS actually gives you. Kernel confinement is Landlock, so it's Linux only, and it derives whether a tool writes from a catalogue while taking where it may write from the invocation, which is a weaker construction than the specification clause asks for. The crate says so in its own documentation rather than pretending.
The formal side stops earlier than "machine-checked" sounds
The Lean model and the Rust implementation are compared by a differential test over 1,500 conformance vectors. There's no refinement theorem connecting them, and a comparison finds differences without establishing equivalence.
The distribution of the theorems is its own lesson. Roughly 65% of them sit in the three deepest semantic files. The artifact that actually reaches an external consumer carries three, and exactly one theorem in the whole model has boundary vocabulary in its name. The defects found afterwards were at the boundary. Rigour drifts toward whatever is interesting to prove, so a theorem count measures where the fun was, not where the coverage is.
The model also cannot express decode parity. Neither a decode function nor a raw-byte representation exists in the Lean tree, so no theorem there can state that decoding a canonical value returns the original bytes. Whether a refinement relation can be stated at all for this system is an open question, and "no, and here's why" would be a publishable answer.
Two of the nine layers have zero implementation: the search layer and the evolution layer. Where the design describes them, it's describing a target.
Smaller ones that are still real
Engine::plan fixes its prediction target to None unconditionally, so nothing anywhere compares a predicted outcome with what actually happened. Where fixtures appear to supply a prediction, the fixture is supplying it.
engine_version is never captured or shown, so no receipt records which implementation produced a given verdict. That's awkward, given the load-bearing claim in the design is that a layer's interface should include who is answering.
The on-disk index cache holds one transformation per intent. It's a line, not a tree, so it can't represent a branching undo history, and any feature that lets an intent branch needs that changed first.
The public CLI names things only the project's internal vocabulary explains, and several flags you need for correct use aren't shown by --help. A first-time reader meets that surface before meeting any of this writing.
There's also a third-party product with the same name on a .dev domain, found during a naming survey. Live collision, not a resolved one.
The reply I want
If you find a limit that isn't on this list, that's the useful reply, and it's the one that costs me nothing to receive because it turns straight into inventory. The list being wrong by omission is the failure mode I can't detect from the inside.
github.com/TraceFold/tracefold, Rust, Apache-2.0. Not released. Correction 2026-09-01: one Linux x86_64 tarball has been on the v0.1.0-alpha tag since 2026-08-31, built outside CI. Not on any package registry, which is what the struck words were trying to say and no longer quite do.
Top comments (10)
Hello Mahiro Hirakawa, I am Kane Lim from Hong Kong. I have over 10 years of development experience. I am writing this because your post was interesting.
What stands out to me is that you are treating limitations as part of the verification model rather than as documentation debt. That is exactly the right direction for an agent mediated change system.
The next step I would consider is making the limitation inventory executable. Every adapter could expose explicit capability claims covering observation, mutation, rollback, durability, confinement and provenance. The conformance harness could then generate negative tests directly from those claims, so an unsupported substrate becomes a mechanically visible state rather than documentation that can drift.
For the trust problem, I would separate local consistency from external authenticity. A signed append only log should periodically commit its Merkle root to an independent transparency anchor. Verifiers could then detect equivocation, truncation and divergent histories rather than merely proving internal consistency.
The Lean boundary is equally interesting. Instead of immediately pursuing full refinement, define a minimal byte level observational semantics around canonical encoding and decoding, then connect Rust behavior through generated conformance vectors. That creates a precise seam where differential testing can eventually evolve into a refinement argument.
I also think engine_version and adapter capability hashes belong directly in the receipt. Reproducibility depends not only on what happened, but which implementation and capability contract produced the verdict.
Taking these in order, because three of them map onto things that exist and two of them name real gaps.
Executable capability claims: the closest thing in the tree is the substrate conformance suite. Every adapter answers the same contract, and the suite runs deliberately flawed substrate implementations against it to prove the checks can go red. What it doesn't do yet is what you describe. Our negative tests are hand-built flaw cases, not derived from declared claims, so an adapter that overstates a capability only fails if we anticipated that exact overstatement. Generating refusal tests from the claim set is the stronger form, and I don't have a counterargument to it.
Transparency anchor: agreed that internal consistency is the weaker half. The log already exports its checkpoint in C2SP note form, which is the entry point for the cross-anchoring you describe. Committing that root to an independent anchor on a cadence isn't wired up, so today a verifier can catch tampering within the history it holds, but equivocation between histories is out of scope, and the limits page says so rather than hoping nobody asks.
The Lean seam: your byte-level observational semantics suggestion is close to the shape we landed on. Canonical encode and decode as the boundary, generated vectors pinned with the exact rust sha and Lean toolchain they were cut against, differential now, refinement maybe later. No timeline for the refinement half, and I won't invent one.
engine_version and capability hashes in the receipt: not there today, and I think you're right that they belong. Reproducibility currently leans on the journal, which is a weaker position than the receipt saying it itself.
Any of these is worth pulling on further, and this thread is a good place to do it.
that's perfect. I am glad to hear that my reply was of some help.
I would like to get to know you better. Would you please contact me? You can find contact information in my Bio.
I send you google message. please check.
Nothing has reached me, and I would rather say so than leave you waiting on a reply that was never coming.
I do not have Google Chat or Gmail wired to this account, so a message sent there lands somewhere I never open. That is my gap, not yours.
If it is about the thread, put it here and I will answer it in the open where the rest of the discussion is. If it is genuinely not for a public thread, the address on my profile reaches me and I do read that.
One that isn't on the list: your differential test can only report a difference, so it can't distinguish "the two sides agreed" from "the two sides were never actually given different input". A vector generator that quietly stops varying something reads as 1,500 passes.
We lost a while to that shape once. A falsification step whose edit didn't apply, so the gate it was supposed to prove dead came back green and read as alive. The fix was cheap and ugly: assert that the mutation landed before trusting the comparison, so a no-op fails loudly instead of passing.
I'd guess your conformance harness already pins the vectors as fixtures rather than generating them, which would kill most of this. Does it?
Pinned, yes. The cross-language differential suite is 1,500 vectors in six JSONL files, 250 per property, committed as fixtures, and every line carries the rust git sha and the Lean toolchain string it was generated against. So a generator that quietly stops varying something can't silently shrink the space: the vectors it would have produced are already frozen in the tree, and regeneration shows up as a diff, not as 1,500 quieter passes. The violation side is frozen too. The admissibility file alone holds 113 vectors where the expected answer is refusal, so a comparator that lost its inputs starts failing on those before it gets to flatter the agreement side.
One honest caveat: those fixtures live in the dev tree and aren't in the public repo yet, so today you can't check me on this, which is exactly the kind of claim I tell people not to trust. The adapter conformance tests are what's public.
Your "assert the mutation landed" fix is the same discipline we converged on from the other side: don't trust a gate until you've watched the injection actually draw red. Had a version of your shape this week, a fault that every runtime suite waved through, and it only went red when a new end-to-end probe asserted the injection itself had landed before comparing. Cheap and ugly beats elegant and blind.
And you're right that it wasn't on the list. It should be. "Differential agreement is only meaningful if the inputs actually varied" is a limit of the method, not of the implementation, and those are the worst ones to leave implicit.
The strongest part here is treating “verified” as a bounded claim rather than a trust claim. One thing I’d add is that every verification result should carry its coverage boundary as data, not just documentation: adapter/version, substrate, policy version, execution path, and whether the effect was actually observed or only inferred. Otherwise a perfectly valid receipt can get reused as evidence for a case it never covered. In agentic systems especially, the dangerous failure isn’t an invalid proof it’s a valid proof being interpreted outside the conditions under which it was produced.
The observed-versus-inferred part is the one we already carry as data: the undo attestation's witness field is an enum on the wire, Attested or Unobservable with a reason, so "we watched the effect" and "we concluded the effect" can't collapse into one claim after the fact. That distinction being wire-level rather than doc-level is load-bearing for exactly the reuse problem you describe.
The rest of your list is where we're thinner, and I'd rather say so than nod along. Adapter identity and version, policy version, engine build: none of those are in the receipt today. Engine version and a capability hash are on the convert list, not shipped, and until they land a receipt genuinely can't tell you which implementation produced its verdict.
Your framing of the failure is the right one, a valid proof read outside its production conditions. It's why the limits page here is written as a set of dated conditions instead of prose apologies. But a receipt carrying its own boundary is stronger than the project carrying a boundary page, and we're only partway from the second to the first.
Some comments may only be visible to logged-in visitors. Sign in to view all comments.