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.