Syntaxe is a technology company: a systems lab building inspectable computational engines for security, law, science and critical infrastructure, plus an engineering practice for organisations solving difficult technical problems.
Reach the lab at hello@syntaxeltd.com · Syntaxe Ltd.
Every guard in the agentic-security market ships the same shape of product: watch an AI agent’s behaviour, and raise a probabilistic flag when something looks wrong. It is a genuinely useful shape of product. It is also, structurally, an alarm, not a proof, and the difference matters more than it sounds like it should.
An alarm tells you that, based on a model of normal behaviour, a particular action looked unusual enough to flag. It does not tell you the action was impossible. It tells you it was improbable. That distinction is invisible on a good day and catastrophic on a bad one: an alarm-based system is only as good as the behaviours it happened to have seen before, and an agent under prompt injection, or one simply operating at the edge of a case nobody anticipated, does not have to look unusual to do real damage. It only has to be unmonitored for the one action that matters.
KERN starts from a different question: not “does this look wrong,” but “can this happen at all, given exactly what this agent mesh is allowed to touch.” It compiles the mesh’s declared tools, its data labels, and its authority boundaries into a finite, bounded system, small enough that “for every possible input” becomes a question with a computable answer rather than a hope. A monotone fixpoint computation then settles the actual question: can a protected label ever reach a forbidden sink, under any sequence of actions the mesh is capable of taking. The output is not a confidence score. It is either a proof that the boundary holds, or a concrete counterexample: the exact path an attacker could take, shown, not asserted.
That proof becomes a portable certificate, and this is the part that actually changes who can trust it. A confidence score is only as credible as the vendor issuing it; you either believe them or you don’t. A certificate is different: an outsider, an auditor, an insurer, a counterparty agent that had no part in building the mesh, can re-run the proof themselves, in an air-gapped room if they want to, and get the same answer, because the answer never depended on trusting KERN in the first place. It depended on trusting the math, which anyone can check.
Run a live prompt-injection exfiltration attempt against a mesh KERN has certified, and the attempt is caught at the boundary before it happens, not flagged after the fact, with the specific unauthorised route shown as the reason it was blocked. Try to present a forged certificate, and it is rejected outright, because a forged certificate does not re-derive to the same proof a real one does. Neither outcome depends on the attempt looking suspicious. It depends on the attempt being, or not being, actually possible under the mesh’s declared boundaries.
For agents that move money, “the data didn’t leak” is necessary but not sufficient. KERN’s value predicates prove the arithmetic too: that a keeper agent can never withdraw more than a position actually holds, for every input, not just the ones a test suite happened to cover. That is the same kind of guarantee auditors already expect from formal verification in other domains, discharged here as a proof rather than a fuzzing campaign that merely failed, so far, to find a counterexample.
Proof is a smaller claim than it sounds like at first. KERN’s guarantee holds over the mesh as declared: the tools, labels and boundaries it was actually given, not code it never saw and not a mesh operating outside its stated bounds. That is a real limitation, and we say so rather than paper over it, because a proof that quietly overclaims is worse than an alarm that honestly doesn’t know: at least the alarm isn’t lying about what it covers. Multi-step running invariants and live on-chain label capture are on the roadmap precisely because they are not solved yet.
An alarm is enough if the person reading it built the system and trusts their own judgment about what “looks wrong” means. A proof is what you need the moment someone else has to trust an agent they didn’t build: an insurer pricing the risk of a mesh they’ll never audit line by line, an auditor who has to sign off on a system engineered by a team they don’t work with, a counterparty agent that has to decide, automatically, whether to transact with a system it has never met. A certificate that re-runs in their hands, not ours, is the only shape of answer that actually works for them.