A Trace Is Not a Replay

In March I published Agentic AI and the Verifiable Trace. It argued that every data protection concern about autonomous agents "reduces to a single question. Can you prove what the agent did?" and it offered the verifiable trace as the answer. This chapter corrects it. Some of what it said survives. The central noun does not.

Thesis. "Verifiable trace" has to be split into four guarantees: recording what happened, replaying the deterministic steps, regenerating the model's output, and checking a certificate. No one of them implies any other, which I prove below in a small model. To establish that a run obeyed a rule you need a faithful record and a passing check, and you need nothing from the generator's reproducibility. Regeneration is the guarantee accountability needs least.

The claim that would embarrass me if wrong is the third sentence of that thesis. If a court or regulator refuses to treat a record plus a checked certificate as evidence unless the output can also be regenerated, then for practical purposes I am mistaken, and I say below what would count.

A disclosure. I build AI systems for law firms, and the systems this chapter criticises are mine. The essay named them as reasons to trust the architecture and sent readers to the Elan page. What I audit below is what that page describes today, built days after the essay: the record type and HMAC modules date from 6 and 7 April 2026. I have not audited the event log that existed in March. So this is not the code the essay rested on. It is what I built next, in the essay's vocabulary, and it inherited the category error.

What I claimed

These sentences are from the March essay, verbatim.

1. "Every agent action, including intermediate reasoning steps, tool invocations, and data accesses, is recorded in a durable, append-only audit log with git-native provenance."
2. "When a data subject exercises their right of access, the system can reconstruct exactly what data the agent accessed, what decisions it made, and what outputs it produced, all the way down to the individual reasoning step."
3. "The certificate is the trace."
4. "The receipt is a durable, tamper-evident artifact that travels with the output through downstream systems."
5. "The trust anchor is the Lean kernel, not the company's infrastructure."

The essay uses the phrase for recording and for certificates, and blurs replay through "reconstruct exactly". The words "replay" and "regenerate" do not occur in it. It says a conventional system's "output is reproducible" and that an agent's "behaviour may vary between invocations", and never says whether that variation touches the evidence. The defect is a category error. Sentence 3 identifies two different kinds of object. Sentence 2 uses "reconstruct" for what a log, a replay and an explanation would each have to do separately.

Sentence 5 needs its sequel, because the essay did state a limit: "This does not solve the problem of a deliberately malicious operator who fabricates the premises (garbage in, garbage out)", and "The remaining attack surface is social, not cryptographic: lying about facts, not about logic." That second sentence is the wrong one. A rewritten log is not a social problem. It is a question of keys, anchoring and audit, and those are exactly what I had not built.

What survives is the essay's split between proved, attested and judgment-dependent evidence, and its point that a Lean proof can be checked by someone who does not trust whoever produced it. That split classifies evidence by what you must trust. The essay lacked the second axis: what the evidence establishes.

Temperature zero does not mean the same answer

The cleanest published measurement is from Thinking Machines Lab (He and Thinking Machines Lab, 2025). They sampled 1,000 completions from one model, Qwen3-235B-A22B-Instruct-2507, at temperature 0, with one prompt, "Tell me about Richard Feynman", generating 1,000 tokens each. They got 80 unique completions, the most common occurring 78 times. All were identical for the first 102 tokens. At the 103rd, 992 went on to "Queens, New York" and 8 to "New York City". With their batch-invariant kernels, all 1,000 were identical.

The result for one request depends on how many others share its batch, because kernels choose different numerical reduction strategies at different batch sizes, and batch size depends on server load. The post's phrasing is "the primary reason nearly all LLM inference endpoints are nondeterministic is that the load (and thus batch-size) nondeterministically varies".

Three limits apply.

1. It is one model and one prompt. It gives no rate for other models.
2. The performance figures are from a different setup: one GPU, Qwen-3-8B, 1,000 sequences of 90 to 110 tokens. Total time was 26 seconds on default vLLM, 55 deterministic and 42 with an improved attention kernel, so about 2.1 and 1.6 times slower. That is workload time, not per-request latency, on kernels the authors had not put significant effort into optimising.
3. Batch invariance removes one cause, and regeneration has several. vLLM now offers a batch-invariant mode, off by default (vLLM source, read 02/11/2026), on a listed set of NVIDIA, AMD and Intel accelerators (vLLM docs). Its documentation adds that "vLLM only provides reproducibility when it runs on the same hardware and the same vLLM version" (vLLM reproducibility).

