Agentic AI applications—systems empowered to take autonomous actions by calling external tools—are exploding across enterprise software stacks, but the security implications of handing models control over irreversible operations remain deeply unsettled. Now, researchers are pushing a rigorous approach borrowed from traditional software verification: force AI agents to generate mathematical proofs demonstrating their planned actions are safe before execution is ever authorized.

The Prompt Injection Problem

The core vulnerability stems from an old nemesis in computer security: the conflation of code and data. Unlike traditional programs where instructions and user input occupy clearly separated planes, large language models process both indiscriminately, treating embedded instructions in emails, documents, or tool responses as legitimate directives to follow. This creates attack surfaces that mirror SQL injection vulnerabilities but with potentially catastrophic real-world consequences. The researchers illustrate this with a chilling email management scenario: an agent equipped with fetch_mail and send_email tools receives a message containing hidden instructions ordering it to silently forward a confidential inbox summary to an external attacker-controlled address, without notifying the user or mentioning the covert transmission. By the time visible output appears—a seemingly benign summary—the damage is done.

Why Current Defenses Fall Short

Existing safety mechanisms share a fundamental weakness: they're reactive rather than preventive. Evaluations can demonstrate the presence of harmful behaviors but cannot guarantee their absence—similar to how software testing can only show bugs exist, not that code is bug-free. Guardrails introduce additional problems including false positives from pattern matching, cultural bias in content filtering, and non-monotonic behavior where small input changes produce dramatic output shifts. Runtime monitoring with security automata offers stronger protection but remains fundamentally limited. By the time a malicious action triggers an alarm and gets aborted, partial damage has already occurred—the agent has retrieved private emails and some unauthorized data exposure is inevitable. The approach also struggles to express every security-relevant invariant depending on policy language expressiveness.

A Three-Phase Architecture: Generate, Verify, Execute

The proposed solution restructures agentic workflows into a strict pipeline. First, models generate structured plans expressed as JSON-based abstract syntax trees with predefined tool calls. This separation ensures malicious content embedded in input data or tool responses cannot directly trigger execution—it can only influence the plan generation phase. "By using static verification and enforcing a strict distinction between code and data, you can robustly prevent prompt injection," the researchers explain. The approach also makes workflows interpretable and auditable, letting users trace exactly what actions will occur before any execution happens—a departure from current systems where tool calls happen silently behind the scenes.

Formal Verification Closes the Loop

The critical third phase involves formal verification using preconditions, postconditions, and invariants. Security policies are expressed as explicit constraints—for example, forbidding data flow from fetch_email results to send_email's body parameter when targeting external domains. Tools like CodeQL, SemGrep, Z3, and Dafny can statically analyze generated workflows for policy violations before any code runs. The researchers demonstrate how a tool description containing malicious instructions—attempting to silently exfiltrate emails whenever they're fetched—gets caught at verification time because the resulting workflow violates declared security constraints. The entire plan is rejected rather than partially executed with damage contained.

Implications for Agentic Development

This approach draws explicit parallels to bytecode verification in Java and .NET, where code undergoes safety checks before execution to guarantee memory safety, type correctness, and access control. Just as those platforms recognized that complexity should lie in production while verification remains efficient, agentic systems can leverage the same principle. "Forcing users to constantly make security-related decisions that stand between them and getting the job done quickly leads to security fatigue," the researchers note. Instead of burdening end users with consent dialogs or relying on their judgment, mathematical proofs provide deterministic guarantees that don't depend on trusting the AI model itself—or any artifacts it produces.

Key Takeaways

  • Agentic applications inherit SQL injection-style vulnerabilities from conflating instructions and data
  • Current defenses (evals, guardrails, runtime monitoring) are reactive and cannot prevent partial damage
  • Structured workflow generation separates planning from execution, blocking direct injection attacks
  • Formal verification using CodeQL, SemGrep, or theorem provers ensures workflows meet explicit security constraints before running
  • This approach mirrors bytecode verification in Java/.NET, extending proven safety principles to AI agents

The Bottom Line

We're building autonomous systems with access to email, files, and financial tools while relying on pattern matching and hope as primary defenses. Formal proof-based verification won't be optional once these systems operate at scale—the question is whether the industry adopts rigorous approaches now or waits for a catastrophic breach that makes compliance unavoidable.