形式化验证公司 &Truth 结束隐身,获 7000 万美元种子轮融资
&Truth 是一家今年初成立的公益公司,总部位于帕洛阿尔托和新加坡,宣布获得 7000 万美元种子资金。公司在做一台“通用验证机”:读取任意编程语言的代码,用数学证明它安全、正确,证明可由任何人独立核验。联合创始人包括斯坦福教授 Clark Barrett 和新加坡国立大学副教授 Ilya Sergey,Lean 4 共同架构师 Sebastian Ullrich 也在团队中。
为什么重要:AI 写的代码越来越多,形式化验证开始吸引资金;Wired 提到,同类公司 Harmonic 本周也宣布其 Aristotle 可验证 C 代码。

