Comment by hershel

Here they describe it in detail:

http://ertos.nicta.com.au/research/l4.verified/proof.pml

Basically they plugged a lot of the possible holes, but it's not done yet.