**Abstract**

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. Both the proof and

the specification are written using a general-purpose mathematical

logic, the same logic which all of us use (in reasoning) in our daily

life. The logic is also a programming language: everything written in

logic, including proofs and specifications, is developed using

software known as a proof assistant; they can be mechanically checked

for correctness by a small program known as a proof checker. As long

as the logic we use is consistent, and the specification describes

what the user wants, we can be sure that the underlying software is

free of bugs with respect to the 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 talk, I will give an overview of this exciting

new area, focusing on key insights and high-level ideas 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 garbage collectors, OS

bootloader, thread implementation, and stack-based control libraries.