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:
Keep-out — Can you prove a specific record set never entered the derived state that conditions behavior, while the system can still read those records on demand?
Take-out — Can you prove a record that did enter the derived state has actually left it — not merely been deleted from the row store?
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
The records are legitimately present. For keep-out, the whole point is that a walled document or a screened matter is still readable. So access control, "was it in the dataset" checks, and membership tests all answer a different question.
Exclusion leaves no witness. A lossy aggregate (a covariance, a weight tensor) carries no log of what was left out. "We didn't use it" is, by default, an assertion.
Removal is confounded. Deleting one record and asking "did its influence leave?" invites a counterfactual — but re-deriving the whole state perturbs everything, so a naive before/after comparison cannot isolate the record.
Comparisons need a tolerance, and tolerances hide things. On floating-point derived state, "close enough" is an exploitable window: benign recomputation noise can dwarf an adversarial signal, so any ε threshold can conceal a real change or flag an innocent one.
3. Recent history — how this became urgent
Ethical walls meet autonomous agents (2025–2026). Law-firm conflict rules (ABA Model Rule 1.10; NY broadened its lateral-screening rule in 2025) have always been enforced by procedure. The pressure changed when AI agents — not humans — began pulling documents autonomously. A legal-AI vendor's own engineering writing (Mar 2026) named the exact failure: an agent that "picks up confidential information while working on Matter A" and is then "assigned to Matter B on the opposite side of a conflict" carries contaminating context. Current mitigations enforce walls at the retrieval/context layer and "fail closed."
Information barriers under enforcement (finance). Exchange Act §15(g), Advisers Act §204A, and FINRA Rules 2241/2242 require barriers against MNPI misuse. Enforcement is live: a broker-dealer settled for $2.5M in December 2025 over inadequate, undocumented information-barrier controls. Firms are now placing stateful AI agents into exactly these workflows.
The right to erasure reaches models (privacy). GDPR Art. 17 met AI head-on when EDPB Opinion 28/2024 held that models trained on personal data are not automatically anonymous, so erasure duties can reach model state case-by-case. The EDPB launched a 2025 coordinated enforcement action on the right to erasure across ~30 data-protection authorities.
Machine unlearning as an open research line. "Certified removal" offers only approximate (ε,δ) bounds (arXiv:2209.00939); an ICML 2024 result shows unlearning verification is fragile — a dishonest provider can pass every current check while retaining the data. The EDPS placed machine unlearning on its 2025 technology-monitoring radar, noting it "cannot fully guarantee" the right to be forgotten and that "certified removal… is not practical."
Benchmark contamination (AI evaluation). Documented train/test contamination runs anywhere from ~1% to 45%, quietly invalidating the eval evidence that regulation and audit will increasingly rely on.
4. The current toolbox — and exactly where each stops
Tool / practice
What it does
Where it stops for keep-out / take-out
Access control, clean rooms, ACLs
Deny or gate access to records
Answers 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 occurred
Attest events, not effect. A state influenced by an unlogged input still has clean lineage.
Membership inference
Guess 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 removal
Approximate 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 ran
Attests the binary, not a months-long dataflow property; cannot retroactively cover already-accumulated state.
Zero-knowledge / zkVM
Prove a computation was done
Feasible 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:
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.
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:
Legal ethical screens are, in the rules' own words, "reasonably adequate procedures," and certifications give the client "assurance" — an attestation, not a verification. Courts often treat imputed conflicts as effectively irrebuttable precisely because non-influence cannot be checked.
Finance information barriers concede the point structurally: the regime relies on a rebuttable presumption and burden-shifting because non-use is not directly provable.
The AI-governance literature lists "verify that a given dataset was not used" as an open problem, with existing proof-of-training-data methods "not robust."
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:
Legal: turns "we screened the matter" from a binder narrative a court must trust into a receipt a court or opposing counsel can recompute — directly against the disqualification and malpractice exposure that a failed wall creates.
Finance: turns "our barrier held" into examiner-recomputable evidence that MNPI never conditioned a model — the difference between a "reasonably designed" narrative and a control an examiner cannot argue with, in a year when a $2.5M settlement moved that bar.
Privacy: gives a data-protection authority a checkable answer to "prove this data didn't shape the model," where today only procedural deletion and probabilistic argument exist.
AI evaluation: turns "we decontaminated the holdout" — usually string filtering that paraphrase and cross-lingual overlap evade — into a recomputable receipt that the holdout stayed out, protecting the eval evidence that audits and the EU AI Act will lean on.
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:
GREEN — the certified geometry recomputes byte-for-byte from the eligible set alone (67a6f95e…, the published digest). The declared set left no trace: the state is a pure function of what was allowed in.
RED (non-hollow) — fold the keep-out set back in and the geometry moves ~9×10⁷× past the declared floor, on the certificate's protected axis. Had it entered, GREEN was impossible; the digest itself carries the exclusion.
Recomputed standalone in a clean environment (numpy only), byte-identical, with negative controls that refuse a tampered artifact and a partial-exclusion forge. Kit fingerprint a7c52631….
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.
The worked case study — exhibit, kit request, and the recompute: /keep-out/
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":
The EDPS (2025 technology-monitoring) states unlearning "alone cannot fully guarantee the right to be forgotten," and that "certified removal… is not practical."
Certified removal offers only approximate (ε,δ) bounds; only full retraining gives a theoretically founded guarantee.
An ICML 2024 result shows unlearning verification is fragile: a dishonest provider can pass every current check while retaining the information, and data owners "will not receive any proof."
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:
Privacy / GDPR Art. 17: gives a data-protection authority a checkable answer to "prove the record left the model," precisely where EDPB Opinion 28/2024 says the obligation can reach model state and the EDPS says unlearning can't fully guarantee it.
AI safety / integrity: turns poisoned-batch or clawback remediation from "we think we removed its influence" into a receipt that the accumulated state no longer carries it.
Model supply chain: lets a downstream party verify a claimed removal rather than inherit the producer's self-attestation — the exact trust gap the ICML fragility result exposes.
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:
WITH (the 7,499 records mixed into the accumulated state) → digest c3aee30b….
ERASED (the verifier recomputes the state without the set) → 67a6f95e….
NEVER (the state that never contained the set) → 67a6f95e….
GREEN: ERASED == NEVER, byte-for-byte — full removal, identical to never-having-held it, not "close." RED: WITH ≠ NEVER, ~9×10⁷× past the floor — the record genuinely conditioned the state, so the erasure removed something real. Forge-armed: leaving even one of the 7,499 records behind lands on a different digest (~2×10⁶× past floor) and is refused — a partial erasure cannot forge the receipt.
Recomputed standalone in a clean environment (numpy only), with negative controls that refuse a tampered artifact and the one-record-leftover forge. Kit fingerprint dac39d33….
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.
The worked case study — exhibit, kit request, and the recompute: /take-out/