Aristotle把形式化验证带进C与Verilog：在Tensordyne最难的模块里挖出深达11万周期的缺陷
核心概要
Harmonic将原本用于研究数学的Aristotle扩展到软件与硬件形式化验证，首批支持C和Verilog。与只覆盖部分行为的代码审查和测试不同，它用机器可检验的证明判断指定性质是否在定义系统内的所有可能输入上成立，并从代码中提出待证性质、报告哪些被证明以及每条证明依赖的假设。在Tensordyne团队认为最难验证的模块中，它找到深达110000周期的缺陷；在LibTomMath上修复三个缺陷，并使模幂运算在基准中快31–38%，加速后的代码针对同一规格得到证明。
深度剖析
形式化验证开始面向普通工程团队，而不再只是少数专家的工具，首批覆盖的语言是C和Verilog。 此前形式化验证一直缓慢且昂贵，使用范围基本限于专家。 Harmonic把已在研究数学中验证过的同一套技术迁移到软件与硬件，并称其目标是让任何工程团队都能用上形式化验证。
工具从现有代码中提出待证性质，逐条报告证明结果和证明所依赖的假设，工程师审阅后把性质提交到代码仓库，并在每次提交时于CI中运行。 代码审查和测试只检查可能行为的一部分，而形式化验证针对定义系统内的所有可能输入做数学证明。 对C，它按指定需求验证功能正确性以及若干类未定义行为的不出现；对Verilog，它覆盖控制路径的活性与安全性以及数据路径的数学性质。
在真实代码上，Aristotle在Tensordyne团队自认最难验证的模块中找到深达110000周期的缺陷。 该深度远超常规测试能触及的行为范围。 这一结果来自Tensordyne的实际模块，而非合成示例。
在Tcl与Dropbear SSH背后的大数库LibTomMath上，Aristotle修复三个缺陷，并在Harmonic的基准中使模幂运算快31–38%。 加速后的代码针对同一规格得到证明，速度提升与正确性证明同时成立。 该对比是Harmonic自报的基准结果，覆盖LibTomMath的模幂运算。
启示与展望
已展示的范围是C与Verilog两类语言：C侧验证功能正确性与若干类未定义行为的不出现，Verilog侧覆盖控制路径的活性与安全性以及数据路径的数学性质；工具今日可用，提供自助的按用量计费与企业方案。
证明结果依赖于所提出的性质与每条证明所依赖的假设，工程师需要审阅这些性质；性能数字来自Harmonic自己的基准，缺陷深度与加速幅度均针对文中点名的具体代码库。