Connecting things up: verified stacks
Connecting large verification projects together is a fun and worthy challenge. I've connected my work up with various completely separate projects (listed below) and that way created various verified stacks (or extensions of such).
seL4: The seL4 microkernel is a general-purpose OS developed at NICTA. The L4.verified project at NICTA has proved functional correctness of this microkernel in the Isabelle/HOL theorem prover. Their original proof verified correctness of a 10,000-line C implementation. During three visits to NICTA, I applied my decompiler to the seL4 microkernel and, together with Thomas Sewell, extended the original L4.verified proof down to the concrete machine code that gcc produces from the C code. A paper describing this work will appear at PLDI'13.
Milawa: The reflective Milawa theorem prover is a prover developed by Jared Davis. Milawa implements an ACL2-like logic but is unlike ACL2 in that it features a small LCF-like kernel. At start up, Milawa performs a long sequence of verified reflective extensions which install more elaborate kernels in place of the previous one. With Jared's help, I developed a verified Lisp runtime that is able to host the Milawa theorem prover and proved that, when his theorem prover is run on this runtime, then Milawa is sound (down to the 64-bit x86 machine code on which it runs). Click here to read more.
HOL Light: The HOL Light theorem prover is John Harrison's contribution to the HOL family of theorem provers. HOL Light implements the same logic as all HOL provers, namely higher-order logic (HOL), and aims to be a minimal and clean implementation. Harrison has formalised its logic (HOL) inside itself and proved the logic sound. Using Scott and my work on proof-producing synthesis of ML, we are working on construction of verified implementations of HOL Light. We aim to do for HOL Light what Jared and I did for Milawa. Initial results are described here.