The CertiKOS project aims to develop a novel and practical programming infrastructure for constructing large-scale certified system software. By combining recent advances in programming languages, operating systems, and formal methods, we hope to attack the following research questions: (1) what OS kernel structure can offer the best support for extensibility, security, and resilience? (2) which semantic models and program logics can best capture these abstractions? (3) what are the right programming languages and environments for developing such certified kernels? and (4) how to build automation facilities to make certified software development really scale?