Lanyon AI 披露了1060万美元的融资，用于经过形式化验证的科学代码

Why it matters

Formal verification can make AI-generated scientific software auditable, but its value depends on whether the certified specification captures the engineer's real intent.

Jonathan Gorard, Ammar Hakim, and James "Jimmy" Juno 在 8 月 17 日披露了对 Lanyon AI 的 1,060 万美元初始融资轮，支持他们尝试让 AI 生成的科学软件证明其满足规范要求的努力。

根据 Lanyon AI 的公告，Dimension 领投了本轮融资，Industrious Ventures 参与了投资。这家位于新泽西州普林斯顿的研究实验室将目标瞄准航空航天、推进、核能、物理仿真、GPU 优化和 AI 推理等领域，在这些领域中一个看似合理的答案仍可能带来危险后果。

本轮融资为由形式数学与计算等离子体物理背景组建的创始团队提供了资金支持。Gorard 是 Lanyon AI 的 CEO，此前在 Wolfram Research 从事自动定理证明和量子计算方面的工作，并与 Stephen Wolfram 共同创立了 Wolfram Physics Project。Hakim 是 Lanyon AI 的 CTO，是普林斯顿讲师和首席研究物理学家，他的工作包括聚变、空间等离子体、托卡马克湍流以及用于偏微分方程的机器学习。Juno 是首席科学家，来自 Princeton Plasma Physics Laboratory，是 Gkeyll 等离子体仿真框架的核心开发者。

他们的赌注是：通用编码代理从错误的语言开始。“为什么代理仍然在用不完美的人类语言进行推理和编码？”Gorard 在 8 月 17 日的公告 中这样问道。Lanyon AI 则希望其代理通过一种为数学、物理和科学计算构建的精简形式语言来进行推理。

One source for the code and the proof

Lanyon AI 的架构将创造性工作分配给底层语言模型，后者在 Lanyon AI 的领域特定语言中提出一个形式规范。然后，一个符号编译器同时将该规范展开为实现代码和机器可检查的证明。如果规范无法被证明，Lanyon AI 表示系统会暂缓生成代码并重试。

这种设计针对的是自动形式化系统的一个特定弱点。传统代理可以先写出代码，然后再生成一个 Lean 证明以通过类型检查，同时描述了与实现不同的内容。Lanyon AI 将这种失败称为“错误形式化”。从同一来源导出这两种成果旨在防止证明与其所认证的代码发生偏离。

目前可获得的最有力证据来自 Lanyon AI 自身。在 公司主导的基准测试（发布于 7 月） 中，Juno 在线性对流和 Maxwell 方程求解器上测试了前沿模型，对每个模型使用了三次试验以及详细和简洁的提示。Lanyon AI 报告称，其参考线性对流求解器生成大约需要 7 秒钟并输出约 800 个标记，而其 Maxwell 求解器大约需要 23 秒并输出约 600 个标记。

这些数字支持的论断比 8 月公告中与前沿模型的广泛比较要窄得多。测试由 Lanyon AI 围绕适合其架构的科学问题设计、执行并评分。尚需独立复现来确定该方法在更广泛工程工作集上的表现如何。

Lanyon AI 还在 GitHub 上发布了 六个求解器仓库，涵盖对流-扩散方程、Maxwell 方程、广义相对论形式的 Maxwell 方程、Burgers 方程、可压缩 Euler 方程以及静电 Vlasov 方程。这些仓库使用 C 和 Lean，为研究人员提供了可检查的示例，展示了 Lanyon AI 声称背后的形式验证工作。

The specification remains the boundary

形式验证可以证明实现符合形式规范。它无法自动证明该规范是否捕捉了用户的真实科学意图、物理假设或部署条件。

Gorard 在 Lanyon AI 7 月的介绍 中承认了这一界限。他将代码、证明与规范相匹配的句法保证，与将用户的自然语言请求翻译为正确规范的语义问题区分开来。Lanyon AI 将语义正确性描述为一个开放的研究领域。

在 Lanyon AI 所瞄准的行业中，这一区别很重要。证明可以认证一个求解器，但仍可能无法回答工程师是否选择了正确的控制方程、边界条件、材料属性或故障阈值。因此 Lanyon AI 的产品挑战集中在工程师与形式语言之间的接口处。符号编译器只能在该接口产生正确规范后，才对下游的一切进行审查。

这一市场已经吸引了技术雄心勃勃的团队。Axiomatic AI 在 2026 年 3 月披露获得了 1,800 万美元的种子轮融资，用于以验证为中心的工程 AI，而 Harmonic 则将其 Aristotle 系统集中于形式数学推理和已验证软件。Lanyon AI 正在为可执行仿真和数值方法划定一个更靠近实用的位置，直接借鉴了 Hakim 和 Juno 在为等离子体物理构建软件方面的经验。

投资者阵容也反映了这一产业方向。Dimension 将其使命描述为在科学与计算领域进行投资。Industrious Ventures 专注于航空航天、能源、制造业以及其他软件错误会与硬件成本和安全要求相碰撞的物理行业。

Lanyon AI 目前仍在呈现一个研究计划，而不是一个完整记录的商业业务。其公开材料并未确立定价、客户采用情况或通用产品发布。公司页面 正在招聘形式验证、计算物理、应用数学和 AI 基础设施方面的研究科学家和工程师。

创始团队已经提出了一个连贯的技术论点，并公开了足够的代码，使其部分内容可被检查。他们接下来的考验是将该架构转变为工程师可以使用的系统，而不会将最难发现的错误从生成的代码转移到控制该代码的规范上。