TL from the project here: you're right, the changes to the kernel are not yet formally verified, but that's on the roadmap -- there's quite a lot of work that has been done here, and tons more to come. The vast majority of changes we have made have involved lots of conversations with folks on the seL4 mailing list including Gernot Heiser and video conferences to work out the best way to do what we're doing.

I realize the blog post comes out pretty strongly on this topic, and that's my oversight -- I let my aspirations leak out instead of tempering them (this is not your typical PM-driven project) properly.

Please understand that this is an engineer-driven project in Research with a very small team where we're doing our hardest to do the right thing, so please bear with us.