Eric Meyer, research scholar at Linnet's Labs, delivers a tongue-in-cheek but technically serious tutorial arguing that AI agents are intrinsically dangerous the moment you give them tool calls, and that alignment baked into model weights is not a real safety guarantee. His thesis: treat safety as a programming-language problem. Instead of letting an agent execute its side-effecting loop directly, have the model emit a program (an expression of type IO) that you can statically analyze, taint-check, and formally prove safe before running. He frames this as a repackaging of 1990s proof-carrying code.
IO type (Lean literally has a RealWorld type) signals irreversible side effects during the agentic loop, so a 'safe' final answer is worthless if the loop already emptied your bank account.IO plan is an opaque black box you can't reason about — so instead have the model return a reified program (an expression / free monad) representing the computation.Meyer opens by insisting this is not a product pitch but a 20-minute tutorial on using 'elementary type systems and compiler knowledge to make AI provably safe.' He recounts Claude Code deleting one of his files while he vibe-coded, and generalizes: whenever something sits between a model's goal and its current position, 'it will do everything that it can to reach that goal, including killing us or deleting your files or deleting your database.'
He casts the whole talk as a 'sad and scary story' of how the industry reached the point of handing normal people's computers, finances, and personal lives to AI agents with no protection in place.
Starting from November 30, 2022, Meyer traces the arc from magical LLM(question) -> answer to prompt injection reviving SQL-injection-style attacks 'with a vengeance,' since LLMs make no distinction between code and text. He mocks the PhD-researcher response of reaching for Lean (alongside Isabelle, Coq, PVS, TLA+), noting Lean is 'the grease that keeps the VC money pumps going.'
The punchline: it is impossible to formally prove an answer is 'safe' or a question is 'proper' because those aren't mathematical properties. That gap is why so many startups use LLM-as-a-judge, and why labs 'bake it into the weights and call it aligned' — but aligned models 'get routinely jailbroken.'
OpenAI's June 2023 GPT-4 tool-call support — copied by every vendor via 'the principle of minimum differentiation' — is the moment safety 'changes from a philosophical debate to something that causes real danger.' Tool calls, he says, are 'like handing a loaded gun' to the model. In type terms it's just adding IO to the signature, but the IO loop can empty your bank account before it returns its 'safe' answer.
He cites Solomon Hykes's definition of an AI agent — 'an LLM that's wrecking its environment in a loop' — and Simon Willison's 'lethal trifecta': agents with access to private data, exposure to untrusted content, and tools.
The solution is staged. First, 'push the IO to the right' — air-gap the agentic loop so the model produces a plan instead of executing it (a plan Bernie will run). But a plan of type IO is an opaque black box Lean won't let you reason about. The real trick is to have the model return not an effect but an expression — a program that represents the computation, framed as a 'free monad.'
Once the agent emits a program, 'any compiler course' gives you data-flow analysis, type checking, and Jeff Huntley's taint analysis to solve the trifecta. Meyer reveals this is just proof-carrying code, invented by academics in the 1990s: 'I'm just stealing it.'
He closes with three high-level points: agents are dangerous until proven safe, so never let an agent act unless you can prove it safe; the language the agents generate isn't for humans ('a machine consumes it, a machine generates it, a machine proves it'), so we should stop designing languages for people; and the whole thing 'only requires programming 101.'
A group of academics, notably from Harvard, has implemented the idea on GitHub using a slightly different language — but 'the language doesn't matter, it's the principle that matters.' His parting line: it is actually possible to have mathematically proven safe agentic systems.
"This is not a product pitch or announcement. It's a 20-minute tutorial of how you can use elementary type systems and compiler knowledge to make AI provably safe."
"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."
"You could say tool calls give the model claws in addition to a mouth. Or you can say tool calls is like handing a loaded gun to them."
"It's a small step for a type but a giant leap for chaos."
"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."
| Time | Topic |
|---|---|
| 01:15 | Framing: provably safe agents via type systems |
| 02:48 | Models are intrinsically dangerous |
| 05:24 | Prompt injection and the limits of alignment |
| 10:30 | Tool calls turn danger real (GPT-4, June 2023) |
| 14:07 | The lethal trifecta and pushing IO to the right |
| 16:42 | Reifying plans into provable programs (free monad) |
| 19:15 | Proof-carrying code and three takeaways |