When SeL4 came out, the proofs were much more limited. IIRC we are now largely waiting for advancements on mixed criticality and multicore proofs. Is the proof process expected to force API changes? Is there no value in a high assurance (but not verified) “beta” version being released first?
There is no need to wait, there are multiple high assurance products out there for seL4 already that work with the current version of verified features, and there are also products out there that use unverified features of seL4, such as multicore (currently mostly the SMP configuration).
For the features that currently are undergoing verification (e.g. MCS and multikernel as you said), we don’t expect major changes from the proofs. If at all, only minor tweaks. MCS overall might see more design changes as people gain more experience with it, but not from the proofs – the design-level proofs are already done for MCS.
This is not at all obvious from SeL4’s communications. For a time, I kept up on every SeL4 and CHERI related paper. I have watched (albeit in the background) every SeL4 conference talk. The website talks about the verification timelines for the above features, it does not present them as ready for use by implementers.
If I don’t know about this, then virtually no one outside SeL4 circles knows about it.