This proof establishes that seL4's abstract specification is a formal refinement (i.e. a correct implementation) of its capDL specification. It is described as part of an ICFEM '13 paper.
To build from the l4v/ directory, run:
./isabelle/bin/isabelle build -d . -v -b DRefine
The top-level theory where the refinement statement is established over
the entire kernel is Refine_D; the state-relation that
relates the state-spaces of the two specifications is defined in
StateTranslation_D and the basic
correspondence property proved over each kernel function is defined in
Corres_D.