Erik Meijer separates an agent's uncertain language-model reasoning from the trusted system that performs external actions. Instead of executing a tool callAI tool calling lets a model request a structured operation from software instead of only returning natural-language text. immediately, the agent builds a deferred program that can be inspected, transformed and checked first.
He connects this design to free monads, proof-carrying codeFormal verification uses precisely stated properties and logical methods to check whether a system or argument satisfies those properties. and policy enforcementA guardrail is a technical or procedural control that limits unsafe, disallowed, deceptive, or otherwise unwanted AI behavior.. Safety claims travel with the proposed action, while a smaller trusted base verifies those claims before granting effects such as network access, file changes or financial transactions.
The approach does not make model output reliable by itself. It moves critical guarantees into explicit interfaces and verification steps, where software can reject unsafe behavior even when the model is confused, manipulated or maliciously prompted.
Watch on YouTube
