# In Code They Act, In Proof We Trust — Erik Meijer — session 2026-06-30T23:50:00.000Z → 2026-07-01T00:10:00.000Z

_31 transcript lines · 0 slides · source: full recording_

## Transcript

And then once we've done the program design, we can do this thing called vertical slices, which is the order of implementation, multi repo coordination, how we're gonna build this across our entire system and how are we gonna check it along the way. I've talked a little bit about how models have horizontal plans. I won't go too deep into it. If you want to learn more about this, you can go watch Talk from AI Engineer Miami. Couple shots of a doc like this going through the tests and the steps in between each phase. The main idea here is thirty minutes over here in preplanning and alignment can save you hours in review, and so it's actually feasible to still read every line of code. We'll skip this part. Basically, the the summary here is like you don't have too many PRs. You're drowning in PRs, you actually have too many bad PRs, because a good PR is a joy to to review. It's it's you're just reading through like, yep, this is great. This is what we discussed. This is what we talked about. But even if a PR needs 20% rework, which is generous for a lot of AI vibe coded slop, it's an emotional and intellectual burden on both the reviewer and the submitter. And so if you use model assisted planning alignment, your alignment is shorter because you use AI to get all the information at once. Your code review is faster because you aligned upfront and your coding Faster because AI did it. And so you're now you're actually really moving faster, but you're still reading everything and you're still owning the code. So closing advice, it's easy to hear all this and be a little bummed out. I really like the world where we just YOLO everything and we can just like not have to ever read code ever again. But, we're engineers and these are just constraints and models are good at certain things and they're not good at other things and so go figure out. On how to solve problems given a set of constraints. Use loops, they're great. Go solve hard problems, seek leverage. If you wanna help with this, we're building HumanLayer. HumanLayer is an AI IDE and collaboration platform. It's building blocks for your software factory, and soon to be better verifiers for software quality. We've got sort of a Figma for cloud code and codec style collaborative workspace. It walks you through the workflows for doing this sort of work, and, we are talking to design partners. We are hiring founding engineers here in San Francisco, and, These slides are live. You can go get them right now. You can try HumanLayer at humanlayer.com. It's free for small teams. Go solve hard problems in complex code bases. Thank you all for your energy. Please Welcome to the stage, the research scholar at Leibniz Labs, Eric Meyer. Well, can you go back one slide? Sorry. Alright. 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 twenty 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 got, like, you know, created a provably safe agentic harness. Or who knows? Maybe some of you have already solved it. Let me know. Oh, 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 site, pipe coding on the site. And then when my attention wait 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 When Cloud 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 Aldo'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 kind of, 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 kind of like have Some characters, like Claude and we will see Dario, Daniela, Sam, Bernie. But, the main character is is our friendly pit, Claude here. I think you can all remember, 11/30/2022. 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. 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. Alright. 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 string. 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. 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 Into 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 are very, very easy to trick. And this, I think, is a bigger problem than SQL injection ever was. But it was not Injection only that's 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? 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. Unsolve it before, you know, the 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 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 are writing, like, multibillion dollar checks if you just say that you're doing something with lean. And, of course, these PhD type 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.

## Slides