No. See any of the papers, eg http://ssrg.nicta.com.au/publications/nictaabstracts/Elphins.... The maintenance effort is quite reasonable. They've managed to evolve, and continue to evolve, the kernel even with the ever more stricter properties proven about it.
The seL4 team certainly built tools to make the job easier. However, their work takes even more effort than the development of some early designs. Lipner and others indicated it took several quarters to turn a major change on a product. Schell's company usually quoted 2 years per new design based on their highly-assured GEMSOS kernel. The STOP OS, INTEGRITY-178B, and VxWorks MILS similarly moved slowly in new features due to assurance requirements. Now, most of these were evaluated against all kinds of security and functional criteria whereas seL4 just did development assurance: other stuff for seL4 is ongoing research at NICTA while finished for alternatives. So, in some ways it's less work and others it's a lot of work.
So, rule of thumb is that you will have these issues: less features, slower development, slower time-to-market (critical weakness), slower maintenance, less HW support, possibly worse interface/management, and performance hits potentially. Also, worst part is that anything you apply high assurance to that hasn't been dealt with in CompSci requires fresh R&D then the actual work. That with time-to-market and feature gap were huge, deal-breakers in the past.
So, all that might be fine depending on the nature of the problem. It might not even all show up in the project. Yet, you should assume it because it showed up in many projects and products before. Still does. It's just that high assurance systems are precise, labor-intensive, custom developments that also require uncommon to rare expertise. No wonder seL4 is still behind even ancient QNX in what it can pull off and is actually behind the separation kernels in functionality. Assurance target just makes it that much harder. Maybe labor available, too.
