凭借这个新版本的 SPARK Pro 工具集，AdaCore 向着高效且愉快地编写经过验证的软件的目标迈进了一步。 作为其新的 SPARK Pro 16 集成开发和验证环境的一部分，AdaCore 进一步简化了软件工程师向更多依赖静态验证和形式证明的过渡，而无需具备数学逻辑方面的专业知识。 SPARK Pro 16 还增强了对 SPARK 2014 语言特性的覆盖，现在支持 Ravenscar 任务配置文件，从而将形式验证方法的好处扩展到 Ada 2012 并发编程功能的安全子集。 这个新的 SPARK Pro 可以生成无法证明的验证条件的反例，从而使开发人员更容易找到功能代码或提供的合约中的缺陷。 最后，SPARK Pro 16 还改进了对按位/模运算的处理，并且该产品的证明引擎现在包括 Z3 SMT 求解器。