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:
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 and here.