quality takes time and money
This is really nice and good news.
However, the cynic in me notes that, when a recent Reg forum discussed injecting formal engineering discipline into software development, some folks were all over formal methods and how they would do away with our amateurish and non-engineering worthy practices. "It's a solved problem, we have formal methods", is almost what some seemed to be claiming.
Whatever the merits of formal methods are in this case, and I assume there are plenty, it would seem as if applying them took considerable resources and time in order to bring this project to fruition.
I hope this serves as a timely reminder to both camps. Yes, formal methods can help. But, they also don't quite seem to be a universally applicable silver bullet at the current time. Unless, of course, everyone can afford a team of 70-100 engineers and PhDs for 4 years as an entry price. Seems there is some work left for the rest of us informal slhackers ;-)
On the other hand, I really like the fact that they weeded out errors in existing libraries and can be used to do that in the future. This type of effort should be deployed more often on oft-reused core critical subsystems that have stable and detailed specs already.