People who don't want to read the first line of the article, rejoice!
It sounds like a good decision though. Formal verification tends to make more sense in highly concurrent situations where there is a high-value stable API to be supported. That describes graphics cards and surrounding environments really well so it makes sense that Nvidia would find use cases.
Something more from the article is also that they made the decision with a pilot project that went well. It'd be nice to have more details about it; that sort of thing is important to do well and always interesting. Lo and behold, we do have more details about it! https://blog.adacore.com/when-formal-verification-with-spark... - there is a video in there that looks to be worth a watch.
It sounds like a good decision though. Formal verification tends to make more sense in highly concurrent situations where there is a high-value stable API to be supported. That describes graphics cards and surrounding environments really well so it makes sense that Nvidia would find use cases.
Something more from the article is also that they made the decision with a pilot project that went well. It'd be nice to have more details about it; that sort of thing is important to do well and always interesting. Lo and behold, we do have more details about it! https://blog.adacore.com/when-formal-verification-with-spark... - there is a video in there that looks to be worth a watch.