From Proof to Product: Why Formal Methods is Finally Ready

For most of its history, formal methods has been a discipline of proof rather than product: rigorous, powerful, and largely confined to academia. That is changing rapidly.

At the seL4 Summit in Vancouver in September 2026, Martin Dehnel-Wild argued that formal methods is finally ready to deliver secure, resilient systems in the real world, and that the obstacles left are largely self-inflicted: a history of over-promising, tools that are painful to use and barely interoperate, and a habit of staying in the lab rather than supporting customers through real, evolving deployments.

Drawing on systems we're building today for a wide range of government and commercial partners, Martin made the case that security is fundamentally an economic argument rather than a quest for perfection: the goal is to make attacking a system so costly that adversaries focus elsewhere. Reaching that at scale depends far less on stronger proofs than on ruthless attention to wider adoption: on meeting real customers in the messy, changing environments they actually deploy into.

Regardless of your views on AI, it is rapidly lowering the barrier to entry. In his keynote presentation, Martin demonstrates what becomes possible when modern AI is combined with formal tools and seL4. This is a talk for anyone who wants formal methods to matter beyond academia.

Watch here: