AWS Open Source Blog
Introducing Dogwood: runtime verification for AI agents
Part of what makes AI agents so useful is their ability to interact with the external world by running tools. But these tool calls are also the source of the biggest risks when it comes to making agents safe to use. The best way to address these risks in a dependable and reliable manner is to put a layer of control at the tool-call boundary that regulates what an agent is allowed to do. By enforcing rules about how agents may use tools, we get rigorous guarantees about the ways agents can affect the external world. To do this effectively, we need a way to precisely specify and enforce rules about agent behavior. Today, we’re releasing Dogwood, an open source governance language designed for agents and their tools.
We previously made the case for regulating agent tool use with AgentCore Policy, the layer in Amazon Bedrock AgentCore that decides, on every tool call, whether an agent’s action is allowed. AgentCore Policy launched using Cedar as the language those policies are written in. Cedar is fast, readable, and analyzable through automated reasoning, and it gives a guarantee that audit and enforcement depend on: identical requests yield identical decisions, regardless of evaluation order or system state. Why Policy in Amazon Bedrock AgentCore chose Cedar for securing agentic workflows explains that choice in detail, and why automated reasoning matters so much for it. Cedar supports efficient point-in-time authorization decisions where each request is evaluated in isolation, with no dependency on past actions. As a result, it can draw a safety envelope around any single action, but it was not designed for expressing rules about sequences of actions. Point-in-time decisions make sense for many forms of access control, but when agents compose multiple actions into longer workflows, the sequence itself becomes something teams want to govern. Dogwood gives them a language for expressing policies over sequences, in order to capture constraints on prerequisites, rate limits, and ordering. For example, we might want to require an agent to get approval before acting, stay under a running limit, or never contact external parties once it has accessed confidential information. To enforce these kinds of restrictions, the policy layer has to be able to look back beyond the current request.
In Dogwood, policies can look back over an agent’s recent events, not just the current request. Dogwood supports evaluating existing Cedar policies and adds in a new and powerful tool: temporal conditions. Temporal conditions refer to the history of prior events, which makes it possible to state policies that ensure that an agent uses tools in the correct order, stops using some tools after others, and limits the frequency of some tools. Dogwood is based on a precise mathematical foundation, called temporal logic, giving it the strength required to solve the most critical agentic safety problems.
We’ve also launched Dogwood policy support inside AgentCore Policy. Because Dogwood is compatible with existing Cedar policies, customers can continue to use their current policies without any need for migration. They can now make use of Dogwood’s temporal conditions to extend existing policies and craft new ones. With the open source release of the Dogwood language, customers can define their policies using their favorite IDE or coding agent and explore their behavior with the Dogwood parser, validator, and reference interpreter. The Dogwood language is released under an Apache 2.0 license.
Temporal policies
A Cedar policy condition in a when { ... } clause sees only the current authorization request. Dogwood adds a second kind of clause — when temporal { ... } — whose condition can also look at what came before the request. These temporal clauses express properties about traces of events. Each event corresponds to either a tool call request or its outcome and records data associated with the tool call (e.g. input arguments, requesting principal, etc.). The set of tool calls a policy can talk about is the action schema, and for an agent that schema is generated from tools it already exposes over the Model Context Protocol (MCP). We’ll tour through Dogwood’s operators for temporal policies by working through a series of examples involving a stock trading agent whose tools include ApproveSale, SellShares, and Transfer.
Looking back: approve before you sell
For our first example, let’s say we want to ensure that an agent may sell shares only if it already received approval for that exact amount. Thus, a SellShares tool call depends on an earlier event, so a point-in-time condition can’t see it, but in Dogwood we can express it as follows:
// Permit a sale only if approval for the same amount of the same
// stock came back granted within the last hour.
permit ( principal, action == AgentCore::Action::"SellShares", resource )
when temporal {
formerly within 1h AgentCore::Action::"ApproveSale"::response{
input.stock: context.input.stock,
input.shares: context.input.shares,
output.approved: true
}
};The formerly operator is backward-looking: it holds if the condition it describes occurred at least once in a specified time window. Here, the window is within 1h, so it looks back over the past hour to see if the specified condition held at any point. The condition is that a corresponding ApproveSale::response event occurred, which represents the outcome of some prior ApproveSale tool call. That ApproveSale must have had input.stock and input.shares fields that match the current request’s context.input.stock and context.input.shares. In addition, the output.approved flag of that call must have been true, indicating that the request was in fact approved.
To further explain this policy, let’s consider what happens on an example trace of events shown below. Each line of the trace describes an event. An event description starts with a timestamp of the form “@n”, where n indicates when the event occurred, measured in seconds. In Dogwood policies, all temporal conditions use time on a relative basis, measuring the time difference between a request and earlier events, so the absolute value of this timestamp does not matter. For simplicity, in each of our examples, we’ll start the first event at a timestamp of 0. After the timestamp, the event description records the action and kind of event: the name of the tool call and whether it was a request or response. Next, enclosed in curly braces, we have the arguments associated with the event. Finally, when the event is a request, the line ends with the authorization verdict given by the policy, either DENY or ALLOW.
@0 SellShares::request { stock: "AMZN", shares: 100 } -> DENY
@1700 ApproveSale::response { stock: "AMZN", shares: 100, approved: true }
@1800 SellShares::request { stock: "AMZN", shares: 100 } -> ALLOW
@7200 SellShares::request { stock: "AMZN", shares: 100 } -> DENYReplaying a stream of events against this policy shows the verdict change as the recent past changes. The first event is a request that is denied because there has been no approval on record. The second event is a response to a sale approval request. This is not a request, so it has no verdict attached, but it is recorded in the event history and affects later requests. The third event is another request, which this time is approved, because in this case there is an approval within the time window. However, the request in the fourth event is denied again as the approval is outside the window.
Notice that in this trace, the last SellShares::request occurs before the response of the previous allowed request. This can happen because agents can make parallel tool calls and interact with tools asynchronously. Moreover, while we’ll focus on policies for a single agent in our examples, this kind of interleaving can also arise in multi-agent settings. Thus, it is important to keep this kind of concurrency in mind when writing policies.
Mixing temporal and non-temporal clauses
That previous policy was entirely temporal, but most real rules combine a fact about the recent past with a plain fact about the request itself. To support this, Dogwood allows embedding temporal clauses inside a Cedar expression: the temporal { ... } marker is an expression, so it drops straight into an ordinary when clause alongside the Cedar you already write. For example, here a sale must be both small and recently approved:
// Permit a sale only if it is small (a plain, point-in-time check on
// this request) AND approval for the same stock and amount came back
// granted within the last hour (the temporal check, inline via the
// `temporal` marker).
permit ( principal, action == AgentCore::Action::"SellShares", resource )
when {
context.input.shares <= 100
&& temporal {
formerly within 1h AgentCore::Action::"ApproveSale"::response{
input.stock: context.input.stock,
input.shares: context.input.shares,
output.approved: true
}
}
};The context.input.shares <= 100 is exactly the Cedar policy you’d write without Dogwood — it looks only at the current request. The temporal { ... } next to it looks back over recent events. Both must hold for the request to be authorized, as we can see in the following trace:
@0 SellShares::request { stock: "AMZN", shares: 50 } -> DENY
@60 ApproveSale::response { stock: "AMZN", shares: 50, approved: true }
@120 SellShares::request { stock: "AMZN", shares: 50 } -> ALLOW
@180 ApproveSale::response { stock: "AMZN", shares: 500, approved: true }
@240 SellShares::request { stock: "AMZN", shares: 500 } -> DENYThe request in the first event here is denied, because even though the share count is below the threshold set by the Cedar expression, there is no approval in the history, so the temporal half fails. For the request on the third line the share count is small and there is an approval in the history, so it is allowed. However, for the last request at the end, it is denied despite having an approval in the history, because the share count exceeds the threshold from the Cedar expression.
Counting: how many times
Another class of common policies requires knowing not just that something has happened in the past, but how many times it has happened. The simplest is a plain count of all the times an event occurred in some window. These can be used to write rate-limiting policies. For example, “no more than five transfers in an hour, however small each one is”, can be expressed as follows:
// Forbid a transfer once five have already
// gone out in the last hour.
forbid ( principal, action == AgentCore::Action::"Transfer", resource )
when temporal {
count_within(1h, AgentCore::Action::"Transfer"::request{ input.amount: _ }) > 5
};As the name suggests, this count_within will count over the last hour (1h) every Transfer request — the _ is a wildcard that says we don’t care about the amount, just that it happened — and compare the count to five. This leads to the following verdicts on this event trace:
@0 Transfer::request { amount: 20 } -> ALLOW // 1st transfer
@60 Transfer::request { amount: 20 } -> ALLOW // 2nd
@120 Transfer::request { amount: 20 } -> ALLOW // 3rd
@180 Transfer::request { amount: 20 } -> ALLOW // 4th
@240 Transfer::request { amount: 20 } -> ALLOW // 5th
@300 Transfer::request { amount: 20 } -> DENY // 6th in the window exceeds limitCounting distinct things
Sometimes the count you want is not of events but of distinct values across them: not “how many transfers” but “how many different recipients.” For example, we can express “an agent may make transfers to at most three distinct recipients in an hour”:
// Forbid a transfer that would make it the fourth distinct
// recipient paid in the last hour.
forbid ( principal, action == AgentCore::Action::"Transfer", resource )
when temporal {
count_distinct_within(u, 1h, AgentCore::Action::"Transfer"::request{ input.user: u }) > 3
};Here the recipient is bound to u, and count_distinct_within counts the distinct values of u seen in the window — so paying the same recipient twice counts once, but a new payee bumps the tally. We can see what happens when we have five transfers to bob, carol, dave, erin, then bob again:
@0 Transfer::request { user: "bob" } -> ALLOW // 1 distinct recipient
@60 Transfer::request { user: "carol" } -> ALLOW // 2
@120 Transfer::request { user: "dave" } -> ALLOW // 3
@180 Transfer::request { user: "erin" } -> DENY // would be 4th distinct recipient
@240 Transfer::request { user: "bob" } -> DENY // still 4 (bob, carol, dave, erin)The fourth distinct recipient is refused even though everything about that single transfer is fine; the repeat to bob afterwards stays denied because the window already holds too many distinct payees.
Summing: stay under a running total
In addition to counting, Dogwood also provides ways to sum the data associated with events. For example, for tools that transfer money, we might want to limit the total number of dollars that can be transferred in a window, not just the number of transfer events. The sum_within operation allows us to express policies like “no more than $5,000 transferred in the last hour, however many transactions it takes”:
// Forbid a transfer once more than $5,000 has been
// transferred in the last hour, across any number of transfers.
forbid ( principal, action == AgentCore::Action::"Transfer", resource )
when temporal {
sum_within(a, 1h, AgentCore::Action::"Transfer"::request{ input.amount: a }) > 5000
};sum_within mirrors count_within, but instead of tallying events it binds each transfer’s amount to a and adds those up.
Rate limiting requests vs. responses
In the previous rate-limiting policies, we have expressed the rate limits in terms of Transfer::request events, not Transfer::response. This is important for securely achieving the rate-limiting we intend in the presence of concurrent and asynchronous tool calls. The Transfer::request event includes any requests (including the one whose authorization is under consideration), while Transfer::response only includes transfers that have completed. Let’s consider how an agent could therefore circumvent the intended rate limit if we used the following incorrect policy based on Transfer::response instead:
// Forbid a transfer once more than $5,000 has already
// settled in the last hour.
forbid ( principal, action == AgentCore::Action::"Transfer", resource )
when temporal {
sum_within(a, 1h, AgentCore::Action::"Transfer"::response{ input.amount: a }) > 5000
};The only change from the previous policy is one word: it sums Transfer::response events instead of Transfer::request events. Because this policy only sums the amounts associated with responses, an agent can circumvent the intended limit by issuing many concurrent transfer requests before any one of them resolves, as we can see with the following example trace:
response request
@0 Transfer::request { amount: 2000 } ALLOW ALLOW
@1 Transfer::request { amount: 2000 } ALLOW ALLOW
@2 Transfer::request { amount: 2000 } ALLOW DENY
@3 Transfer::response { amount: 2000 }
@4 Transfer::response { amount: 2000 }
@5 Transfer::request { amount: 2000 } ALLOW DENYThe difference starts on the third Transfer::request: at that point there is $6,000 total requested “in flight”, so with the version of the policy that sums the amounts from Transfer::request events, this results in a denial. However, at that point, there have been no Transfer::response events yet, so the variant of the policy that uses Transfer::response for the sums instead allows the request.
Comparing the total against a request variable
Every cap so far compared a window total to a fixed number. But the interesting threshold is sometimes the request being checked right now. “A single transfer must not exceed everything that’s already settled this hour” is an anti-spike rule: it lets an agent operate at the scale it has established, and refuses the one payment that suddenly dwarfs the rest. That needs the window total to have a name, so the current request can be compared against it:
// Forbid a transfer larger than everything already
// settled in the last hour, combined.
forbid ( principal, action == AgentCore::Action::"Transfer", resource )
when temporal {
bind(prior,
sum_within(a, 1h, AgentCore::Action::"Transfer"::response{ input.amount: a }),
context.input.amount > prior)
};bind lets us associate a name with the aggregate — here the settled total becomes prior — and then write an ordinary condition about it. context.input.amount is the amount on the transfer being decided, so context.input.amount > prior forbids exactly the transfer that exceeds all the settled ones put together. Here is how this policy behaves on an example trace:
@0 Transfer::response { amount: 1000 } // $1,000 settled this hour
@60 Transfer::request { amount: 500 } -> ALLOW // 500 <= 1,000 settled
@120 Transfer::request { amount: 2000 } -> DENY // 2,000 > 1,000 settled
@180 Transfer::request { amount: 800 } -> ALLOW // 800 <= 1,000 settledThe $2,000 is the only one refused, because it was out of proportion to the agent’s own recent, settled behavior.
Temporal logic
These examples have illustrated the scenarios that come up commonly, with each having a convenient operation for describing common policy shapes:
- Did this happen?:
formerly - How many?:
count_within - How many different?:
count_distinct_within - How much in total?:
sum_within
In fact, these last three operations, as well as bind, are not primitives in Dogwood, but are instead defined as macros in Dogwood’s standard library. These macros are defined in terms of a core subset of temporal operators drawn from a logic called Metric First-Order Temporal Logic (MFOTL). While we expect many users will be able to express their policies using these higher-level macro operations, more advanced policies can be written directly using the underlying operations from MFOTL. MFOTL has its roots in a branch of formal methods called runtime verification, the discipline of checking a running system against a formal specification of how it should behave. Dogwood combines the powerful features of MFOTL with Cedar’s support for point-in-time authorization.
Because runtime verification generalizes authorization rather than replacing it, Dogwood could build directly on Cedar instead of departing from it: any syntactically valid Cedar policy is a syntactically valid Dogwood policy, so an existing Cedar policy set can be reused as-is, with no rewrite and no migration. Users can keep writing plain Cedar wherever plain Cedar suffices. Dogwood keeps Cedar’s authorization semantics intact, too, with deny by default behavior in which forbid overrides permit. This means that the guarantees audit and enforcement already rely on carry over unchanged.
On the other hand, the expressivity of temporal policies does not come for free: evaluating them requires stateful tracking of events, and the time complexity of evaluation can depend on the length of the event log. In addition, temporal conditions do not currently support the powerful automated reasoning analysis tools that Cedar provides. We believe that tradeoff is appropriate for policies governing agentic actions, but it might not be right for all of the other ways in which a policy language like Cedar has been used. That’s part of the reason why we decided to develop a new language rather than adapting Cedar.
Configuring Dogwood
The examples above used Dogwood exactly as it ships, but almost every piece is configurable when you need it. You can define your own macros to name recurring patterns and build a shared library beyond the standard one; declare a richer event model that incorporates additional kinds of events beyond request/response events for tool calls, allowing you to express properties that refer to other events in an agent’s environment. Dogwood also supports defining new information providers — small sandboxed functions that compute a fact (a pattern match, a denylist check, a classifier’s verdict) that a policy can then read inline. To aid in getting started, Dogwood includes a way to generate the action schema straight from an agent’s MCP tool manifest, one action per tool, onto a ready-made template that already models the identities an agent authenticates as. The guide included with Dogwood covers each of these features.
Where this is going
Dogwood today verifies safety: it looks at the recent past and forbids the actions that would break your rules. That’s a first step, with a few other features already on the way:
Richer operators, including absolute time. Every window today is relative — “within an hour” means the last sixty minutes, a sliding window that follows the clock forward. Many real rules are anchored to non-sliding windows instead. For example, a daily quota that resets at midnight or “before end of business.” Those call for absolute-time operators — windows pinned to wall-clock boundaries rather than measured backward from now.
Beyond safety: liveness. Safety says what must not happen. Its counterpart, liveness, says what must happen — an approval must eventually be followed through, a started task must reach a terminal state, a resource that was opened must be released. Verifying liveness needs operators that reason about the future as well as the past, and MFOTL already models these concepts. Extending Dogwood to support them is a natural next step.
Orchestration for multi-agent systems. As work spreads across several cooperating agents, the properties worth checking stop being about one agent and become about the ensemble: who may hand off to whom, which agent holds a lock, whether the group as a whole is making progress. Bringing runtime verification to that setting is where we ultimately want Dogwood to go.
The goal of these plans is to increase the expressivity of policies, reflecting the growing scope and autonomy of agents.
Get started
Dogwood is open source under Apache 2.0. In addition to the reference code, there is also an accompanying language guide that walks through the full language with practical examples. While we are not yet accepting direct contributions to Dogwood, we welcome community feedback on the language design and future directions. We’ve already shared Dogwood with members of the Cedar community and incorporated their early input. Our plan is to grow openness iteratively: gather reactions and feedback first, then open contributions as the language stabilizes, and build governance together with the community that forms around it.