当 AI 开始大规模生成代码、自动发现漏洞，甚至自主执行攻击任务时，传统依赖扫描、测试和修补的软件安全机制，正在面临新的挑战。

一种已有数十年历史的技术——形式化验证（Formal Verification），因此重新受到关注。

近日，AI 软件验证初创公司 &Truth 宣布结束隐身研发阶段（Stealth Mode），并获得 7000 万美元种子轮融资。公司试图利用 AI 与数学证明技术，实现软件安全性与正确性的自动化验证。

这笔融资值得关注的，不仅是金额，更是其背后正在发生的技术变化：AI 能否让过去成本高昂的形式化验证，成为一种可以规模化应用的软件安全能力？

01.从发现漏洞，到证明软件安全

传统软件安全主要依赖代码审查、漏洞扫描、渗透测试和持续修补。这些方法可以不断发现问题，却很难证明软件在所有可能的运行条件下都符合特定安全要求。

形式化验证提供了另一种思路。

它利用数学逻辑、形式化模型和定理证明，验证软件是否满足预先定义的功能与安全属性。

例如，对于身份认证系统，传统测试可以检查大量合法与非法访问场景；形式化验证则尝试从数学层面证明，在明确的模型与假设条件下，未经授权的用户无法获得相应权限。

这并不是一项新技术。形式化方法早已应用于航空航天、芯片设计、操作系统等高可靠性领域，seL4 微内核就是具有代表性的成果。

但长期以来，形式化验证依赖专业研究人员进行建模和证明，成本高、周期长，难以在普通商业软件中普及。

AI 的出现，可能正在改变这一局面。

02.AI 正在改变形式化验证的成本结构

&Truth 的核心技术方向，是利用 AI 自动完成部分过去依赖人工的形式化建模、证明构造和验证工作。

公司以开源定理证明系统 Lean 为技术基础，结合 Mathlib 等开源项目，开发面向不同软件系统的自动化验证能力。

其中一个重要环节，是通过 Specification Factory，将自然语言描述的需求转换为机器能够理解和验证的形式化规格说明（Formal Specification）。

按照公司的公开介绍，AI 已经能够显著提高部分形式化证明任务的效率，而其自动化技术希望进一步将过去需要数月甚至数年的验证工作，压缩至数小时或数分钟。

这些效率提升仍有待独立验证，但其技术方向具有明确的产业意义。

如果形式化验证能够摆脱对少数专家的高度依赖，就有机会从高成本、定制化的专业工程，逐渐进入日常软件开发和 DevSecOps 流程。

03.学术团队与 7000 万美元融资

&Truth 成立于 2026 年，总部位于美国 Palo Alto，并在 Singapore 设立国际总部。

其创始团队具有较强的形式化方法与自动推理研究背景。

联合创始人 Clark Barrett 是 Stanford University 计算机科学教授，长期研究自动推理与形式化验证；Ilya Sergey 曾在 National University of Singapore 创立 VERSE Lab，专注于程序验证与编程语言研究。

团队还包括 Lean 4 共同架构师 Sebastian Ullrich，以及具有投资与企业管理背景的联合创始人 Chris Hsu。

&Truth 的目标并非推出另一款传统漏洞扫描产品，而是构建能够大规模验证软件正确性与安全属性的平台。

7000 万美元的种子轮融资，也反映出资本市场开始关注 AI 与形式化方法结合的商业潜力。

不过，公司目前仍处于早期阶段，其实际商业客户、规模化部署能力与长期商业模式，还有待进一步验证。

04.AI 安全为什么需要形式化验证？

AI 对网络安全的影响，正在同时发生于软件开发和攻击两个方向。

一方面，AI Coding 大幅提高代码生产速度，软件规模和变化频率持续增加；另一方面，AI 也在提高漏洞发现、利用与自动化攻击的效率。

当开发与攻击都开始以 Machine Speed 运行，安全验证机制也需要相应升级。

尤其在 Agentic AI 场景中，AI 不再只是生成内容，而是能够调用工具、访问数据、执行代码，并对真实系统产生影响。

如何确保 AI Agent 不会突破既定权限边界？如何保证关键操作始终满足安全约束？

形式化验证有机会在这些问题上发挥作用。

例如，通过数学证明验证权限控制逻辑、执行环境隔离性、关键状态转换及特定安全约束，为 AI 系统提供更强的确定性保障。

但形式化验证并不意味着能够证明整个 AI 系统绝对安全。

证明的有效性始终依赖于模型、规格说明及其前提假设。即使软件满足已经定义的安全属性，也不代表这些属性覆盖了全部真实风险。

因此，形式化验证更可能成为 AI 安全体系中的重要基础能力，而非替代漏洞检测、运行时防护和安全治理的万能方案。

05.从研究技术，走向新的商业市场

&Truth 并不是唯一关注这一方向的企业。

包括 Harmonic 在内的技术团队，也在探索 AI 辅助数学证明、自动推理与软件验证。

这一趋势反映出一个值得关注的变化：过去主要存在于学术研究和少数高可靠性工程领域的形式化方法，正在尝试进入更广泛的商业软件市场。

但真正的挑战仍然存在。

真实软件系统结构复杂，安全需求未必能够完整地形式化表达；验证能力需要持续适应代码变化，并融入现有开发流程；企业也需要衡量验证成本与实际安全收益。

更重要的是，形式化验证能否从证明局部代码属性，扩展到复杂系统中的关键安全保证，仍需要大量工程实践。

结语:从发现问题，到证明问题不会发生

网络安全产业长期建立在持续发现漏洞、检测攻击和修补缺陷的机制之上。

形式化验证则提供了另一种安全保障方式：对于能够精确定义的安全属性，不仅要通过测试寻找问题，还可以尝试通过数学证明，确认某些问题在特定条件下不会发生。

有意思的是，AI 一方面正在加快软件开发和网络攻击，另一方面也可能突破形式化验证长期面临的成本与规模限制。

&Truth 的 7000 万美元融资，可以视为资本市场对这一技术方向的一次重要押注。

形式化验证能否成为 AI 安全挑战下的新解药，仍有待市场验证。但从经验性测试走向可证明的安全保证，正在成为值得网络安全产业关注的新方向。

原文链接：

https://andtruth.com/press/andtruth-emerges-from-stealth/

声明：本文来自安全喵喵站，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。