1 00:00:00,000 --> 00:00:00,000 again for the second time at Seattle Systems. 2 00:00:00,440 --> 00:00:04,520 I will say thank you to the Momento folks, 3 00:00:05,500 --> 00:00:07,520 the antithesis folks for sponsoring the food. 4 00:00:08,440 --> 00:00:11,840 You should not trust those antithesis folks, they will break your software and destroy 5 00:00:11,840 --> 00:00:15,420 your ego, so just be careful around them. 6 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 7 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, 8 00:00:28,300 --> 00:00:31,560 we'll talk about databases and hopefully some other fun things. 9 00:00:32,780 --> 00:00:34,400 So let's start with what is Dogwood? 10 00:00:35,400 --> 00:00:39,520 Dogwood is a governance language, you can think of it as a programming language, which 11 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 12 00:00:44,480 --> 00:00:50,680 agents, for describing what programs can do, agents are kind of general programs, and 13 00:00:50,680 --> 00:00:57,500 so we designed Dogwood to be for agents, but you can actually describe behaviors of any 14 00:00:57,500 --> 00:00:59,400 program in Dogwood. 15 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, 16 00:01:06,160 --> 00:01:13,080 teams at Amazon built Cedar, which is now open source, and Cedar is a policy language, 17 00:01:13,080 --> 00:01:15,200 it is a pro -authorization language, 18 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 19 00:01:20,840 --> 00:01:25,060 with Cedar or you're familiar with those kinds of authorization languages, and so it 20 00:01:25,060 --> 00:01:30,600 has these keywords like permit and forbid, when, unless, etc. 21 00:01:31,500 --> 00:01:35,380 What Dogwood adds is the idea of time and order, 22 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 23 00:01:40,740 --> 00:01:46,320 this now, you can talk about things like since, once, before, after, and so on. 24 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, 25 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, 26 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 27 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 28 00:02:08,920 --> 00:02:15,380 a new runtime for Dogwood, which is really easy to add into your own products, 29 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 30 00:02:20,280 --> 00:02:24,580 not the kind of programming language you would necessarily want to write a ton of yourself, 31 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 32 00:02:29,720 --> 00:02:32,560 to be written by tools rather than people. 33 00:02:34,770 --> 00:02:39,550 So why did we build Dogwood? Well, we built Dogwood because we were thinking about an 34 00:02:39,550 --> 00:02:45,190 agent policy problem, of how do you describe, given an agent or an agentic application, 35 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 36 00:02:50,950 --> 00:02:55,970 very open -ended agents, to a customer service chatbot, to whatever kind of agent you're 37 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 38 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. 39 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 40 00:03:13,010 --> 00:03:19,710 doing LLM as a judge type techniques, they're having models watch agents, having heuristics 41 00:03:19,710 --> 00:03:24,950 watch agents, all of those things are good, valuable techniques, but we wanted to build 42 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, 43 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 44 00:03:36,070 --> 00:03:39,550 when you express something in Dogwood, it has a particular behavior. 45 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, 46 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 47 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, 48 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 49 00:03:59,970 --> 00:04:04,430 things. Those aren't things you can really do deterministically because they are in this 50 00:04:04,430 --> 00:04:11,110 realm of natural language and a realm of very fuzzy social expectations, 51 00:04:11,270 --> 00:04:15,230 right? Like it might even be that in one country saying a particular word is offensive 52 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 53 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 54 00:04:25,130 --> 00:04:31,050 tools could be accessing the file system. It could be calling Git, it could be calling 55 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 56 00:04:36,870 --> 00:04:41,410 an email, right? Like all of these things that agents do in their environment, that makes 57 00:04:41,410 --> 00:04:46,690 them interesting and useful. And so this is the core tension we have with agents, is 58 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 59 00:04:52,010 --> 00:04:58,530 problems persistently, some might even say creatively, but we also want to be able 60 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 61 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 62 00:05:08,570 --> 00:05:14,290 a particular path, well, then you've just invented a very expensive, very slow workflow. 63 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 64 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. 65 00:05:31,800 --> 00:05:32,640 For example. 66 00:05:33,820 --> 00:05:34,980 So credit to some folks. 67 00:05:35,920 --> 00:05:41,640 John Tristan is really the kind of core inventor of Dogwood, you know, fantastic scientist. 68 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 69 00:05:48,840 --> 00:05:54,620 team of engineers and folks around Amazon and a growing open source community. 70 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 71 00:06:02,980 --> 00:06:03,380 that. 72 00:06:05,000 --> 00:06:07,320 So let's dive into some examples. 73 00:06:08,900 --> 00:06:15,260 And here we want to say I need pre -approval to sell Amazon stock. 74 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 75 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. 76 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, 77 00:06:34,800 --> 00:06:42,000 approved sale, before I can sell my shares. And so what this policy says is 78 00:06:42,000 --> 00:06:49,100 within formally, so before, within one hour, a approval response happened for 79 00:06:49,100 --> 00:06:55,600 an amount of stock, amount of shares, and the approval was true. And if all of 80 00:06:55,600 --> 00:07:01,900 those things are true, then I can call this sell shares API. 81 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 82 00:07:09,180 --> 00:07:14,600 have the ability to reason about time in this way. You could say, 83 00:07:15,520 --> 00:07:20,320 you know, you could write a non -time -based or non -ordering -based version of this 84 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 85 00:07:25,620 --> 00:07:29,520 idea of Dogwood, is being able to reason about time, reason about order. 86 00:07:31,600 --> 00:07:34,000 And I'll show you some future examples, 87 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 88 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 89 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 90 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 91 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 92 00:07:59,360 --> 00:08:04,540 to be allowed, right? Because within one hour, I had the approval. And then two hours 93 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 94 00:08:09,720 --> 00:08:12,920 an approval within one hour. So far so good. 95 00:08:15,800 --> 00:08:21,800 Here's another one. Very, very common request when I talk to customers about things they 96 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 97 00:08:26,060 --> 00:08:30,620 of them is access commercial data or confidential data, and the other is send email. 98 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 99 00:08:36,600 --> 00:08:41,300 data. I'm absolutely not okay with an agent sending email after reading the confidential 100 00:08:41,300 --> 00:08:45,740 data because there is a probability that that confidential data will make its way into 101 00:08:45,740 --> 00:08:47,580 the email that it sent. 102 00:08:48,800 --> 00:08:50,000 And so here again, 103 00:08:50,980 --> 00:08:57,520 I can write this policy that says formally within 24 hours, if there's 104 00:08:57,520 --> 00:09:04,340 a read confidential, then we are going to forbid this sending of 105 00:09:04,340 --> 00:09:04,680 email. 106 00:09:06,120 --> 00:09:12,760 Similarly, I want to make sure that my agent is running the tests 107 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 108 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 109 00:09:27,280 --> 00:09:34,020 last thing I did was a successful cargo test. So if I do a cargo test, 110 00:09:34,780 --> 00:09:40,920 that exits with zero, get commit. That's great. Cargo test, that fails, and then try 111 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 112 00:09:45,600 --> 00:09:52,140 files, denied, or if I wait too long, denied. So this is 113 00:09:52,140 --> 00:09:56,740 really cool, right? Like I can write these policies that express these sort of common 114 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 115 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 116 00:10:07,300 --> 00:10:10,900 thinking about these concepts of before and after and so on. 117 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 118 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. 119 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 120 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 121 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. 122 00:10:39,320 --> 00:10:41,000 Let's keep it respectful. 123 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 124 00:10:47,440 --> 00:10:49,000 track of number, and so on. 125 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 126 00:10:57,590 --> 00:11:06,170 here is that you can set policy on requests or responses to 127 00:11:06,170 --> 00:11:06,730 two calls. 128 00:11:07,630 --> 00:11:12,430 And if you set policy on requests incorrectly, then policies might mean something other 129 00:11:12,430 --> 00:11:15,230 than what you are expecting. 130 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, 131 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 132 00:11:28,170 --> 00:11:32,790 going to want tools to help us reason about what these policies mean. 133 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 134 00:11:37,870 --> 00:11:39,930 the same logic in Python, 135 00:11:40,970 --> 00:11:45,470 for example, you would have exactly the same subtlety, but it would be less obvious. 136 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 137 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 138 00:11:56,310 --> 00:11:57,290 reason about. 139 00:11:58,330 --> 00:12:00,510 I'll get to more of that in a second. 140 00:12:02,070 --> 00:12:08,510 Another example, no sudden spikes, and some within an hour, and make sure that the rate 141 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 142 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 143 00:12:19,230 --> 00:12:24,290 like a relatively limited and ultimately is a relatively limited policy language. 144 00:12:27,220 --> 00:12:30,940 So then, yeah, why not a general purpose language? Why not Python, why not Rust, why 145 00:12:30,940 --> 00:12:36,020 not TypeScript, whatever? And there are a couple of reasons for that. One of them is 146 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 147 00:12:41,980 --> 00:12:48,180 about policy. I don't also be thinking about I .O. or logging or imports 148 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 149 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 150 00:12:57,980 --> 00:12:59,060 particular topic. 151 00:13:00,260 --> 00:13:04,160 And the analysis tools are only having to worry about this particular topic. 152 00:13:05,520 --> 00:13:08,320 I want this language to be analyzable, 153 00:13:09,460 --> 00:13:14,720 which I'm going to certainly roughly say easy to understand what programs mean. And I 154 00:13:14,720 --> 00:13:17,520 don't really mean that for humans, but I mean that for tools. 155 00:13:18,480 --> 00:13:24,860 And I'm very interested in applying formal reasoning, applying automated reasoning, 156 00:13:25,000 --> 00:13:30,920 applying formal methods to programs. In general, that is a very hard thing to do. 157 00:13:31,600 --> 00:13:36,140 It is something that is actually pretty tractable for large code bases, but it's very 158 00:13:36,140 --> 00:13:42,700 easy to write a program that cannot be analyzed formally 159 00:13:42,700 --> 00:13:47,860 where you can't say meaningful things about its properties. For example, you might have 160 00:13:47,860 --> 00:13:53,540 run into the collapse conjecture, which you could write as a four -line Python program 161 00:13:53,540 --> 00:13:59,440 that is an open mathematical question about whether it terminates or not for arbitrary 162 00:13:59,440 --> 00:14:00,280 size integers. 163 00:14:02,200 --> 00:14:08,660 And so I want an analyzable program. Cedar was very carefully designed to be analyzable, 164 00:14:08,660 --> 00:14:15,180 to be analyzable in a subset of SMT, to be analyzable with a particular 165 00:14:15,180 --> 00:14:22,040 set of tools. It was really targeted at that, and that is hugely valuable. But 166 00:14:22,040 --> 00:14:27,760 it also means that Cedar has some things you can't express, especially these sort of 167 00:14:27,760 --> 00:14:28,960 ordering properties. 168 00:14:30,260 --> 00:14:35,460 And so when Cedar was designed, we had a certain set of tools for analyzing programs. 169 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 170 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 171 00:14:47,760 --> 00:14:49,860 programs, find proofs, and so on. 172 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 173 00:14:56,100 --> 00:15:00,940 -form analyzability. And the output I want from this, the output I want from this is 174 00:15:00,940 --> 00:15:07,500 the ability to write, in some cases, formal proofs that a program I have written 175 00:15:07,500 --> 00:15:13,240 in this language has certain properties. I'm going to write a formal proof that this 176 00:15:13,240 --> 00:15:19,860 million lines of policy code will never allow me to spend over $1 ,000 on my 177 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 178 00:15:25,640 --> 00:15:31,180 for analyzability, it's easier. The other property that matters to us here is composability, 179 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 180 00:15:35,520 --> 00:15:40,320 way. This, again, is really hard to do with general -purpose programs, 181 00:15:43,820 --> 00:15:49,800 but with a carefully designed language, it becomes much easier, and it becomes much easier 182 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 183 00:15:53,980 --> 00:15:57,700 that program, run that program, et cetera. You can actually take them, you can put them 184 00:15:57,700 --> 00:16:02,320 in a mathematical bucket, shake the bucket, and come out with a smaller program with 185 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 186 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 187 00:16:12,200 --> 00:16:16,920 policy in your head. Your CISOs office might have some organization -wide policy. 188 00:16:19,460 --> 00:16:24,220 Your compliance auditors might have a certain amount of policy in their heads, and so 189 00:16:24,220 --> 00:16:28,820 there might be 10 different people who are writing policy about what your agent can do, 190 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 191 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 192 00:16:38,420 --> 00:16:38,820 meaning. 193 00:16:54,160 --> 00:16:58,780 Well, yeah, I mean, if regulation comes along, this is a powerful tool for that, but 194 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 195 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 196 00:17:08,760 --> 00:17:14,400 make small purchases, you know, that kind of thing. Much more prosaic stuff than grand 197 00:17:14,400 --> 00:17:15,820 political machinations. 198 00:17:19,500 --> 00:17:24,220 We have a current open source implementation. We actually released a new version of this 199 00:17:24,220 --> 00:17:29,720 today with a whole bunch of new capabilities. This is on GitHub. Again, Apache 2. This 200 00:17:29,720 --> 00:17:34,380 is optimized for local with no cloud dependencies. It's not AWS -dependent in any way. 201 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 202 00:17:39,300 --> 00:17:44,040 out to the Internet. It's also bad because it means that all those temporal properties, 203 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 204 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 205 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 206 00:17:58,700 --> 00:17:59,760 development for sure. 207 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. 208 00:18:06,040 --> 00:18:09,760 And part of that is just because you have limited local storage and limited compute and 209 00:18:09,760 --> 00:18:10,280 so on. 210 00:18:12,320 --> 00:18:16,860 And then we have a cloud implementation, and currently the cloud implementation is in 211 00:18:16,860 --> 00:18:21,880 Agent Core policy, and so this is the gateway component in our Agent Core platform for 212 00:18:21,880 --> 00:18:23,520 running agents at AWS. 213 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 214 00:18:29,780 --> 00:18:33,140 places in AWS, and I'm sure you're going to see Dogwood from other providers. 215 00:18:34,440 --> 00:18:39,440 But the Agent Core policy is the current cloud -side implementation of Dogwood in AWS. 216 00:18:39,440 --> 00:18:45,420 It is multi -tenant, hosted, serverless, nothing to manage. You don't have to worry about 217 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 218 00:18:50,100 --> 00:18:50,900 and their tools. 219 00:18:52,860 --> 00:18:58,570 Temporal policies apply across agent sessions, across time, across multiple machines, 220 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 221 00:19:03,200 --> 00:19:08,980 production agents that need to have these promises beyond a single device. Temporal policy 222 00:19:08,980 --> 00:19:13,920 state is durable and highly available, which again, if you want to make these as high 223 00:19:13,920 --> 00:19:14,960 -quality decisions, 224 00:19:16,180 --> 00:19:20,520 you want those properties just like you want those properties for any kind of state you 225 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 226 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 227 00:19:30,600 --> 00:19:34,360 scale this out to very large numbers of users. 228 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 229 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 230 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, 231 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 232 00:19:59,720 --> 00:20:04,640 core observation that John Tristan made, is the semantics of Dogwood and the semantics 233 00:20:04,640 --> 00:20:11,600 of SQL are actually pretty compatible. It's a fairly simple compiler that compiles Dogwood 234 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 235 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 236 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, 237 00:20:29,840 --> 00:20:35,500 durably, isolated all day long, and so compiling Dogwood to SQL lets us take advantage 238 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 239 00:20:39,540 --> 00:20:40,020 decades. 240 00:20:41,320 --> 00:20:45,500 You get durability, scalability, and high availability kind of for free by running on 241 00:20:45,500 --> 00:20:50,140 those backends rather than building one for yourself. You get strong consistency. It's 242 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, 243 00:20:54,700 --> 00:21:00,760 which is also nice, and strong consistency is super important when you're a policy language 244 00:21:00,760 --> 00:21:05,760 because an eventually consistent policy language isn't pretty useless. 245 00:21:08,560 --> 00:21:13,660 Dsql lets us scale to lots of requests, lots of data, et cetera, without overhead, and 246 00:21:13,660 --> 00:21:14,420 that's nice. 247 00:21:15,520 --> 00:21:20,980 I will say that this kind of SQL is actually significantly faster to run on something 248 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 249 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 250 00:21:30,400 --> 00:21:35,440 kind of scalability story, especially to data volume, because some of this data can get 251 00:21:35,440 --> 00:21:36,100 pretty big. 252 00:21:37,300 --> 00:21:41,960 And, you know, it's actually not surprising, but quite cool how well the temporal policies 253 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 254 00:21:48,440 --> 00:21:52,420 a cool story about that compiler and how the team optimized it, 255 00:21:53,440 --> 00:21:58,200 but let me talk about the scalability limits. And fundamentally, the scalability limits 256 00:21:58,200 --> 00:22:04,820 of a language like this are limited by concurrency control. And if you're a database 257 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 258 00:22:08,140 --> 00:22:13,320 question, what the hell is concurrency control? And concurrency control is the simple 259 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, 260 00:22:17,800 --> 00:22:23,300 I want to keep the properties of that data whole while allowing concurrent access. And 261 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 262 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 263 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 264 00:22:39,740 --> 00:22:44,140 calls to that tool stamp on each other because you're going to get incorrect results. 265 00:22:45,380 --> 00:22:52,360 Decisions need to be atomic, and they need to be isolated when there are multiple concurrent 266 00:22:52,360 --> 00:22:55,200 decisions going on about a particular policy. 267 00:22:57,000 --> 00:23:01,080 And so by atomic, these are the standard asset properties. What do we mean about atomic? 268 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 269 00:23:05,500 --> 00:23:12,260 about isolated is if I am running multiple concurrent ones, I can have an ordering of 270 00:23:12,260 --> 00:23:16,700 those things that just pretends not to be concurrent and is still well -formed. 271 00:23:18,520 --> 00:23:22,560 And that is because multiple concurrent agents could be returning to the same policy, 272 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 273 00:23:26,540 --> 00:23:28,760 policy. And so having these semantics, 274 00:23:29,720 --> 00:23:34,380 again, stolen from the world of databases as, you know, good systems people, we like 275 00:23:34,380 --> 00:23:37,340 to borrow ideas from the past quite heavily. 276 00:23:39,260 --> 00:23:40,880 Okay, so let's look at an example. 277 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, 278 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 279 00:23:55,150 --> 00:24:00,250 sales exactly one -to -one. And so I can only sell once per approval, 280 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 281 00:24:09,230 --> 00:24:14,970 redacted some bits of this because this is not the most succinct programming language 282 00:24:14,970 --> 00:24:21,290 in the world, but it's probably about double this long, fully expanded. Again, one of 283 00:24:21,290 --> 00:24:24,090 the limits of TUI slides as a format. 284 00:24:25,430 --> 00:24:28,130 But the important thing here is that I am saying 285 00:24:29,350 --> 00:24:33,890 matching up one -to -one these approvals and sales, one -to -one approvals and sales, 286 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, 287 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 288 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 289 00:24:49,350 --> 00:24:54,030 end, right? I've broken the semantics of the policy language and what I promised the 290 00:24:54,030 --> 00:24:55,570 agent was not allowed to do. 291 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 292 00:25:01,270 --> 00:25:05,650 read committed? And here I'm using PostgreSQL's definition of read committed rather than 293 00:25:05,650 --> 00:25:05,890 NC's 294 00:25:08,130 --> 00:25:12,730 because PostgreSQL's definitions are much saner. Different topic for a different talk, 295 00:25:12,830 --> 00:25:17,630 I guess, but at read committed, read committed allows lost rights, and that means that 296 00:25:17,630 --> 00:25:22,470 two concurrent transactions could be writing the same row and they could both end up 297 00:25:22,470 --> 00:25:22,890 committing. 298 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 299 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 300 00:25:36,110 --> 00:25:38,730 we have an approval. We're trying to sell both shares. 301 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 302 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, 303 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 304 00:25:54,730 --> 00:25:58,010 they will both go ahead and commit, and now I've sold those shares twice, 305 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 306 00:26:03,470 --> 00:26:10,070 this. So we're going to upgrade our world to snapshot isolation, the best isolation 307 00:26:10,070 --> 00:26:10,550 level. 308 00:26:12,730 --> 00:26:17,870 And so read committed allows lost rights. Snapshot isolation does not allow lost rights. 309 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 310 00:26:24,290 --> 00:26:26,330 parallel, exactly the same as the last time. 311 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 312 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. 313 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. 314 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 315 00:26:50,890 --> 00:26:53,250 and it says, no, you cannot commit this transaction. 316 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 317 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 318 00:27:04,430 --> 00:27:11,230 gets denied, which is great because only one says okay, and I manage to 319 00:27:11,230 --> 00:27:12,010 meet my promises. 320 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 321 00:27:20,490 --> 00:27:24,310 of semantic is actually serializable at the snapshot isolation level. I don't really 322 00:27:24,310 --> 00:27:25,870 have time to go into that. 323 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 324 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 325 00:27:38,750 --> 00:27:43,230 saying, for this agent, apply this policy with these temporal things, it is that key 326 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 327 00:27:49,170 --> 00:27:51,970 the next event, this is the next event, this is the next event. 328 00:27:53,250 --> 00:27:57,670 And so all concurrent transactions on that log cause write -write conflicts at the tip 329 00:27:57,670 --> 00:28:03,510 of the log. This is fundamentally the kind of per session, per agent scalability level. 330 00:28:04,590 --> 00:28:07,610 And then, yeah, yay for logs. Append -only data structures, they're cool. 331 00:28:09,830 --> 00:28:15,010 So then one more topic I wanted to cover, and that is MFOTL. 332 00:28:16,790 --> 00:28:19,450 And you might be saying, what is this? 333 00:28:20,470 --> 00:28:25,490 And let me explain. But I'm going to start off by explaining temporal logic. 334 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 335 00:28:33,710 --> 00:28:37,310 with those concepts. If you aren't, you should learn about them. They're pretty cool. 336 00:28:38,710 --> 00:28:45,450 And temporal logic adds some new operators to our logic to reason about time and order. 337 00:28:46,170 --> 00:28:51,690 We get operators like always and eventually and at the next step and until. 338 00:28:52,930 --> 00:28:55,610 And so with these operators, we can reason about. 339 00:28:56,610 --> 00:28:57,710 We did this thing. 340 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, 341 00:29:05,710 --> 00:29:06,570 this thing is true. 342 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 343 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 344 00:29:17,550 --> 00:29:19,610 ones that we lean in heavily in Dogwood. 345 00:29:20,610 --> 00:29:26,830 And these operators, just like those logic operators, give us this really cool foundation 346 00:29:26,830 --> 00:29:32,090 for all kinds of programming logic. These temporal operators give us a firm mathematical 347 00:29:32,090 --> 00:29:35,770 foundation for expressing these time -based policies. 348 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 349 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. 350 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 351 00:29:51,510 --> 00:29:53,710 of other newer, better operators. 352 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 353 00:30:01,850 --> 00:30:08,010 slides, there exists a typo D such there is a typo in the slides. 354 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 355 00:30:16,030 --> 00:30:21,370 about. And so the reason this was controversial with our science teams was when you talk 356 00:30:21,370 --> 00:30:26,590 about analyzability, as soon as you start to add these kind of quantifiers to logic, 357 00:30:27,150 --> 00:30:29,650 the analyzability becomes much, much more difficult. 358 00:30:31,650 --> 00:30:36,870 And then we can have metric first order temporal logic where we add temporal logic and 359 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 360 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 361 00:30:48,990 --> 00:30:54,110 say, less complete or less powerful logics. But these are very useful things to be able 362 00:30:54,110 --> 00:30:56,730 to use a policy language. 363 00:30:57,650 --> 00:31:03,530 And so putting these pieces together, we end up with a firm mathematical foundation in 364 00:31:03,530 --> 00:31:09,110 this well -defined logic that people have been studying for in parts hundreds of years 365 00:31:09,830 --> 00:31:14,650 to be able to reason about exactly what these policies mean when we look at them. 366 00:31:17,330 --> 00:31:23,950 And so temporal logic gives us a firm mathematical foundation. It gives us a 367 00:31:23,950 --> 00:31:30,130 very well -defined understanding of what policies mean and the ability to take those 368 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 369 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 370 00:31:41,870 --> 00:31:48,170 about these programs. Or if an auditor or compliance officer comes along, we can say, 371 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 372 00:31:52,530 --> 00:31:58,830 to do, which is actually very useful occasionally. And I hope you never run into the 373 00:31:58,830 --> 00:32:00,810 cases where that kind of thing is very useful. 374 00:32:03,730 --> 00:32:08,390 And metric temporal logic matches how our customers think about time. Because it turns 375 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, 376 00:32:13,090 --> 00:32:16,750 very common among humans. It really pisses mathematicians off. 377 00:32:17,670 --> 00:32:19,830 But it is useful for customers. 378 00:32:21,650 --> 00:32:26,070 And fundamentally, a firm foundation helps us with analysis and composition, the ability 379 00:32:26,070 --> 00:32:28,090 to reason about programs and how they join together. 380 00:32:29,830 --> 00:32:35,430 Anyway, so you should try out Dogwood. We haven't actually shipped the Dogwood Playground 381 00:32:35,430 --> 00:32:38,230 yet. It's a little bit annoying. I was hoping to show it off. 382 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 383 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 384 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 385 00:32:51,490 --> 00:32:51,990 things. 386 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, 387 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 388 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 389 00:33:05,350 --> 00:33:10,370 you give the Dogwood documentation to Claude Code or Claude, it's a pretty credible job 390 00:33:10,370 --> 00:33:16,190 of writing good Dogwood policies. Not perfect, but fairly creditable. So that is a good 391 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 392 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 393 00:33:25,990 --> 00:33:32,490 to the whole ecosystem of agents 394 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 395 00:33:39,070 --> 00:33:43,810 or know or trust every five milliseconds. And so that's my whole motivation for building 396 00:33:43,810 --> 00:33:44,370 this stuff. 397 00:33:45,490 --> 00:33:48,070 Thank you all so much. Any questions? 398 00:33:52,440 --> 00:33:52,780 Yeah. 399 00:33:57,160 --> 00:34:01,660 I'm assuming it's not the only mechanism of deployment of Agent Core Policy, correct? 400 00:34:01,820 --> 00:34:06,620 There's probably other manners that Agent Core Policy is deployed. I'm just unfamiliar 401 00:34:06,620 --> 00:34:11,980 with the subservice. Yes, Agent Core Policy is attached to Agent Core Gateway in the 402 00:34:11,980 --> 00:34:15,400 cloud. You sort of put your agents behind a VPC. 403 00:34:16,460 --> 00:34:20,080 You put the gateway between them and their tools. And then you apply Agent Core Policy 404 00:34:20,080 --> 00:34:24,120 there. You can write those policies in Dogwood. You can write those policies in Cedar. 405 00:34:24,460 --> 00:34:28,060 Or you can write those policies as custom Lambda functions. And so then you can write 406 00:34:28,060 --> 00:34:32,820 those policies as Python or TypeScript or Java or whatever takes your particular fancy. 407 00:34:33,380 --> 00:34:37,400 And then one clarifying question for your slides. The portion that was on read commits, 408 00:34:37,400 --> 00:34:39,380 I'm assuming that that was basically 409 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 410 00:34:45,640 --> 00:34:50,240 second system that was trying to replicate a task. Was that what the main component of 411 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. 412 00:34:55,480 --> 00:34:58,420 Yeah, exactly. So those are these things turn into database transactions. 413 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 414 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 415 00:35:08,980 --> 00:35:13,720 that has that approval in it because it's strongly consistent because that is the right 416 00:35:13,720 --> 00:35:14,560 thing to do. 417 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 418 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. 419 00:35:27,060 --> 00:35:31,600 And this is a write write conflict, which is exactly the thing that snapshot isolation 420 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 421 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 422 00:35:42,160 --> 00:35:45,580 tend to do that because it annoys people when throughput drops to zero. 423 00:35:46,480 --> 00:35:47,260 Thank you. 424 00:35:51,280 --> 00:35:56,420 Mark, you mentioned that one of the primary motivations for Dogwood was to allow agents 425 00:35:56,420 --> 00:36:00,540 to be creative, but have an appropriate sandbox around them. 426 00:36:02,440 --> 00:36:08,520 Does Dogwood have the ability to explain why a policy violation has occurred, like why 427 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 428 00:36:13,920 --> 00:36:14,600 like yet. 429 00:36:15,500 --> 00:36:18,940 So this is one of the super interesting things about agents 430 00:36:20,560 --> 00:36:26,580 is how useful error messages are. And it's just this lesson that everyone's learning 431 00:36:26,580 --> 00:36:29,840 of if you give good error messages, agents can do much smarter things. 432 00:36:30,920 --> 00:36:34,980 You know, security folks have always wanted authorization languages not to give good 433 00:36:34,980 --> 00:36:39,640 error messages and just say no, because it stops you from probing the policy and reverse 434 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 435 00:36:43,920 --> 00:36:48,660 does give an explanation for why it said no. Those explanations aren't quite good enough 436 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 437 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 438 00:36:59,580 --> 00:37:05,060 and hopefully make another plan to meet their goal that is within the both letter and 439 00:37:05,060 --> 00:37:06,020 spirit of the policy. 440 00:37:08,280 --> 00:37:14,940 Yeah. So actually I have two questions. The first one is when you design this 441 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 442 00:37:22,080 --> 00:37:27,220 at your code, I feel something is kind of very similar stuff around that area because 443 00:37:27,220 --> 00:37:28,060 you know, 444 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. 445 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 446 00:37:39,540 --> 00:37:46,160 fairly similar goals of analyzability and composability for the same reason. I 447 00:37:46,160 --> 00:37:50,740 haven't personally looked at the relationship between those in detail. Some of the folks 448 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. 449 00:37:55,880 --> 00:37:57,980 I feel maybe something there. I also want to dig in later. 450 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 451 00:38:03,200 --> 00:38:07,400 in that community, right? So we can borrow something here and we can, you know, with 452 00:38:07,400 --> 00:38:11,500 faster. Yeah. I mean, fundamentally solidity is like, oh, I want to say these things 453 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 454 00:38:14,620 --> 00:38:19,000 of this log. And so they are very fundamentally similarly structured. Yeah. That's kind 455 00:38:19,000 --> 00:38:19,400 of my feeling. 456 00:38:20,980 --> 00:38:26,080 Something really familiar there. I was like on the digging details. Thank you. 457 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? 458 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 459 00:38:48,980 --> 00:38:53,620 that is a little bit of an escape patch on Dogwood into imperative code. 460 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 461 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, 462 00:39:05,020 --> 00:39:06,480 convert that into Dogwood. 463 00:39:07,600 --> 00:39:11,820 Python and TypeScript are particularly difficult for this because they have particularly 464 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 465 00:39:18,180 --> 00:39:18,820 TypeScript. 466 00:39:19,740 --> 00:39:21,420 But there's nothing there that's impossible. 467 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 468 00:39:27,100 --> 00:39:31,860 analyze things. But if you're writing a typical authorization type policy in Python, 469 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 470 00:39:35,700 --> 00:39:38,840 thing to want to exist. We just haven't built it yet. 471 00:39:42,070 --> 00:39:47,210 The implementation is in Rust, our reference implementation, but you could implement 472 00:39:47,210 --> 00:39:48,890 the language in whatever you wanted. 473 00:39:50,170 --> 00:39:52,070 You can implement it in Lean, for example. 474 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 475 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 476 00:40:10,240 --> 00:40:13,500 be a common thing. I wouldn't say most people think about it that way. 477 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 478 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 479 00:40:24,400 --> 00:40:28,580 versions of the program that should have the bugs found by the specification. 480 00:40:29,540 --> 00:40:33,900 And I think that would be good practice in something like this, is writing those kind 481 00:40:33,900 --> 00:40:39,980 of negative cases. And one set of tools that's really interesting is 482 00:40:41,820 --> 00:40:43,160 you could imagine 483 00:40:44,560 --> 00:40:49,500 property -guided fuzzers that could generate lots and lots and lots of those kinds of 484 00:40:49,500 --> 00:40:51,000 tests to test your programs. 485 00:40:51,940 --> 00:40:53,060 Test your Dogwood programs. 486 00:40:55,840 --> 00:40:58,880 But yeah, negative tests. They're good for authorization, for sure. 487 00:40:59,940 --> 00:41:02,620 I wouldn't say that's common, but I would say it's a good idea. 488 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. 489 00:41:13,510 --> 00:41:14,090 Awesome. 490 00:41:18,340 --> 00:41:19,380 That's a great idea. 491 00:41:20,700 --> 00:41:22,640 I will stop sharing my screen. 492 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 493 00:41:32,970 --> 00:41:35,790 confidential and then write an email. 494 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 495 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 496 00:41:48,330 --> 00:41:48,650 commit. 497 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 498 00:41:54,510 --> 00:41:58,770 express and whether you want to address them? That's a great question. 499 00:42:00,090 --> 00:42:04,650 You can express something like I showed in the cargo example where you used the previously 500 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 501 00:42:09,850 --> 00:42:16,190 approval workflow or some model or something and not allow edits between them. 502 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 503 00:42:21,870 --> 00:42:28,670 into a general purpose programming language, is call an LLM as a judge and check 504 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. 505 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 506 00:42:40,710 --> 00:42:41,450 have 507 00:42:42,430 --> 00:42:48,290 some kind of heuristic for is this traffic evil? With 5 % probability and you might want 508 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 509 00:42:54,230 --> 00:42:57,550 steps, non -deterministic steps to deterministic policy. 510 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 511 00:43:01,990 --> 00:43:02,730 much in the vision. 512 00:43:07,620 --> 00:43:13,560 Has this shown a success with agents that have a very wide range of capabilities? For 513 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 514 00:43:18,920 --> 00:43:22,740 anything that you could do. Run commands or 515 00:43:24,000 --> 00:43:27,900 run commands on your machine or to git or to basically do anything. 516 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 517 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 518 00:43:39,160 --> 00:43:45,000 problem is a well -known one in security and is basically not great. You could express 519 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 520 00:43:48,700 --> 00:43:52,800 something like OpenClaw, that set of things might be so big that you couldn't reasonably 521 00:43:52,800 --> 00:43:54,120 express all of them. 522 00:43:56,100 --> 00:44:02,000 Generally, I would say that those are exception cases. Even if I'm using something like 523 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 524 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 525 00:44:12,080 --> 00:44:18,200 example, and nothing beyond that. You can express those kinds of policies. But fundamentally, 526 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 527 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, 528 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 529 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 530 00:44:42,500 --> 00:44:44,160 might have seen this in a lot of the headlines, 531 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 532 00:44:50,780 --> 00:44:54,020 ways around the obstacle very, I would say, creatively. 533 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 534 00:45:00,720 --> 00:45:06,140 listing problem of allow listing a set of allowed behaviors rather than a deny listing 535 00:45:06,140 --> 00:45:09,240 problem of trying to exhaustively list all of the bad things in the world. 536 00:45:15,580 --> 00:45:21,320 Yeah. So how do you debug a temporal policy denial in production? Can Dogwood tell you 537 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 538 00:45:27,500 --> 00:45:33,260 very reduced form exactly what was not allowed, which is really nice. It tells you that 539 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 540 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 541 00:45:44,060 --> 00:45:50,320 the team is working on making that debugging experience a ton more useful. And the good 542 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. 543 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 544 00:46:00,140 --> 00:46:00,960 the policy language. 545 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 546 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 547 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 548 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. 549 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 550 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 551 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 552 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 553 00:46:41,580 --> 00:46:44,920 I'm going to buy a gift that is maybe fifty bucks instead. 554 00:46:45,840 --> 00:46:48,760 And so in some cases, yes, you do want to give that feedback to the agent. 555 00:46:49,680 --> 00:46:53,700 In security cases, for example, you might not, and this is, you know, always been the 556 00:46:53,700 --> 00:46:59,760 philosophy with authorization folks is you don't want to allow an adversary to explore 557 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 558 00:47:03,900 --> 00:47:08,140 information. And so it is actually an interesting set of tradeoffs about what you tell 559 00:47:08,900 --> 00:47:13,500 the contained thing about why it wasn't allowed to do the thing it was doing. 560 00:47:17,380 --> 00:47:20,380 Where do you draw the line or where do you draw the boundary between 561 00:47:21,340 --> 00:47:27,120 dogwood determining what an agent is allowed to do in the system deciding which of several 562 00:47:27,120 --> 00:47:30,200 allowed actions it should actually take? 563 00:47:32,420 --> 00:47:34,740 Yeah, that's a fantastic question. So 564 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, 565 00:47:44,740 --> 00:47:47,900 go left. When you go to this place, go right. You can do that in 566 00:47:48,800 --> 00:47:52,960 many, many different workflow languages that have existed for a long time. You almost 567 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 568 00:47:58,100 --> 00:47:59,640 driving a workflow? That would be silly. 569 00:48:00,540 --> 00:48:03,540 You can sort of build a let's say sort of shaped 570 00:48:04,540 --> 00:48:08,320 pipe around a workflow that sort of guides it in one direction or another. 571 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 572 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 573 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 574 00:48:25,860 --> 00:48:30,940 will call safety, which is nothing bad happens, rather than liveness, which is the something 575 00:48:30,940 --> 00:48:33,760 good eventually happens half of the problem. 576 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 577 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 578 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 579 00:48:49,660 --> 00:48:51,820 the right shape of that is. 580 00:48:53,780 --> 00:48:57,420 And so there are a lot of kind of precondition, post condition type things that people 581 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 582 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 583 00:49:05,860 --> 00:49:08,100 of innovation, of how do you really just 584 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 585 00:49:14,160 --> 00:49:16,240 the cool things that agents can do. 586 00:49:17,600 --> 00:49:21,720 A ton of innovation possible there. And we certainly haven't figured it out yet. 587 00:49:24,120 --> 00:49:24,560 Hi, 588 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 589 00:49:31,240 --> 00:49:36,260 write something like commentable expressions with something as something. So where there 590 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 591 00:49:41,400 --> 00:49:46,360 evaluate or compile that these should be changed and these are still valid policies? 592 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 593 00:49:53,140 --> 00:49:57,240 level of policy complexity and policy size, where you can't do that in the industry. 594 00:49:57,440 --> 00:50:00,080 We do that compiler does admit like tons of CTEs. 595 00:50:02,980 --> 00:50:09,020 But this is where the composability comes in, is that almost most policies are actually 596 00:50:09,020 --> 00:50:12,020 expressing a fairly simple set of 597 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 598 00:50:17,880 --> 00:50:23,200 very redundant and duplicative way. And so you can do a kind of minimization step first, 599 00:50:23,200 --> 00:50:27,580 which helps you avoid these kinds of problems. And then you know, when you have policies 600 00:50:27,580 --> 00:50:32,340 with multiple clauses, the fact that the composition of those clauses is very well defined 601 00:50:32,340 --> 00:50:36,860 helps the compiler figure out how to write the sequel that composes those expressions 602 00:50:36,860 --> 00:50:38,200 together in the correct way. 603 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 604 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 605 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. 606 00:50:59,060 --> 00:51:02,350 But the idea is fully proven to be correct 607 00:51:03,300 --> 00:51:09,340 and is actually the rest version of that compiler runs in production is derived from 608 00:51:09,340 --> 00:51:10,660 the lean implementation. 609 00:51:11,740 --> 00:51:13,960 We're not there yet, but that's the goal. 610 00:51:15,280 --> 00:51:21,160 Would it be something like here there plus protocols would it be basic unit testing? 611 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 612 00:51:28,860 --> 00:51:34,400 concepts to TLA plus or TLA proof system if you're familiar with that. 613 00:51:35,600 --> 00:51:37,980 We just tend to use lean because it's more powerful 614 00:51:39,280 --> 00:51:43,400 and TLA proof system is, I don't want to offend anyone, but a bit weird. 615 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 616 00:51:48,000 --> 00:51:52,640 it is fundamentally unsound and so it doesn't really meet our needs. 617 00:51:54,400 --> 00:52:00,920 Last question. So I was curious about the local case. Does like Dogwood protect 618 00:52:00,920 --> 00:52:06,680 against Dogwood? Like the agents messing up with the policy evaluation? 619 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 620 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 621 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 622 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, 623 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 624 00:52:31,400 --> 00:52:35,960 around it. And so Dogwood isn't a complete solution to agent sandboxing because you still 625 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 626 00:52:40,460 --> 00:52:43,460 with agent core runtime and an agent core gateway, 627 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 628 00:52:50,280 --> 00:52:56,540 of innovation going on in the local agent sandboxing space right now. Okay, and were 629 00:52:56,540 --> 00:53:00,420 there any unexpected challenges developing something like this and like you mentioned 630 00:53:00,420 --> 00:53:05,600 also compiling forcing all of this into SQL? Yeah, I mean the SQL compiler stuff was 631 00:53:05,600 --> 00:53:09,720 interesting, it was super fun, actually the team wrote this really cool super optimizer 632 00:53:09,720 --> 00:53:14,420 loop that used the lean proof to find more and more and more efficient compilers which 633 00:53:14,420 --> 00:53:17,260 is just a super fun technique I'm really excited about. 634 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, 635 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 636 00:53:26,660 --> 00:53:31,380 to be analyzable always in, you know, under a set of assumptions. 637 00:53:32,560 --> 00:53:36,720 Dogwood is not always analyzable and so, you know, the analyzer is always forced into 638 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 639 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 640 00:53:48,100 --> 00:53:50,480 ton of different people had different opinions. 641 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 642 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 643 00:54:01,140 --> 00:54:06,400 power to the proof ecosystem over the last couple of years and certainly even more over 644 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 645 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. 646 00:54:17,820 --> 00:54:18,960 Cool. Thank you all so much.