OpenAI's seed parameter documentation says "Determinism is not guaranteed" (OpenAI Cookbook). Models are also withdrawn: Anthropic "regularly retires older ones" (Anthropic, model deprecations), and on Google's Gemini API a shut-down model is "completely turned off, and the endpoint is no longer available" (Google, Gemini deprecations). Regenerating a 2026 decision in 2031 requires weights the deployer may never have held.

My own published schema carries the error in one line. The Elan page lists model_temperature: Float, # 0.0 for deterministic mode, for a record whose example model is a hosted API. At temperature 0 a hosted endpoint has lost one source of randomness. It is not in a deterministic mode.

Four guarantees

The table below is the chapter's main artefact. "Replay" has several meanings, so these definitions are closed. Replay here means pushing recorded steps back through the deterministic harness. It does not mean an attacker re-presenting a valid message, and it does not mean Lean's lean4checker, which "replays" proofs through the kernel, which in this table is checking.

None of this distinction is mine. Each row has its own literature.

Recording. Crosby and Wallach define tamper evidence by an audit process rather than by a data structure: the logger "must be able to prove that individual logged events are still present, and that the log, as seen now, is consistent with how it was seen in the past", and without auditing "the log is not tamper-evident" (Crosby and Wallach, 2009). Certificate Transparency uses Merkle trees and still warns that its auditing "can be circumvented by a misbehaving log that shows different, inconsistent views of itself to different clients" (RFC 9162).

