Aristotle把形式化验证带进C与Verilog：在Tensordyne最难的模块里挖出深达11万周期的缺陷
Harmonic将原本用于研究数学的Aristotle扩展到软件与硬件形式化验证，首批支持C和Verilog。与只覆盖部分行为的代码审查和测试不同，它用机器可检验的证明判断指定性质是否在定义系统内的所有可能输入上成立，并从代码中提出待证性质、报告哪些被证明以及每条证明依赖的假设。在Tensordyne团队认为最难验证的模块中，它找到深达110000周期的缺陷；在LibTomMath上修复三个缺陷，并使模幂运算在基准中快31–38%，加速后的代码针对同一规格得到证明。