Autonomous AI Defense Has a Trust Problem. This Paper Says Math Can Solve It.

NodeZero can now autonomously adjust Microsoft Defender policies. That is not a demo. That is a production AI system making security decisions inside enterprise networks, and it is the most concrete evidence to date that the security industry has crossed the line from "AI recommends" to "AI acts."

The reason most security teams have kept AI on a short leash is that large language models behave unpredictably under adversarial pressure. Give an LLM the keys to your network and it may do something sensible or something no one anticipated. Horizon3.ai's NodeZero team, in a paper released May 4 on arXiv, argues the unpredictability is not a property of the model. It is a property of the loop. And loops can be designed.

The paper claims the first machine-checked proof, verified in Lean 4, a dependently typed programming language where every step is a formal check, not an assumption, that a tool-mediated LLM controller is stable under adversarial conditions. The authors built a composite Lyapunov function combining a semantic component tracking the gap between what the agent believes and what is true, plus a regularization term penalizing tool use that violates catalog constraints, and formally certified the system is Input-to-State Stable against intelligent adversarial disturbance. The paper explicitly claims "zero sorry," meaning every logical step in the proof is verified, none left as an assumption. Full paper on arXiv has the full formal apparatus.

The empirical evidence runs alongside the proof. Horizon3 tested the system against 282 real enterprise attack graphs from production penetration tests, spanning 161 organizations across 25 industries. The game value, a measure of attacker expected payoff, dropped from 0.84 to 0.34 against a deterministic greedy baseline, a 59% reduction that the company says translates to meaningful defender advantage. The system showed zero variance across 40 runs at four different temperatures, meaning the result is not a lucky run. The loop behaves the same way every time.

The speed at which the system converges matters as much as the endpoint. 97.7% of the total improvement typically occurs in the first round of the attack graph traversal. Further rounds add almost nothing. The implication is that the tool-mediated loop learns to constrain the model into a safe operating envelope quickly, and then stays there. The model is not becoming smarter. The loop is becoming more restrictive. The authors call this "catalog-bounded" behavior: the system's safety comes from what it cannot do, not from what it can.

The operational consequence is already live. NodeZero can now autonomously adjust endpoint detection and response policies, including Microsoft Defender, with formal assurance that those changes will not degrade overall defensive posture. Horizon3 reports zero off-catalog hallucinations across more than 420 production deployments. That means no matter which underlying model was used or what temperature was set, the system never proposed an action outside its approved catalog.

The verification standard is what separates this from ordinary benchmark claims. Formal methods, mathematical proof of system properties, sit uneasily in security product marketing because they are hard to audit and easy to overstate. The Lean 4 proof is a real artifact, not a press release talking point. But the proof only covers what the formal model describes. If the catalog constraints are themselves incomplete, or if the threat model the Lyapunov analysis assumes does not map to a real adversary, the bounded guarantee may be narrower than it appears.

The paper notes that weaker controllers, specifically a Claude Haiku 4.5 controller, converge to suboptimal game values while staying catalog-bounded. Architectural stability does not depend on model capability, the authors write. That is both the point and the caveat. The loop enforces the constraint, but the constraint is only as good as the catalog design. A bounded unsafe system is still unsafe if the bounds are wrong.

What independent researchers make of the Lean 4 apparatus is the open question. No third party has publicly audited the formal proofs or stress-tested the threat model assumptions against real enterprise network conditions. The paper does not claim the proof covers arbitrary attack scenarios. It claims the specific closed-loop structure described is stable. Whether that structure maps to a production enterprise SOC with legacy systems, incomplete asset inventories, and novel attacker techniques is a different question the paper does not resolve.

The practical test is not whether formal methods work in theory. It is whether they can be productized at scale. Horizon3 is betting yes, and the fact that autonomous Microsoft Defender policy adjustment is already in customers' hands means the question is no longer hypothetical.

What to watch: whether independent security researchers reproduce the Lean 4 verification, whether enterprise defenders report consistent behavior at scale, and whether the formal methods approach spreads to other autonomous security products. The paper's core claim, that safety is a property of the loop and not the model, is a testable thesis. The next test is production.