🤖 AI

Formal Policy Enforcement for Real-World Agentic Systems

This paper introduces FORGE, a framework that leverages aspect-oriented programming and Datalog-based formal verification to enforce security policies with rigorous guarantees across agentic systems, addressing the limitations of natural-language prompt-based compliance in multi-agent environments.

Original authors: Nils Palumbo, Sarthak Choudhary, Jihye Choi, Guy Amir, Prasad Chalasani, Somesh Jha

Published 2026-05-12

📖 6 min read🧠 Deep dive

CC BY 4.0

Original authors: Nils Palumbo, Sarthak Choudhary, Jihye Choi, Guy Amir, Prasad Chalasani, Somesh Jha

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you hire a very smart, very eager personal assistant (an AI agent) to handle your email, book flights, and manage your bank account. You give them a list of rules in their morning briefing: "Don't send top-secret files to strangers," "Always get my boss's approval before spending money," and "Only buy airline tickets if I explicitly say yes."

In the current world of AI, you are relying entirely on the assistant's honor system. You hope they read the rules, remember them, and decide to follow them even when a tricky user tries to trick them with a fake "emergency" message. Sometimes they do; often, they don't. They might get confused, tricked, or just too eager to be "helpful" and break the rules.

This paper introduces FORGE, a system that stops relying on the assistant's memory or honesty. Instead, it puts a bouncer at every single door the assistant tries to open.

The Core Idea: The "Bouncer" and the "Rulebook"

Think of the AI agent as a worker in a massive office building.

The Old Way: You tell the worker, "Please don't open the vault unless you have a key." The worker is left alone with the vault. If someone whispers a fake code to them, they might open it.
The FORGE Way: You install a bouncer (called a Reference Monitor) right in front of the vault. Every time the worker tries to open a door (send an email, call an API, read a file), they have to stop and ask the bouncer.
- The bouncer doesn't care what the worker thinks or what they were told in the morning.
- The bouncer checks a formal, unbreakable rulebook (written in a precise logic language called Datalog).
- The bouncer looks at the worker's history (did they get approval? did they just read a secret file?).
- If the rules say "No," the bouncer physically stops the action. The door doesn't open. Period.

How It Works: The "Aspect" Analogy

The paper uses a concept called Aspect-Oriented Programming. Imagine the AI agent is a movie.

