How do organizations deploy more agents with greater autonomy when oversight and audit are limited by human review? New Vijil research develops a neuro-symbolic approach that makes agent behavior auditable and oversight scalable - and that flags policy violations more reliably than the strongest LLM judges.
The bottleneck to deploying more agents with increasing autonomy isn't just whether agents are capable enough. It's whether organizations can assure, with evidence that scales, that agents are behaving as intended when there are too many agents, actions, and interactions for humans to inspect individually. This observation changes the nature of the trust problem.
For a conventional software system, an organization can often test the software before deployment and rely on deterministic controls during operation. An AI agent is different: its behavior depends on context, it can make decisions over many steps, and the same underlying model can produce different actions across interactions. As organizations deploy more agents across more workflows, the question is no longer simply can this agent perform the task? It is whether we can monitor that the deployed agents are behaving within the boundaries we intended throughout their lifecycle?
Today, that assurance is difficult to scale. Humans can review a handful of consequential decisions; they cannot inspect every conversation, tool call, and action across thousands of agents operating continuously. Organizations therefore turn to automated evaluations, LLM-as-Judge systems, guardrails, traces, and other monitoring mechanisms. But these mechanisms create an oversight problem of their own: if an automated LLM-as-Judge misses a violation, how much confidence should we place in its verdict? And if the monitor itself requires human review to establish that it works, have we really solved the scaling problem? This is the central challenge behind scalable oversight: building oversight mechanisms whose reliability does not depend on inspecting every behavior they are meant to oversee. For now, this remains an open research problem.
Vijil Research Scientist Abhishek Kulkarni, joined by Chief Scientist Tim G. J. Rudner presented Vijil's approach to this problem at ILIAD, a conference bringing together researchers in AI alignment and agent foundations. The talk laid out the research bet at the core of Vijil's fundamental research agenda — formal methods for trustworthy AI agent — and walked through a new neuro-symbolic monitoring approach, currently under review at NeurIPS, which leverages formal logic and LLM-as-Judges to detect agent’s policy violations more reliably and robustly than six frontier LLM judges used alone.
An LLM judge may tell us whether an agent broke a rule. But who checks the judge? Oversight that needs a human evaluation at every level cannot scale.
Vijil's answer: formal specifications can close the gap.
The Challenge: When Agents Outpace Human Oversight
For organizations deploying at increasing levels of autonomy , the oversight problem appears at three levels: at runtime, monitoring agents to check whether their behavior remains compliant with their policy, steering them when they go off course; and at training time, supervising them to make future agents safer by design. As agents become more capable and autonomous, all three sub-problems must scale beyond what humans can inspect directly.
The obvious response is to automate oversight. But every automated overseer available today is itself a learned system, and each inherits a version of the problem it was meant to solve.
Reward models offer a scalable proxy for human judgment, but agents can game the specification and learn to maximize the proxy without satisfying the intent behind it [DeepMind].
LLM-as-Judge systems evaluate behavior at scale, but their verdicts shift with the choice of model, prompt, and rubric, and their errors are hard to detect without an independent source of ground truth [arXiv].
Performance of both approaches degrades on long, multi-turn interactions, where compliance depends on the ordering and context of many messages and actions rather than on a final output [Judgment Labs].
Monitoring an agent's stated reasoning does not escape this either: what a model says about why it acted is not guaranteed to be faithful to why it actually did.
The deeper issue is that automating oversight does not make oversight trustworthy. It produces another system whose correctness must be established, and if that system needs human review to confirm it works, the scaling problem has only moved. The question therefore becomes:
Can we isolate and reduce the risks rather than relying entirely upon another learned system to judge their correctness?
We answer this question with formal methods.
How It Works: Writing Policies Down, and Checking Them
Vijil’s fundamental research team introduces a neuro-symbolic approach that uses formal languages instead of natural languages to maintain oversight. They do not remove the language model. They shrink its job and put the parts of oversight that must be trusted into a form we can inspect and verify.
Our approach has three components:
- a formal language for policies
- a computational model that checks compliance
- and, a grounding layer that enables interpreting agent trajectories in terms of formal language and the computational model
A formal language for policies: The first step is to turn a policy written in natural language into a precise specification that a machine can check. A natural language policy could be ambiguous. A formal specification gives the policy a fixed, reviewable meaning that can also be analysed before deployment—for example, to identify conflicting norms or cases where a policy leaves behavior unspecified.
We introduce a new formal language called Temporal I/O Logic (TIOL). TIOL represents an agent policy in terms of four elements:
- what sequence of events trigger an obligation
- what the agent must do to discharge it
- when the agent must do it
- and, what it should do if the obligation is violated
Consider a retail agent handling a return request. When the user requests a return, that is the trigger. The agent then has an obligation to list the details of the return action. That obligation has a deadline: the details must be listed before the agent asks for confirmation, denies the request, or moves on to a new request. If the agent violates this obligation—for example, by proceeding with the return without first listing the details—the policy specifies a reparation: revert the action, then list the details and obtain confirmation before proceeding again.
This last component is important for real-world policies. Violations may occur due to circumstances that agents cannot control, such as networking or latency issues, etc. They do not always make an interaction irrecoverable; a policy may prescribe how the agent should recover. TIOL captures these contrary-to-duty reparations explicitly, allowing the monitor to distinguish an agent that complied immediately from one that violated an obligation but subsequently recovered.
An automaton that checks them. A policy specification captures intended agent behavior in an unambiguous way. Temporal I/O automaton (TIOA) is a computational model that checks whether a given agent trajectory complies with a given TIOL spec. At every step, it determines whether the interaction remains compliant, has violated the k-th obligation but can still recover, or has become non-compliant (no further reparations possible).
A grounding layer that connects both to language. The automaton operates on discrete events, not natural language. The grounding layer converts each natural language message (e.g. messages exchanged between user and customer service agent) into the atomic propositions the monitor needs—for example, did the user request a return?, did the agent list the action details?, or did the user confirm? The truth of these propositions can be determined either deterministically from the trace, such as whether a tool was called or a database field was changed, or by an LLM when language understanding is required, such as recognizing user intent.
The LLM is therefore used only for narrow binary grounding questions, rather than judging the conversation as a whole. The resulting division of labor is deliberate: deterministic sensors establish what can be observed directly; LLM-based sensors identify events that require language understanding; and the formal monitor interprets the resulting sequence of events to determine compliance.
Symbolic monitoring over the formal specification provides a machine-checkable basis for the compliance verdict, while the language model is confined to the part of the problem where language understanding is actually needed.
The Results: Logic Beats the Strongest LLM Judges
Monitoring results on τ-bench retail conversations. The logic-based monitor outperforms all six frontier LLM judges (0.87 vs. 0.73 balanced accuracy) and remains robust as conversations grow longer — exactly where LLM judges degrade.
We evaluated the monitor on τ-bench retail (964 conversations checked against 38 norms) and compared it with six frontier LLM judges. The results point to a practical advantage for organizations that need to monitor agents at scale: oversight can become more than a confidence score; it can provide a reliable, auditable account of whether an agent followed policy.
1. It outperforms every frontier judge.
0.91 vs. 0.81 AUROC on retail; 0.94 vs. 0.89 on telecom.
Measured against the error the best judge still leaves, the monitor removes roughly half of it in both domains. That gap is what separates a confidence score from a verdict an enterprise can act on.
2. Where behavior is observable, the verdict is exact.
100% accuracy on norms grounded in tool calls and structured fields.
No learned judge decides whether an account was changed or a refund was issued; the monitor reads those facts directly from the system trace. For language-dependent norms, error is confined to the grounding step rather than compounded by temporal reasoning performed by an LLM-as-Judge.
3. Reliability remains largely unaffected as conversations grow longer.
LLM judges degrade with trajectory length; the monitor does not.
Temporal reasoning over ordering, deadlines, and reparations is handled by the automaton, not by a model reconstructing a long history. The LLM only ever answers per-message yes/no questions.
4. Every verdict is auditable.
A violation points to the specific norm, message, and proposition that triggered it.
An enterprise can see why an agent was flagged, decide whether the policy or the agent needs to change, and retain evidence of compliance instead of an opaque score.
The broader implication is that trustworthy oversight need not scale by asking humans to inspect more conversations or by asking a larger model to judge them. It can scale by moving the part that requires assurance into a system whose behavior can itself be checked.
A Step Toward Verifiable AI Governance
This work is part of Vijil's investment in fundamental research as the basis for trustworthy AI agents in production. Vijil already evaluates agents with more than LLM judges. Monitors with formal guarantees are the next step: they are auditable, they stay reliable as conversations grow longer, and they improve as policies are refined. That is what enterprises will need to govern agents against real policies, whether internal operating procedures or regulatory requirements.
The paper introducing temporal I/O logic and the runtime monitor is currently under review at NeurIPS.
.png)
.png)