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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.