一句话看懂：Wired 报道，一批初创公司正用生成式 AI 降低“形式化验证”的门槛，试图让软件用数学证明来减少漏洞；但这项技术目前仍处原型阶段，成本和落地方式都还不确定。
事件核心：发生了什么
据 Wired AI 报道，斯坦福研究者 Chuyue Sun 与同行开发了一款 AI 工具，在不到半天、花费不到 500 美元的条件下完成了一个工程项目；同样工作由三名熟练专家手工完成约需五个月。该结果来自 Sun 近期论文。Sun 于 8 月加入初创公司 &Truth，该公司已融资 7000 万美元，目标是最终能验证任何编程语言，并演示了用 AI 验证 Signal 加密通信部分代码。
竞品 Harmonic 由 Robinhood CEO Vlad Tenev 联合创办，融资 2.95 亿美元。该公司称其数学导向 AI 智能体 Aristotle 支持验证 C 语言软件和 Verilog 硬件设计，并正与 Tensordyne、Nvidia 等潜在用户评估合作。此外，Anthropic 与验证初创公司 Theorem 上周联合宣布，用 AI 协助发现开源软件中“数万亿次测试未检出”的 bug，并为 Claude 推出验证插件；首批项目成本未披露。
为什么重要
形式化验证要求把代码目标写成精确陈述，再转成可验证的数学公式，长期以来只用于波音飞机、亚马逊服务器、苹果设备等安全关键场景。AI 若能把撰写证明和转换公式的繁重工作自动化，就有机会把这套方法从少数核心系统扩展到更广泛的软件开发流程。对正在用 Vibe Coding 快速生成代码的开发者来说，这相当于补上一道“数学检查”，而不是只依赖常规测试。
但行业分歧明显。Antithesis 创始人 Will Wilson 称形式化验证对数学爱好者是“陷阱”，其公司花费数百万美元验证自身网络安全防御，过程“极其痛苦”，且仍用自家工具发现了额外错误。以太坊创始人 Vitalik Buterin 也公开表示“形式化验证不是万灵药”，但仍认为它是防御 AI 发动网络攻击的重要一环。
对用户/开发者/创作者的影响
普通用户短期不会直接感知变化，但若验证成本下降，支付、通信、云服务等底层软件的安全性可能逐步改善。对开发者而言，目前公开信息显示这些工具多处于原型或评估阶段，适合先在安全相关、容错要求高的模块试用，不宜替代完整测试。中型科技公司向 Wired 反映，验证工程师短缺、成本高于潜在风险，以及等待数周验证可能拖慢创新，仍是采用障碍。
AI 工具推荐
想把多个 AI 模型放在一个入口？
GamsGo AI 集成 ChatGPT、DeepSeek、Gemini、Claude、Midjourney、Veo 等常用模型，适合写作、绘图、视频和日常 AI 工作流。
推广链接：通过此链接购买，我可能获得佣金，不影响你的价格。
值得关注的后续
一是 &Truth 和 Harmonic 的客户名单能否从评估转为正式采购，定价是否公开；二是 Anthropic 与 Theorem 的 Claude 验证插件能否形成可复用的开发者工作流；三是形式化验证能否覆盖用户误操作和硬件故障等非代码类问题，目前专家对此仍存疑。
来源：Wired AI
