Harmonic 将 Aristotle 形式化验证扩展到 C 和 Verilog

Harmonic 宣布 Aristotle 从研究数学扩展到软件与硬件，首批支持 C 和 Verilog。该工具会从代码中提出待验证性质，报告哪些已证明、哪些未证明以及每条证明依赖的假设，工程师审核后提交到仓库，并在每次提交时于 CI 中运行 Aristotle。