Normal, verified kernel could easily be EAL7, if someone bothered to get it certified. SMP codebase breaks assumptions that are made for the proofs, so much lower, EAL6 at most, but that would still be difficult to achieve.
Considering that the most any traditional operating system can hope to achieve is EAL4, you are DEFINITELY selling unverified seL4 short! AFAICT should qualify for EAL5 no problem and EAL6 would be achievable if it wasn’t cheaper to skip it and go for EAL7 directly.
I find this to be a VERY frustrating part of seL4’s communications: y’all hold yourself to a higher bar than anyone else on the planet. Sure, there are high-level proofs for some crypto libraries but is there any other production system that extends the proofs to the binary level? AFAIK there are no API changes anticipated from verification and thus the unverified stack would qualify as high-assurance 1.0 by any other measure.