habitat
docs · provable data boundaries

Proving what did — or did not — shape a system’s behavior.

A neutral survey of the terrain, then the two capabilities the field currently cannot deliver — keep-out and take-out — each with a worked, recomputable case study behind it.

Provable Data Boundaries — an industry landscape

A neutral survey of one problem and its terrain: proving what did, or did not, shape a system's behavior. Written to be read cold — history, examples, the current toolbox, and where it runs out. It ends at two capabilities the field currently cannot deliver; each is examined in its own case study.


1. The problem, in plain terms

Modern systems — models, long-lived agents, analytic pipelines — carry derived state: a set of numbers (weights, covariances, learned memories, summaries) that is a function of the data they were exposed to, and that conditions everything they do next. Two questions about that derived state are now being asked in law, finance, privacy, and AI governance, and they are the same question pointed two ways:

Both are claims about the derived state, not about a database. That is what makes them hard, and it is why the tools built for databases point the wrong way.

2. Why it is structurally hard

3. Recent history — how this became urgent

4. The current toolbox — and exactly where each stops

Tool / practiceWhat it doesWhere it stops for keep-out / take-out
Access control, clean rooms, ACLsDeny or gate access to recordsAnswers the inverted problem (deny read); the need here is read preserved, influence excluded. Says nothing about derived state.
Audit logs, lineage (W3C PROV)Attest which events occurredAttest events, not effect. A state influenced by an unlogged input still has clean lineage.
Membership inferenceGuess whether a record was in training"Statistically unsound" as proof (Tramèr group, arXiv:2409.19798); weak at single-record granularity; addresses inclusion, not exclusion.
Machine unlearning / certified removalApproximate removal from weights(ε,δ) bounds only — a bound is a place for residual influence to hide; verification is defeatable (ICML 2024).
Trusted execution (TEE)Attest which binary ranAttests the binary, not a months-long dataflow property; cannot retroactively cover already-accumulated state.
Zero-knowledge / zkVMProve a computation was doneFeasible only as a bespoke build at tiny scale; impractical at high dimension / continuous ingestion; cannot cover state built outside the circuit.

The gap, in one line: every existing approach is either procedural (it attests events or policy) or probabilistic (it bounds influence). None produces a decidable, third-party-recomputable receipt over the derived state itself.

5. Where the terrain ends: two unsolved capabilities

Two specific receipts do not exist in the field today:

  1. Keep-out — a decidable, recomputable receipt that a readable-but-declared set never conditioned the derived state. Documented status: open/unsolved; handled by procedural attestation.Case Study 1.
  2. Take-out — a decidable, recomputable receipt that a record which entered the derived state has fully left it. Documented status: only approximate bounds; a regulator on record that it "cannot be fully guaranteed"; verification shown to be defeatable.Case Study 2.

Each case study states the problem, what a solution is worth, and — in its conclusion only — how a demonstrated instrument addresses it, with the demonstration recomputable by the reader.


Sources

ABA Model Rule 1.10 / 1.0(k); NY 2025 Rule 1.10 amendment · Harvey, "Long Horizon Agents and Ethical Walls" (Mar 2026); Intapp–Harvey ethical-wall integration (Feb 2026) · SEC information-barrier settlement (Dec 2025, $2.5M); Exchange Act §15(g); Advisers Act §204A; FINRA 2241/2242 · GDPR Art. 17; EDPB Opinion 28/2024; EDPB coordinated enforcement action (2025) · EDPS TechSonar 2025 (machine unlearning) · ICML 2024 (arXiv:2408.00929, unlearning verification fragility); certified removal (arXiv:2209.00939); membership-inference unsoundness (arXiv:2409.19798); AI-governance verification survey (arXiv:2407.14981) · EU AI Act GPAI obligations (in force Aug 2025; enforcement Aug 2026) · benchmark-contamination literature.

Case Study 1 — Keep-out: the read-but-don't-learn receipt

A record set stays present and readable, yet is proven never to have entered the state that conditions a system's behavior — and the proof is recomputable by anyone. Today the field handles this with procedure and assertion. This case study shows it done, and hands the reader the recompute.


Intro — the problem and who has it

Some records must remain readable while being kept out of what a system learns. A lawyer may need to open a walled matter's files without that matter conditioning an agent's later work on the other side. A bank's private-side deal data must stay accessible to the deal team while never shaping a public-side model. A revoked-consent record may still need to be servable for the user's own access, while excluded from anything trained. An evaluation holdout must be reachable for scoring, yet provably absent from training.

In every one of these, the owed claim is identical: this declared set did not condition the derived state — and here is proof.