The Old Way: The script (the agent's code) has the rules written into the dialogue. If the actor forgets the line, the rule is broken.
The FORGE Way: The rules are like a special effects layer woven over the entire movie. No matter what scene the actor is in, the "special effects" (the bouncer) check the rules before the scene plays out. The actor doesn't even need to know the rules exist; the system just ensures the rules are followed automatically.

The "Rulebook" (Datalog)

Instead of writing rules in messy English (which can be ambiguous), FORGE uses Datalog.

English Rule: "Don't send emails to bad people." (Who is a bad person? What if they look nice?)
Datalog Rule: "If the recipient is external AND the email contains sensitive data derived from an untrusted source, THEN DENY."
Why it matters: This is like a math equation. It has no room for "maybe." It can also handle complex chains, like: "If Person A manages Person B, and Person B manages Person C, then Person A is the boss of Person C." The system can trace these relationships perfectly, something English prompts often struggle with.

The "Black Box" of History (Provenance)

One of the biggest problems with AI is that it forgets the cause of its actions.

The Problem: An AI reads a secret file, then gets tricked by a user, and then sends an email. The AI might think, "I'm just sending an email," forgetting that the email content came from that secret file.
The FORGE Solution: FORGE keeps a dependency graph (a family tree of actions). It knows that Event C (the email) is a child of Event B (the trick), which is a child of Event A (the secret file).
Even if the AI tries to lie or forget, the bouncer sees the whole family tree and says, "I see this email is connected to a secret file. Denied."

What They Tested (The Results)

The authors tested FORGE in three real-world scenarios to see if it actually works:

The "Trickster" Test (Prompt Injection):
- Scenario: Attackers tried to trick AI agents into stealing top-secret data by pretending to be system administrators.
- Result: Without FORGE, the AI gave up the secrets 100% of the time. With FORGE, the bouncer blocked the theft 100% of the time. The AI tried, but the door was locked.
The "Customer Service" Test:
- Scenario: AI agents trying to book flights or process refunds, where they often get confused by tricky user requests (e.g., "Cancel this flight because I changed my mind" when the policy says "No cancellations for change of mind").
- Result: Without FORGE, the agents followed the user's tricks and broke the rules 42% of the time. With FORGE, they followed the rules 98% of the time. The agents still did their jobs, but they couldn't break the rules.
The "Medical Research" Test:
- Scenario: A team of AI agents working together to research drug safety. One agent needs to access a sensitive government database, but only if a supervisor approves it first.
- Result: Without FORGE, the agents accessed the database 40 times without permission. With FORGE, they were blocked every single time until they actually got the supervisor's approval.

The Cost

Is this magic slow or expensive?

Speed: It adds a tiny bit of time (about 20–30% slower) because the agent has to wait for the bouncer to check the rules.
Money: It costs a fraction of a cent more per task.
Success: The agents still finished their tasks successfully. They just did it the right way.

Summary

FORGE is a framework that stops treating AI safety as a "please be good" request and starts treating it as a "you must be good" law. It inserts a formal, mathematical bouncer between the AI and the real world. The AI can still think, plan, and try to do things, but it cannot act on anything unless the bouncer checks the rulebook, verifies the history, and gives the green light.

It's the difference between asking a child to "be careful with the cookies" and putting a lock on the cookie jar that only opens with a specific key.

Technical Summary: Formal Policy Enforcement for Real-World Agentic Systems

Problem Statement

Contemporary agentic systems, which integrate Large Language Models (LLMs) with external tools to perform tasks like sending emails, executing code, and querying databases, lack robust mechanisms for enforcing security and organizational policies. Current approaches predominantly rely on embedding natural-language policies within an agent's system prompt, delegating compliance to the agent's reasoning capabilities. This methodology suffers from three critical limitations:

Lack of Formal Guarantees: Compliance is heuristic and contingent on the model's ability to follow instructions, offering no deterministic enforcement.
Inability to Express Causal History: Natural-language prompts struggle to enforce policies dependent on the causal history of an execution (e.g., "only allow action X if approval Y was obtained in a previous step").
Scalability in Multi-Agent Systems: Existing approaches are ill-suited for multi-agent environments where enforcement must reason across agent boundaries and partial orderings of events, rather than linear traces.

These gaps leave agentic systems vulnerable to prompt injection, unauthorized tool use, and adversarial reframing, limiting their safe deployment in real-world scenarios.

Methodology

The authors propose FORGE (FOrmal Runtime Guarantee Enforcement), a framework that treats policy enforcement as a cross-cutting concern, grounded in Aspect-Oriented Programming (AOP). The framework decouples policy logic from agent reasoning, enforcing rules at every policy-relevant decision point without modifying the underlying agents.

Core Architecture

Aspect-Oriented Formulation:
- Join Points: Defined as candidate actions (e.g., tool invocations) awaiting authorization.
- Pointcuts: Boolean functions over the execution state that determine which actions a rule applies to.
- Advice: The enforcement computation performed by a Reference Monitor, which evaluates the policy and returns an Allow or Deny verdict.
- Weaver: An instrumentation layer that intercepts tool calls, suspends execution, consults the monitor, and proceeds only upon approval.
Policy Language (Datalog):
- Policies are specified in Datalog with stratified negation and foreign-function extensions.
- Expressivity: Supports declarative rule specification and recursion, enabling the definition of transitive relationships (e.g., supervisory chains) and relationship-based access control (ReBAC).
- Analyzability: Enables static analyses for contradiction detection, redundancy, subsumption, and conditional reachability, allowing authors to verify policy intent and resolve ambiguities inherent in natural-language specifications.
- Translation: A pipeline translates natural-language policy documents into Datalog programs, annotated with clause-level links to source text for coverage and entailment verification.
Policy Substrate and Environment Contract:
- Substrate ( $\Sigma$ ): A set of abstract predicates (Role, Provenance, Domain-specific) that describe the execution context.
- Observability Service: Maintains a causal dependency graph of events (messages, tool calls, results) and populates the substrate predicates.
- Assume/Guarantee Contract: Correctness is guaranteed under the assumption that the environment satisfies a contract: it must soundly and sufficiently populate the substrate predicates with facts consistent with their intended interpretations (e.g., accurate causal lineage). If the contract holds, the reference monitor's decisions coincide with the policy's intended semantics.

Key Contributions

Formal Framework for Agentic Enforcement: The paper presents the first framework capable of automatically enforcing policies in multi-agent systems with formal correctness guarantees, utilizing an AOP paradigm to separate cross-cutting concerns from core logic.
Datalog-Based Policy Specification: It introduces Datalog as a policy language for agentic systems, leveraging its support for recursion and static analysis to handle complex, stateful policies that natural-language prompts cannot express.
The FORGE System: A practical implementation comprising an aspect weaver, an observability service, and a reference monitor. FORGE instruments agent frameworks (e.g., Langroid, $\tau^2$ ) to enforce policies at runtime without altering agent code.
Correctness Theorem: The authors prove an assume/guarantee theorem stating that if the environment satisfies the substrate contract, the runtime enforcement decisions are correct with respect to the policy's intended semantics.

Evaluation Results

The framework was evaluated on three quantitative case studies and two real-world deployments:

Prompt Injection Defense (Information Flow):
- Goal: Prevent data exfiltration via prompt injection.
- Result: Non-instrumented agents had a 100% attack success rate. FORGE reduced this to 0% while maintaining 100% utility on benign tasks.
- Overhead: Latency increased by ~12–15 seconds per trial; cost increase was negligible (<$0.003).
Customer Service Workflows ( $\tau^2$ -Bench):
- Goal: Enforce business rules (cancellations, refunds, baggage) across three frontier models.
- Result: Compliance improved from 58% to 98%. Task success was preserved or improved (e.g., pass rates rose from 58% to 98%).
- Overhead: End-to-end latency increased by 19–38% (median sub-millisecond authorization decision); cost increase was < $0.05 per trial.
Multi-Agent Pharmacovigilance (MALADE):
- Goal: Enforce approval workflows for FDA data access across a multi-agent pipeline.
- Result: Unauthorized FDA accesses dropped from 40 to 0 across 15 trials. Task accuracy remained at 100% (15/15 correct predictions).
- Overhead: Latency increased from 72.5s to 95.4s (driven by blocked-then-retry cycles); cost increased from $0.072 to $0.103 per trial.

Real-World Deployments: The paper also describes successful application in OpenClaw (inter-agent privacy enforcement) and VS Code Copilot Chat (gating git push until static analysis passes).

Significance and Claims

The paper claims that FORGE represents a significant advancement by bridging the gap between informal policy specifications and rigorous runtime enforcement in agentic systems. Its primary significance lies in:

Deterministic Guarantees: Unlike prompt-based approaches, FORGE eliminates policy violations by construction, provided the environment contract is met.
Stateful Enforcement: It uniquely supports policies dependent on causal history and transitive relationships across multiple agents, a capability missing in existing stateless or linear-trace-based systems.
Modularity: By weaving enforcement into the runtime, it allows for the enforcement of complex organizational policies without requiring changes to the agent's internal reasoning or the underlying tools.
Analyzability: The use of Datalog allows for the detection of policy contradictions and ambiguities before deployment, treating policies as reviewable artifacts rather than opaque prompts.

The authors maintain modesty regarding the translation pipeline, acknowledging that while the translation from natural language to Datalog is realized via LLMs, it currently lacks formal correctness guarantees and requires manual review and iterative validation. They identify the robustness of this translation and the extension to non-expert policy authors as open problems for future work.