Formal methods have long promised strong security guarantees for critical software, yet their adoption in industry remains limited: the cost of proving every line of code is too high for most real-world programs. This talk presents a different approach: using the isolation guarantees of a formally verified microkernel as a practical, deployable security primitive, without requiring proof obligations on the application code itself.

We describe our experience building production systems on Kry10 OS, a capability-based operating system built on the seL4 microkernel, the world's first formally verified OS kernel. seL4's proofs guarantee that the kernel correctly enforces inter-component isolation: no component can access the memory, resources, or capabilities of another unless explicitly granted permission. Kry10 OS exposes these guarantees through a structured platform that lets architects reason about security at the component boundary, rather than line by line.

The central insight is that this shifts the assurance burden significantly. Rather than proving the correctness of all application code — an often intractable task — engineers can decompose a system so that even untrusted or unproven components are tightly constrained in the damage they can do. The kernel's proofs guarantee that a component cannot exceed its granted capabilities, so an attacker who compromises one component does not automatically gain material advantage into others. Attacks can still propagate, but only by finding and exploiting a vulnerability at each boundary in turn: a much higher bar than in a monolithic system, and one that shrinks the trusted computing base to something an engineer can actually reason about. Where a boundary handles untrusted input, this residual risk can be closed further by pairing seL4's isolation with formally verified parsers, eliminating entire classes of boundary vulnerabilities. This is formal methods made usable: targeted, composable, and grounded in deployed systems rather than research prototypes.

We illustrate this through case studies drawn from systems we have built and deployed. These span domains with markedly different threat models and safety requirements: from network-facing infrastructure requiring strong information-flow guarantees to resource-constrained embedded platforms where real-time behaviour and fault isolation must coexist. Together these show how the same architectural principles apply across diverse critical applications.

For each, we discuss how the component decomposition was designed, which properties were enforced by the kernel and which required additional assurance effort, and what developing within this model was actually like. We are honest about the challenges: the shift from monolithic or POSIX-based development, the tooling maturity curve, and the effort of decomposing complex subsystems.

Capability-based isolation is not a silver bullet, but it is a deployable improvement in secure-by-design engineering that closes the gap between what formal methods can realistically deliver today and what developers and systems architects actually need. We aim to leave you with a concrete understanding how seL4-based isolation applies to real systems, what it does and does not guarantee, and how to compose verified and unverified components in a principled way.