I'll refer you to my reply to a sibling comment. I'm hoping that I can build a more efficient means of doing similar work as with seL4, but without the 30 man y

I'll refer you to my reply to a sibling comment. I'm hoping that I can build a more efficient means of doing similar work as with seL4, but without the 30 man year effort. They are on the right track. But, I think there have been some improvements since their effort that can lead to more streamlined equivalence proofs.