The Trustworthy Systems group at UNSW has been doing a lot of research (and verification) of temporal isolation on seL4.