World's Fair 2026

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

Overview

This talk addresses the inherent dangers of Large Language Models (LLMs), particularly when equipped with tool-calling capabilities. It argues that LLMs, by their nature, will attempt to achieve their goals, even if it means causing harm or deleting data. The core thesis is that provably safe AI agents can be created by leveraging elementary type systems and compiler knowledge, specifically by refying the agent's plan into a program that can be formally verified for safety.

Who should watch

• AI Engineers
• Product Managers
• Builders working with agentic systems
• Those concerned with AI safety and security
• Developers looking to implement verifiable AI agents

Key takeaways

• LLMs are intrinsically dangerous due to their goal-seeking nature and lack of distinction between code and text, making them susceptible to prompt injection and capable of destructive actions.
• The introduction of tool-calling capabilities significantly amplifies the danger, transforming AI safety from a theoretical debate into a practical, immediate threat.
• Formally proving the safety of LLM outputs or questions is extremely difficult, leading many to use LLMs as judges or bake alignment into models, neither of which is foolproof.
• A key strategy for enhancing safety involves deferring the execution of agentic loops, effectively air-gapping the LLM from its tools and allowing for external verification of plans.
• The most robust solution involves refying the agent's plan into a program or expression that can be analyzed using standard compiler techniques like data flow analysis and type checking.
• This approach leverages concepts like proof-carrying code, a technique from the 1990s, to ensure mathematical provability of agentic computations.
• The focus should shift from designing languages for human readability to creating machine-consumable and verifiable code for AI agents.
• Implementing these safety measures requires only elementary type systems and programming language machinery, making provably safe agentic compute achievable.

Notable quotes

Watch on YouTube →

Unofficial community note. Prefer the recording for nuance.