A question I had about how the sel4 project is run internally: What is your process of developing ongoing changes and how does verification fit into it? Do you maintain the proofs with kernel modifications on an ongoing basis? On a semi-regular basis?
Is the "experimental" branch verified? When time slices are no longer global, will those changes be verified? etc...
Tim