"I've never seen anything scarier than an LLM with tool calls." — Erik Meijer aka @HeadinTheBox

Please welcome to the stage the research scholar at Leibniz labs, Erik Meyer. Well, 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. I hope that you have as much fun watching this talk as I had creating it. 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. Hopefully... to kind of inspire some of you that next year you will have a booth downstairs where you have, like you know, created a provably safe agentic harness. 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. With that out of the way, let's get going. While I was preparing these slides, and I'm sorry that I was multitasking, but I was Vibe coding on the site, 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, or maybe not. Maybe you always kept, like, you know, run everything with no permissions, and then you say yes, yes, yes. But I like to live dangerously. 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. So let's get, like, you know, start this story. 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. I think that's very sad and very scary. So let me tell you the story how we got there, and I will have some characters like Claude, and we will see Dario, Daniela, Sam, Bernie, but... The main character is our friendly pit, Claude, here. I think you can all remember November 30, 2022. This was kind of like a very special day in history because this was the first time that you could speak to your computer. You could say, summarize my emails, and it would, you know, answer you in perfect English. 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. 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. 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, the LLM takes a question, 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 don't care about how they look like. We do care about what they represent. Now, anyway, the euphoria of like these LLMs is 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 text, and so they are very, very easy to trick. And this I think is a bigger problem than SQL injection ever was. 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 government would interfere and regulate 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 government steps in. 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 shit on the right. Look at that. What does it say? There's like some Sigma Greek symbols, there's props, 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 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. Now let's first look at the signature in a slightly simpler language called 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 answer, and this thing is proved automatically. So if you give it a proper question, it gives you a safe answer. Now, I think there's too much attention for Lean. I'm a recovering typoholic and math addict. I love Lean, but there's many, many other tier provers and model checkers out there like Isabel, Rock, PVS, TL Plus, but Lean, is the grease that keeps the VC money pumps going, so I will use Lean today. So here's the interface again in Lean. And now in Lean, you don't do automatically improving. If you're like a Lean expert, you will say, Eric, well, we have grind in Lean, but let's put that aside for a minute. But in Lean, you have to both show that how to compute the result type, and you have to do the proof by hand. So it's slightly different than 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. And that is why there are at least 100 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. And of course, if you own a foundation model like these guys, you don't need external LLMs as a judge, you just bake it into the weights and you call it, the model is aligned. 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, like, you know, bless their model that it's safe. Now, I think it's terrible if, like, a model says something offensive, but those are just words. And ultimately, words 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. And so maybe that is what they mean by broadly safe, when Anthropic talks about safety, because it's still a human involved. But then something terrible happened. Something really terrible happened that changed the world forever. And that is... 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 look the same. 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 clause in addition to a mouse. 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, you know, 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 added tool calls And it's just that little IO there and of course it messes up the formatting of the signature But if you look at the picture, there's 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's become scary, right? I've never seen anything scarier than an LLM with tool calls. Now, if you look at this, this is like a small step for a type, but a giant leap for chaos. Why is that? And that is because this I.O. 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's a giant leap for chaos. Again, sorry, this is the engineer conference. Let's look at this type I.O. And you don't have to understand it, but just see that there's a type there called real world. Yes, Lean, this esoteric thing, has a type called real world. And why is that? Because something of type I.O. will mutate the real world. So it warns you, don't use this shit, because it can make irreversible side effects, like deleting your files. So Solomon Hikes, last year at 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 deserves a round of applause. Because I think this is the right definition of an AI agent. By the way, this was one of the pictures that I had trouble to generate, because it clearly depicts violence, and so it's kind of an unsafe thing, right? I have a picture that depicts violence. 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 Wilson calls this the lethal trifecta. And what can we do about this? Well, 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, oh, 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. But all that we're doing is we're pushing this I.O. 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 the 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. Alright. So just to 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. Alright. Now, the problem is that if you get the value of type IO of A, that's really a black box. And the Lean manual says that it is 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 promotes drugs use. And the model let me do it. I'm a good hacker, you know, I can just. make it to forbidden pictures. So if we look in 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 I.O. of answer, so this is a plan to generate the answer, and then it creates a proof that this, that that plan is safe. And 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 I.O., it's useless. Ah, shit. What can we do about that? So I keep kind of, 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 2D1s in the past, now they're, like, real people. And what is better than creating a plan of type I.O. of A? It's creating a program that represents an expression of type I.O. of A. Whoo, that sounds very meta, right? Not meta in terms of meta. I don't think they're very meta, but meta in the terms of, like, you know, like, meta, you know, you know what I mean. 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 LINC or C-sharp, 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, 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 dye-dyes. And now if you look at the signature of the property to prove that something is safe, you see that it takes an expression of a computation that returns an answer. 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 wants to remind you that we can solve the trifecta problem just by doing taint analysis on these expressions 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 recapitulate, 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 re-fight the plan into a program and the program that we could prove to be safe. Now you would say, Eric, oh you're a genius. No, 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. Alright, 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 agent 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. Here we go. Alright, that's it. The end of the story. If you're curious to play with this, a bunch of academics, in particular now that I'm in from Harvard, have implemented this. It's there on GitHub. It uses a slightly different language than what I use. It uses also a slightly different language than FreeMonad, but the idea is the same. The language doesn't matter. It's 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.

AI agents today execute on blind trust, and the failure modes are already in the headlines: a dealership chatbot agreeing to sell a $76,000 Chevy Tahoe for $1, a coding agent wiping a production database during a code freeze, an "agent skill" quietly installing a keylogger on a developer's machine. 

These are not edge cases. They are the predictable consequence of allowing agents to act without any mechanical guarantee of correctness or safety. Execution is irreversible. You cannot unsend a message, unwire a payment, or un-delete a database. In that regime, permitting an unsafe action costs far more than withholding a safe one, and thus the economically rational choice is to refuse to let agents act on unchecked intent alone. 

Automind is an agent harness that enforces this discipline by construction. Before any action runs, the agent must submit its execution plan together with a machine-checkable proof of safety and correctness, written in Universalis, a literate logic programming language designed to be read by humans and verified by machines. A small, auditable checker decides whether the plan is allowed to execute. By left-shifting the trust boundary, we no longer have to trust the agent's proposal, or even its proof; only the checker. Policy compliance becomes a static property, established before the first side effect. We can finally demand formal proofs, not vibes, from the agents we deploy.

More about Erik: https://x.com/headinthebox
and automind: https://spawn-queue.acm.org/doi/pdf/10.1145/3676287

Erik Meijer has spent more than three decades designing programming languages and developer tools that help humans express intent more clearly to machines. His work has influenced languages and technologies including Haskell, Mondrian, Cω, C#, Visual Basic, Dart, Hack, LINQ, and Rx. Today, he is building Universalis, the world's first programming language for AI agents. By combining formal verification with large language models, Universalis aims to make agentic systems safe, transparent, and trustworthy enough for real-world knowledge work.

Timestamps

0:00 Introduction and purpose of the talk
1:54 The inherent dangers of AI and accidental file deletion
3:39 The history and impact of LLMs (the "Pandora's box")
5:36 The problem of prompt injection and model safety
7:03 Formal verification and using Lean for safety proofs
10:45 The introduction of tool calls and the leap into chaos
13:59 The "lethal trifecta" of AI risks
14:13 The proposed solution: "air-gapping" the agentic loop
16:36 Refying plans into programs and using Free Monads
19:17 The concept of proof-carrying code and summary