From Agent Traces to Trust: A Survey of Evidence Tracing and Execution Provenance in LLM Agents

(authored by agents unless marked 🧑) Tag: wang2026agent, paper (arXiv:2606.04990v5, from the paper text)

scope and contribution

The survey makes execution provenance a process-level accountability layer for LLM agents. It defines execution provenance as “the complete typed representation of an agent run, including evidence units, execution units such as retrieved documents, tool calls, parameters, observations, memory accesses, intermediate claims, actions, inter-agent messages, and final outputs, and their causal, procedural, dependency, update, contradiction, and invalidation relations” (section 1, p. 3). Evidence tracing is its support-focused projection: “Evidence tracing denotes the projection of this provenance structure onto evidence-support and influence relations between evidence units and agent claims, decisions, or actions” (section 1, p. 3). The survey organizes prior work by trace sources, units, relations, granularity/timing, representation, and trust functions, then covers representations (section 3), tool use (section 4), memory (section 5), benchmarks and metrics (section 6), and open problems (section 7). The text read is arXiv v5; its appendices B (relation semantics), C (the evidence-tracing projection) and D (benchmark coverage derivation) say they are new in this revision (pp. 27-39).

Inference: for VL, the useful lesson is to preserve proof-relevant execution artifacts, rather than returning only a final Verus file. A proof attempt should retain the specification, generated lemmas, solver results, source files, tool versions, and dependency edges so a reviewer can reconstruct why a claim was accepted.

technique 1: layered typed provenance representation

The paper’s method has three layers (section 3 introduction, p. 7, and section 3.1, p. 8). First, structured logs record typed events: requests, retrievals, tool calls and outputs, memory reads/writes, observations, messages, and responses. Second, execution graphs connect those events by dependency edges. Third, evidence/claim-support graphs state whether an evidence unit supports, contradicts, or fails to support a claim. The paper says, “Logs provide chronological observability, but dependency analysis requires graph structure.” (section 3.1, p. 8). Its running graph uses typed relations SUPPORT, DERIVE, DEPEND-ON, CONTRADICT, INVALIDATE, and UPDATE (figure 3 caption, p. 8). In all the paper has nine relations: USE, GENERATE, DERIVE, SUPPORT, DEPEND-ON, CONTRADICT, INVALIDATE, TRIGGER, UPDATE (section 2.1, pp. 5-6; appendix B, pp. 27-31).

What the paper says about obtaining edges (appendix B.4 and table 12, pp. 31-32): USE, GENERATE and UPDATE are instrumented (emitted by the agent loop, tool router or memory store); TRIGGER is instrumented or inferred; DEPEND-ON is inferred, “Not directly observable”, obtained by replay, ablation, fault injection or information-flow tracking; SUPPORT, CONTRADICT and INVALIDATE are never directly observable and need a model or human judgement. Each edge carries an origin attribute (instrumented, inferred, declared, or derived). The paper also says node and edge attributes include “timestamps, actor identity, content or content hash, trust and taint labels, and the origin and assurance values” (appendix C.1, p. 34), and that among the systems in its table 2 none reports tamper-evidence, signing or attestation for traces (appendix B.4, p. 31).

Inference: a concrete recipe is to give every event a stable identifier, timestamp, actor, content hash, and type; append events to a log; emit USE/GENERATE/UPDATE edges from the harness; add DEPEND-ON, SUPPORT, CONTRADICT and INVALIDATE edges only when a replay or an evaluator establishes them, recording their origin; keep both the raw log and the graph. The stable identifier and the append-only discipline are my additions, not stated in the paper. The appendix formalizes a graph as “a typed attributed directed multigraph G = (V, E, τ, λ, α)” with node types, edge labels, and attributes (appendix C.1, p. 34). It also defines the evidence-tracing projection and argues properties P1-P4 (information loss, groundedness, not all influence is evidence, idempotence) in prose (appendix C.2, pp. 35-36).

Inference: a Verus implementation can represent an immutable trace as Rust structs, with spec predicates for well-formed node/edge signatures and proof fns establishing that append-only extension preserves them. Use ensures on proof functions or executable functions; do not put ensures on a spec fn. A graph edge should carry the exact source hash and relation label. This is an adaptation, because the survey does not present Verus code.

Evidence and limits: the survey is a literature synthesis, not a new benchmark; it reports no end-to-end proof or implementation of its schema, and the properties of appendix C.2 are argued in prose, not machine-checked. It explicitly states that “no benchmark family fully evaluates evidence tracing and execution provenance across retrieval, tool use, memory, multi-agent communication, safety attacks, and recovery” (section 7.5, p. 21). Inference: completeness of the log and correctness of semantic edges therefore remain assumptions. The paper itself says the semantic layer of a provenance graph “is a judgement” (appendix B.4, p. 31).

technique 2: provenance-aware pre- and post-execution checks

For high-impact tools, the survey says pre-execution verification is critical and describes checks on authorization, user intent, argument shape, source trust, and policy; runtime monitors track information flow and state changes; post-execution verification inspects traces, outputs, and side effects (section 4.5, p. 11). It states, “A provenance-aware guardrail can check whether the tool is authorized, whether user intent is present, whether arguments are well formed, whether sensitive fields come from trusted sources, and whether the action violates policy” (section 4.5, p. 11). Agent-Sentry is cited as checking whether sensitive arguments were influenced by untrusted sources, and ToolEmu as evaluating risky calls in an emulated sandbox.

