当代码以超人的速度被生成，也以超人的速度被攻破
2026年9月，一场针对打印管理软件漏洞的攻击在48个国家撕开了395家组织的防线。攻击者没有使用传统工具，而是部署了数百个AI代理协同作战。同一个月，全球公布的软件漏洞数量达到14,959个——公司通稿称这一数字约为一年前的3.5倍。这两个数据点勾勒出一个正在成形的现实：AI不仅让代码的生产速度脱离了人类节奏，也让代码的破坏速度进入了新的量级。
软件行业赖以运转的信任机制建立在测试之上。测试能提供信心，但测试只能覆盖已知的输入和已知的路径。当AI生成代码的比例在Google新增代码中达到75%——这是公司通稿援引的Google CEO Sundar Pichai的说法——传统质量保障体系的边际效用正在被稀释。Veracode在2026年的测试发现，AI模型在涉及安全的编码任务中近半数失败。问题不再是如何更快地写代码，而是如何在代码被部署之前，确定它不会以某种未曾预料的方式失败。
2026年10月29日，一家名为&Truth的公益公司结束了隐身状态，宣布完成7000万美元种子轮融资。这家公司试图回答的正是上述问题：如果测试只能提供信心，那么什么能提供保证？
| 字段 | 内容 |
|---|---|
| 公司 | &Truth（AndTruth） |
| 轮次 | 种子轮 |
| 金额 | 7000万美元 |
| 投资方 | 未披露具体机构名单；公司称来自“AI安全与风投领域的领军者” |
| 总部 | 美国帕洛阿尔托（美国总部）与新加坡（国际总部） |
| 创始人 | Clark Barrett、Ilya Sergey、Chris Hsu |
| 官网 | https://andtruth.com |
一笔没有投资方名单的7000万美元种子轮
7000万美元的种子轮在任何市场环境下都是异常值。更异常的是，这笔交易的参与方至今没有被点名。公司通稿仅称资金来自“AI安全与风投领域的领军者”，没有披露领投方、跟投方、估值或股权结构。在通常以透明度为惯例的风险投资生态中，这种刻意留白本身构成了一种信息：要么投资方不希望在此刻暴露策略，要么公司的资本结构包含非传统安排。
从已披露的信息看，这笔资金的结构性特征比名单更值得关注。种子轮通常用于验证产品与市场的匹配，而7000万美元的规模意味着&Truth从一开始就被赋予了超出常规验证周期的资本纵深。公司成立于2026年初，到10月公布融资时运营不足一年。没有客户数量、收入或产品上线指标被披露。这意味着投资方押注的不是现有商业牵引，而是创始团队的技术积累与一个尚未被证明可规模化的技术路径。
投资方匿名化的另一个可能解释在于公益公司（public benefit corporation）的法律结构。&Truth选择了这一实体形式，意味着公司治理需要在股东利益与公共利益之间取得平衡。对于某些投资方而言，参与一家以“软件信任”为公共使命的公司，可能涉及品牌与合规考量。但这只是编辑推断，来源材料未提供投资方匿名的具体原因。
从“氛围编程”到“验证编程”：形式化验证的第二次机会
&Truth的核心命题是构建一台“通用验证机”：读取任意编程语言的代码，用数学方式证明其安全、可靠与正确，并产出任何人可独立核验的证明。公司通稿将这一愿景概括为从“vibe-coding”到“veri-coding”的转变——前者指AI辅助下凭感觉写代码的文化，后者指代码在部署前经过数学验证的状态。
形式化验证并非新技术。它已经存在数十年，但长期被困在专家手工构造证明的高成本牢笼中。公司通稿援引的历史案例是seL4微内核：约8,700行代码的最初证明耗费了约20人年的专家工作。这个投入产出比解释了为什么形式化验证此前只被应用于少数关键系统——航空航天、国防、芯片设计——而从未进入主流软件开发流程。
&Truth的技术主张建立在两个加速层上。第一层来自AI：公司通稿称AI可将形式化证明工作效率提升100倍以上。第二层来自公司自身的证明自动化技术：据公司披露，这一层可再带来约100倍的提升。两者叠加，公司称可将证明生成从数年或数月缩短到数小时或数分钟。需要注意的是，另一来源Fundz的融资数据库页面将这一加速描述为“最高10,000倍”，与公司通稿的“100倍+100倍”口径存在表述差异。本次来源材料未提供独立验证，两个口径之间的关系尚不明确。
技术底座是开源的。&Truth构建在Lean证明系统之上——这是一个由AWS副总裁兼杰出科学家Leonardo de Moura创造的定理证明器——以及Mathlib库，后者包含超过两百万行数学定义与定理。公司还涉及CSLib等开源形式化验证技术。选择开源底座意味着&Truth的核心壁垒不在于底层证明系统本身，而在于其“规格工厂”技术——将人类意图与业务需求转译为精确形式化规格的能力——以及证明自动化层的工程实现。
三位创始人的学术资本与一个未经验证的商业假设
&Truth的创始团队配置在形式化验证领域具有罕见的学术密度。联合创始人兼联席CEO Clark Barrett是斯坦福大学计算机科学Corbel教授、斯坦福AI安全中心创始联合主任、斯坦福自动推理中心主任，同时是CSLib的联合创造者和cvc5自动推理引擎项目负责人。联合创始人兼首席科学官Ilya Sergey在新加坡国立大学创立了VERSE Lab，并共同创建了开源验证器Veil与Velvet。联合创始人、联席CEO兼执行主席Chris Hsu则带来了不同的背景：他是Lean Focused Research Organization战略顾问委员会成员、Infinitude Foundation总裁，曾任Kilometre Capital CEO与Citadel Investment Group董事总经理。
这个组合的意图清晰：Barrett和Sergey提供形式化验证与自动推理的学术纵深，Hsu提供资本运作与组织建设经验。公司通稿还点名了多位核心成员，包括前BlueRock Security形式化方法负责人Gregory Malecha、Lean 4联合架构师Sebastian Ullrich、前Kilometre Capital管理合伙人Linus Lee，以及前Fastino Labs首席商务官Drew Harman。
但学术资本与商业可行性之间的鸿沟正是&Truth面临的核心待验证假设。形式化验证的历史瓶颈不仅在于证明构造的速度，还在于规格书写的难度。要让开发者将业务需求精确地形式化，需要一种此前从未在软件行业大规模存在过的技能组合。&Truth的“规格工厂”试图用技术手段弥合这一鸿沟，但公司尚未披露该技术在任何真实客户场景中的表现。从已披露的信息看，&Truth的验证路径是：先建立通用形式化词汇表，再通过AI与自动化降低规格书写和证明构造的成本，最终让验证成为开发流程的常规环节。但“规格工厂”能否将模糊的人类意图可靠地转译为精确规格，以及这种转译本身是否会被视为可信，均未在本次来源中得到验证。
开源策略与商业化之间的张力
&Truth计划将基础库以开源方式发布，并与Lean Focused Research Organization及开源社区合作。这一策略在形式化验证领域具有战略合理性：Lean和Mathlib本身就是开源项目，&Truth的技术栈深度依赖社区生态。通过开源基础库，公司可以降低采用门槛、吸引研究者与开发者参与，并建立事实上的行业标准。
但开源策略同时制造了一个商业模式的未解方程。如果基础库免费开放，&Truth的付费产品是什么？公司通稿未披露具体收费模式。可能的路径包括：企业级证明自动化服务、规格工厂的SaaS化交付、对关键系统的验证认证服务，或围绕“可独立核验证明”的信任基础设施收费。但这些均为编辑推断，公司未提供任何商业化细节。
更深层的张力在于“独立可核验”与“商业信任”之间的关系。Ilya Sergey在公司通稿中的表述值得注意：“软件信任应当建立在可独立核验的证明之上，而非任何公司的说法——包括我们自己的。”这句话既是技术承诺，也是商业定位的自我约束。如果&Truth的客户必须依赖&Truth来生成证明，那么“独立核验”的价值取决于证明是否能在不依赖&Truth的情况下被检查。开源基础库是这一承诺的必要条件，但并非充分条件——证明的生成工具链、规格的书写质量、以及验证过程本身的透明度，共同决定了“独立核验”的实际可信度。
竞争格局：没有直接对手，但有替代路径
来源材料未披露&Truth的具体竞争对手。这并不意味着公司没有竞争压力，而是反映了形式化验证市场的早期状态。目前与&Truth形成替代关系的路径至少包括三类：传统测试与静态分析工具、AI代码审查平台，以及大型科技公司内部的形式化验证团队。
传统测试与静态分析是&Truth最直接的替代方案。它们成本低、工具链成熟、开发者熟悉度高。&Truth的差异化主张在于“证明提供保证，而测试只提供信心”——这是Lean创造者Leonardo de Moura在公司通稿文章中被引用的一句话。但这个差异化只有在证明生成成本下降到与测试可比时才能转化为商业优势。在成本曲线交叉之前，&Truth面对的是一个惯性巨大的替代品市场。
AI代码审查平台构成了另一类竞争。这些平台利用大语言模型识别代码缺陷与安全漏洞，部署速度快、覆盖语言广，但本质上仍属于概率性方法——它们能发现可能的错误，不能证明错误的不存在。&Truth的形式化验证在数学严格性上具有类别优势，但在速度和易用性上可能处于劣势。公司通稿援引的Veracode测试结果——AI模型在安全相关编码任务中近半数失败——正是对这一替代路径的批判性论据，但该数据来自公司通稿引用的第三方测试，本次来源未提供独立核验。
大型科技公司内部的形式化验证团队则构成了人才与标准层面的竞争。AWS、Google、Microsoft等公司都在形式化验证领域有持续投入。&Truth的创始团队本身与这一生态深度交织——Barrett来自斯坦福，Sergey来自新加坡国立大学，Hsu与Lean FRO有关联。这种交织既是资源，也是约束：&Truth需要在开源社区中建立标准影响力，同时避免与大型科技公司的内部能力形成正面冲突。
资金用途与新加坡的支点角色
公司通稿披露的资金用途集中在两个方向：构建通用验证机本身，以及扩充研究、工程、产品与市场团队。新加坡办公室被明确列为扩张重点，覆盖研究、工程、产品与市场推广工作。新加坡数字产业发展司高级副总裁兼联合主管Low Jin Yong在公司通稿中表示，该总部将深化新加坡的信任与安全能力，并强化其作为可信AI企业基地的地位。
新加坡在&Truth的全球布局中扮演的角色超出了普通区域办公室的范畴。Ilya Sergey在新加坡国立大学的学术根基、新加坡政府对可信AI的政策倾斜、以及东南亚市场对软件供应链安全的日益关注，共同构成了新加坡作为国际总部的合理性。从已披露的信息看，&Truth的双总部结构并非简单的市场覆盖策略，而是将美国学术资源与亚洲商业落地能力进行结构性整合的尝试。但公司未披露两地团队的具体规模或分工细节。
风险与待验证假设：一个尚未被证明的加速叙事
&Truth的融资叙事建立在一个核心假设上：AI加速与证明自动化的叠加，可以将形式化验证的成本降低到主流软件开发可接受的水平。这个假设目前只有公司单方面声明支撑。公司通稿称AI加速100倍以上、自身技术再加速100倍；另一来源称“最高10,000倍”。两个口径之间的差异本身就是一个信号：加速倍数的测量基准、适用场景和边界条件均未披露。
更根本的待验证问题在于“任意编程语言”的承诺。形式化验证的历史经验表明，不同编程语言的语义复杂性差异巨大。为一个语言建立精确的数学语义模型本身就是一项研究级工作。&Truth声称的“通用验证机”需要为每种语言建立形式化模型，这意味着工程工作量与语言数量成正比。公司在Lean和Mathlib上的积累为函数式语言验证提供了坚实基础，但将其扩展到主流工业语言——C、C++、Java、Python、JavaScript——的路径和进度均未披露。
商业验证的缺失是另一个显著风险。公司成立于2026年初，10月公布融资时没有披露任何客户、收入或产品上线指标。7000万美元的种子轮给了公司较长的验证窗口，但也提高了后续轮次的期望值。如果&Truth无法在资金消耗期内证明其技术能在真实企业环境中产生可核验的价值，下一轮融资的谈判条件将显著恶化。
投资方匿名的长期影响也值得关注。在AI安全领域，投资方的身份往往构成信号——它暗示着战略协同、客户资源或技术生态的接入。&Truth选择不披露投资方，可能保护了公司的独立性，但也放弃了这种信号价值。当公司需要向企业客户证明其长期稳定性时，资本结构的透明度可能成为一个被审视的维度。
从已披露的2026年时间线看，形式化验证领域正在经历一个被AI重新激活的窗口期。公司通稿文章提到，2026年9月Anthropic开发的AI模型在11天内于Lean中形式化了费马大定理的完整证明；同年早些时候，Lean FRO的高级研究软件工程师Kim Morrison使用Anthropic的Claude在极少人工指导下构建了zlib压缩库的Lean版本并证明了其解压精确性。这些事件如果属实，表明AI在数学证明领域的进展正在向软件验证领域溢出。但它们同时提出了一个&Truth必须回答的问题：如果AI模型本身已经能在Lean中完成复杂证明，&Truth的证明自动化技术提供的增量价值究竟是什么？公司通稿的回答是“规格工厂”——将人类意图转译为形式化规格的能力——以及跨语言的通用验证基础设施。但这个回答尚未经过任何公开的客户验证。
本项目的统计口径与验证边界需要集中说明：本轮7000万美元的金额、种子轮的轮次定位、2026年初的成立时间、以及三位创始人的身份，均来自公司通稿及转载报道，本次来源未提供独立核证。加速倍数的表述在来源间存在不一致，投资方名单、估值、客户与收入数据均未披露。公司通稿援引的第三方数据——包括Google的75% AI生成代码比例、Veracode的测试结果、14,959个漏洞数量、seL4的20人年证明成本、Anthropic的费马大定理形式化——均来自公司通稿的转述，本次来源未提供对原始研究的独立核验。
RecodeX 极客视：&Truth的7000万美元种子轮买下的是一个尚未被证明的加速假设：AI与证明自动化的叠加能否将形式化验证从关键系统的奢侈品变成主流开发的日用品。三位创始人的学术资本足以让这个假设值得被认真对待，但“任意语言”“独立可核验”“规格工厂”这三个承诺中的每一个，都需要在真实代码、真实客户和真实攻击面前兑现。在AI同时加速代码生产与代码破坏的时代，证明的价值从未如此清晰；但证明的成本能否降到市场愿意支付的水平，答案仍在未披露的客户名单和未公开的验证数据之中。
信息来源
本文在采集与核验阶段引用了以下公开来源，按站点去重列出；来源内容归原发布方所有，其口径不代表 RecodeX 的核实结论。