When we move from building chatbots to building agents—systems that can call tools and perform actions—we move from the domain of language modeling into the domain of stateful systems.
In a simple chat interface, a model's mistake is usually a semantic one: it gives a wrong answer or hallucinates a fact. But when an agent has the authority to issue a refund, move a file, or trigger a deployment, a mistake can become an operational failure.
Often, these failures are not caused by the model's reasoning, but by how we have designed the system around it.
Table of Contents
Agents as Distributed Systems
An agent that maintains a memory of its history and interacts with external APIs is, in practice, a small distributed system. It sends messages, waits for responses, and manages its own internal state.
Like any distributed system, it is subject to common failure modes:
- Network Timeouts: An API call to a tool might time out, but the action might have actually succeeded on the server.
- Retries: To be robust, we often program agents to retry failed actions, which can lead to duplicate executions if not handled carefully.
- Concurrency: Multiple agents, or an agent and a human, might attempt to modify the same resource at the same time.
It is tempting to try and solve these issues by adding more instructions to the prompt, such as "Do not issue the same refund twice". However, a prompt is a reasoning tool, not a synchronization primitive. It cannot guarantee at-most-once execution in the face of a network partition or a race condition.
Reliability and System Invariants
To make an agent reliable, we need to define the "rules" of the system that must never be broken. In formal methods, these are called invariants.
For a refund agent, a simple invariant might be: No refund is ever issued without an approved request in the database.
If the code for the agent looks like this:
- Check if the refund is approved
- If yes, call the refund API
- Update the database to mark it as complete
A potential race condition exists. If a human revokes the approval between step 1 and step 2, the agent may still proceed with the refund because it is acting on stale information. This is a system design error, not a "hallucination".
Where TLA+ Fits In
I have written before about why TLA+ (Temporal Logic of Actions) is such a powerful tool for reasoning about distributed systems. It is often associated with cloud infrastructure and database protocols, but it is just as relevant for the control plane of an AI agent.
TLA+ allows us to define an agent's workflow as a set of states and transitions, and then use a model checker to verify that our invariants hold true across all possible interleavings of events.
In the refund example, we would model:
- The States:
Pending,Approved,Executing,Completed,Revoked. - The Actions: A user can
ApproveorRevoke. The agent canExecuteorRetry.
The TLA+ model checker explores every possible sequence. It will find the specific scenario where a Retry and a Revoke happen in an order that violates our safety properties. This allows us to catch design flaws in our orchestration logic before we start implementation.
What This Does Not Solve
TLA+ is a tool for verifying the logic of our systems, but it does not replace other parts of the AI development lifecycle:
- Semantic Correctness: TLA+ cannot tell us if the agent's decision to issue a refund was "correct" based on company policy. We still need evaluations (Evals) for that.
- Model Performance: It doesn't help with the speed or cost of the LLM.
- Implementation Bugs: Even with a verified design, we can still write buggy code.
Conclusion
As agents become more autonomous, the complexity of managing their side effects grows. We can improve reliability by separating the "reasoning" (which the LLM handles) from the "protocol" (which governs how the system behaves).
The use of TLA+ is a straightforward way to ensure that the protocols we build around our agents are sound. It helps us move away from hoping the prompt is "smart" enough to avoid errors, and toward building systems that are safe by design.