SeL4 was not built for multiple CPU cores, it's not going to perform with modern day "high end" hardware and last I looked its formal proofs don't apply to multicore systems.