WEBVTT 00:00:00.000 --> 00:00:00.000 again for the second time at Seattle Systems. 00:00:00.440 --> 00:00:04.520 I will say thank you to the Momento folks, 00:00:05.500 --> 00:00:07.520 the antithesis folks for sponsoring the food. 00:00:08.440 --> 00:00:11.840 You should not trust those antithesis folks, they will break your software and destroy 00:00:11.840 --> 00:00:15.420 your ego, so just be careful around them. 00:00:20.440 --> 00:00:24.300 Yeah, so Dogwood, today I'm going to be talking about temporal policy for AI agents if 00:00:24.300 --> 00:00:28.220 you don't know what that means, I will hopefully explain, we'll do a little bit of math, 00:00:28.300 --> 00:00:31.560 we'll talk about databases and hopefully some other fun things. 00:00:32.780 --> 00:00:34.400 So let's start with what is Dogwood? 00:00:35.400 --> 00:00:39.520 Dogwood is a governance language, you can think of it as a programming language, which 00:00:39.520 --> 00:00:44.480 it technically is, you can think about it as a DSL, but it is a language for governing 00:00:44.480 --> 00:00:50.680 agents, for describing what programs can do, agents are kind of general programs, and 00:00:50.680 --> 00:00:57.500 so we designed Dogwood to be for agents, but you can actually describe behaviors of any 00:00:57.500 --> 00:00:59.400 program in Dogwood. 00:01:01.160 --> 00:01:05.360 A couple of years ago, more than a couple of years ago, probably a decade or so ago, 00:01:06.160 --> 00:01:13.080 teams at Amazon built Cedar, which is now open source, and Cedar is a policy language, 00:01:13.080 --> 00:01:15.200 it is a pro -authorization language, 00:01:16.820 --> 00:01:20.840 and Dogwood you can think of as taking a lot of the ideas of Cedar, if you're familiar 00:01:20.840 --> 00:01:25.060 with Cedar or you're familiar with those kinds of authorization languages, and so it 00:01:25.060 --> 00:01:30.600 has these keywords like permit and forbid, when, unless, etc. 00:01:31.500 --> 00:01:35.380 What Dogwood adds is the idea of time and order, 00:01:37.520 --> 00:01:40.740 where, and I'll go through a bunch of examples, so you don't necessarily need to understand 00:01:40.740 --> 00:01:46.320 this now, you can talk about things like since, once, before, after, and so on. 00:01:49.740 --> 00:01:53.800 And I wouldn't say it actually compiles to Cedar, I think this is sort of old language, 00:01:54.940 --> 00:01:59.760 but it is a, I would think of as a superset of Cedar, and I'll talk a little bit later, 00:01:59.760 --> 00:02:04.420 we actually compiled this to SQL in the back end, which is kind of fun, and it is Apache 00:02:04.420 --> 00:02:08.920 2 licensed, it's on GitHub, you can use it for your own things, actually today we launched 00:02:08.920 --> 00:02:15.380 a new runtime for Dogwood, which is really easy to add into your own products, 00:02:15.980 --> 00:02:20.280 or own projects, all open source, and this is the kind of thing it looks like, it is 00:02:20.280 --> 00:02:24.580 not the kind of programming language you would necessarily want to write a ton of yourself, 00:02:24.700 --> 00:02:29.720 and so it is a language that you can handwrite, but is primarily, I would say, expected 00:02:29.720 --> 00:02:32.560 to be written by tools rather than people. 00:02:34.770 --> 00:02:39.550 So why did we build Dogwood? Well, we built Dogwood because we were thinking about an 00:02:39.550 --> 00:02:45.190 agent policy problem, of how do you describe, given an agent or an agentic application, 00:02:45.350 --> 00:02:50.950 so this is an AI agent, this could be everything from Codex or Claude Code, one of these 00:02:50.950 --> 00:02:55.970 very open -ended agents, to a customer service chatbot, to whatever kind of agent you're 00:02:55.970 --> 00:03:02.410 building, and we want to be able to describe what that agent can do in a way that is 00:03:02.410 --> 00:03:08.950 very exact, in a way that is very crisp, and a way that can be deterministically applied. 00:03:09.670 --> 00:03:13.010 And so if you think about, or if you've been in this space, you'll know that folks are 00:03:13.010 --> 00:03:19.710 doing LLM as a judge type techniques, they're having models watch agents, having heuristics 00:03:19.710 --> 00:03:24.950 watch agents, all of those things are good, valuable techniques, but we wanted to build 00:03:24.950 --> 00:03:30.150 something that would allow us to express policy in a way that we can apply it deterministically, 00:03:30.490 --> 00:03:36.070 in a way that we can reason about it very keenly, and a way that you can know for sure 00:03:36.070 --> 00:03:39.550 when you express something in Dogwood, it has a particular behavior. 00:03:41.150 --> 00:03:46.410 And so a lot of this is around what agents can do. And so when I think about, you know, 00:03:46.450 --> 00:03:50.390 kind of putting a box around agents, I sort of think about that in two categories. One 00:03:50.390 --> 00:03:54.690 of them is what agents can say, and this is the fuzzy kind of guard railing problem of, 00:03:55.170 --> 00:03:59.970 hey, I want my agents to talk respectably to my customers, I want my agents to say helpful 00:03:59.970 --> 00:04:04.430 things. Those aren't things you can really do deterministically because they are in this 00:04:04.430 --> 00:04:11.110 realm of natural language and a realm of very fuzzy social expectations, 00:04:11.270 --> 00:04:15.230 right? Like it might even be that in one country saying a particular word is offensive 00:04:15.230 --> 00:04:19.330 and in another place it's not, right? Like this is not the kind of thing you can encode 00:04:19.330 --> 00:04:25.130 in policy. But what you can encode in policy is how agents use their tools. And here 00:04:25.130 --> 00:04:31.050 tools could be accessing the file system. It could be calling Git, it could be calling 00:04:31.050 --> 00:04:36.870 Cargo, it could be calling a SaaS app, it could be creating a ticket, it could be sending 00:04:36.870 --> 00:04:41.410 an email, right? Like all of these things that agents do in their environment, that makes 00:04:41.410 --> 00:04:46.690 them interesting and useful. And so this is the core tension we have with agents, is 00:04:46.690 --> 00:04:52.010 we want them to be able to do a bunch of stuff on our behalf, we want them to solve hard 00:04:52.010 --> 00:04:58.530 problems persistently, some might even say creatively, but we also want to be able 00:04:58.530 --> 00:05:03.610 to strongly control the set of things they can do. And this is a tension because you 00:05:03.610 --> 00:05:08.570 don't really want, if you over constrain an agent to the point that it has to follow 00:05:08.570 --> 00:05:14.290 a particular path, well, then you've just invented a very expensive, very slow workflow. 00:05:14.910 --> 00:05:19.830 But if you under constrain an agent and let it do whatever it wants to do, well, its 00:05:19.830 --> 00:05:25.430 nature of being very persistent might lead you to places you don't want to be at. 00:05:31.800 --> 00:05:32.640 For example. 00:05:33.820 --> 00:05:34.980 So credit to some folks. 00:05:35.920 --> 00:05:41.640 John Tristan is really the kind of core inventor of Dogwood, you know, fantastic scientist. 00:05:42.360 --> 00:05:48.840 Joe Tessarotti did a whole lot of work on it, especially on the compiler, and a fantastic 00:05:48.840 --> 00:05:54.620 team of engineers and folks around Amazon and a growing open source community. 00:05:56.200 --> 00:06:02.980 And so this is some of my work, but almost in the vast majority, the work of folks like 00:06:02.980 --> 00:06:03.380 that. 00:06:05.000 --> 00:06:07.320 So let's dive into some examples. 00:06:08.900 --> 00:06:15.260 And here we want to say I need pre -approval to sell Amazon stock. 00:06:16.040 --> 00:06:20.660 And I want my agent to do this for me because I want my agents to do all the annoying 00:06:20.660 --> 00:06:26.880 administrative tasks in my life. But I want to make sure that I don't end up in trouble. 00:06:27.460 --> 00:06:34.200 So I want to write a policy that says I have to approve, there has to be an approval, 00:06:34.800 --> 00:06:42.000 approved sale, before I can sell my shares. And so what this policy says is 00:06:42.000 --> 00:06:49.100 within formally, so before, within one hour, a approval response happened for 00:06:49.100 --> 00:06:55.600 an amount of stock, amount of shares, and the approval was true. And if all of 00:06:55.600 --> 00:07:01.900 those things are true, then I can call this sell shares API. 00:07:03.440 --> 00:07:09.180 And this you can't really express in a authorization language like Cedar because it doesn't 00:07:09.180 --> 00:07:14.600 have the ability to reason about time in this way. You could say, 00:07:15.520 --> 00:07:20.320 you know, you could write a non -time -based or non -ordering -based version of this 00:07:20.320 --> 00:07:25.620 policy, but you can't write these kinds of temporal policies. And so this is the fundamental 00:07:25.620 --> 00:07:29.520 idea of Dogwood, is being able to reason about time, reason about order. 00:07:31.600 --> 00:07:34.000 And I'll show you some future examples, 00:07:35.480 --> 00:07:40.240 reason about the speed at which things happen too. So here I'll see, okay, here's my 00:07:40.240 --> 00:07:45.140 timeline of examples. This is where my sort of 2e slides break down a little bit. At 00:07:45.140 --> 00:07:49.260 zero minutes, I'm going to try and do a sell shares, and I'm going to get a deny. Nobody's 00:07:49.260 --> 00:07:54.800 approved yet. Then 28 minutes, I'm going to do an approval. Okay, that worked. Yep, everyone's 00:07:54.800 --> 00:07:59.360 happy. 30 minutes or two minutes later, I'm going to call sell shares. And that's going 00:07:59.360 --> 00:08:04.540 to be allowed, right? Because within one hour, I had the approval. And then two hours 00:08:04.540 --> 00:08:09.720 later, I'm going to try and do sell shares again and denied because there has not been 00:08:09.720 --> 00:08:12.920 an approval within one hour. So far so good. 00:08:15.800 --> 00:08:21.800 Here's another one. Very, very common request when I talk to customers about things they 00:08:21.800 --> 00:08:26.060 want to express to their agents. You have an agent that maybe can do two things. One 00:08:26.060 --> 00:08:30.620 of them is access commercial data or confidential data, and the other is send email. 00:08:31.420 --> 00:08:36.600 I'm okay with an agent sending email. I'm okay with an agent reading the confidential 00:08:36.600 --> 00:08:41.300 data. I'm absolutely not okay with an agent sending email after reading the confidential 00:08:41.300 --> 00:08:45.740 data because there is a probability that that confidential data will make its way into 00:08:45.740 --> 00:08:47.580 the email that it sent. 00:08:48.800 --> 00:08:50.000 And so here again, 00:08:50.980 --> 00:08:57.520 I can write this policy that says formally within 24 hours, if there's 00:08:57.520 --> 00:09:04.340 a read confidential, then we are going to forbid this sending of 00:09:04.340 --> 00:09:04.680 email. 00:09:06.120 --> 00:09:12.760 Similarly, I want to make sure that my agent is running the tests 00:09:12.760 --> 00:09:20.580 and has run the tests before doing a get commit. And so here, I'm going to use this previous 00:09:20.580 --> 00:09:27.280 keyword, and I'm going to make sure that I am only allowed to commit if the 00:09:27.280 --> 00:09:34.020 last thing I did was a successful cargo test. So if I do a cargo test, 00:09:34.780 --> 00:09:40.920 that exits with zero, get commit. That's great. Cargo test, that fails, and then try 00:09:40.920 --> 00:09:45.600 get commit, denied. If I do a cargo test and then something else, I modify one of the 00:09:45.600 --> 00:09:52.140 files, denied, or if I wait too long, denied. So this is 00:09:52.140 --> 00:09:56.740 really cool, right? Like I can write these policies that express these sort of common 00:09:56.740 --> 00:10:01.800 sense -ish things. Now I'll grant it not in a common sense syntax, but we'll sort of 00:10:01.800 --> 00:10:07.300 get to that. But I can express these common sense things about what agents can do by 00:10:07.300 --> 00:10:10.900 thinking about these concepts of before and after and so on. 00:10:12.520 --> 00:10:17.460 I can set rate limits, and so this I've got count within, so I can say this thing is 00:10:17.460 --> 00:10:24.300 only allowed to do, you know, one thing a minute or five things an hour or whatever. 00:10:24.660 --> 00:10:29.020 Count within one hour is greater than five, and so I'm going to deny if I've done this 00:10:29.020 --> 00:10:33.580 more than five times an hour. And so I can even express these kinds of throttling type 00:10:33.580 --> 00:10:38.180 policies where I can say this agent can send emails to my boss, but only one a day. 00:10:39.320 --> 00:10:41.000 Let's keep it respectful. 00:10:42.580 --> 00:10:47.440 And so again, it's just a matter of keeping track of time, keeping track of order, keeping 00:10:47.440 --> 00:10:49.000 track of number, and so on. 00:10:51.250 --> 00:10:57.590 I'm going to skip this example. It's a bit of a weird one, but it's just... The key idea 00:10:57.590 --> 00:11:06.170 here is that you can set policy on requests or responses to 00:11:06.170 --> 00:11:06.730 two calls. 00:11:07.630 --> 00:11:12.430 And if you set policy on requests incorrectly, then policies might mean something other 00:11:12.430 --> 00:11:15.230 than what you are expecting. 00:11:17.030 --> 00:11:22.630 And the key idea there is not that, well, firstly, there's all this power. And secondly, 00:11:22.870 --> 00:11:28.170 that languages like this tend to be very subtle, and so it is quite likely that we are 00:11:28.170 --> 00:11:32.790 going to want tools to help us reason about what these policies mean. 00:11:33.990 --> 00:11:37.870 But the secret here, and I'll get to a little bit of this later, is that if you had written 00:11:37.870 --> 00:11:39.930 the same logic in Python, 00:11:40.970 --> 00:11:45.470 for example, you would have exactly the same subtlety, but it would be less obvious. 00:11:46.230 --> 00:11:50.630 You could have exactly the same bug if you had written this in a general purpose programming 00:11:50.630 --> 00:11:56.310 language. It would be a bug that's harder to see and a bug that is much harder to formally 00:11:56.310 --> 00:11:57.290 reason about. 00:11:58.330 --> 00:12:00.510 I'll get to more of that in a second. 00:12:02.070 --> 00:12:08.510 Another example, no sudden spikes, and some within an hour, and make sure that the rate 00:12:08.510 --> 00:12:12.430 of things flowing through a system, the rate of an agent spending my money doesn't go 00:12:12.430 --> 00:12:19.230 up too fast. So there's just a ton of different things you can encode with what seems 00:12:19.230 --> 00:12:24.290 like a relatively limited and ultimately is a relatively limited policy language. 00:12:27.220 --> 00:12:30.940 So then, yeah, why not a general purpose language? Why not Python, why not Rust, why 00:12:30.940 --> 00:12:36.020 not TypeScript, whatever? And there are a couple of reasons for that. One of them is 00:12:36.020 --> 00:12:41.980 I want to get up to a level of abstraction where I can only be looking at and thinking 00:12:41.980 --> 00:12:48.180 about policy. I don't also be thinking about I .O. or logging or imports 00:12:48.560 --> 00:12:53.580 or all of these other things, right? And so I actually want to limit the power of the 00:12:53.580 --> 00:12:57.980 language so I can be up at an abstraction level where I'm only thinking about this one 00:12:57.980 --> 00:12:59.060 particular topic. 00:13:00.260 --> 00:13:04.160 And the analysis tools are only having to worry about this particular topic. 00:13:05.520 --> 00:13:08.320 I want this language to be analyzable, 00:13:09.460 --> 00:13:14.720 which I'm going to certainly roughly say easy to understand what programs mean. And I 00:13:14.720 --> 00:13:17.520 don't really mean that for humans, but I mean that for tools. 00:13:18.480 --> 00:13:24.860 And I'm very interested in applying formal reasoning, applying automated reasoning, 00:13:25.000 --> 00:13:30.920 applying formal methods to programs. In general, that is a very hard thing to do. 00:13:31.600 --> 00:13:36.140 It is something that is actually pretty tractable for large code bases, but it's very 00:13:36.140 --> 00:13:42.700 easy to write a program that cannot be analyzed formally 00:13:42.700 --> 00:13:47.860 where you can't say meaningful things about its properties. For example, you might have 00:13:47.860 --> 00:13:53.540 run into the collapse conjecture, which you could write as a four -line Python program 00:13:53.540 --> 00:13:59.440 that is an open mathematical question about whether it terminates or not for arbitrary 00:13:59.440 --> 00:14:00.280 size integers. 00:14:02.200 --> 00:14:08.660 And so I want an analyzable program. Cedar was very carefully designed to be analyzable, 00:14:08.660 --> 00:14:15.180 to be analyzable in a subset of SMT, to be analyzable with a particular 00:14:15.180 --> 00:14:22.040 set of tools. It was really targeted at that, and that is hugely valuable. But 00:14:22.040 --> 00:14:27.760 it also means that Cedar has some things you can't express, especially these sort of 00:14:27.760 --> 00:14:28.960 ordering properties. 00:14:30.260 --> 00:14:35.460 And so when Cedar was designed, we had a certain set of tools for analyzing programs. 00:14:36.020 --> 00:14:41.720 And since then, we've had things like Lean come along, and we're big investors in Lean 00:14:41.720 --> 00:14:47.760 at AWS. And we've had LLMs come along and agents come along that can help us analyze 00:14:47.760 --> 00:14:49.860 programs, find proofs, and so on. 00:14:50.760 --> 00:14:56.100 And so now we can build a more powerful language with the same kind of level of closed 00:14:56.100 --> 00:15:00.940 -form analyzability. And the output I want from this, the output I want from this is 00:15:00.940 --> 00:15:07.500 the ability to write, in some cases, formal proofs that a program I have written 00:15:07.500 --> 00:15:13.240 in this language has certain properties. I'm going to write a formal proof that this 00:15:13.240 --> 00:15:19.860 million lines of policy code will never allow me to spend over $1 ,000 on my 00:15:19.860 --> 00:15:25.640 credit card. It's a hard thing to do for languages in general, but if you design a language 00:15:25.640 --> 00:15:31.180 for analyzability, it's easier. The other property that matters to us here is composability, 00:15:31.340 --> 00:15:35.520 and that is the ability to take two policies and stick them together in a well -defined 00:15:35.520 --> 00:15:40.320 way. This, again, is really hard to do with general -purpose programs, 00:15:43.820 --> 00:15:49.800 but with a carefully designed language, it becomes much easier, and it becomes much easier 00:15:49.800 --> 00:15:53.980 to do it efficiently in a way that isn't just run that program, run that program, run 00:15:53.980 --> 00:15:57.700 that program, run that program, et cetera. You can actually take them, you can put them 00:15:57.700 --> 00:16:02.320 in a mathematical bucket, shake the bucket, and come out with a smaller program with 00:16:02.320 --> 00:16:07.320 exactly the same meaning as all the programs you put in. And this one is important because 00:16:07.320 --> 00:16:12.200 of the way that the language like this gets used. You, as an agent user, might have some 00:16:12.200 --> 00:16:16.920 policy in your head. Your CISOs office might have some organization -wide policy. 00:16:19.460 --> 00:16:24.220 Your compliance auditors might have a certain amount of policy in their heads, and so 00:16:24.220 --> 00:16:28.820 there might be 10 different people who are writing policy about what your agent can do, 00:16:28.820 --> 00:16:33.520 and you want to be able to put all of that policy together. You want to be able to compose 00:16:33.520 --> 00:16:38.420 it together, and you want to be able to analyze it and ask questions about its collective 00:16:38.420 --> 00:16:38.820 meaning. 00:16:54.160 --> 00:16:58.780 Well, yeah, I mean, if regulation comes along, this is a powerful tool for that, but 00:16:58.780 --> 00:17:04.580 it's also just powerful for other practical things, like, hey, I don't want Claude Claude 00:17:04.580 --> 00:17:08.760 to delete my hard drive. I want to give an agent my credit card, but only allow it to 00:17:08.760 --> 00:17:14.400 make small purchases, you know, that kind of thing. Much more prosaic stuff than grand 00:17:14.400 --> 00:17:15.820 political machinations. 00:17:19.500 --> 00:17:24.220 We have a current open source implementation. We actually released a new version of this 00:17:24.220 --> 00:17:29.720 today with a whole bunch of new capabilities. This is on GitHub. Again, Apache 2. This 00:17:29.720 --> 00:17:34.380 is optimized for local with no cloud dependencies. It's not AWS -dependent in any way. 00:17:35.560 --> 00:17:39.300 The state only lives on one device, which is great. It's local. It doesn't have to reach 00:17:39.300 --> 00:17:44.040 out to the Internet. It's also bad because it means that all those temporal properties, 00:17:44.140 --> 00:17:49.480 if I'm running this on my laptop, apply separately to the agents on my laptop, the agents 00:17:49.480 --> 00:17:53.520 on my phone, the agents on my desktop, and the agents in the cloud, because their state 00:17:53.520 --> 00:17:58.700 is split. And so this one is a little bit of a double -edged sword, but it is nice for 00:17:58.700 --> 00:17:59.760 development for sure. 00:18:01.180 --> 00:18:04.920 And the open source implementation, I'd say, doesn't scale super well over lots of events. 00:18:06.040 --> 00:18:09.760 And part of that is just because you have limited local storage and limited compute and 00:18:09.760 --> 00:18:10.280 so on. 00:18:12.320 --> 00:18:16.860 And then we have a cloud implementation, and currently the cloud implementation is in 00:18:16.860 --> 00:18:21.880 Agent Core policy, and so this is the gateway component in our Agent Core platform for 00:18:21.880 --> 00:18:23.520 running agents at AWS. 00:18:25.080 --> 00:18:29.780 And we are, I'd say, building more of these, and you're going to see Dogwood in more 00:18:29.780 --> 00:18:33.140 places in AWS, and I'm sure you're going to see Dogwood from other providers. 00:18:34.440 --> 00:18:39.440 But the Agent Core policy is the current cloud -side implementation of Dogwood in AWS. 00:18:39.440 --> 00:18:45.420 It is multi -tenant, hosted, serverless, nothing to manage. You don't have to worry about 00:18:45.420 --> 00:18:50.100 any of the infrastructure. It's just a kind of magic API that you put between your agents 00:18:50.100 --> 00:18:50.900 and their tools. 00:18:52.860 --> 00:18:58.570 Temporal policies apply across agent sessions, across time, across multiple machines, 00:18:59.220 --> 00:19:03.200 across multiple regions, all of these good things that you'll want to do if you are building 00:19:03.200 --> 00:19:08.980 production agents that need to have these promises beyond a single device. Temporal policy 00:19:08.980 --> 00:19:13.920 state is durable and highly available, which again, if you want to make these as high 00:19:13.920 --> 00:19:14.960 -quality decisions, 00:19:16.180 --> 00:19:20.520 you want those properties just like you want those properties for any kind of state you 00:19:20.520 --> 00:19:25.460 keep in your system. No state is lost if an agent dies. I'll talk about where it's stored 00:19:25.460 --> 00:19:30.600 in a second, and it scales across tenants and events per tenant, and so you can actually 00:19:30.600 --> 00:19:34.360 scale this out to very large numbers of users. 00:19:37.160 --> 00:19:41.600 Last time I was here at Seattle Systems, just over a year ago, I spoke about the design 00:19:41.600 --> 00:19:46.640 of Aurora D -SQL. This is our scalable SQL database. It was a very fun thing to talk 00:19:46.640 --> 00:19:53.180 about, and this time I got to use D -SQL as a customer to build with the team, 00:19:53.260 --> 00:19:59.720 the scalable backend of Dogwood in the cloud. The cool way this works, and this was a 00:19:59.720 --> 00:20:04.640 core observation that John Tristan made, is the semantics of Dogwood and the semantics 00:20:04.640 --> 00:20:11.600 of SQL are actually pretty compatible. It's a fairly simple compiler that compiles Dogwood 00:20:11.600 --> 00:20:18.340 to SQL. This seems like a little bit of a wild thing to do, but if you think about how 00:20:18.340 --> 00:20:24.140 good SQL is at saying, before this key in a table, is this thing true? How many keys 00:20:24.140 --> 00:20:29.500 are in this range? These are the kinds of things that SQL databases do at scale, reliably, 00:20:29.840 --> 00:20:35.500 durably, isolated all day long, and so compiling Dogwood to SQL lets us take advantage 00:20:35.500 --> 00:20:39.540 of all of that great systems and database work that has been going on for decades and 00:20:39.540 --> 00:20:40.020 decades. 00:20:41.320 --> 00:20:45.500 You get durability, scalability, and high availability kind of for free by running on 00:20:45.500 --> 00:20:50.140 those backends rather than building one for yourself. You get strong consistency. It's 00:20:50.140 --> 00:20:54.560 not quite for free. Strong consistency is never quite for free, but you get it for cheap, 00:20:54.700 --> 00:21:00.760 which is also nice, and strong consistency is super important when you're a policy language 00:21:00.760 --> 00:21:05.760 because an eventually consistent policy language isn't pretty useless. 00:21:08.560 --> 00:21:13.660 Dsql lets us scale to lots of requests, lots of data, et cetera, without overhead, and 00:21:13.660 --> 00:21:14.420 that's nice. 00:21:15.520 --> 00:21:20.980 I will say that this kind of SQL is actually significantly faster to run on something 00:21:20.980 --> 00:21:25.720 like Aurora Postgres where all the data, if all the working set fits in memory, it's 00:21:25.720 --> 00:21:30.400 super fast there. So it's a little bit slower in Dsql, but it does give us a really nice 00:21:30.400 --> 00:21:35.440 kind of scalability story, especially to data volume, because some of this data can get 00:21:35.440 --> 00:21:36.100 pretty big. 00:21:37.300 --> 00:21:41.960 And, you know, it's actually not surprising, but quite cool how well the temporal policies 00:21:41.960 --> 00:21:48.440 map to concepts in SQL and how simple the compiler is. If we have some time, I'll tell 00:21:48.440 --> 00:21:52.420 a cool story about that compiler and how the team optimized it, 00:21:53.440 --> 00:21:58.200 but let me talk about the scalability limits. And fundamentally, the scalability limits 00:21:58.200 --> 00:22:04.820 of a language like this are limited by concurrency control. And if you're a database 00:22:04.820 --> 00:22:08.140 person, hopefully you know what I'm talking about. If you're not, you might have this 00:22:08.140 --> 00:22:13.320 question, what the hell is concurrency control? And concurrency control is the simple 00:22:13.320 --> 00:22:17.520 idea that if I have multiple things trying to access a piece of data at the same time, 00:22:17.800 --> 00:22:23.300 I want to keep the properties of that data whole while allowing concurrent access. And 00:22:23.300 --> 00:22:29.500 so I want to control concurrent access in a sane, well -structured way. And so you can 00:22:29.500 --> 00:22:34.520 imagine that if you have a policy that is saying, you know, allow this thing, but only 00:22:34.520 --> 00:22:39.740 if that response is true five times an hour, you can't just let all of the different 00:22:39.740 --> 00:22:44.140 calls to that tool stamp on each other because you're going to get incorrect results. 00:22:45.380 --> 00:22:52.360 Decisions need to be atomic, and they need to be isolated when there are multiple concurrent 00:22:52.360 --> 00:22:55.200 decisions going on about a particular policy. 00:22:57.000 --> 00:23:01.080 And so by atomic, these are the standard asset properties. What do we mean about atomic? 00:23:01.260 --> 00:23:05.500 Well, what we mean about atomic is they either happen or they don't. And what we mean 00:23:05.500 --> 00:23:12.260 about isolated is if I am running multiple concurrent ones, I can have an ordering of 00:23:12.260 --> 00:23:16.700 those things that just pretends not to be concurrent and is still well -formed. 00:23:18.520 --> 00:23:22.560 And that is because multiple concurrent agents could be returning to the same policy, 00:23:22.660 --> 00:23:26.540 and sometimes lots and lots and lots and lots of agents could be referring to the same 00:23:26.540 --> 00:23:28.760 policy. And so having these semantics, 00:23:29.720 --> 00:23:34.380 again, stolen from the world of databases as, you know, good systems people, we like 00:23:34.380 --> 00:23:37.340 to borrow ideas from the past quite heavily. 00:23:39.260 --> 00:23:40.880 Okay, so let's look at an example. 00:23:43.690 --> 00:23:49.050 Here I'm going to say, sell once with approval. And so this is my stock sale example, 00:23:49.430 --> 00:23:55.150 but even more complicated. And here I'm going to say I need to match up approvals to 00:23:55.150 --> 00:24:00.250 sales exactly one -to -one. And so I can only sell once per approval, 00:24:04.370 --> 00:24:09.230 and I have to sell exactly the same amount of shares that were approved. And so I've 00:24:09.230 --> 00:24:14.970 redacted some bits of this because this is not the most succinct programming language 00:24:14.970 --> 00:24:21.290 in the world, but it's probably about double this long, fully expanded. Again, one of 00:24:21.290 --> 00:24:24.090 the limits of TUI slides as a format. 00:24:25.430 --> 00:24:28.130 But the important thing here is that I am saying 00:24:29.350 --> 00:24:33.890 matching up one -to -one these approvals and sales, one -to -one approvals and sales, 00:24:33.910 --> 00:24:37.870 one -to -one approvals and sales. And so you can see why this is a concurrency problem, 00:24:37.870 --> 00:24:43.330 because if I have an approval and I let two sales go through because they arrived concurrently 00:24:43.330 --> 00:24:49.350 or tried to happen concurrently, well, then I've broken my policy rules just in the back 00:24:49.350 --> 00:24:54.030 end, right? I've broken the semantics of the policy language and what I promised the 00:24:54.030 --> 00:24:55.570 agent was not allowed to do. 00:24:56.610 --> 00:25:01.270 So now I can get into database isolation, and I can say, well, what if I ran this at 00:25:01.270 --> 00:25:05.650 read committed? And here I'm using PostgreSQL's definition of read committed rather than 00:25:05.650 --> 00:25:05.890 NC's 00:25:08.130 --> 00:25:12.730 because PostgreSQL's definitions are much saner. Different topic for a different talk, 00:25:12.830 --> 00:25:17.630 I guess, but at read committed, read committed allows lost rights, and that means that 00:25:17.630 --> 00:25:22.470 two concurrent transactions could be writing the same row and they could both end up 00:25:22.470 --> 00:25:22.890 committing. 00:25:24.190 --> 00:25:30.790 This is not acceptable behavior, but it is widely used. And so what would happen is Agent 00:25:30.790 --> 00:25:36.110 A gets approval to sell. Agent A and Agent B start selling the shares in parallel, so 00:25:36.110 --> 00:25:38.730 we have an approval. We're trying to sell both shares. 00:25:40.050 --> 00:25:44.870 The reading, the state, which says there's an approval, nobody's written yet that there's 00:25:44.870 --> 00:25:50.390 a sale, says, okay, let's go ahead. Now they both try and commit, and at read committed, 00:25:50.470 --> 00:25:54.730 I'm okay with this because they're both going to write like, yep, yep, I've sold, and 00:25:54.730 --> 00:25:58.010 they will both go ahead and commit, and now I've sold those shares twice, 00:25:59.030 --> 00:26:03.470 and I don't know, maybe I'm going to go to jail or something. This is bad. I don't want 00:26:03.470 --> 00:26:10.070 this. So we're going to upgrade our world to snapshot isolation, the best isolation 00:26:10.070 --> 00:26:10.550 level. 00:26:12.730 --> 00:26:17.870 And so read committed allows lost rights. Snapshot isolation does not allow lost rights. 00:26:18.470 --> 00:26:24.290 And so we've got Agent A gets approval. Agent B and A now try and sell their shares in 00:26:24.290 --> 00:26:26.330 parallel, exactly the same as the last time. 00:26:27.410 --> 00:26:32.530 Both read Agent A's approval, and both say, yep, I should be allowed, but I need to commit 00:26:32.530 --> 00:26:37.770 before I'm allowed to give that response. Both try to commit. Let's say B wins the race. 00:26:37.770 --> 00:26:44.070 B gets committed, okay, and now it can go to its client and say, yep, go ahead and sell. 00:26:44.430 --> 00:26:50.890 A tries to commit, and under OCC, or either at commit time or before, A gets aborted 00:26:50.890 --> 00:26:53.250 and it says, no, you cannot commit this transaction. 00:26:54.150 --> 00:27:00.650 And A has no option but to retry from the beginning of time. When it retries from the 00:27:00.650 --> 00:27:04.430 beginning of time, either it gets a new approval, or there is no new approval and it 00:27:04.430 --> 00:27:11.230 gets denied, which is great because only one says okay, and I manage to 00:27:11.230 --> 00:27:12.010 meet my promises. 00:27:14.850 --> 00:27:20.490 So this is kind of fun, and the reason this works is that it turns out that this kind 00:27:20.490 --> 00:27:24.310 of semantic is actually serializable at the snapshot isolation level. I don't really 00:27:24.310 --> 00:27:25.870 have time to go into that. 00:27:27.210 --> 00:27:33.870 The same is true of TPCC, by the way. So each approval is appended to a per session logical 00:27:33.870 --> 00:27:38.750 log. And that per session log, this is kind of the concurrency key. And so when you're 00:27:38.750 --> 00:27:43.230 saying, for this agent, apply this policy with these temporal things, it is that key 00:27:43.230 --> 00:27:49.170 for this agent. And each one gets its own logical log that we just append to. This is 00:27:49.170 --> 00:27:51.970 the next event, this is the next event, this is the next event. 00:27:53.250 --> 00:27:57.670 And so all concurrent transactions on that log cause write -write conflicts at the tip 00:27:57.670 --> 00:28:03.510 of the log. This is fundamentally the kind of per session, per agent scalability level. 00:28:04.590 --> 00:28:07.610 And then, yeah, yay for logs. Append -only data structures, they're cool. 00:28:09.830 --> 00:28:15.010 So then one more topic I wanted to cover, and that is MFOTL. 00:28:16.790 --> 00:28:19.450 And you might be saying, what is this? 00:28:20.470 --> 00:28:25.490 And let me explain. But I'm going to start off by explaining temporal logic. 00:28:27.450 --> 00:28:33.710 So you all know logic and or XOR and so on. I mean, I hope everyone in this room is familiar 00:28:33.710 --> 00:28:37.310 with those concepts. If you aren't, you should learn about them. They're pretty cool. 00:28:38.710 --> 00:28:45.450 And temporal logic adds some new operators to our logic to reason about time and order. 00:28:46.170 --> 00:28:51.690 We get operators like always and eventually and at the next step and until. 00:28:52.930 --> 00:28:55.610 And so with these operators, we can reason about. 00:28:56.610 --> 00:28:57.710 We did this thing. 00:28:58.990 --> 00:29:05.430 And after that thing, something is true forever. We did this thing. And at the next step, 00:29:05.710 --> 00:29:06.570 this thing is true. 00:29:07.710 --> 00:29:11.790 Then we also get these operators that can allow us to reason about the past, where we 00:29:11.790 --> 00:29:17.550 can say things like once and at the previous step and since and so on. These are the 00:29:17.550 --> 00:29:19.610 ones that we lean in heavily in Dogwood. 00:29:20.610 --> 00:29:26.830 And these operators, just like those logic operators, give us this really cool foundation 00:29:26.830 --> 00:29:32.090 for all kinds of programming logic. These temporal operators give us a firm mathematical 00:29:32.090 --> 00:29:35.770 foundation for expressing these time -based policies. 00:29:36.790 --> 00:29:40.530 But we can't really stop there. And we have to go up to another logic. And this is where 00:29:40.530 --> 00:29:45.830 I get, let's say this was very controversial with some of the scientists I work with. 00:29:46.090 --> 00:29:51.510 We are going to expand to first order logic. And first order logic gives us a couple 00:29:51.510 --> 00:29:53.710 of other newer, better operators. 00:29:54.670 --> 00:30:01.850 And the interesting ones here are for all and there exists. And so I can say for all 00:30:01.850 --> 00:30:08.010 slides, there exists a typo D such there is a typo in the slides. 00:30:10.470 --> 00:30:16.030 And this, again, is a very powerful set of tools. This is a hard set of tools to reason 00:30:16.030 --> 00:30:21.370 about. And so the reason this was controversial with our science teams was when you talk 00:30:21.370 --> 00:30:26.590 about analyzability, as soon as you start to add these kind of quantifiers to logic, 00:30:27.150 --> 00:30:29.650 the analyzability becomes much, much more difficult. 00:30:31.650 --> 00:30:36.870 And then we can have metric first order temporal logic where we add temporal logic and 00:30:36.870 --> 00:30:41.610 first order logic and this metric idea. And the metric idea is that we can say things 00:30:41.610 --> 00:30:48.990 like in the last hour or since 1 p .m., which you can't say in, let's 00:30:48.990 --> 00:30:54.110 say, less complete or less powerful logics. But these are very useful things to be able 00:30:54.110 --> 00:30:56.730 to use a policy language. 00:30:57.650 --> 00:31:03.530 And so putting these pieces together, we end up with a firm mathematical foundation in 00:31:03.530 --> 00:31:09.110 this well -defined logic that people have been studying for in parts hundreds of years 00:31:09.830 --> 00:31:14.650 to be able to reason about exactly what these policies mean when we look at them. 00:31:17.330 --> 00:31:23.950 And so temporal logic gives us a firm mathematical foundation. It gives us a 00:31:23.950 --> 00:31:30.130 very well -defined understanding of what policies mean and the ability to take those 00:31:30.130 --> 00:31:36.330 policies and turn them into formal mathematics in a way that we can feed to an SMT solver 00:31:36.330 --> 00:31:41.870 or we can feed to Lean or we can feed to a proof assistant or something to help us reason 00:31:41.870 --> 00:31:48.170 about these programs. Or if an auditor or compliance officer comes along, we can say, 00:31:48.470 --> 00:31:52.530 here is a ream of mathematics that proved that we did exactly the thing that we promised 00:31:52.530 --> 00:31:58.830 to do, which is actually very useful occasionally. And I hope you never run into the 00:31:58.830 --> 00:32:00.810 cases where that kind of thing is very useful. 00:32:03.730 --> 00:32:08.390 And metric temporal logic matches how our customers think about time. Because it turns 00:32:08.390 --> 00:32:12.690 out the ability to think about things like since yesterday and in the last hour is very, 00:32:13.090 --> 00:32:16.750 very common among humans. It really pisses mathematicians off. 00:32:17.670 --> 00:32:19.830 But it is useful for customers. 00:32:21.650 --> 00:32:26.070 And fundamentally, a firm foundation helps us with analysis and composition, the ability 00:32:26.070 --> 00:32:28.090 to reason about programs and how they join together. 00:32:29.830 --> 00:32:35.430 Anyway, so you should try out Dogwood. We haven't actually shipped the Dogwood Playground 00:32:35.430 --> 00:32:38.230 yet. It's a little bit annoying. I was hoping to show it off. 00:32:39.690 --> 00:32:42.850 But you should try Dogwood. It's on GitHub. You can download it. You can use it. You 00:32:42.850 --> 00:32:46.190 can use that local runtime. You can build it into your own stuff. You can help us extend 00:32:46.190 --> 00:32:51.490 the language. You can tell us what you think. You can build analyzers. All kinds of fun 00:32:51.490 --> 00:32:51.990 things. 00:32:53.130 --> 00:32:57.770 With the open source version, you can try it in Agent Core Policy. In Agent Core Policy, 00:32:57.810 --> 00:33:01.490 we have a kind of natural language policy builder that makes it a lot easier to work 00:33:01.490 --> 00:33:05.350 with if you don't feel like writing these things yourself. Although I will say that if 00:33:05.350 --> 00:33:10.370 you give the Dogwood documentation to Claude Code or Claude, it's a pretty credible job 00:33:10.370 --> 00:33:16.190 of writing good Dogwood policies. Not perfect, but fairly creditable. So that is a good 00:33:16.190 --> 00:33:20.190 way to play around too. And so, yeah, please use Dogwood in your own stuff. Please tell 00:33:20.190 --> 00:33:25.990 us what you think. And, you know, we're very excited to see this kind of capability come 00:33:25.990 --> 00:33:32.490 to the whole ecosystem of agents 00:33:32.490 --> 00:33:39.070 and programs and policy and so on. And I just want to be able to use a service 00:33:39.070 --> 00:33:43.810 or know or trust every five milliseconds. And so that's my whole motivation for building 00:33:43.810 --> 00:33:44.370 this stuff. 00:33:45.490 --> 00:33:48.070 Thank you all so much. Any questions? 00:33:52.440 --> 00:33:52.780 Yeah. 00:33:57.160 --> 00:34:01.660 I'm assuming it's not the only mechanism of deployment of Agent Core Policy, correct? 00:34:01.820 --> 00:34:06.620 There's probably other manners that Agent Core Policy is deployed. I'm just unfamiliar 00:34:06.620 --> 00:34:11.980 with the subservice. Yes, Agent Core Policy is attached to Agent Core Gateway in the 00:34:11.980 --> 00:34:15.400 cloud. You sort of put your agents behind a VPC. 00:34:16.460 --> 00:34:20.080 You put the gateway between them and their tools. And then you apply Agent Core Policy 00:34:20.080 --> 00:34:24.120 there. You can write those policies in Dogwood. You can write those policies in Cedar. 00:34:24.460 --> 00:34:28.060 Or you can write those policies as custom Lambda functions. And so then you can write 00:34:28.060 --> 00:34:32.820 those policies as Python or TypeScript or Java or whatever takes your particular fancy. 00:34:33.380 --> 00:34:37.400 And then one clarifying question for your slides. The portion that was on read commits, 00:34:37.400 --> 00:34:39.380 I'm assuming that that was basically 00:34:40.280 --> 00:34:45.640 logging when a read occurs so that if it's done later, you basically cancel like that 00:34:45.640 --> 00:34:50.240 second system that was trying to replicate a task. Was that what the main component of 00:34:50.240 --> 00:34:55.300 that was? Or was I misunderstanding? I mean, so, you know, this is all backed by a database. 00:34:55.480 --> 00:34:58.420 Yeah, exactly. So those are these things turn into database transactions. 00:34:59.380 --> 00:35:04.680 A's write gets approval and commits. Then B, A and B both start a new transaction. They 00:35:04.680 --> 00:35:08.980 both try and do, they do a read. And so they read the latest snapshot of the database 00:35:08.980 --> 00:35:13.720 that has that approval in it because it's strongly consistent because that is the right 00:35:13.720 --> 00:35:14.560 thing to do. 00:35:15.680 --> 00:35:21.280 And then they both try so that their reads say it's OK because they read a snapshot of 00:35:21.280 --> 00:35:25.840 the database. There's been no write since. And they both go ahead and try and commit. 00:35:27.060 --> 00:35:31.600 And this is a write write conflict, which is exactly the thing that snapshot isolation 00:35:31.600 --> 00:35:37.860 says is not allowed to happen. And so only one of them gets to commit on that write write 00:35:37.860 --> 00:35:42.160 conflict. It'd be technically OK for the database to abort both of them too, but we don't 00:35:42.160 --> 00:35:45.580 tend to do that because it annoys people when throughput drops to zero. 00:35:46.480 --> 00:35:47.260 Thank you. 00:35:51.280 --> 00:35:56.420 Mark, you mentioned that one of the primary motivations for Dogwood was to allow agents 00:35:56.420 --> 00:36:00.540 to be creative, but have an appropriate sandbox around them. 00:36:02.440 --> 00:36:08.520 Does Dogwood have the ability to explain why a policy violation has occurred, like why 00:36:08.520 --> 00:36:13.920 reject, why invocation has been rejected? Yes, it does. But it's not as good as we would 00:36:13.920 --> 00:36:14.600 like yet. 00:36:15.500 --> 00:36:18.940 So this is one of the super interesting things about agents 00:36:20.560 --> 00:36:26.580 is how useful error messages are. And it's just this lesson that everyone's learning 00:36:26.580 --> 00:36:29.840 of if you give good error messages, agents can do much smarter things. 00:36:30.920 --> 00:36:34.980 You know, security folks have always wanted authorization languages not to give good 00:36:34.980 --> 00:36:39.640 error messages and just say no, because it stops you from probing the policy and reverse 00:36:39.640 --> 00:36:43.920 engineering it. And so there's a bit of a balance here. You'll see that the Dogwood runtime 00:36:43.920 --> 00:36:48.660 does give an explanation for why it said no. Those explanations aren't quite good enough 00:36:48.660 --> 00:36:52.700 yet. And so that's one of the areas that we're working on is making those explanations 00:36:52.700 --> 00:36:58.060 much more helpful so the models can look at them and say, well, this is why I was denied 00:36:59.580 --> 00:37:05.060 and hopefully make another plan to meet their goal that is within the both letter and 00:37:05.060 --> 00:37:06.020 spirit of the policy. 00:37:08.280 --> 00:37:14.940 Yeah. So actually I have two questions. The first one is when you design this 00:37:15.640 --> 00:37:22.080 language, have you put this together with solidity and UVM? I feel a lot of, when I look 00:37:22.080 --> 00:37:27.220 at your code, I feel something is kind of very similar stuff around that area because 00:37:27.220 --> 00:37:28.060 you know, 00:37:29.020 --> 00:37:34.280 there's no solidity, right? Yeah. It's been a while since I looked at the solidity ecosystem. 00:37:35.020 --> 00:37:39.540 I do see the parallels there. I think it's solidity in some sense is a language with 00:37:39.540 --> 00:37:46.160 fairly similar goals of analyzability and composability for the same reason. I 00:37:46.160 --> 00:37:50.740 haven't personally looked at the relationship between those in detail. Some of the folks 00:37:50.740 --> 00:37:55.780 on the team might have, but it is an interesting and certainly I see the parallels. Yeah. 00:37:55.880 --> 00:37:57.980 I feel maybe something there. I also want to dig in later. 00:37:59.340 --> 00:38:03.200 Check checks. It's certainly similar stuff we can, because there's a lot of assets already 00:38:03.200 --> 00:38:07.400 in that community, right? So we can borrow something here and we can, you know, with 00:38:07.400 --> 00:38:11.500 faster. Yeah. I mean, fundamentally solidity is like, oh, I want to say these things 00:38:11.500 --> 00:38:14.620 about the history of this log and this thing that I'm trying to put at the beginning 00:38:14.620 --> 00:38:19.000 of this log. And so they are very fundamentally similarly structured. Yeah. That's kind 00:38:19.000 --> 00:38:19.400 of my feeling. 00:38:20.980 --> 00:38:26.080 Something really familiar there. I was like on the digging details. Thank you. 00:38:31.000 --> 00:38:36.420 Yeah. How do you express my logic in Dogwood and I have to write like Python code? 00:38:43.480 --> 00:38:48.980 Yeah. So we do have this sort of Rust variant called Rye that you can write things in 00:38:48.980 --> 00:38:53.620 that is a little bit of an escape patch on Dogwood into imperative code. 00:38:54.900 --> 00:38:59.940 I think with a piece of Python, I think what I might want to do is analyze that piece 00:38:59.940 --> 00:39:04.640 of code, maybe try and extract a spec in something like Lean and compile that into Dogwood, 00:39:05.020 --> 00:39:06.480 convert that into Dogwood. 00:39:07.600 --> 00:39:11.820 Python and TypeScript are particularly difficult for this because they have particularly 00:39:11.820 --> 00:39:18.180 weird semantics. And so things like Rust are way easier to do that in than Python and 00:39:18.180 --> 00:39:18.820 TypeScript. 00:39:19.740 --> 00:39:21.420 But there's nothing there that's impossible. 00:39:22.840 --> 00:39:27.100 In general, I think certainly in the specifics, there are a lot of cases that you can't 00:39:27.100 --> 00:39:31.860 analyze things. But if you're writing a typical authorization type policy in Python, 00:39:31.860 --> 00:39:35.700 being able to extract the meaning of that and turn that into Dogwood is a very reasonable 00:39:35.700 --> 00:39:38.840 thing to want to exist. We just haven't built it yet. 00:39:42.070 --> 00:39:47.210 The implementation is in Rust, our reference implementation, but you could implement 00:39:47.210 --> 00:39:48.890 the language in whatever you wanted. 00:39:50.170 --> 00:39:52.070 You can implement it in Lean, for example. 00:40:00.560 --> 00:40:05.160 Is it a common thing to write tests against your Dogwood policy that do bad things to 00:40:05.160 --> 00:40:10.240 make sure that it can't do the bad things? That is an excellent idea. I do think it should 00:40:10.240 --> 00:40:13.500 be a common thing. I wouldn't say most people think about it that way. 00:40:15.440 --> 00:40:19.800 I've spent a lot of time working with TLA +, for example, and one of the things that 00:40:19.800 --> 00:40:24.400 I find super useful is writing tests that I know are going to fail and writing buggy 00:40:24.400 --> 00:40:28.580 versions of the program that should have the bugs found by the specification. 00:40:29.540 --> 00:40:33.900 And I think that would be good practice in something like this, is writing those kind 00:40:33.900 --> 00:40:39.980 of negative cases. And one set of tools that's really interesting is 00:40:41.820 --> 00:40:43.160 you could imagine 00:40:44.560 --> 00:40:49.500 property -guided fuzzers that could generate lots and lots and lots of those kinds of 00:40:49.500 --> 00:40:51.000 tests to test your programs. 00:40:51.940 --> 00:40:53.060 Test your Dogwood programs. 00:40:55.840 --> 00:40:58.880 But yeah, negative tests. They're good for authorization, for sure. 00:40:59.940 --> 00:41:02.620 I wouldn't say that's common, but I would say it's a good idea. 00:41:07.530 --> 00:41:13.050 You'll need to tell me when I'm done, but I will keep going until you give me the crook. 00:41:13.510 --> 00:41:14.090 Awesome. 00:41:18.340 --> 00:41:19.380 That's a great idea. 00:41:20.700 --> 00:41:22.640 I will stop sharing my screen. 00:41:26.530 --> 00:41:32.970 In some of your examples, I think the commit one, for example, and then also the read 00:41:32.970 --> 00:41:35.790 confidential and then write an email. 00:41:37.270 --> 00:41:42.310 I was just thinking that time may not be the only thing that you care about. Maybe you 00:41:42.310 --> 00:41:48.330 want to say that there should have been no changes or something to the repo before you 00:41:48.330 --> 00:41:48.650 commit. 00:41:49.750 --> 00:41:54.510 Can you talk a bit about those kinds of limitations and what kinds of things you can 00:41:54.510 --> 00:41:58.770 express and whether you want to address them? That's a great question. 00:42:00.090 --> 00:42:04.650 You can express something like I showed in the cargo example where you used the previously 00:42:04.650 --> 00:42:09.850 key word to say literally the last thing must be that this email was approved by some 00:42:09.850 --> 00:42:16.190 approval workflow or some model or something and not allow edits between them. 00:42:16.790 --> 00:42:21.870 What you can't currently express today, except if you go through one of the escape hatches 00:42:21.870 --> 00:42:28.670 into a general purpose programming language, is call an LLM as a judge and check 00:42:28.670 --> 00:42:35.410 that it's happy with the tone of this email and only send it if its score is over 0 .7. 00:42:35.690 --> 00:42:40.710 That's one of the areas that we're extending it. This is super common in security. You'll 00:42:40.710 --> 00:42:41.450 have 00:42:42.430 --> 00:42:48.290 some kind of heuristic for is this traffic evil? With 5 % probability and you might want 00:42:48.290 --> 00:42:54.230 to allow that, with 75 % probability, no. You do want those to be able to add those deterministic 00:42:54.230 --> 00:42:57.550 steps, non -deterministic steps to deterministic policy. 00:42:58.630 --> 00:43:01.990 That's something that we haven't completely built into the language yet, but it's very 00:43:01.990 --> 00:43:02.730 much in the vision. 00:43:07.620 --> 00:43:13.560 Has this shown a success with agents that have a very wide range of capabilities? For 00:43:13.560 --> 00:43:18.920 example, I've had OpenClaw running on my machine and OpenClaw wants to be able to do 00:43:18.920 --> 00:43:22.740 anything that you could do. Run commands or 00:43:24.000 --> 00:43:27.900 run commands on your machine or to git or to basically do anything. 00:43:28.840 --> 00:43:33.540 I feel like expressing all the things that you want the agent not to do is very, very 00:43:33.540 --> 00:43:39.160 hard. You can express all the things that you want the agent not to do. That deny listing 00:43:39.160 --> 00:43:45.000 problem is a well -known one in security and is basically not great. You could express 00:43:45.000 --> 00:43:48.700 all the things you want the agent to do, but you're exactly right that if you're using 00:43:48.700 --> 00:43:52.800 something like OpenClaw, that set of things might be so big that you couldn't reasonably 00:43:52.800 --> 00:43:54.120 express all of them. 00:43:56.100 --> 00:44:02.000 Generally, I would say that those are exception cases. Even if I'm using something like 00:44:02.000 --> 00:44:07.680 Claude Code on my desktop, I don't want it to do such a broad range of things. I might 00:44:07.680 --> 00:44:12.080 want it to be able to do pretty much arbitrary stuff within a particular git repo, for 00:44:12.080 --> 00:44:18.200 example, and nothing beyond that. You can express those kinds of policies. But fundamentally, 00:44:18.380 --> 00:44:23.500 if you're going to put an agent in a deterministic box, you have to know what the shape 00:44:23.500 --> 00:44:28.000 of that box is. If the shape of that box is, well, just allow it to do everything, 00:44:33.340 --> 00:44:36.980 then the policy is not going to help you that much. If it's allow it to do everything 00:44:36.980 --> 00:44:42.500 except these things, that might be useful. But I will say that what we've seen and you 00:44:42.500 --> 00:44:44.160 might have seen this in a lot of the headlines, 00:44:45.460 --> 00:44:50.780 if you say to an agent, you're allowed to not do anything but this, it tends to find 00:44:50.780 --> 00:44:54.020 ways around the obstacle very, I would say, creatively. 00:44:55.080 --> 00:45:00.720 I do tend to mentally think about most people should be thinking about this as an allow 00:45:00.720 --> 00:45:06.140 listing problem of allow listing a set of allowed behaviors rather than a deny listing 00:45:06.140 --> 00:45:09.240 problem of trying to exhaustively list all of the bad things in the world. 00:45:15.580 --> 00:45:21.320 Yeah. So how do you debug a temporal policy denial in production? Can Dogwood tell you 00:45:21.320 --> 00:45:27.500 which aspect of the program causes denial? Yeah, it can. So it can tell you in a actually 00:45:27.500 --> 00:45:33.260 very reduced form exactly what was not allowed, which is really nice. It tells you that 00:45:33.260 --> 00:45:39.300 today in a, I would say, a way that is helpful if you are a temporal logic enthusiast 00:45:39.300 --> 00:45:44.060 and not particularly helpful if you aren't. And so that is one of the ways that I think 00:45:44.060 --> 00:45:50.320 the team is working on making that debugging experience a ton more useful. And the good 00:45:50.320 --> 00:45:55.740 news there is, as I alluded to earlier, is that that helps both humans and agents substantially. 00:45:55.760 --> 00:46:00.140 And so there's a huge amount of overlap in the needs of these two kind of customers for 00:46:00.140 --> 00:46:00.960 the policy language. 00:46:06.180 --> 00:46:10.080 Real quick, and then there's a couple of other people over there. OK, I feel like maybe 00:46:10.080 --> 00:46:14.080 a policy violation, that would be something that you'd want a human to take a look at 00:46:14.080 --> 00:46:17.400 rather than to have an agent try and figure out a way around it, because it seems like 00:46:17.400 --> 00:46:21.320 a policy violation here would be you'd want it to be something that's very, very bad. 00:46:22.540 --> 00:46:27.740 Yeah, I mean, maybe, you know, you might want to say, like I might want to say to my 00:46:27.740 --> 00:46:32.860 agent, you know, buy my daughter a birthday gift and it tries to buy her a car and, you 00:46:32.860 --> 00:46:36.300 know, it gets a no, you can't spend more than a thousand dollars. And that's useful input 00:46:36.300 --> 00:46:41.580 to the agent to sort of calibrate my expectations a little bit and say, OK, well, now 00:46:41.580 --> 00:46:44.920 I'm going to buy a gift that is maybe fifty bucks instead. 00:46:45.840 --> 00:46:48.760 And so in some cases, yes, you do want to give that feedback to the agent. 00:46:49.680 --> 00:46:53.700 In security cases, for example, you might not, and this is, you know, always been the 00:46:53.700 --> 00:46:59.760 philosophy with authorization folks is you don't want to allow an adversary to explore 00:46:59.760 --> 00:47:03.900 the shape of the box. You just want to say, no, you can't go this way with no further 00:47:03.900 --> 00:47:08.140 information. And so it is actually an interesting set of tradeoffs about what you tell 00:47:08.900 --> 00:47:13.500 the contained thing about why it wasn't allowed to do the thing it was doing. 00:47:17.380 --> 00:47:20.380 Where do you draw the line or where do you draw the boundary between 00:47:21.340 --> 00:47:27.120 dogwood determining what an agent is allowed to do in the system deciding which of several 00:47:27.120 --> 00:47:30.200 allowed actions it should actually take? 00:47:32.420 --> 00:47:34.740 Yeah, that's a fantastic question. So 00:47:38.500 --> 00:47:44.700 there is a you could write a workflow in dogwood that says when you get to this way, 00:47:44.740 --> 00:47:47.900 go left. When you go to this place, go right. You can do that in 00:47:48.800 --> 00:47:52.960 many, many different workflow languages that have existed for a long time. You almost 00:47:52.960 --> 00:47:58.100 definitely don't want to do those things because, you know, why would you burn LLM tokens 00:47:58.100 --> 00:47:59.640 driving a workflow? That would be silly. 00:48:00.540 --> 00:48:03.540 You can sort of build a let's say sort of shaped 00:48:04.540 --> 00:48:08.320 pipe around a workflow that sort of guides it in one direction or another. 00:48:10.860 --> 00:48:14.800 And it's certainly possible. I think it's something that we haven't really figured out 00:48:14.800 --> 00:48:21.020 what the right way to express that and think about those sort of things is. And part 00:48:21.020 --> 00:48:25.860 of it is because I think we've given a lot more thought to what, you know, formal people 00:48:25.860 --> 00:48:30.940 will call safety, which is nothing bad happens, rather than liveness, which is the something 00:48:30.940 --> 00:48:33.760 good eventually happens half of the problem. 00:48:34.960 --> 00:48:40.600 And so it would be really nice to be able to, you know, sort of guide workflows, guide 00:48:40.600 --> 00:48:45.340 agents along their paths, you know, with this kind of language. I'm not sure it's quite 00:48:45.340 --> 00:48:49.660 the right language for that. And I, you know, I don't think we've quite figured out what 00:48:49.660 --> 00:48:51.820 the right shape of that is. 00:48:53.780 --> 00:48:57.420 And so there are a lot of kind of precondition, post condition type things that people 00:48:57.420 --> 00:49:02.220 have tried, you know, to do that kind of guidance for agents. I would say none of them 00:49:02.220 --> 00:49:05.860 have worked out quite as nicely as we would like. And so I think it's an area of sort 00:49:05.860 --> 00:49:08.100 of innovation, of how do you really just 00:49:09.960 --> 00:49:14.160 guide an agent along without over constraining it to the point that it can't do all of 00:49:14.160 --> 00:49:16.240 the cool things that agents can do. 00:49:17.600 --> 00:49:21.720 A ton of innovation possible there. And we certainly haven't figured it out yet. 00:49:24.120 --> 00:49:24.560 Hi, 00:49:25.620 --> 00:49:31.240 great speech. So when you said this down compile into SQL, I would assume you're gonna 00:49:31.240 --> 00:49:36.260 write something like commentable expressions with something as something. So where there 00:49:36.260 --> 00:49:41.400 may be an edge case, I'm wondering if you change certain policies together, how do you 00:49:41.400 --> 00:49:46.360 evaluate or compile that these should be changed and these are still valid policies? 00:49:46.900 --> 00:49:53.140 Yeah, that's a really good question. And so part of that is you know, we you get some 00:49:53.140 --> 00:49:57.240 level of policy complexity and policy size, where you can't do that in the industry. 00:49:57.440 --> 00:50:00.080 We do that compiler does admit like tons of CTEs. 00:50:02.980 --> 00:50:09.020 But this is where the composability comes in, is that almost most policies are actually 00:50:09.020 --> 00:50:12.020 expressing a fairly simple set of 00:50:13.160 --> 00:50:17.880 fairly simple set of logic. They might just express it in a very long form way and a 00:50:17.880 --> 00:50:23.200 very redundant and duplicative way. And so you can do a kind of minimization step first, 00:50:23.200 --> 00:50:27.580 which helps you avoid these kinds of problems. And then you know, when you have policies 00:50:27.580 --> 00:50:32.340 with multiple clauses, the fact that the composition of those clauses is very well defined 00:50:32.340 --> 00:50:36.860 helps the compiler figure out how to write the sequel that composes those expressions 00:50:36.860 --> 00:50:38.200 together in the correct way. 00:50:39.660 --> 00:50:44.620 We have a I don't know, I don't think it's an open source repo yet, but we do have one 00:50:44.620 --> 00:50:50.220 of the things that we do is that we have a lean proof of some pieces of the compiler 00:50:50.220 --> 00:50:56.220 exactly to find edge cases like this. It doesn't cover quite as much as we would like. 00:50:59.060 --> 00:51:02.350 But the idea is fully proven to be correct 00:51:03.300 --> 00:51:09.340 and is actually the rest version of that compiler runs in production is derived from 00:51:09.340 --> 00:51:10.660 the lean implementation. 00:51:11.740 --> 00:51:13.960 We're not there yet, but that's the goal. 00:51:15.280 --> 00:51:21.160 Would it be something like here there plus protocols would it be basic unit testing? 00:51:22.720 --> 00:51:28.860 It's a proof in lean and so it is an actual formal proof. It uses a lot of the similar 00:51:28.860 --> 00:51:34.400 concepts to TLA plus or TLA proof system if you're familiar with that. 00:51:35.600 --> 00:51:37.980 We just tend to use lean because it's more powerful 00:51:39.280 --> 00:51:43.400 and TLA proof system is, I don't want to offend anyone, but a bit weird. 00:51:44.500 --> 00:51:48.000 And TLC, which is the model checker that most people use with TLA plus is great, but 00:51:48.000 --> 00:51:52.640 it is fundamentally unsound and so it doesn't really meet our needs. 00:51:54.400 --> 00:52:00.920 Last question. So I was curious about the local case. Does like Dogwood protect 00:52:00.920 --> 00:52:06.680 against Dogwood? Like the agents messing up with the policy evaluation? 00:52:07.640 --> 00:52:14.080 Yup. So Dogwood does not do isolation and so you need a way to isolate your agent and 00:52:14.080 --> 00:52:18.000 force, you need a way to isolate and you need a way to intercept and so you need a way 00:52:18.000 --> 00:52:23.560 to put the agent in a box and you need a way to apply Dogwood to everything it's trying 00:52:23.560 --> 00:52:27.680 to do. If you don't do that and it can just do arbitrary stuff, well then it can just, 00:52:27.840 --> 00:52:31.400 you know, it's like having a fence with a gate and having no fence and it can just walk 00:52:31.400 --> 00:52:35.960 around it. And so Dogwood isn't a complete solution to agent sandboxing because you still 00:52:35.960 --> 00:52:40.460 need that isolate piece and you still need the intercept piece. In the cloud that's done 00:52:40.460 --> 00:52:43.460 with agent core runtime and an agent core gateway, 00:52:44.740 --> 00:52:50.280 local, it's not a complete solution to that yet and as I'm sure you know there is a ton 00:52:50.280 --> 00:52:56.540 of innovation going on in the local agent sandboxing space right now. Okay, and were 00:52:56.540 --> 00:53:00.420 there any unexpected challenges developing something like this and like you mentioned 00:53:00.420 --> 00:53:05.600 also compiling forcing all of this into SQL? Yeah, I mean the SQL compiler stuff was 00:53:05.600 --> 00:53:09.720 interesting, it was super fun, actually the team wrote this really cool super optimizer 00:53:09.720 --> 00:53:14.420 loop that used the lean proof to find more and more and more efficient compilers which 00:53:14.420 --> 00:53:17.260 is just a super fun technique I'm really excited about. 00:53:18.400 --> 00:53:22.420 You know, one of the challenges here is when we talk about analyzability that is a spectrum, 00:53:22.760 --> 00:53:26.660 I think, you know, Cedar is like really at one end of that and it's very carefully designed 00:53:26.660 --> 00:53:31.380 to be analyzable always in, you know, under a set of assumptions. 00:53:32.560 --> 00:53:36.720 Dogwood is not always analyzable and so, you know, the analyzer is always forced into 00:53:36.720 --> 00:53:42.320 sometimes saying I don't know as an answer to analysis questions and how far we could 00:53:42.320 --> 00:53:48.100 push that I would say was you know, figuring that out right was tough and you know, a 00:53:48.100 --> 00:53:50.480 ton of different people had different opinions. 00:53:51.820 --> 00:53:56.340 You know, time will tell whether we found the right balance on that spectrum but I am 00:53:56.340 --> 00:54:01.140 very encouraged by how tools like Lean and how LLMs have just brought a huge amount of 00:54:01.140 --> 00:54:06.400 power to the proof ecosystem over the last couple of years and certainly even more over 00:54:06.400 --> 00:54:12.080 the last six months and so I think our bet on first order logic, for example, it's harder 00:54:12.080 --> 00:54:16.820 to analyze I think is going to turn out to be the right one but time will tell. 00:54:17.820 --> 00:54:18.960 Cool. Thank you all so much.