用数学证明代码无 bug：AI 能否让形式化验证走出关键系统

斯坦福研究者 Chuyue Sun 用 AI 工具在不到半天、花费不到 500 美元的情况下完成了一项工程任务，而三位资深专家手工完成同样工作需五个月。她加入的初创公司 &Truth 已融资 7000 万美元，并于周四公开亮相，目标是最终能验证任何编程语言。竞争对手 Harmonic 本周宣布其数学 AI 智能体 Aristotle 支持验证 C 语言软件和 Verilog 硬件设计。