seL4 Summit 2026

The emergence of formally verified building blocks across the stack, from memory-safe languages to verified microkernels like seL4, represents a hard-won foundation. But it raises a deeper challenge: local correctness does not translate to system reliability. Each component may behave exactly as proven, while the system as a whole remains unpredictable.

This talk introduces Software Understanding as a new discipline: the science of formally verifying that software-controlled systems perform correctly across normal, abnormal, and hostile conditions, and making that reasoning legible across the teams responsible for them. As critical infrastructure becomes increasingly autonomous and AI-driven, the gap between what we build and what we can reason about continues to widen. Closing that gap requires more than proof; it requires bringing mathematical rigor into the pace and complexity of real-world operations.

Drawing on lessons from national security and mission-critical systems, this talk examines what it will take to move formal methods from technical scripture to organizational discipline, and why verified microkernels like seL4 are not the end of the story, but the beginning.

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. I'll argue that FM 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, I'll make 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. I'll show — not just tell — 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.