Building certifiably hacker-resistant operating systems is widely considered a grand challenge. Many people believe that the combination of concurrency and an OS kernel’s functional complexity makes formal verification of functional correctness intractable, and even if it is possible, its cost would be prohibitive. In this talk, we present a novel compositional approach for building certified system software. We advocate abstraction over a particularly rich class of specification (called deep specification) and present new methodologies and tools for formally specifying, programming, verifying, and composing abstraction layers. Using these new technologies, we have successfully developed the CertiKOS certified OS kernel and verified its contextual functional correctness in the Coq proof assistant. CertiKOS is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. This is the world’s first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking.