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.
Top comments (2)
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.
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.