Keyword here is "automated". Quoting, "In the end, the Verve design, implementation, and verification described in this paper took just 9 person-months, spread between two people". This is considerably less than, say, seL4, which took 20 person-years(!). Well, seL4 is larger than Verve, but still.
It's disappointing that little verified OSs like these don't show up little boxes that need them, such as home DSL routers, printers, webcams, and various IoT devices. Those all have one job, and run a fixed program or programs. You want them to do that one job and nothing else. Not act as attack vectors against other systems.
(2010)<p>Whatever happened to that? Several papers in 2010, then nothing. Wikipedia says there was a 2013 release.<p>Microsoft had a later project, Ironclad (2014) which built on that to build some simple applications.[1] That's an active project at Microsoft.[2]<p>[1] <a href="https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-hawblitzel.pdf" rel="nofollow">https://www.usenix.org/system/files/conference/osdi14/osdi14...</a>
[2] <a href="https://www.microsoft.com/en-us/research/project/ironclad/#" rel="nofollow">https://www.microsoft.com/en-us/research/project/ironclad/#</a>
Reminded me of this bit from Guido van Rossum's PyCon 2012 keynote:<p><a href="https://youtu.be/EBRMq2Ioxsc?t=1374" rel="nofollow">https://youtu.be/EBRMq2Ioxsc?t=1374</a><p>"I know my operating system kernel will never be proven correct."