[seL4] active development and verification

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