先了解这件事
&Truth于2026年10月29日结束隐身状态并公开上线,同时披露7000万美元种子轮融资。据Unite.AI报道,该公司计划构建能读取任意编程语言代码并数学证明其安全、正确、可靠的通用验证机,技术基于开源证明系统Lean和超过两百万行的Mathlib库,并称其证明自动化技术可将证明生成从数年或数月缩短到数小时或数分钟,还计划将基础库开源。联合创始人包括斯坦福大学教授Clark Barrett和新加坡国立大学VERSE Lab创始人Ilya Sergey,公司总部设在帕洛阿尔托和新加坡。WIRED同日报道称,生成式AI正把形式化验证推向商业化,但该技术仍处原型阶段,客户付费意愿和采用方式不明;Antithesis的Will Wilson称形式化验证是“陷阱”,只能提供部分保证。
AI 根据公开报道生成
最新进展 · 正式报道
&Truth 获 7000 万美元种子轮，要用 Lean 构建代码通用验证机事件进展
1 个已确认进展
- 来源：Wired AI
报道与讨论时间线
按时间查看正式报道与传播讨论；两类内容的证据等级保持独立。
10月30日
Unite.AI
&Truth 获 7000 万美元种子轮，要用 Lean 构建代码通用验证机
&Truth 于 10 月 29 日结束隐身状态，披露 7000 万美元种子轮融资，计划构建能读取任意编程语言代码并数学证明其安全、正确、可靠的通用验证机。公司基于开源证明系统 Lean 和超过两百万行的 Mathlib 库，称其证明自动化技术可将证明生成从数年或数月缩短到数小时或数分钟，并计划将基础库开源。联合创始人包括斯坦福大学教授 Clark Barrett 和新加坡国立大学 VERSE Lab 创始人 Ilya Sergey，公司总部设在帕洛阿尔托和新加坡。
10月29日
Wired AI
AI 推动形式化验证创业潮，&Truth 融资 7000 万美元
WIRED 报道，生成式 AI 正在把形式化验证推向商业化，&Truth 已融资 7000 万美元并公开上线，Harmonic 累计融资 2.95 亿美元，其数学 AI 智能体 Aristotle 支持验证 C 代码和 Verilog 硬件设计。斯坦福研究者 Chuyue Sun 用 AI 工具在不到半天、花费不到 500 美元完成一项工程项目，而三位专家手工完成同一工作用了五个月。报道同时指出该技术仍处原型阶段，客户付费意愿和采用方式不明，Antithesis 的 Will Wilson 称形式化验证是“陷阱”，只能提供部分保证。
本事件热度走势
- 当前
- 6
- 区间峰值
- 16 10月30日 16:00
- 近 24 小时变化
- -50%
移动指针或点击图表可查看每小时热度；键盘可用左右方向键切换。