Replay. Record-and-replay debuggers such as rr exist in part for "'black box' forensic analysis of failures in deployed systems" (O'Callahan et al., 2017). Temporal, a durable execution system, already places the model on the correct side of the line: "To handle non-deterministic operations like API calls, LLM/AI invocations, database queries, and other external interactions, put them in Activities. Activities execute outside the replay path" (Temporal docs). In that design the model's output is an input to replay, read back from history. Nobody asks the model again.

Regeneration. Reproducible builds define it exactly: "any party can recreate bit-by-bit identical copies of all specified artifacts" (Reproducible Builds).

Checking. Translation validation for seL4 proves a refinement between C semantics and binary semantics, on "binaries generated by unmodified gcc 4.5.1" (Sewell, Myreen and Klein, 2013). The compiler is left unverified and its output is checked. The earlier proof had to "assume correctness of compiler, assembly code, and hardware" (Klein et al., 2009), so a generator left the trusted base untouched. The Guaranteed Safe AI framework has the same shape, with a world model, a safety specification and a verifier that provides "an auditable proof certificate", which holds "relative to the world model" (Dalrymple et al., 2024). AlphaProof is the striking case: a reinforcement learning system that searches for proofs in the Lean environment and produced proofs of three of the five non-geometry problems at the 2024 IMO (Hubert et al., 2025). The paper does not make this point, so take it as my inference: those theorems stand whether or not the search could ever be rerun to the same proof.

The model

I use the Ashdown instruction, the book's worked example, an invented legal-intake case. A research agent holds a grant to read and summarise a privileged advice document. It does not hold a grant to send that document externally.

A generator proposes a step, given the current state and the server load, and a deterministic harness applies it. Load stands in for whatever a batch-sensitive kernel responds to. Reads leave no footprint in the tracked state. Everything below compiles on Lean v4.29.1 with no libraries, copied from lean/BuildingInSteel/Replay.lean. It contains no neural network, no Lean kernel and no deployed system.

Replay does not care about the generator. This compiles, and it is proved by induction over the run.

theorem replay_reproduces_any_generator (g : Gen) (w : World) (s : State) (ls : List Load) :
    replay w s (logOf g w s ls) = finalState g w s ls := by
  induction ls generalizing s with
  | nil => rfl
  | cons l ls ih => exact ih (apply w s (g s l))

It holds for every generator, batch-invariant or not. replay_needs_same_world shows divergence when a tool result was not pinned. replay_blind_to_reads shows that inserting a read anywhere leaves the replay result unchanged. In data protection the access is often the harm, and a matching replay cannot tell you whether an agent looked at something.

Regeneration is a separate matter. invariant_regenerates proves that batch invariance suffices when everything else is held equal, and regeneration_not_guaranteed exhibits a generator that gives different logs at different loads. verdict_survives_nonregeneration proves that those two different logs both pass the checker, the Feynman result in miniature. steadyLeak_invariant and regenerating_is_not_passing give the reverse case, a generator that regenerates perfectly and leaks at every step, so that on any non-empty run no certificate passes. Determinism is not correctness.

The checker takes no generator argument. Any function that lacks a parameter cannot depend on it, so "the verdict is independent of the generator" is, on its own, a consequence of a type signature. The substance is check_sound, and its corollary check_sound_any_generator: the check is sound with no assumption about where the log came from. Two illustrations go with it. provenance_checker_unsound is the contrast case, a checker I defined to be bad, which consults the vendor's name and so passes a leak. two_generators_one_fact shows what the kernel sees: by proof irrelevance, a proof obtained with decide and one written as rfl are one object. That is true of any two proofs and could not have been false, but it is about real Lean and not my toy.

The main positive result composes two guarantees and uses no property of the generator. It compiles.

theorem faithful_and_certified_establish_run (P : Policy) (g : Gen) (w : World) (s : State)
    (ls : List Load) (recorded : List Step) (c : Cert)
    (hf : recorded = logOf g w s ls) (hc : check P recorded c = true) :
    Compliant P (logOf g w s ls) = true := by
  subst hf
  exact check_sound P _ c hc

The hypothesis hf is doing the work, and certificate_silent_without_record shows it cannot be dropped. "The certificate is the trace" is false because a certificate is about the record, and the record might be false.

The independence result is the formal core of the thesis. It also compiles.

theorem no_guarantee_implies_another (a b : Guarantee) (hne : a ≠ b) :
    ∃ s, holds a s = true ∧ holds b s = false := by
  refine ⟨only a, ?_, ?_⟩
  · rw [each_witness_has_exactly_one]; simp
  · rw [each_witness_has_exactly_one]; simpa using fun h => hne h.symm

The proof rests on four concrete scenarios, each satisfying exactly one guarantee. all_four_jointly_satisfiable rules out one cheap way to get independence, an unsatisfiable guarantee. It does not rule out the other: regenerate and certify read disjoint fields of Scenario, so that pair comes apart by the shape of the model. The formal result shows that the concepts come apart once modelled separately. The argument for modelling them separately is the table above and the failures below.

The bare guarantees are independent, but they do compose. record_and_pinned_gives_replay proves that a faithful record and a pinned world give replay, and onlyRecord escapes it only because the world changed. So in the model, where a log holds whole steps, what replay adds over recording is the pinned tool results. A real record also has to keep the content, as a hash-only record below does not.

Proved, then: everything named above, with kernel-checked proofs depending at most on propext, Classical.choice and Quot.sound, and on no sorry. Sketched: that real systems behave like the model. The certificate here is a list of grant indices, and since compliance in the model is decidable it could simply be recomputed. A certificate earns its keep when finding it is far harder than checking it, as with a Lean proof, and the model does not show that gap. The record, replay and regenerate tests all compare with the true run, a view no outside verifier ever has. A real replay compares with a stored result, which is itself only as good as the record. For the distance between a model and running code, see The Proof Passed. The Wrong Thing Ran.

What my own artefacts did

A theorem about tampering that is not about tampering. The Elan page says of its hash chain: "valid_chain?/1 verifies the full chain integrity; proved in Lean 4 (chain_tamper_evident theorem)". I reread that theorem and the module's validity check, which sits in a private repository, so I describe it here rather than quote it. The check walks the chain and compares each record's stored previous-hash string with the stored hash string of the record before it.

No hash is computed anywhere in it. The theorem then assumes the chain is valid and that a link is broken, and derives False. So what it says is that a chain with no broken links has no broken links, and nothing in the statement relates a record's contents to its hash. Worse, when I ran the file today on Lean v4.29.1 it failed at its own header, an import placed after a module comment, and with that moved a module it depends on failed too. The directory pins no toolchain and I have not tested older ones, so I cannot say whether it ever built. Either way, this is what the book exists to catch: a formidable name over a statement that claims nothing. link_check_ignores_contents makes the point in this chapter's file: for a link check of that shape, editing every payload leaves the verdict unchanged. The Elixir valid_chain?/1 the page names has the same shape. A separate verify_record/1 recomputes one record's hash, and I found no code that calls it. So "verifies the full chain integrity" and "proved in Lean 4" are both false.

Chains and keys. The same page says GroundtraceRecord is "signed". The code that builds that record, which sits in a sister repository and not in Elan's, computes an unkeyed SHA-256 and holds no key, and the listed schema has no signature field. Anyone with write access can edit a record and recompute every later hash. rebuilt_chain_verifies proves that generally: any log can be sealed into a chain that verifies.

Elan is not all like this. The page also lists an "Immutable HMAC-chained event log" and a "Cryptographic HMAC chain-of-custody", and the two modules behind them do key their chains. I read those modules for the chain and the key only. A key does not answer the question. It is a symmetric secret the operator holds, and in that code it falls back to a development default unless configured, so an operator can still rewrite and re-key. Keying stops an outsider. It does not stop the party whose conduct the log records.

anchor_binds gives the condition under which rewriting stops: equal digests against a head out of the operator's reach, a collision-free hash, and a committed log length, which is what a transparency log's tree size supplies. The injectivity assumption is an idealisation of collision resistance, anchor_hypothesis_satisfiable shows it is not empty, and weak_digest_collides shows what happens when it fails. Then green_evidence_wrong_run puts it together: chain verifies, check passes, and the actual run contained a leak nobody logged. Anchoring attests the log. It does not attest the world.

A logger that fails open. The page says of its telemetry: "Graceful no-op if agent not running or store path not writable." For evidence, that means the agent keeps acting while the record stops. failOpen_faithful_iff proves that such a log is faithful exactly when the store never went down, and failClosed_faithful gives the other side, true by construction in a model where the accepted write and the step are one atomic event. Real logging has to earn that atomicity: a step can fail after its record, or bypass capture altogether. Still, missing provenance has to block the step.

Reconstruction from hashes. The page says "An auditor with the record can reconstruct the full execution path without access to the original runtime", and the record stores prompt_hash and raw_response_hash. A hash lets you confirm a text you already hold. It cannot give you the text. Replay needs the plaintext, and keeping plaintext prompts and responses collides with the retention section of my own essay. I did not name that trade-off, and Nobody Is Paid to Delete and Yesterday's Permission deal with what follows.

Reasoning steps. "All the way down to the individual reasoning step" invites reading recorded reasoning as an account of the cause. Turpin et al. found chain-of-thought explanations "can systematically misrepresent the true reason for a model's prediction" (Turpin et al., 2023). Chen et al., testing reasoning models across six kinds of hint, report that where models used a hint the reveal rate "is often below 20%" (Chen et al., 2025). Those are hints planted in tests, not agents processing access requests, but they are enough: a recorded reasoning step is text the model emitted, and may not be why it acted. That question belongs to interpretability research, which the four guarantees complement and do not replace.

Public means checkable. The essay said "The implementations are public." On 02/11/2026 the Elan repository linked from its page returned 404 to an anonymous request, and so did the repository holding that theorem. A reader cannot check what I have just described. The essay's own boundary note said Elan's design and specification were public. Then it said the implementations were. The second sentence is the false one today, and I cannot now show it was ever true.

I read the record module, its Lean counterpart, the two HMAC modules and the public page, and I have not audited those systems as a whole. The verdicts above are on GroundtraceRecord unless I say otherwise.

What the sentences should have said

The essay's claim that a reader can verify a proof "without trusting the system that produced it" is true only with conditions. Lean's own documentation distinguishes honest from malicious proof attempts and says the malicious class "includes un-reviewed AI-generated proofs and programs" (Lean reference manual). Building a Lean file runs its metaprograms, so a hostile generator may change how a statement is interpreted. Its gold standard, comparator, builds in a sandbox, exports the proof term, replays it outside the sandbox, and checks that theorems "Prove the same statement as provided in Challenge" (comparator), assuming "The Lean kernel is correct". Separating generation from checking has to be enforced by the environment. The model gets it free because it has no such attack.

How it fails

• Operator rewrites the log. A hash chain alone will not notice. Publish heads to witnesses the operator does not control, and audit them, or the log is not tamper-evident by Crosby and Wallach's definition.
• Signing key stolen. Records anchored before the compromise stand. Records after it are unattested until re-anchored under a new key, and they should be labelled so.
• Witnesses disagree. That is the split view RFC 9162 warns about. Treat it as a blocking failure.
• Checker bug. Certificates can all be re-checked after a fix, and with more than one checker. Lean4Lean is a second typechecker for Lean 4, running between 20% and 50% slower (Carneiro, 2024).
• Certificate presented for another run. The statement must name the anchored digest of the log it concerns. My model's check is relative to a log given as input, so it does not address this.
• Stale policy. verdict_follows_policy shows a pass under the grant as issued and a refusal under the revoked one, for the same step at tick 6. The verdict is exactly as current as its inputs.
• Wrong statement. Every certificate stays valid and none of them helps. No checker catches this, which is the subject of Who Gets to Write the Specification?

What exists and what is proposed

Exists: the Lean file and its proofs; batch-invariant kernels from Thinking Machines and a vLLM mode; durable execution with model calls outside the replay path; transparency logs; the Lean kernel, lean4checker and comparator. Exists and is defective: GroundtraceRecord's unkeyed, fail-open chain and its vacuous theorem.

Proposed, and not built by me: an evidence manifest for agent runs. The nearest existing work is in software supply chains. The in-toto Attestation Framework specifies "verifiable claims about any aspect of how a piece of software is produced" (in-toto), SLSA defines a provenance predicate within it (SLSA), and Rekor is a transparency log auditors can monitor for consistency (Sigstore docs). A manifest should be built on those formats, not beside them. As far as I can see, it adds two things: a rule that each label carries required premises and cannot be issued without them, and a compliance predicate over agent runs in place of a statement about a build. Every claim about a run carries one of the four labels and the premises that label requires, and a claim with a missing premise cannot be issued. The roles stay distinct: the harness signs records, independent witnesses co-sign heads, and a checker the generator cannot reach issues the verdict. The compliance claim needs a recording label with an externally anchored head, written fail-closed, and a certificate label bound to that head's SHA-256 digest over one stated canonical serialisation. Its trusted base is then explicit: the capture point, the signing key, the witnesses, the kernel, the statement. The gap between harness and model would need differential testing of the deployed harness against replay, which I have not done. "Would the model say this again?" needs the regeneration label, and most deployments will honestly never be able to issue it. Open: how to keep content for replay and still honour erasure. I have a direction, which is to encrypt per data subject and chain over ciphertext, but no worked design, and erasure would then remove the ability to replay that step.

What the law asks for

I looked at two texts. This is not legal advice. Article 12 of the EU AI Act says high-risk systems "shall technically allow for the automatic recording of events (logs) over the lifetime of the system" (Regulation (EU) 2024/1689, Article 12). The UK's Article 22C requires safeguards that "enable the data subject to contest such decisions" (Data (Use and Access) Act 2025, s.80). Neither provision mentions regeneration, which is consistent with the thesis, though two provisions do not settle it. Contest is the limit of this chapter, and A Proof Is Not an Appeal takes it up.

Reading s.80 exposed a second, unrelated error. The March essay relies on "Article 22, which gives data subjects the right not to be subject to decisions based solely on automated processing". That section substituted Articles 22A to 22D for Article 22, in force on 05/02/2026 (SI 2026/82, reg. 2), seven weeks before I published. Article 22B's restriction now concerns decisions based on special category data or on Article 6(1)(ea), with Article 22C safeguards more widely.

Objections

"Reproducibility is the standard of evidence. If you cannot rerun it, it is not evidence." Thinking Machines opens with "Reproducibility is a bedrock of scientific progress", and for science and for debugging that is right. Accountability asks a different question: what happened on that occasion, and was it allowed? Verdict: rejected for accountability, accepted for research and debugging. I would change my mind if a court or regulator rejected a faithful, anchored record plus a checked certificate on the ground that the output could not be regenerated.

"Regeneration is the only guarantee that ties an output to the model. A log can be forged, and rerunning catches it." This is partly correct, and the supply-chain school will press it: independent rebuild is how a third party catches a compromised builder. invariant_regeneration_detects_forgery proves that under batch invariance a mismatch exposes a false record, and noninvariant_mismatch_false_alarm proves that without invariance the same mismatch accuses an honest log. So regeneration has one real job, when a party other than the operator holds the weights. Verdict: narrowed, not defeated. It is a forgery check available to whoever holds the weights and the matching stack, which excludes nearly everyone relying on a hosted model. Provider signatures over responses could do the same job more cheaply, though I have not surveyed what providers offer. I would change my mind if disputes turned out to be mainly about whether a given model produced a given output.

"Batch invariance cost a factor of 1.6 to 2.1 on one measurement, so just turn it on and the distinction collapses." Turn it on where you hold the weights and want it. The distinction does not collapse, because no_guarantee_implies_another is about what the guarantees mean. A perfectly regenerable agent can still leak (steadyLeak_invariant) and still be falsely logged (onlyRegenerate). Verdict: rejected. I would change my emphasis if hosted APIs guaranteed byte-identical output over a retention period.

"Certificates only cover boundary claims. Most of what matters in an agent's output, such as whether the advice is any good, has no formal statement at all." Correct. Verdict: accepted as a limit on scope. The compliance claim I defend is about permissions and boundaries, and the essay's claim that its eight items satisfied every concern in the article it answered was an overclaim I withdraw. I would change my mind about the value of the whole approach if, on real deployments, the proportion of disputes turning on checkable boundary properties proved negligible.

"Your main theorem is subst plus check_sound. It assumes the record equals the run, and that equality is the whole problem. You have proved that a true record of a compliant run shows a compliant run." This is the objection I find hardest, and as a statement about the theorem it is correct. The theorem says nothing about how to get a faithful record, and capture needs the generator's effects to pass through a point it cannot bypass, so "nothing from the generator" holds only for its reproducibility. Verdict: accepted as what the theorem does not do; the thesis survives. What the theorem does is relocate the burden. It shows where the burden does not lie, in the model's reproducibility, and so where the effort belongs: capture, anchoring and fail-closed writes. Those are engineering problems with known forms, which regenerating a hosted model in 2031 is not. I would change my mind if agents routinely acted through side channels no capture point could see, because then the hypothesis could not be met and the theorem would describe nothing.

Goodhart, and what is lost

Score a team on "percentage of steps with a passing certificate" and it will prove weak statements. Score it on log completeness and it will route sensitive actions through a channel the logger does not see, which then looks complete. The manifest should therefore be read as a set of premises to attack, never as a number, and the statements themselves must be reviewed by someone with no stake in their passing.

Formalising loses something. The word "trace" let a reader picture one continuous account of what happened, and a data subject may want exactly that: a story, in words. Four labels with premises are more accurate and less humane. Whether a legitimate interest outweighs a person's rights still has no checkbox, and a manifest could help a controller pretend otherwise. The labels do not discharge the duty to explain a decision to the person affected.

Predictions

1. By 31/12/2027, none of OpenAI, Anthropic or Google will publicly guarantee byte-identical outputs for repeated identical requests to a hosted model. Refuted by a public documentation or contract term making that guarantee for a named model. Baseline: OpenAI's documentation disclaims it, and I found no such term in the Anthropic and Google API references I read.
2. On 31/12/2027, VLLM_BATCH_INVARIANT will still default to off in vLLM's main branch. Refuted by the default being on, or by batch invariance becoming unconditional. Baseline: default 0 on 02/11/2026.
3. By 31/12/2028, no published ICO statutory code on AI and automated decision-making, and no final EU harmonised standard on AI logging, will require deployers to be able to regenerate a model's output. Refuted by such a requirement in the published text of either. Both will ask for records. If neither is published by then, the prediction is untested and I will say so.

If those hold, the effort belongs on anchoring, fail-closed logging and the choice of statements. Those are the parts of my own work that failed.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.