So one kinda cool direction is what they do for the sel4 prject. They have a sequence of high to low level impls and prove correctness wrt spec of the high lev

So one kinda cool direction is what they do for the sel4 prject. They have a sequence of high to low level impls and prove correctness wrt spec of the high level etc and prove that each lowering is an implementation of a refinement of the higher level implementation