arXiv — Tool-Mediated LLM Architecture with Lean 4 Proofs for Autonomous Cyber Defense
Autonomous LLM agents in security operations face a fundamental tension: the models' creative problem-solving is valuable, but their non-determinism makes formal guarantees impossible. A new arXiv paper (2605.03034) proposes a tool-mediated architecture that resolves this — LLMs select from finite action catalogs, while deterministic tools (Stackelberg best-response solvers, Bayesian observers, attack-graph primitives) execute the actual operations.
Key findings
- A composite Lyapunov function was machine-checked in Lean 4 with zero
sorry(no admitted proofs), certifying controllability, observability from asymmetric sensor data, and Input-to-State Stability under adversarial disturbance. - Evaluated on 282 real enterprise attack graphs — the stability claims hold with margin across the entire dataset.
- A tool-mediated Claude Sonnet 4 controller reduced the attacker's expected payoff (game value) by 59% relative to a deterministic greedy baseline, with zero variance across 40 runs at four different temperatures.
- A smaller Claude Haiku 4.5 controller converged to suboptimal game values but stayed catalog-bounded, demonstrating that architectural stability is model-agnostic.
- The architecture lets LLM non-determinism fuel creative strategy exploration while the tool interface enforces system stability guarantees.
Why it matters
As SOC teams experiment with autonomous LLM-driven incident response, the lack of formal guarantees is a blocker for production deployment. This paper demonstrates that tool-mediated architectures can provide machine-checked stability proofs while still leveraging LLM reasoning — a pattern directly applicable to autonomous agent deployments in any high-stakes domain, not just cyber defense.
The Lean 4 verification with zero admitted lemmas is notable: formal verification of AI agent behavior at this level of rigor remains rare in applied security research.
What to do
- Teams building autonomous AI agents for SOC, IR, or other high-stakes operations should evaluate tool-mediated architectures that separate LLM decision-making from deterministic execution.
- Security architects should consider formal stability proofs as a deployment prerequisite for autonomous agents, not an afterthought.
- The finite action catalog pattern — constraining LLM outputs to a bounded set of safe operations — is applicable to any agent system with tool access.