SPARK Pro 是 Altran Praxis 和 AdaCore 联合开发的产品，它为工程高可靠性软件提供了语言、工具集和设计规范。开发者表示，SPARK Pro 的新版本 11 在处理函数和证明函数的方式上提供了许多增强功能。据说这些更改通过消除以前手动编码的大部分规则来提高项目效率。 主要变化包括更强大的用于指定证明函数的语言，以及在任何证明上下文中使用这些函数的能力。 这大大简化了为关键软件编写和维护功能合约的任务，从而以更低的成本提供更高的保证。 SPARK Pro 将 Altran Praxis 的 SPARK 语言和验证工具与 AdaCore 的 GNAT Programming Studio 和 GNATbench 集成开发环境相结合。 公司表示，SPARK 版本基于 Ada 83、Ada 95 和 Ada 2005，因此所有标准 Ada 编译器和工具都可以直接与 SPARK 一起使用