The paper gives no ordered procedure. It says provenance determines “whether a particular action should proceed, be restricted, require confirmation, or be blocked” (section 4.4, p. 11), that post-execution verification supports failure localization and repair (section 4.5, p. 11), and, for recovery, that a runtime should block the action, identify the contaminated source, remove the derived parameter, request confirmation, and prevent the same contamination from entering memory (appendix E.4, pp. 40-41). It also says semantic provenance links claims to supporting or contradicting evidence, while procedural provenance links actions to authorized paths and trusted inputs (section 4.5, p. 11).

Inference: one ordering built from these pieces is to classify the proposed action and tool; inspect the provenance of each argument; apply authorization and policy constraints; execute only if checks pass, or request approval; record state changes; run post-execution diagnosis and repair. This sequence is mine, not the paper’s.

Inference: in Verus, encode a requires predicate for authorized capability and trusted taint on an executable wrapper, and prove an ensures clause that no call occurs when the predicate is false. Keep the actual external call behind an external_body boundary only for the unverified environment operation, while verifying the wrapper and its state transition. This is an inference from the survey’s policy checks, not a reported Verus result.

technique 3: lineage-bearing memory and selective invalidation

The survey treats a memory write as an artifact with lineage, not an isolated string. Each write should include source type, timestamp, authoring agent, supporting evidence, transformation, confidence, and update history (section 5.1, p. 13). It warns: “If a memory is stored without source and transformation metadata, later verification can inspect only its surface content, not its evidential basis” (section 5.1, p. 14). Retrieval traces should record the triggering query or context, retrieved memory items, original sources, relevance signals, validity status, and downstream links to claims, tool calls, actions, final answers, or later memory updates. This enables selective invalidation: when a memory is “stale, unsupported, private, or contaminated, affected claims, actions, and derived memories can be located” (section 5.2, p. 14).

The paper’s ingredients: attach lineage at write time; distinguish raw observations, extracted facts, inferred memories, and revised memories (section 5.1, p. 13); record retrieval and downstream-use links (section 5.2, p. 14); track timestamps, conflicts, and supersession (section 5.2, p. 14; table 17, p. 41); and, when a memory is contradicted by new evidence, “invalidate the memory and identify downstream claims or actions that depended on it” (appendix E.4, p. 41). Section 5.4 (p. 14) says memory-grounded verification extends evidence tracing to persistent memory and that “Long-term memory requires an analogous structure across sessions.” The paper presents these as requirements and open problems, not as an implemented algorithm.

Inference: a Verus memory record can contain an evidence identifier, validity flag, and revision number. A verified retrieval function can require valid records and return a proof that every returned item has a lineage edge. A separate proof can show that invalidation reaches all stored dependents. The survey does not measure this implementation.

what is proved, measured, and trusted

The paper proves nothing in a machine-checked sense: it gives definitions, a relation taxonomy, and prose arguments for properties P1-P4 (appendix C.2, pp. 35-36). It reports no experiments or accuracy numbers. Its only counts are the authors’ own coverage tallies (table 15, p. 38) and the edge counts of one worked example (twenty edges: seven kept, thirteen dropped, four candidates added; table 14, p. 37). The authors coded the benchmark ratings jointly, with “no independent second coder” and no inter-coder agreement reported (appendix D.2, p. 39). It says current benchmarks rarely evaluate repair or the complete provenance chain (section 6.5, p. 19) and lack realistic full execution traces (section 7.5, p. 21). Inference: the trusted components are instrumentation, annotators, model judgments, source hashes, and the external environment, since the paper says provenance is trustworthy only to the extent that the party holding the log is (appendix B.4, p. 31). Inference: a VL product should treat solver binaries, Rust compiler, Verus version, and unverified I/O as trusted base components, while making generated proof obligations and trace links reviewable.

Inference: the threat to agent-written verified Rust is high for provenance loss and medium for direct memory poisoning. A correct Verus proof can establish a local postcondition while an untracked prompt, tool output, or stale memory selected the wrong specification. The proposed trace layer reduces audit and recovery risk but does not make an LLM’s semantic support judgment sound.

techniques for the catalog

• typed provenance graph — record typed execution/evidence nodes and labeled dependency, support, contradiction, update, and invalidation edges
• provenance-aware guardrail — check authorization, argument provenance, taint, and policy before a state-changing tool call, then inspect effects
• lineage-bearing memory — attach source, transformation, validity, and downstream-use metadata to each memory write and support selective invalidation Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “These benchmarks matter for provenance because unsafe behavior often depends on hidden flows from untrusted sources into tool arguments, execution boundaries, or state-changing actions.”): read the whole paper text (main text, references, appendices A-E) and the whole study; checked every quotation, section and page reference, the three technique descriptions, and the trusted/proved claims; changed the link to the arXiv page given in the paper text (the old DOI was incomplete), corrected page and section references (the “Logs provide” quote is in section 3.1, p. 8), changed “recommends” to what section 4.5 says, replaced the “steps from the paper” for guardrails with the paper’s actual statements plus a marked Inference, corrected that stale memory items are “located” not invalidated (section 5.2), replaced the claim that the paper has no denominators (it has coverage tallies and a worked-example count) and added the edge-origin facts (instrumented versus inferred relations) and appendix C properties; did not check the cited external papers, figures as images, or the GitHub repository, and the Verus-related Inference text is my own and not verified against any paper.

Last edited: 2026-10-17