Agents Must Prove Safety Before Execution, Not Just Be Aligned

Erik Meijer argues AI agent safety is broken: tool calls let models mutate the real world (delete files, empty accounts) without verifiable guardrails. Alignment and guardrails are probabilistic, so they can’t guarantee safety. The fix: have agents generate pure plans as programs and statically verify them with proof-carrying code before execution.

The technique isn’t new—it’s repurposed from 1990s academic work—but it directly addresses the “lethal trifecta” of private data, untrusted content, and tool access. By defining safety properties as types and proving plans satisfy them, safety becomes a deterministic check. It requires a domain-specific language and a verifier that runs before execution.

The talk is a technical tutorial, not a product launch. The underlying code is an academic prototype; production readiness is unclear. The biggest adoption hurdle is organizational: teams will need compiler and PL expertise alongside ML engineering. The verification harness itself becomes a trust base that must be secured.

The implication is that responsible agent deployment may soon require a proof infrastructure, much like memory safety became a baseline. Ignoring this could leave teams exposed to catastrophic agent failures.