[kevlar700]

SPARK is free for all to use and is open source. They chose to pay for Adacores pro support services and verified pro Ada compiler over the FSF GCC/Gnat Ada compiler. Spark is actually part of the Gnat compiler (compatibility) but actually the slower analysis is done by gnatprove thereby keeping compilation and iterative development fast. Nvidia can certainly afford to do so of course.

[simon4ada]

AdaCore's pro support includes more recent releases and, in case of problems, wavefronts. That said, the free version is fairly recent, and you can get community (and sometimes vendor) support.

[SkyMarshal]

What are wavefronts? Not getting many search results on that, besides a few github issues mentioning them.

https://github.com/AdaCore/RecordFlux/issues/955

https://learn.adacore.com/search.html?q=wavefront&check_keyw... (nada)

https://docs.adacore.com/spark2014-docs/html/ug/search.html?... (nada)

https://github.com/AdaCore/spark2014/issues?q=wavefront%20 (nada)