Axiom以16亿美元估值融资2亿美元，用“形式化验证”打造可信AI编程助手

硅谷初创公司Axiom在成立仅一年、团队约20人规模之际，成功完成了由Menlo Ventures领投的2亿美元A轮融资，估值高达16亿美元。该公司致力于开发名为“Verified AI”的系统，其核心创新在于利用形式化验证技术，确保AI生成的代码具备数学意义上的确定性正确性。Axiom的系统基于编程语言Lean构建，能够对AI生成的每一个推理步骤进行机器检查，从而确定性地捕获错误，而非依赖传统统计方法。该公司最初在数学证明领域进行技术训练，随后将这一能力迁移至代码验证领域。这项技术不仅能证明代码产生正确的输出，更重要的是，它能从理论上证明代码不会引入意料之外的安全漏洞或攻击面，为高安全性应用场景（如金融、基础设施、操作系统内核等）的自动化编程提供了新的解决方案。此举标志着AI辅助软件开发正从“概率正确”迈向“可证明正确”的新阶段，对软件工程的安全性与可靠性范式可能产生深远影响。