Articles

Proving what AI agents can reach, instead of watching for trouble

The difference between a security tool that raises an alarm and one that issues a proof anyone can check, and exactly what Kern proves.

Syntaxe

A dark data centre aisle lined with server racks.

Security products for AI agents share the same basic design. They watch what an agent does and raise a warning, based on probability, when something looks wrong. This is useful. But it is an alarm, not a proof, and the difference matters more than it first appears.

What an alarm tells you

An alarm tells you that an action looked unusual compared with a model of normal behaviour. It does not tell you the action was impossible. It tells you the action was unlikely. On a normal day this difference goes unnoticed, but on a bad day it can be very costly.

An alarm-based system can only recognise problems that resemble behaviour it has seen before. Consider an agent under prompt injection, an attack where hidden instructions in text the agent reads make it do something its user never asked for, or an agent handling a situation nobody planned for. Neither has to look unusual to cause real damage. It only has to go unnoticed for the one action that matters.

What Kern does instead

Kern asks a different question. It does not ask “does this look wrong?” It asks “can this happen at all, given exactly what these agents are allowed to use?”

To answer it, Kern takes the tools the agents are declared to use, the labels on their data and the limits on their authority. It turns these into a precise model of the system with a limited number of states. Because the model is limited, the question “what happens for every possible input?” has an answer that can be calculated, instead of one that has to be hoped for.

Kern then runs a calculation that keeps adding every route a piece of labelled data could take, until no new routes appear. This settles the real question: can data labelled as protected ever reach a destination where it is forbidden, through any sequence of actions the agents are able to take? The result is not a confidence score. It is either a proof that the limits hold, or a concrete example of how they fail: the exact route an attacker could take, shown step by step.

Anyone can check the proof for themselves

Kern packages the proof as a certificate that can be taken away and checked elsewhere. This changes who can trust the result. A confidence score is only as believable as the company that issued it: you either trust that company or you do not.

A certificate works differently. An outsider who had no part in building the agents can re-run the proof and get the same answer. That outsider might be an auditor, an insurer or another organisation’s AI agent. They can do it on a computer with no network connection if they want to.

The answer never depended on trusting Kern. It depends on mathematics that anyone can check.

What happens when it is tested

When someone runs a live prompt-injection attack that tries to extract data from a set of agents Kern has certified, the attempt is stopped at the boundary before it happens. It is not flagged afterwards. Kern shows the specific unauthorised route as the reason it was blocked.

When someone presents a forged certificate, it is rejected outright, because a forged certificate does not produce the same proof when it is re-checked. Neither result depends on the attempt looking suspicious. Each depends only on whether the attempt is actually possible within the limits the agents were given.

Kern also proves rules about amounts of money

For agents that move money, proving that data did not leak is necessary, but it is not enough. Kern can also prove rules about the numbers. For example, it can prove that an agent managing funds (a keeper agent) can never withdraw more than a position actually holds. This holds for every possible input, not only the inputs a test suite happened to try.

Auditors already expect this kind of guarantee in other fields, where it comes from formal verification: mathematical proof that software follows its rules. Kern delivers it as a proof. The usual alternative is fuzzing, which feeds a system large numbers of random inputs. When fuzzing finds no problem, that only means it has not found one so far.

The limits of Kern’s proof

A proof is a narrower claim than it may first sound. Kern’s guarantee covers the agents as they were declared: the tools, labels and limits Kern was actually given. It does not cover code Kern never saw, or agents that operate outside their stated limits.

That is a real limitation, and we state it openly. A proof that quietly claims more than it covers is worse than an alarm that admits what it does not know, because the alarm is at least honest about its coverage.

Two further capabilities are on our roadmap because they are not solved yet. The first is proving rules that must keep holding across a long series of steps. The second is attaching data labels automatically to live data read from a blockchain.

Who needs a proof rather than an alarm

An alarm is enough when the person reading it built the system and trusts their own sense of what “looks wrong” means. A proof is needed as soon as someone else has to trust an agent they did not build.

That includes an insurer judging the risk of a set of agents it will never review line by line, and an auditor who must approve a system built by a team they do not work with. It also includes another organisation’s AI agent, which must decide automatically whether to deal with a system it has never encountered. For each of them, a certificate they can re-check themselves, without relying on us, is the only kind of answer that works.

Share this article

Leave a comment

Comments are read before they appear. Your email address is never shown.

0 comments

Questions about this article?

Email us. We reply to every message.

Explore Syntaxe.