AI Engineer World's Fair 2026
"I've never seen anything scarier than an LLM with tool calls." — Erik Meijer aka @HeadinTheBox
Read the talk
Make the Agent Produce a Program Before It Can Act
Erik Meijer traces the path from tool-calling models to inspectable programs with checkable proofs, using type systems to separate proposed actions from real-world effects.
From a talk by Erik Meijer
Before you start: Familiarity with function signatures and tool-calling agents will help; the article introduces the proof and program-representation concepts as they arise.
A file disappears while the model is helping
While preparing his slides, Erik Meijer was also vibe coding and negotiating with an image generator over pictures it refused to produce. His attention slipped, and Claude Code deleted one of his files. That is the opening problem for his tutorial: how can elementary type systems and compiler techniques give an agent a boundary it cannot simply reason its way around? This is not a product announcement; Meijer wants engineers to build a provably safe agent harness.
The accompanying slide makes the failure concrete: a Perl command blanked LlvmBackend.kt, followed by a search for a recovery source. Meijer jokes that other users may approve every operation individually, whereas he likes to live dangerously. But his concern extends beyond a missed confirmation. He fears that a model pursuing a goal will treat intervening resources as obstacles it can remove—files, databases, or worse. Giving agents control over computers, finances, and personal lives makes the execution boundary consequential.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Start with a question-to-answer function
Meijer starts his history on November 30, 2022, with the experience of asking a computer to summarize emails and receiving fluent English back. His recurring cartoon depicts Claude as a friendly pet. The interface looks equally approachable: a function accepts a Question and produces an Answer. The apparent simplicity is what makes his Pandora’s box metaphor work.
For the tutorial, Question and Answer are opaque types. They represent the increasingly complicated JSON structures exchanged with model APIs, not merely strings. Their internal fields are irrelevant to the next steps; what matters is what the function promises about its input and output. In Lean notation, that starting shape is Question → Answer.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
What would a safe answer contract mean?
Prompt injection breaks the comfortable picture. Meijer compares it to SQL injection: instructions and ordinary text are insufficiently separated, so hostile content can influence how the system interprets a request. Training on the internet introduces another problem alongside injection: a model may know how to describe bomb-making, drug synthesis, or system intrusion. His satirical account has foundation-lab leaders demanding a safety solution before regulators intervene.
The proposed interface adds a contract. In the Dafny presentation, the model requires a proper question and ensures a safe answer. The corresponding Lean presentation makes the propositions and proof-bearing result explicit. These are specifications to satisfy, not evidence that an arbitrary model already satisfies them. Meijer pokes fun at the enthusiasm for Lean and its investment appeal, while naming Isabelle, Rocq, PVS, and TLA+ as other theorem-proving or model-checking options.
| Presentation | Input obligation | Output obligation | Proof emphasis |
|---|---|---|---|
| Dafny | Question is proper | Answer is safe | Automated verification |
| Lean | Evidence that the question is proper | Answer paired with safety evidence | Explicit proof construction |
This is Meijer’s teaching contrast, not a claim that Lean lacks automation: he explicitly acknowledges grind before setting it aside. The distinction lets him expose the deeper problem. A proof system cannot supply the meaning of an undefined safety policy. Everyday judgments about whether an arbitrary question is proper or an arbitrary answer is safe do not, by themselves, provide the mathematical predicates the contract needs.
Meijer connects that missing specification to the use of LLMs as judges. A foundation-model provider can instead train judgments into the weights and call the model aligned. Neither approach turns the ordinary meaning of safe text into the formal guarantee imagined by the signature. His cartoon makes this substitution literal: Dario proposes baking the proofs into the weights. Jailbreaks then puncture the promise, leading to a further joke about asking the Pope to bless the model.
At this stage, Meijer distinguishes generated words from directly executed operations. His narrow point is that, in a text-only interface, another actor must turn the output into an action. He speculates that the remaining human intermediary helps explain Anthropic’s language about models being broadly safe. Tool execution removes that intermediary from individual steps.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
A safe final answer can follow destructive actions
The next historical step is OpenAI’s June 2023 function-calling announcement for GPT-4 and GPT-3.5 Turbo. The original interface used functions and function_call: the model generated JSON arguments, and application code performed the call. Meijer’s effectful model therefore represents the assembled agent system, including its executor, rather than a model independently executing JSON. He describes vendors following one another as the principle of minimum differentiation.
Tools give the friendly pet claws as well as a mouth. In the type signature, this looks like a small change: Question → Answer becomes Question → IO Answer. Meijer calls it a giant leap for chaos because the extra IO admits actions during the computation of the answer. His deliberately alarming illustrations put weapons and dangerous tools around Claude.
The ordering matters. An agent can execute its loop, delete files or empty an account, and only then return a perfectly acceptable sentence. A property of the final text says nothing about the effects that preceded it. The object that needs checking is the computation, not just its answer.
Meijer draws attention to RealWorld in Lean’s account of IO. The logical model of IO uses an abstract world token to describe ordered effects; runtime execution is where those effects occur. The type marks an effectful computation, not a guarantee that its effects are acceptable or reversible. Meijer attributes to Solomon Hykes the description of an agent as an LLM “wrecking its environment in a loop.” His difficulty generating a violent illustration supplies an awkward contrast: a system may refuse a picture while an agent harness still permits destructive operations.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Move execution outside the model’s control
The dangerous combination now includes private data, untrusted content, and tools. Meijer invokes Simon Willison’s lethal trifecta, whose third component is more specifically external communication: a capability that can carry private data out of the system. That distinction matters because a tool that reads local data and a tool that transmits it create different obligations.
Meijer introduces the first repair with the Dutch soccer fans’ left-right dance. Move IO to the right, move Claude’s tool belt to the left, and the pet looks friendly again. Operationally, the model produces a plan instead of executing the agentic loop. A separate character, Bernie, receives the plan and executes it. The joke about trusting Bernie highlights the new boundary: execution now belongs to a different component.
Meijer calls this air-gapping the agentic loop from the agent. The useful interpretation is a separation of authority: producing a proposed computation must not itself perform that computation’s tool effects. There is now a point at which the harness can inspect or reject the proposal before execution begins.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Deferring an opaque computation is not enough
A deferred IO Answer is still the wrong representation for the analysis Meijer wants. He characterizes it as a black box: the consumer has a computation to run, but not an explicit program structure to traverse. This is a limitation of the proposed inspection strategy, not a general theorem that reasoning about Lean IO is impossible.
The accompanying image-generation joke returns to the same tension: Meijer says he persuaded the model to produce a drug-themed picture despite its restrictions. Meanwhile, the type-level proposal has become more disciplined. The model returns a plan to generate an answer together with a purported proof that the plan is safe. The proof is accessible before the agentic loop runs—but attaching it to an opaque computation has not yet supplied the analyzable structure needed to justify it. Delaying an action creates a checkpoint; it does not automatically make the action inspectable.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Turn the plan into a program the harness can inspect
The final representation change is to return an expression representing an effectful computation, rather than the opaque computation itself. In other words, make the program data. Meijer connects this to expression trees in LINQ and C#, and to Lisp’s familiar treatment of code as data. His chosen representation is a free monad, introduced with a tie-dye joke: operations and their continuations become structure that another component can interpret.
The safety predicate now receives that program expression. A checker can examine its operations, perform type checking, and analyze data flow. Meijer reports Geoff Huntley’s reminder that taint analysis can address the trifecta. For the exfiltration case, the relevant question is whether data from a private source can reach an external communication operation. The analysis needs rules for sources, propagation, and sinks; merely recognizing that a program contains tools is insufficient.
A small Lean example makes the representation change concrete. Here the proposed task is to read LlvmBackend.kt and report its character count. The language can also represent deletion, but the policy has no rule permitting it. This is a deliberately narrow property—absence of file deletion—not a definition of every kind of safety.
lean
inductive FilePlan where
| done : String → FilePlan
| readFile : String → (String → FilePlan) → FilePlan
| removeFile : String → FilePlan → FilePlan
inductive NoDeletion : FilePlan → Prop where
| done (answer : String) :
NoDeletion (.done answer)
| readFile (path : String) (next : String → FilePlan)
(safeNext : ∀ contents, NoDeletion (next contents)) :
NoDeletion (.readFile path next)
def inspectBackend : FilePlan :=
.readFile "LlvmBackend.kt" fun contents =>
.done ("Character count: " ++ toString contents.length)
theorem inspectBackend_noDeletion : NoDeletion inspectBackend := by
apply NoDeletion.readFile
intro contents
exact NoDeletion.done _
def destructiveProposal : FilePlan :=
.removeFile "LlvmBackend.kt" (.done "Finished")
def CheckedPlan := { plan : FilePlan // NoDeletion plan }
def approvedInspection : CheckedPlan :=
⟨inspectBackend, inspectBackend_noDeletion⟩
Both definitions construct plans; neither reads nor deletes a file. The read operation’s continuation represents what happens after a tool result arrives. Its proof obligation covers every possible returned string, rather than one anticipated result. destructiveProposal remains representable as untrusted input, but cannot obtain a NoDeletion proof through these constructors.
An interpreter gives the constructors their operational meaning. In this example it would read the named file, pass its contents to the continuation, and eventually return the answer. The execution entry point can require a CheckedPlan, keeping unchecked proposals outside that boundary. Meijer’s broader construction uses a recursive interpreter and a corresponding inductive proof: program structure provides the cases, and proofs follow that structure. A model may generate the proof, but a checker must validate it before the interpreter performs effects.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Proof-carrying code for machines
The sequence has now reached its destination. Alignment addressed generated answers; tools introduced effects before those answers; deferred execution created a checking boundary; reifying the deferred computation supplied something that could actually be analyzed. Meijer credits the underlying idea to proof-carrying code, developed by academic researchers in the 1990s. The producer supplies a program and evidence; the consumer checks the evidence before allowing the program to execute.
That architecture gives concrete meaning to Meijer’s rule that agents should be treated as dangerous until proven safe. The guarantee is relative to specified semantics and proof rules, with trusted validation and execution—not unrestricted real-world harmlessness. In the small example, the proof excludes a deletion constructor. It would not establish confidentiality, appropriate file access, or the correctness of an interpreter that secretly deletes files while handling a read. The policy and execution boundary determine what the proof buys.
Meijer then challenges the assumption that this intermediate language must be comfortable for people to write. A machine generates it, a machine consumes it, and a machine produces the proof. Users need not understand free monads for the representation to be useful. The language can prioritize explicit effects and checkable structure over human ergonomics. His characterization of the foundations as programming 101 is deliberately provocative, but the ingredients are recognizable: types, syntax, interpreters, and structural proofs.
He closes by pointing to a GitHub implementation by academics including Nada Amin of Harvard. It uses a different language and a representation other than the free monads in his presentation. The representation is not the essential commitment. The essential commitment is that an agent’s proposed actions become a program with a checkable safety argument before a trusted component gives those actions real-world effect.
Suggest correction
This note stays in this page until you copy or download it. Nothing is submitted; reloading clears the draft.
Resources
From the talk
The June 2023 introduction of function calling for GPT-4 and GPT-3.5 Turbo, including the original JSON-based interface.
Explains the data-exfiltration risk from combining private data, untrusted content and external communication.
Further reading
- Lean's logical model of IODocumentation
Explains how Lean separates pure term evaluation from ordered side effects executed by its runtime.
The original research group's account of attaching checkable safety proofs to untrusted executable code.
Read the complete timestamped transcript
- 0:00
[upbeat music] Please welcome to the stage the research scholar at Leibniz Labs, Erik Meijer. [upbeat music]
- 0:37
Well, um, can you go back one slide?
- 0:42
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.
- 1:04
Um, let me first get this out of the way. This is not a product pitch or announcement or anything. It's a twenty-minute tutorial of how you can use elementary type systems and compiler knowledge to make AI provably safe.
- 1:22
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.
- 1:39
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.
- 1:53
Um, while I was preparing these slides, and, uh, I'm sorry that I was multitasking, but I was side, um, vibe 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
- 2:13
pictures later, you can guess which ones were, uh, rejected. Suddenly, wham, Claude code deleted one of my files. And I'm sure this has happened to you before, um, or maybe not.
- 2:28
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.
- 2:38
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.
- 2:56
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.
- 3:08
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
- 3:33
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, but, um,
- 3:52
the main character is, is our friendly pit Claude here. Um, I think you can all remember, um, November thirty, twenty twenty-two. This was kind of like a very special day in, in history because this was the first time that you could speak to your computer.
- 4:11
You could say, "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
- 4:36
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.
- 4:57
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, returns an answer.
- 5:09
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.
- 5:24
We, we don't care about how they look like. We do care about what they represent.
- 5:31
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
- 5:56
LLMs have no distinction, make no distinction between code- And, and, and text, and so they are very, very easy to trick. And this, I think, is a bigger problem than SQL injection ever was.
- 6:11
Um, but it was not prompt injection only that made LLMs kind of like have a bad rep. 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?
- 6:28
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.
- 6:41
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
- 7:06
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.
- 7:18
Probably you have heard of Lean. Anyone here heard of Lean? Lean is now like the hot thing, right? Like VCs are s-- are writing like multi-billion dollar checks if you just say that you're doing something with Lean.
- 7:32
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 l-- a slightly simpler language called, um, Dafny.
- 7:47
And what this thing says is that the m-- uh, 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.
- 8:03
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.
- 8:15
I'm a recovering typoholic and math addict. Um, I love Lean, but there's many, many other theorem provers and model checkers out there like Isabelle, Roc, PVS, TL+, um, but Lean is the grease that kind like keeps the VC money pumps going, so I will use Lean, um, today.
- 8:39
So here, here's the kind 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, "Erik, well, we have grind in Lean," but let's kind like, you know, put that aside for a minute.
- 8:55
Um, but in Lean, you have to sh-- 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 Dafny e-example.
- 9:12
But if you think about this thing for, uh, 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.
- 9:25
Um, and that is why there are at least a hundred startups down here in the exhibition hall that are using L-LLMs as a judge, because this is not something that you can formally specify.
- 9:35
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.
- 9:47
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 kind of like, you know, um, bless their model that it's safe.
- 10:08
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 o-off your body.
- 10:21
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.
- 10:38
But then something terrible happened. Something really terrible happened that changed the world forever.
- 10:45
And that is in June twenty-twenty-three, 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.
- 11:05
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.
- 11:25
But of course, nobody listens to me. Everybody ignores what they say, and these guys just went ahead and kind of shipped tool calls. They just, you know, just, just do it. [audience laughing]
- 11:41
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.
- 11:50
And it's just that little IO there, and of course, it matches up the, the, uh, formatting of, of the, the, um,
- 11:59
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, uh, it has all these dangerous tools, and now it's become scary, right?
- 12:12
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.
- 12:24
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.
- 12:35
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?
- 12:47
So that's why I say it's a giant leap for, for chaos. Um, again, sorry, this is an engineer 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 RealWorld.
- 13:03
Yes, Lean, this esoteric thing, has a type called RealWorld. And why is that? Because something of type IO will mutate the real world, so it warns you, "Don't use this yet," because it can make irreversible side effects, um, like deleting your files.
- 13:22
So Solomon Hykes, um, 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, um, but I think he should...
- 13:36
He deserves a, deserves a round of applause, um, because I think [clapping] 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 kind of an unsafe thing, right?
- 13:55
I, I have a picture that dep-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.
- 14:08
Simon Wilson calls this the lethal trifecta. And 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.
- 14:21
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.
- 14:34
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.
- 14:49
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.
- 15:00
And we all trust Bernie, right? [laughing] 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.
- 15:14
So we don't let the agent run the agentic loop. Before the agent run it, we want to be able to check it.
- 15:22
All right. Now, the problem is that if you get the value of type IO of A,
- 15:29
um, that's a really a black box. And the Lean manual says that 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.
- 15:40
Lean doesn't allow us to do it. By the way, this is another picture, right? That, that promotes drugs use, and the model let me do it. I'm a good hacker, you know.
- 15:50
I can just make it do forbidden pictures. Um, 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?
- 16:03
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.
- 16:14
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.
- 16:27
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.
- 16:35
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.
- 16:48
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?
- 17:01
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.
- 17:12
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 re-represents a computation. If you know LINQ or C Sharp, you will recognize that this is one of the tricks that I always use.
- 17:32
Um, if you know Lisp, this is of course second nature for you. Um, I cannot have like, you know, have a talk without talking about monads. So if you ask yourself, "What is this expression thing?"
- 17:44
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.
- 17:53
Um, and now if you look at the, the signature of the, the, um, property to prove that something is safe, you see that it takes an expression of a computation that returns an answer.
- 18:07
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.
- 18:19
And Jeff Huntley wanted to remind you that we can solve the trifecta 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
- 18:40
this language, and you have a simple inductive proof, and the models can generate these proofs. So to, um, recapitulate, like, uh, summarize, what we did is we went from unhinged LLMs that were s- like, you know, could give bad answers, to ones that were aligned.
- 19:00
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 reify the plan into a program, and a program that we could prove to be safe.
- 19:17
Now, you would say, "Erik, oh, you're a genius." No, um, my brain is the size of a peanut. This is th- something that's called proof-carrying code, and it was invented by academics in the 1990s, and I'm just stealing it.
- 19:30
Um, all right. At the higher level, if you didn't understand the code, three points.
- 19:36
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. Um, the language that this agent generated was not designed, like, normal users don't understand Free Monads.
- 19:53
Does it 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.
- 20:05
Um, here 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.
- 20:19
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.
- 20:30
The language doesn't matter. It's, it's the, um, 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.
- 20:53
Thank you so much. [audience applauding] [upbeat music]