Agentical: Provably Sound Replay, Crash Recovery, and Noninterference for Nondeterministic LLM Agents

Agents built on large language models run for minutes or hours, call tools with real side effects, and crash. Because model calls are nondeterministic, re-running a crashed agent re-samples every call and can repeat work that already happened. Durable-execution engines avoid this by recording each nondeterministic result and replaying it, but they treat each result as an opaque value and say nothing about the distribution it came from.

This paper gives a small probabilistic semantics for an LLM agent in which every model call is a draw from an abstract probability measure and every response is recorded in an append-only journal, with record, replay, and resume modes. It proves that replaying a run from its journal reproduces it exactly, so record and replay induce the same distribution over traces, and that after a crash at any point, resuming with fresh randomness behaves exactly like an uninterrupted run whose randomness is spliced at the crash point, provided the crash does not depend on a response that was never journaled.

Both results extend to systems of concurrently running agents that share memory and exchange messages, under any deterministic scheduler and with a single global journal. For such systems the paper proves a probabilistic noninterference theorem: under a floating-label discipline and a priority scheduler whose priorities depend only on public events, an agent’s secret data does not influence, even statistically, what public observers see.

• Replay soundness. Replaying a run from its journal reproduces its trace and journal exactly, so replay succeeds with probability 1 and recording then replaying induces the same distribution over traces as recording alone.
• Crash recovery. After a crash, resuming continues the run with exactly the distribution it would have had without the crash, conditioned on what survived, whenever the crash does not depend on a response that was never journaled.
• Many agents. Under a deterministic scheduler with one global journal, a whole system of agents behaves as a single program, so replay soundness and crash recovery hold for it, including every memory, message, and spawn step.
• Noninterference. With fixed labels on memory and channels and a priority scheduler that sees only public events, the public trace of a system is identical whatever its secret data, for every assignment of randomness and hence in distribution.
• Machine-checked. The core of replay soundness and crash recovery, and their lifting to any deterministic system, are proved in Lean 4 with no unproven steps; the multi-agent instantiation and noninterference are proved on paper.
• Measured. On a dependency-free Rust runtime, 1,000 of 1,000 replays matched exactly, recovery succeeded from all 4,664 crash points tried without repeating a committed side effect, and journaling costs about 100 nanoseconds a step.

@misc{bandlamudi2026agentical,
  author = {Aniketh Bandlamudi},
  title = {Provably Sound Replay, Crash Recovery, and Noninterference for Nondeterministic {LLM} Agents},
  year = {2026},
  month = nov,
  howpublished = {\url{https://aniketh.net/research/agentical/}},
  note = {Preprint}
}

I developed this work with Anthropic’s Claude as a collaborator on the proofs, code, and writing. Any errors are my own.