Michael was working on verifying functional correctness for the MCS version of seL4. He is now at Proofcraft.
More contact information is available at the Contact page.