Agent verification

Classical agents

The theoretical underpinnings for artificial (inorganic) agents emerged in the mid 20th century, with establishment of cybernetics and artificial intelligence. Oliver Selfridge's 1958 Pandemonium - A Paradigm for Learning paper was an important early theoretical contribution in establishing agent oriented architecture. Practical implementations of agents for real world applications began to become widespread in the 1990s, after the introduction of the belief–desire–intention software model (BDI), and agent-oriented programming. Pure digital agents were deployed in computer infrastructure for purposes such as monitoring, while agents connected to real-world sensors and actuators were increasingly used in industrial control systems.^[1][4][5]

While the concept of artificial agents was interwoven with early artificial intelligence studies right from the start, early agents lacked general purpose reasoning capabilities, often only having simple if then logic. Even a device as simple as a thermostat, which has a sensor and a means of acting, can be considered a proto agent in this sense. Verifying the behaviours of a simple single agent system is not generally especially difficult, but it can be a different matter when several simple agents coexist in the same system. Craig Reynolds's work on boids showed that relatively complex, "intelligent" behaviour can emerge from a number of such simple agents working together in a Multi-agent system (MAS). By the 1990s, even the behaviour of a single agent system could sometimes be quite complex; in accordance with the Belief–desire–intention software model, agents could have believes that might evolve over time. Agents were increasingly introduced that were controlled by quite large decision tree models, which had new vulnerabilities to adversarial attack. It was becoming increasingly apparent that traditional software verification methods had limitations for testing such agents, or even for the more primitive type of agents when they were deployed as part of a MAS.^[4][3][1]

It was the use of agents for industrial control systems, sometimes associated with robotics, that lent urgency to the practice of agent verification. Informal testing might be acceptable for digital agents used say to monitor whether each of an organisation's computer is properly licenced. But with an increasing potential for faulty agents to result in a failiure that might cause a large fire to break out at a chemical manufacturing plant, a botched medical operation or even a crashed aircraft, the need to develop reliable means of verifying the behaviour of such agents was considered urgent. The Foundation for Intelligent Physical Agents was established in 1996. In the late 90s, a growing number of industry and university based scientists began working on the problem, with reasearchers publishing papers on the verification of both single and multi agent systems. Much of this work showed how formal verification techniques like model checking could be used to gain a high level of assurance that agent based systems would conform with their specification. A 2018 systematic review covering 231 studies found that model checking was the most common technique for agent verification, with theorem proving the second most commonly used formal verification method. In the first two decades of the 20th century, agents run by AI became more common, with Siri and Alexa being well known examples. But such agents still lacked general reasoning capabilities and did not pose new pressing problems for agent verification.^[6][4][3][1]

General purpose reasoning agents

The advent of LLMs created huge potential for further use of artificial agents, as agents based on them could have general purpose cognitive abilities. Agents run by LLMs (and occasionally non-LLM foundation models) have similar vulnerability to adversarial attack as those run by decision tree models. The wider scope of actions for LLM agents has created new challenges for their verification, over and above those present for classical agents. For example, the LLM's neural network endows it with infinite domains, an especial challenge for traditional formal verification techniques. Academics began to study the problems involved in verifying LLM agents from 2018. Deployment of such agents began to accelerate in late 2023 after OpenAI's "function-calling" API was made available, and especially after Anthropic's late 2024 introduction of Model Context Protocol (MCP), a standardised way for LLM agents to gain contextual awareness, and to act on the world by calling various external tools. The rapid rollout of LLM agents following MCP's release has seen the task of agent verification receive increased attention within accademia, and also from the private sector. In 2024 and 2025 several startups focusing on LLM agent verification have been founded in both Europe and the US to meet growing demand.^[2][4][3][7]

Formal verification

Formal verification involves proving the correctness of some or all aspects of a system using mathematical methods. Such methods can range from manual formal proof, to verfication assisted with automated theorem provers like Isabelle. For agent verification, model checking is by far the most frequently used formal verification method; for pre-LLM models it was often complemented with techniques using computation tree logic. Another common method is theorem proving. Formal verification provides a higher degree of confidence than informal methods, but it is not always used, even when it is possible. Sometimes a person or organisation developing software agents won't have the necessary skills, or may not see it as worth the effort if the agent(s) will not have the ability to cause much harm even if they malfunction. When agents are deployed in systems where errors could have serious consequences, the ability of formal verification methods to provide mathematical certainty tends to be strongly preferred by both regulators and designers themselves. But even for high impact systems, formal verification can be challenging. ^{[3] [1] [6]}

Developers can try to design agent based systems in such a way so as to make it easier to formally verify more of their properties. This can be achieved both by specially designing the agent scaffolding of the core cognitive model controlling the agent, and — in the case of LLMs or other Foundational models — by altering the training. An example of the scaffolding orientated approach has been to introduce governor or arbitrator agents, who can veto actions initiated by more complex core decision making model. The governor agents tend to be relatively simple and therefore easier to formally verify. While this approach has been in use since at least 2009, its refinment after 2018 with the LLM-as-a-Judge paradigm has seen it gain in importance. Yet even with these techniques, formal verification is not always achievable. The compute involve may have a prohibitively high cost (as in it might need whole datacentres worth of computers to run for several years.). It may be that the necessary math is very hard to even formulate. For example, even for simple agents in a MAS, if an indeterminate number of agents can join the system at runtime, the problem is generally undecidable, though solutions are available for specific cases. Even more so in the case of LLM agents , aspects of their verification can be fully undecidable by formal mathematics, or at least NP hard. Accordingly, formal verification is often complemented with informal methods.^[1][7][8][3]

Informal verification

A variety of informal methods can be used to evaluate agents, with software inspection and heuristic evaluation being among the most informal, but often needing much skill on the part of the assessors to achieve a high degree of assurance, except for trivial case where only a small amount of simple code needs to be evaluated. The discipline of software testing includes various other forms of testing that while not requiring the mathematical rigour of formal testing, are often carried out in a relatively structured way, for example functional testing. For agent verification though, a major challenge with traditional informal methods is the difficulty in writing test cases that will cover all the possible scenarios that arise. When different agents must interact to achieve the systems overall goals, the number of permtuations can become extremely high, even if all agents are individually quite simple. Complementing traditional software verification methods with runtime verification^{[note 1]} can further increase confidence that an agent based system conform with specification.^[11][1]