Certified software consists of a machine executable program plus a rigorous proof (checkable by computer) that the software is free of bugs with respect to a particular specification. The conventional wisdom is that certified software will never be practical because any real software must also rely on the underlying operating system which is too low-level and complex to be verifiable. In recent years, however, there have been many advances in the theory and engineering of mechanized proof systems applied to verification of low-level code, including proof-carrying code, certified assembly programming, logic-based type system, and certified or certifying compilation. In this tutorial, I will give an in-depth overview of this exciting new area, focusing on both foundational ideas and key insights that make the work on certified software differ from traditional-style program verification. I will also describe several recent work — done by my group at Yale — on building certified thread implementation, interrupt handlers, stack-based control libraries, garbage collectors, and OS bootloaders.