Does this offer any advantages to Ada/Spark? Having worked in formal method environments there's a lot to be said of a tool that's been around for a while. Even

Does this offer any advantages to Ada/Spark? Having worked in formal method environments there's a lot to be said of a tool that's been around for a while. Even with formal methods you can still have bugs and there's a risk in using new tools. Without getting those millions of hours of development time it's hard to know a tool really works regardless of the theory behind it.