Today that proof does not exist. It is replaced by procedure:

The status is documented and consistent: unsolved, papered over by procedural attestation.

Value — what a real receipt is worth, and why the field can't produce one

A decidable, third-party-recomputable keep-out receipt converts a faith-based assertion into a checkable fact. Concretely:

Why the field cannot deliver it is not for lack of effort — it is structural, per the landscape: access control answers the wrong question (it denies read; here read is preserved), audit logs attest events not effect, membership inference is unsound as proof and addresses inclusion, and unlearning-style tooling offers only bounds. None yields a decidable receipt over derived state.

Conclusion — a demonstrated instrument, recomputable by you

Habitat produces the missing receipt, and the demonstration is recomputable on the reader's own machine — no trust asked.

The worked proof (download-the-kit). In the shipped example, 7,499 declared keep-out records are present and readable inside the kit, and:

Why it holds. The boundary is enforced by construction, not asserted: a read is provably not a write, so a declared record that stays readable cannot have entered the certified state. Read ≠ learn is not a policy; it is a property, and the recompute merely proves it held on this artifact.

What this proves — and does not. It proves a substrate-level keep-out: the declared set, though readable, did not condition the certified covariance geometry, and the exclusion is detectable rather than hollow. It does not speak to other substrates — model weights, retrieval indexes, caches, logs. It is a snapshot ("not in this certified state"), not "never at any time"; each certificate re-proves it for its moment. Verification discloses the vectors to the verifier. A human reads the receipt; it is evidence, never a legal verdict — the wall's legal sufficiency is still for a court to decide.

The field's honest word for this is "unsolved." The receipt above is the same claim, recomputed.

Case Study 2 — Take-out: decidable erasure from consolidated state

A record that did enter a system's accumulated state is removed, and a third party can recompute proof that it fully left — not that it was "approximately forgotten." The field's best today is a probabilistic bound, and a regulator is on record that that bound "cannot fully guarantee" erasure. This case study shows full, decidable removal, and hands the reader the recompute.


Intro — the problem and who has it

When a record has already entered a long-lived system's consolidated state — an agent's learned memory, a fine-tuned model, a summarized profile — and must come out (a right-to-erasure demand, a poisoned batch, a data clawback), the owed claim is: prove it left the state, not just the row store.

Deleting the row is easy and beside the point. In mainstream memory architectures the value lives in the consolidated state: records are folded into model-written profiles or into weights. Removing one record from that is the machine-unlearning problem, and its documented status is stronger than merely "open":

So the honest status here is not just "unsolved" — it is only-approximate, and the verification is defeatable, with a regulator saying so. A bound is precisely a place for residual influence to hide.

Value — what decidable erasure is worth, and why the field can't produce it

A decidable, third-party-recomputable take-out receipt would convert "we ran unlearning; trust the bound" into "recompute it: the state is identical to the one that never held the record." Concretely:

Why the field cannot deliver it is architectural: in weight- or LLM-summary-based memory, the consolidated state is not a recomputable function of anything retained, so removal-from-derived-state can only be approximated and verification can only be probabilistic. Event-sourcing plus re-projection is the strongest near-miss, but LLM re-projection is nondeterministic and numeric re-folds hit the no-universal-tolerance wall — so a third party comparing states is back to negotiating an exploitable ε. Erasure-the-operation is achievable; erasure-the-proof is not — in those architectures.

Conclusion — a demonstrated instrument, recomputable by you

On a substrate where the accumulated state is an exact, canonical function of a provenance-carried record set, erasure becomes recompute-without-the-set and the receipt becomes byte-equality. Habitat is such a substrate, and the demonstration is recomputable on the reader's own machine.

The worked proof (download-the-kit). The kit ships three states and lets you recompute all of them:

Why it holds. The state is an exact, canonical function of its record set, so "erased" and "never had it" either collide exactly or they do not — on any machine. The decidability is the substrate's, not a tolerance's.

What this proves — and does not. It proves a substrate-level take-out: a record that conditioned the accumulated geometry was removed, and the post-erasure geometry is byte-identical to the never-had geometry — decidable, where the field's best is an (ε,δ) bound. It does not reach other substrates — weights, retrieval indexes, caches, backups. Crucially, it requires the record to live on a recomputable substrate in the first place: you cannot erase-with-proof from someone else's opaque memory — which is why this is the frontier capability (the buyer adopts the substrate to get the receipt). It is a snapshot ("out of this certified state"), not "never again." A human reads the receipt; a data-protection authority resolves what it means.

The field's honest words for this are "cannot fully guarantee" and "only approximate bounds." The receipt above is full removal, recomputed.

← Receipts · Ledger