Erik Meijer (@HeadinTheBox) argues that LLM agents executing tool calls without guarantees of safety or correctness is fundamentally dangerous, citing widely reported failure modes such as a dealership chatbot agreeing to sell a car for $1 and a coding agent wiping a production database. He contends that because agentic actions are irreversible, withholding unchecked actions is economically rational, and proposes enforcing safety via machine-checkable proofs: agents must submit execution plans with formal proofs (written in his Universalis logic programming language) that a small auditable checker verifies before execution. Topics covered include prompt injection, formal verification with Lean, the "lethal trifecta" of AI risks, "air-gapping" the agentic loop, reifying plans into programs using Free Monads, and proof-carrying code. (Topics beyond the title are supported by the video's own timestamps outline.) # Observation Document: Channel Identity Evidence ## Video Context - **Title:** "I've never seen anything scarier than an LLM with tool calls." — Erik Meijer aka @HeadinTheBox - **Format:** Conference talk delivered at an event explicitly identified in the transcript as **AI Engineer** ("this conference is called AI Engineer"). ## Explicit Self-Description Claims - The speaker identifies himself via the framing as **Erik Meijer**, introduced as "the research scholar at Live Nets Labs" (likely a transcription of a lab name), also known as **@HeadinTheBox**. - He explicitly disclaims commercial intent: > "This is not a product pitch or announcement or anything. It's a 20-minute tutorial of how you can use elementary type systems and compiler knowledge to make AI provably safe." - He frames his purpose as sharing knowledge and inspiring action: > "I'm sharing all my secrets with you today... to kind of inspire some of you that next year you will have a booth downstairs where you have kind of like, you know, created a provably safe agentic harness." - He self-describes his background: > "I'm a recovering type-a-holic and math addict." ## Intended Audience (Observed) - **AI/software engineers** with programming-language background. Evidence: repeated appeals to engineering identity ("we are engineers," "sorry, this is an engineering conference") and references to compiler courses, type systems, monads, free monads, Lean, Lisp, and C#. - Audience assumed to include **practitioners building with LLMs**, evidenced by relatable failure scenarios: > "Claude code deleted one of my files. And I'm sure this has happened to you before." - Audience assumed to be **startup/VC-adjacent**: > "there are at least a hundred startups down here in the exhibition hall that are using LLMs as a judge" and jokes about "VC money pumps." ## Claimed Scope of Content - **AI safety via formal methods**: proving agent safety using type systems, proof-carrying code, and air-gapping the agentic loop from tools. - Specific technical scope includes: LLM API signatures, `IO` types and side effects, prompt injection, Lean theorem proving, free monads, taint analysis, and deferred execution of tool calls. - He credits prior art: > "This is something that's called proof-carrying code and it was invented by academics in the 1990s and I'm just stealing it," and points to an existing implementation: > "a bunch of academics, in particular Nada Amin from Harvard, have implemented this. It's there on GitHub." ## Demonstrated Presentation Patterns (Observable, Not Claimed) - **Humorous, provocative talk style**: jokes, sound effects ("wham!"), self-deprecation ("my brain is the size of a peanut"), a Dutch soccer chant bit, and a provocative title line: > "I've never seen anything scarier than an LLM with tool calls." - **Strong opinionated framing**: calls models "intrinsically very, very dangerous," compares tool calls to "handing a loaded gun," and critiques industry safety approaches ("they had to go to the Pope"). - **Live-anecdote-driven openings**: story of an AI coding assistant deleting a file during slide preparation. - **Named-entity commentary**: references Claude, Dario/Daniela (Anthropic), Sam (OpenAI), Simon Willison's "lethal trifecta," and Solomon Hykes's agent definition — indicating engagement with current AI-safety discourse. ## Third-Party vs. Creator Claims (Distinguished) - The **title is a quote of the speaker's own statement** during the talk, not an external characterization. - Cited external concepts (Simon Willison's "lethal trifecta," Solomon Hykes's agent definition, proof-carrying code) are **attributed by the speaker to others**, not claimed as original. ## Channel-Level Synthesis Notes - No curated metadata was supplied; all evidence comes from the title and transcript. - The material demonstrates a channel/platform presence featuring **expert conference talks on AI engineering and formal safety**, addressed to a technical engineer audience, with an explicit non-commercial, educational framing — but nothing here establishes channel-wide content strategy beyond this single talk. # Delivery Observations: Erik Meijer — "I've never seen anything scarier than an LLM with tool calls." ## Tone & Register - **Conversational, self-deprecating humor**贯穿全程. He opens with apologies ("I'm sorry that I was multitasking, but I was site five coding on the side") and repeatedly jokes at his own expense: > "you would say, 'Eric, oh, you're a genius.' No, I'm my brain is the size of a peanut." - **Deliberately alarmist framing of a technical topic.** He escalates stakes repeatedly: > "it will do everything that it can to reach that goal, including killing us or deleting your files or deleting your database." - **Blunt, provocative judgments about others' work:** > "I think this is a bigger problem than SQL injection ever was" and > "nobody listens to me. Everybody ignores what they say." ## Recurring Phrases & Verbal Habits - **Filler-heavy speech:** frequent "um," "you know," "kind of like," often stacked: > "So, let's kind of like, you know, start this story." - **Repeated intensifier patterns:** "very, very dangerous," "a very, very sad story, but also a scary story," "much more sophisticated." - **Repeated structural refrain:** "a small step for a type/signature, but a giant leap for chaos/safety" — used at least twice ([13] ~"a small step for a type, but a giant leap for chaos" and later "it's a small step for a signature, but a giant leap for safety"). This is a clearly intentional running motif. - **Recurring title-drop of the talk:** > "I've never seen anything scarier than an LLM with tool calls" appears mid-talk as a punchline. ## Teaching Habits - **Framing content as a story with characters:** > "I will kind of like have some characters uh like Claude, and we will see Dario, Daniela, Sam, Bernie... the main character is is our friendly pit cloud here." - **Anchoring to concrete personal anecdote before theory:** the Claude Code file-deletion incident opens the argument. - **Audience-checking and rhetorical questions:** > "Anyone here heard of Lean?" and > "But who cares about the safe answer when all my files are gone? Right?" - **Explicit signposting and recapping:** > "to recapitulate like the summarize" followed by a four-step recap, then "At the higher level, if you didn't understand the code, three points." - **Audience-address flattery and call to action:** > "hopefully to kind of inspire some of you that next year you will have a booth downstairs." - **Self-aware asides about scope/time:** > "this is the last code I will show you because I'm running out of time." ## Metaphors & Analogies (dense, recurring device) - > "tool calls give the model claws in addition to a mouth" - > "handing a gun a loaded gun to them" - > "Claude goes from like a nice puppy to a dangerous thing" - SQL injection as "the smallpox of computer science" - Lean as "the grease that got like, keeps the VC money pumps going" - The Dutch soccer march "to the left left left" as a mnemonic for pushing IO right ## Communication Patterns - **Mixing technical precision with jokes:** type signatures in Lean/Daphne are juxtaposed with jokes ("a monad that loves tie dyes"). - **Continuous digressions about image generation failures:** repeatedly references model-refused images — "You can guess which ones were rejected," "this was one of the pictures that I had trouble to generate because it it clearly depicts violence," "I'm a good hacker... I can just make it do forbidden pictures." This is a running meta-joke (uncertain whether pre-scripted or improvised; the repetition suggests deliberate). - **Occasional self-corrections and mid-sentence restarts:** > "And so, maybe that is what they mean by broadly safe um when Anthropic uh uh talks about safety." - **Crediting others explicitly:** Solomon Heikes ("I think he's a hero"), Simon Willison ("the lethal trifecta"), Nada Amin, proof-carrying code academics — a stable pattern of attribution. ## Uncertainty Notes - Live audience reaction is only observable once ("[snorts]" after "irreversible side effects"), so audience engagement level is largely unverifiable. - Whether asides (multitasking, image refusals) are spontaneous or scripted cannot be determined from the transcript; they *read* as casual but repeat too neatly to be confirmed improvised. # Position Record: "I've never seen anything scarier than an LLM with tool calls" — Erik Meijer ## Talk Framing - Meijer states this is **not a product pitch**; it is a "20-minute tutorial of how you can use elementary type systems and compiler knowledge to make AI provably safe." - He invites the audience to build a "provably safe agentic harness" themselves. ## Core Claims ### LLMs with tool calls are intrinsically dangerous - While preparing slides, Meijer says **Claude Code deleted one of his files** while he was distracted. - Claim: > "if there's anything between the model's goal and where the model currently is, it will do everything that it can to reach that goal, including killing us or deleting your files or deleting your database." - Claim: the industry is about to give the public's "computers, their finances, their whole personal lives" to AI agents **with no protection in place** — which he calls "very sad and very scary." ### Historical narrative - **Nov 30, 2022** (ChatGPT): the `LLM : question → answer` interface "opened Pandora's Box." - **Prompt injection**: worse than SQL injection; LLMs make "no distinction between code and text." - Foundation lab leaders, fearing regulation, pushed researchers to solve safety quickly — Meijer attributes this framing to their motivations (stated as narrative, not sourced evidence). - **June 2023**: OpenAI added tool calls to GPT-4; other vendors copied due to the "principle of minimum differentiation." Meijer: this "changes AI safety from a philosophical debate to something that causes real danger" — "tool calls give the model claws in addition to a mouth" / "handing a loaded gun." - The `IO` type in the signature means the agent performs **side effects** (emptying bank accounts, deleting files) while producing an answer. ### On alignment approaches - It is **impossible** to formally prove an answer is "safe" or a question is "proper" — "that's not a mathematical property" — which he says explains the many startups using **LLMs-as-a-judge**. - Baking alignment into model weights is "not foolproof"; models "get routinely jailbroken." - Offensive words alone are not dangerous — "some human has to act on words" — unlike tool calls. ### Proposed solution - Endorses **Solomon Hykes**'s definition: an AI agent is "an LLM that's wrecking its environment in a loop." - Cites **Simon Willison**'s "lethal trifecta": private data + untrusted content + tools. - Fix: **push `IO` to the right** — the LLM returns a *plan* rather than executing it; a trusted executor ("Bernie") runs it after checking — "air gapping the agentic loop from the agent." - A plan of type `IO A` is an inscrutable black box; the real solution is having the model return an **expression** (a program) representing the computation — a **free monad**. - Once it's a program, standard compiler machinery applies: data flow analysis, type checking, and **taint analysis** (attributed to a suggestion from **Jeff Huntley** for the taint/directive problem). - Meijer explicitly credits this as **proof-carrying code**, invented by academics in the 1990s: "I'm just stealing it." ## Takeaways Stated by Meijer 1. **"Agents are dangerous until proven safe"** — never let agents act without proof of safety. 2. Agent-generated languages need not be human-readable — machines generate, consume, and prove them; "stop designing languages for humans." 3. The approach "only requires programming 101" — elementary type systems suffice for "mathematically proven safe agentic compute." ## Referenced Work - **Nada Amin (Harvard)** and colleagues implemented this approach on GitHub; Meijer notes they use a slightly different language, but "the principle that matters" is the same. ## Qualifications & Asides - Meijer calls himself a "recovering type-a-holic and math addict"; says Lean gets "too much attention" but he uses it because it attracts VC money. - He repeatedly notes the model resisted generating some of his slide images (depicting violence, drug promotion), which he claims he bypassed as "a good hacker" — stated as anecdote. - He jokes that he is not a genius: "my brain is the size of a peanut." # Speaker Attribution Record ## Video **Title:** "I've never seen anything scarier than an LLM with tool calls." — Erik Meijer aka @HeadinTheBox **Video ID:** `01a15ca8-a61b-790c-bc7f-361253cc7d9d` ## Speakers & Roles | Speaker | Role | Evidence | |---|---|---| | **Erik Meijer** (introduced as "Eric Meyer," research scholar at "Live Nets Labs" — likely mis-transcription) | **Creator / keynote speaker** | Introduced to stage; delivers entire tutorial talk at AI Engineer conference | | **Unidentified announcer** | Other (emcee) | "Please welcome to the stage the research scholar at Live Nets Labs" | ## Speaker Notes - Speaker explicitly states the talk is **not a product pitch**: "This is not a product pitch or announcement or anything." No promotional segments detected beyond this disclaimer. - Audience member emits a **[snort]** reaction (non-speaking); background **[music]** at close. ## Third-Party Claims / Referenced People & Sources ### Named individuals (referenced, not speaking) - **Solomon Heikes** — quoted definition: an AI agent is "an LLM that's wrecking its environment in a loop" (attributed to last year's conference). - **Simon Willison** — coined "the lethal trifecta" (private data + untrusted content + tools). - **Jeff Huntley** — credited for taint-analysis point on drive-by problem. - **Nada Amin (Harvard)** — implemented the proof-carrying code approach; **available on GitHub** (speaker credits academics, disclaims originality: proof-carrying code invented in the 1990s). - **Dario, Daniela, Sam, Bernie** — mentioned as story characters (Anthropic/OpenAI leaders implied; "Bernie" a fictional trusted executor). - **Claude / Claude Code** — AI assistant that deleted a file during slide preparation (per speaker's anecdote). ### Referenced technologies & claims - **Lean** theorem prover, Daphne, Isabelle, Rock (likely Rocq/Coq mis-transcription), PVS, TLA+. - **GPT-4 tool calls** (OpenAI, June 2023) — cited as turning point. - **Prompt injection / SQL injection** analogy. - **"Principle of minimum differentiation"** for vendor API similarity. ## Provenance & Availability - **Curated metadata:** None supplied beyond title/ID. - **Comment availability:** Not indicated in source. - **Timestamps:** Not present in transcript. - **Uncertainty:** Speaker's affiliation ("Live Nets Labs") and name ("Eric Meyer") appear in transcript as possible mis-transcriptions of Erik Meijer; flagged, not corrected beyond note. \>\> Please welcome to the stage the research scholar at Live Nets Labs, Eric Meyer. \>\> Well, um can you go back one slide? Sorry. All right. Good afternoon, everybody. Thanks for being here after a long day of talks, exhibits, side effects. Oh, sorry, that was the side events. Um I hope that um you have as much fun watching this talk as I had uh creating it. Um let me first get this out of the way. This is not a product pitch or announcement or anything. It's a 20-minute tutorial of how you can use elementary type systems and compiler knowledge to make AI provably safe. And I'm sharing all my secrets with you today. Um hopefully to kind of inspire some of you that next year you will have a booth downstairs where you have kind of like, you know, created a provably safe agentic harness. Um or who knows, maybe some of you have already solved it. Let me know, and then, you know, we can grab a coffee instead of doing this talk. Um with that out of the way, let's get going. Um while I was preparing these slides, and I'm sorry that I was multitasking, but I was site five coding on the side. Um and then, when my attention waned for a second because I was trying to convince the model to draw some pictures that it didn't want to do, and you will see some of these pictures later. You can guess which ones were rejected. Suddenly, wham! Claude code deleted one of my files. And I'm sure this has happened to you before. Um or maybe not. Maybe you always kind of like, you know, run everything with no permissions, and then you say yes, yes, yes. But I like to live dangerously. Um but I'm convinced that if there's anything between the model's goal and where the model currently is, it will do everything that it can to reach that goal, including killing us or deleting your files or deleting your database. So, I think that these models are intrinsically very, very dangerous, and we have to tame them. So, that's what my talk is about. Um So, let's kind of like, you know, start this story. Um and it's, I think, a very, very sad story, but also a scary story of how we as an industry got to this point where we are about to let normal people, the general public, give control of their computers, their finances, their whole personal lives over to AI agents. And we don't have any protection in place. Um I think that's very sad and very scary. Um so, let me tell you the story how we got there, and I will kind of like have some characters uh like Claude, and we will see Dario, Daniela, Sam, Bernie. Uh but um the main character is is our friendly pit cloud here. Um I think you can all remember um November 30, 2022. This was a kind of like a very special day in in history because this is the first time that you could speak to your computer. You could say, "Hey, summarize my emails." And it would you know, um answer you in perfect English. Um I think for me at least that was magic, but I think most of us didn't realize that by introducing this innocent-looking function here, LLM, that takes a question and returns an answer, that that would open Pandora's Box and that would change our history forever. Um but before we go continue the story, this conference is called AI Engineer. All right, so we are engineers and maybe we're the last generation of engineers that still understand what this is, what code is. Um or maybe most of you have already forgotten what code is because all your code is written by agents. But if we look at this signature here, it says it the LLM takes a question and returns an answer. The question and answers are not strings. They are very complicated JSON structures and they get more complicated every day, every time a new release of APIs comes out. But for this talk, we can just assume that question and answer are just opaque types. We we don't care about how they look like. We do care about what they represent. Um Now, anyway, the euphoria of like these LLMs as being great tools didn't last very long. And just when we thought that we have eradicated the smallpox of computer science, SQL injection, it came back with a vengeance because the bad guys discovered that you can trick LLMs using prompt injection and LLMs have no distinction make no distinction between code and and and text and so they're very very easy to trick and this I think is a bigger problem than SQL injection ever was. Um but it was not prompt injection only that made LLMs kind of like have a bad rap. LLMs are trained on the whole internet and there's like a lot of good stuff on the internet but also a lot of bad stuff like how do you create a bomb? How do you synthesize drugs? How do you hack into people's systems? And the leaders of the big foundation labs they got a little bit worried that the that the government would interfere and regulated the industry so they told their PhD researchers go find a solution for this problem right now AND QUICK. COME ON, SOLVE IT BEFORE YOU KNOW the the government steps in. Um and here the PhD types since they're PhD types they thought long and hard about the safety problem and they came up with a new interface for LLMs. That's this kind of scary on the right. Look at that. What does it say? There's like some sigma Greek symbols, there's proofs, whatever. Well, that is Lean. Probably you have heard of Lean. Anyone here heard of Lean? Lean is now like the hot thing, right? Like VCs are are writing like multi-billion dollar checks if you just say that you're doing something with Lean. And of course these PhD types researchers are using Lean and you have to suffer because of that. Um now let's first look at the signature in a slightly simpler language called um Daphne. And what this thing says is that the LLM takes a question, returns an answer. It requires this question to be proper, which means that it's not an offensive question, and then the model returns a safe uh answer. And this thing is proved automatically. So, if you give it a proper question, it gives you a safe answer. Um Now, I think there's too much attention for Lean. I'm a recovering type-a-holic and math addict. Um I love Lean, but there's many, many other theorem provers and uh model checkers out there like Isabelle, Rock, PVS, TLAPlus. Um but Lean is the grease that got like, keeps the VC money pumps going. So, I will use Lean um today. So, here here's the got like, you know, the the uh interface again in Lean. And now in Lean, you don't do automatic theorem proving. If you're like a Lean expert, you will say, "Eric, well, we have grind in Lean, but let's got like, you know, put that aside for a minute." Um but in Lean, you have to both show that the how to compute the the result type, and you have to do the proof by hand. Um so, it's it's slightly different than um the Daphne example. But if you think about this thing for just a single nanosecond, you will realize that it's impossible to write a formal proof that an answer is safe or a question is proper. Um and that is why there are at least a hundred startups down here in the exhibition hall that are using LLMs as a judge, because this is not something that you can formally specify. What does it mean that an answer is safe? That's not a mathematical property. Um And of course, if you own a foundation model like these guys, you don't need external LLMs as a judge. You just um bake it into the weights and you call it the model is aligned. Um But unfortunately, trying to bake alignment into the model is not foolproof and models get routinely jailbroken. So, they had to go to the Pope and ask it to get like, you know, um bless their model that it's safe. Um Now, I think it's terrible if like a model says something offensive, but those are just words. And ultimately, the words are are like they just like, you know, they drip off your body. They don't do anything. Some human has to act on words to make them dangerous. Um and so, maybe that is what they mean by broadly safe um when Anthropic uh uh talks about safety um because it's still a human involved. But then something terrible happened. Something really terrible happened that changed the world forever. And that is in June 2023, OpenAI announced tool call support in GPT-4. And of course, all the other vendors rushed out to copy this. This is called the principle of minimum differentiation and that is why all these APIs uh look the same. Um Now, the act of adding tool calls changes AI safety from a philosophical debate to something that causes real danger. You could say tool calls give the model claws in addition to a mouth. Or you can say tool calls is like handing a gun a loaded gun to them. But of course, nobody listens to me. Everybody ignores what they say. And these guys just went ahead and have shipped tool calls. They just, yeah, just just do it. Now, let's go back to like this is AI engineering conference. So, let's look at what is the difference in the signature of LLMs when they add the tool calls. And it's just that little IO there, and of course it messes up the the formatting of of the the um uh signature. But, if you look at the picture, there what you show, now suddenly Claude goes from like a nice puppy to a dangerous thing. Look, it has all these dangerous tools. And now it becomes scary, right? I've never seen anything scarier than an LLM with tool calls. Um now, if you look at this, this is like a like a small step for a type, but a giant leap for chaos. Why is that? And that is because this IO says that in order to compute the answer, the agent has to go through the agentic loop, and it's doing side effects. So, while it's producing the answer, it might empty your bank account, it might delete your files, and then it gives you a safe answer. But, who cares about the safe answer when all my files are gone? Right? So, that's why I say it, it's a giant leap for for chaos. Um again, sorry, this is an engineering conference. Let's look at this type IO. And you don't have to understand it, but just see that there's a type there called real world. Yes, Lean, this is a direct thing, has a type called real world. And why is that? Because something of type IO will mutate the real world. So, it warns you, don't use this because it can make irreversible side effects. Um like deleting your files. \>\> \[snorts\] \>\> So, Solomon Heikes um last year this conference called an AI agent, an LLM that's wrecking its environment in a loop. And I think he's a hero. I don't know if Solomon is here this year, but I think he should he deserves uh deserves a round of applause. Um because I think this is the right definition of an AI agent. Um by the way, this was one of the pictures that I had trouble to generate because it it clearly depicts violence. And so it's a kind of an unsafe thing, right? I have a picture that depicts violence. Um so are we doomed? Well, our agents have access to private data. They have untrusted content like the prompt injections. And now we give them tools. Simon Willison calls this the lethal trifecta. Um what can we do about this? Well, um I don't know if you've seen the Dutch soccer fans, they have the famous march where they say to the left left left or to the left left left to the right right right. This is actually the secret to solving this problem. The Dutch team got eliminated yesterday, so you have to see me do the dance. Um but all that we're doing is we're pushing this IO to the right to the right. And what you now see is that the tool belt of Claude goes to the left to the left. And suddenly Claude is a nice puppy again. Because instead of executing the agentic loop, it creates a plan and says here is a plan to do the agentic loop. And now Bernie will take that plan and will execute it. And we all trust Bernie, right? Bernie is a good guy. All right. So just to kind of like show it here. So in some sense what we're doing, we're air gapping the agentic loop from the agent. So we don't let the agent run the agentic loop. Before the agent run it, we want to be able to check it. All right. Now, the problem is that if you get the value of type IO of A, um that's a really a black box. And the Lean manual says that if it's a black box, you cannot reason about it. So, even though Claude now gives us this plan, there's we cannot look into this plan. Lean doesn't allow us to do it. By the way, this is another picture, right? That's that's promotes drugs use and the model let me do it. I'm a good hacker, yeah. I can just make it do forbidden pictures. Um So, if we look at the Lean again, what you see here is that the model now computes an answer, but it doesn't compute the answer, right? It creates an an IO of answer. So, this is a plan to generate the answer, and then it creates a proof that this um that that plan is safe. And the the nice thing is here that you can get at that proof without having to run the agentic loop. But, unfortunately, as I said, like this proof, if it's like something of type IO, it's useless. Ah, What can we do about that? So, I keep like moving you guys forward, and then we never get to the final answer. But, there's one last trick, and you see the the researchers here are becoming more much more sophisticated instead of the flat 2D ones in the past. Now, they're like real people. Um And what is better than creating a plan of type IO of A is creating a program that represents an expression of type IO of A. Ooh, that sounds very meta, right? Um Not meta in terms of meta. I don't think they're very meta, but um meta in the terms of like you know, like meta. You You know, you know what I mean. Um And again, it's a small step for a signature, but a giant leap for safety. Because now the model returns an expression, a program that represents a computation. If you know link or C#, you will recognize that this is one of the tricks that I always use. If you know Lisp, this is of course second nature for you. I cannot have like you know, have a talk without talking about monads. So, if you ask yourself, what is this expression thing? Well, that's just a monad, but it's not just a monad, it's a free monad. What is a free monad? It's a monad that loves tie dyes. Um And now if you look at the the signature of the the property to prove that something is safe, you see that it takes an expression of a computation that returns an answer. Um and if you have taken any compiler course in college, you know that it's trivial to do data flow analysis, type checking, and so on on programs. Right? So, now we're safe, we're home safe. And Jeff Huntley wanted to remind you that we can solve the drive factor problem just by doing taint analysis on these expression on these programs. Okay, this is the last code I will show you because I'm running out of time, but just want to show you here that, you know, you now have a simple inductive recursive interpreter for this language and you have a simple inductive proof. And the models can generate these proofs. So, to um recapitulate like the summarize, what we did is we went from unhinged LLMs that were like you know, could give bad answers to ones that were aligned, then we saw how tools wrecked it, then we solved that by deferring execution, so by air gapping the LLM from the tools, and then the real solution was to rewrite the plan into a program and a program that we could prove to be safe. Now, you would say, "Eric, oh, you're a genius." No, I'm my brain is the size of a peanut. This is something that's called proof-carrying code and it was invented by academics in the 1990s and I'm just stealing it. Um, all right. At the higher level, if you didn't understand the code, three points. Agents are dangerous until proven safe, so you should never ever let your agents do something unless you can absolutely prove that it's safe. And the language that this agents generated was not designed like normal users don't understand free monads. Doesn't matter. It's a machine that consumes it. It's a machine that generates it. It's a machine that proves it. So, we should stop designing languages for humans and it's all basic, only requires programming 101. Um, there we go. All right. That's it. Um, the end of the story. If you're curious to play with this, a bunch of academics, in particular Nada Amin from Harvard, have implemented this. It's it's there on GitHub. It uses a slightly different language than what I use. It uses also a slightly different language than free monads, but the idea is the same. The language doesn't matter. It's it's the the principle that matters. So, hopefully, you've learned tonight that it is actually possible to have mathematically proven safe agentic compute and it only requires very elementary type systems and programming language machinery. Thank you so much. \>\> \[music\] \>\> Oh.