本文为原文前 6,000 字符的节选翻译，完整内容请查看原文。

The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself

Stanford researcher Chuyue Sun and her fellow computer scientists developed an AI tool that completed an engineering project in less than half a day for under $500, compared to the five months it took three highly skilled experts to do the same work manually. The dramatic reduction in time and cost, which Sun reported in a recent paper, is among the early results that are awakening an obscure field of coding and mathematics known as formal verification.

斯坦福大学研究员孙楚月（音译）及其计算机科学家同事开发出一种人工智能工具，仅用不到半天时间、花费不到 500 美元就完成了一项工程项目，而三名高技能专家手动完成同样的工作则需要五个月。孙在最近的一篇论文中报告了这一时间和成本的显著降低，这些初步成果正唤醒一个名为“形式化验证”的冷门编程与数学领域。

For decades, developers have envisioned using math to prove that their software is bug-free. This process is long and laborious, requiring engineers to write precise statements about the goals of their software and convert their code into formulas that can be validated. While companies already run sophisticated tests to identify as many flaws in their software as possible, they rarely shell out for formal verification, which can catch even more erratic behavior.

几十年来，开发人员一直设想利用数学来证明其软件不存在漏洞。这一过程漫长而艰巨，要求工程师针对软件目标编写精确的陈述，并将代码转换为可验证的公式。尽管企业已经运行复杂的测试来尽可能多地识别软件缺陷，但他们很少愿意为形式化验证买单，尽管这种方法能够捕捉到更不规律的行为。

Now, a wave of startups is betting that generative AI will make formal software verification both practical and essential. Among them is &Truth, which Sun joined in August and which publicly launched on Thursday. Sun’s research demonstrated the technology’s potential by using AI to verify part of the code that encrypts conversations in the messaging app Signal.

如今，一批初创公司押注生成式人工智能将使形式化软件验证变得既实用又必要。其中包括孙于 8 月加入并于周四公开推出的 &Truth 公司。孙的研究通过利用人工智能验证消息应用 Signal 中用于加密对话的部分代码，展示了该技术的潜力。

“Bridges, buildings, they don’t collapse, because people did math before constructing them,” says Ilya Sergey, &Truth’s chief science officer. “Why don’t we do the same for code? The technology to mathematically reason was all there, just difficult to scale.”

“桥梁和建筑物之所以不会倒塌，是因为人们在建造前进行了数学计算，”&Truth 首席科学官伊利亚·谢尔盖（Ilya Sergey）表示，“为什么我们不能对代码做同样的事情呢？进行数学推理的技术一直都在，只是难以扩展。”

&Truth has raised $70 million from investors and aims to eventually verify any programming language. Rival Harmonic, which was cofounded by Robinhood CEO Vlad Tenev and has received $295 million in funding, announced this week that its math-focused AI agent Aristotle supports verifying software written in C and hardware designs in Verilog. It is evaluating the technology with potential users, including chipmakers Tensordyne and Nvidia, whose venture capital arm is one of the startup’s investors.

&Truth 已从投资者处筹集了 7000 万美元，旨在最终实现对任何编程语言的验证。其竞争对手 Harmonic 由 Robinhood 首席执行官弗拉德·特内夫（Vlad Tenev）共同创立，已获得 2.95 亿美元融资。该公司本周宣布，其专注于数学的人工智能代理 Aristotle 支持验证用 C 语言编写的软件和用 Verilog 编写的硬件设计。它目前正与潜在用户评估该技术，包括芯片制造商 Tensordyne 和英伟达（Nvidia），后者的风险投资部门正是该初创公司的投资者之一。

And just last week, Anthropic and the verification startup Theorem jointly announced they had used AI to assist in finding bugs in open source software that trillions of tests had failed to detect. They also introduced an add-on for Claude to help other developers with verification. Costs of the initial project were not disclosed.

就在上周，Anthropic 和验证初创公司 Theorem 联合宣布，他们利用人工智能协助发现了开源软件中的漏洞，而这些漏洞在数万亿次测试中都未能被检测出来。他们还为 Claude 引入了一个插件，以帮助其他开发人员进行验证。初始项目的成本并未披露。

The big promise is a future where software runs more reliably with fewer security headaches. But whether AI can bring formal verification beyond the most critical systems at organizations like NASA and Apple and into widespread use remains an open question.

这一技术带来的巨大愿景是：未来软件运行将更加可靠，安全隐患更少。但人工智能能否将形式化验证从 NASA 和苹果等机构的关键系统推广到广泛应用，仍是一个悬而未决的问题。

The technology is still in the prototyping stage. Though demand is high, it’s unclear how much customers are willing to pay and how they prefer to adopt the technology. Formal verification relies on making assumptions about how computers and people interact with software, and some experts are skeptical about its ability to catch bugs stemming from user error and hardware breakdowns.

该技术仍处于原型阶段。尽管需求旺盛，但客户愿意支付多少费用以及他们倾向于如何采用该技术尚不明确。形式化验证依赖于对计算机和人员如何与软件交互做出假设，一些专家对其捕捉由用户错误和硬件故障引起的漏洞的能力持怀疑态度。

Will Wilson, who runs the bug-hunting AI software startup Antithesis, calls formal verification “a trap” for math nerds like himself. Antithesis spent millions of dollars to formally verify some of its cybersecurity defenses, a process Wilson describes as a “pain in the ass.” Yet the startup still uncovered additional errors using its own tool, and Antithesis has also found bugs in software that several of its customers had formally verified. “It can give you some assurance, but only robust exhaustive testing can prove your assurance is true,” Wilson says.

经营漏洞搜寻人工智能软件初创公司 Antithesis 的威尔·威尔逊（Will Wilson）称形式化验证对于像他这样的数学极客来说是“一个陷阱”。Antithesis 花费数百万美元对其部分网络安全防御系统进行了形式化验证，威尔逊将这一过程描述为“极其麻烦”。然而，该公司仍利用自己的工具发现了额外的错误，并且 Antithesis 还在其几位客户已经过形式化验证的软件中发现了漏洞。“它能给你一些保证，但只有稳健的详尽测试才能证明你的保证是真的，”威尔逊说。

Or as Vitalik Buterin, the engineer known for creating the Ethereum cryptocurrency, put it in a blog post earlier this year, “formal verification is not a panacea.” But he and other proponents of the approach still believe it will be an important defense against AI systems launching cyberattacks and wreaking havoc.

正如以太坊加密货币创始人、工程师维塔利克·布特林（Vitalik Buterin）在今年早些时候的一篇博文中指出的那样，“形式化验证并非万灵药。”但他和其他该方法的支持者仍然认为，这将是抵御人工智能系统发动网络攻击并造成破坏的重要防线。

Core Security

核心安全

Boeing planes, Amazon servers, and more than 2.5 billion active Apple devices contain at least some formally verified software, according to company disclosures. The code in question is typically security-related, and vulnerabilities in it could cause serious harm if exploited.

根据公司披露的信息，波音飞机、亚马逊服务器以及超过 25 亿台活跃的苹果设备中至少包含部分经过形式化验证的软件。相关代码通常与安全相关，如果被利用，其中的漏洞可能会造成严重损害。

Byron Cook, a distinguished scientist and vice president at Amazon Web Services, says formal verification has eased customer concerns about cloud security and helped internal teams move faster by squashing big bugs early on.

亚马逊云科技（AWS）杰出科学家兼副总裁拜伦·库克（Byron Cook）表示，形式化验证减轻了客户对云安全的担忧，并通过在早期消除重大漏洞帮助内部团队加快了进度。

But several midsized tech companies tell WIRED they have typically verified only one key feature of their products, if any at all. They cite a lack of verification engineers, costs that outweigh the potential risks, and, perhaps most importantly, concerns that waiting weeks for code to be formally verified could slow innovation.

但几家中型科技公司告诉《连线》（WIRED），他们通常只验证了产品的一个关键功能（如果有的话）。他们提到的原因包括缺乏验证工程师、成本超过潜在风险，以及最重要的一点：担心等待数周进行代码形式化验证会拖慢创新速度。

Earlier this year, Apple’s security team said that some of the issues formal verification uncovered in its “corecrypto” library, which is used for encryption, could not have been found any other way. But the company added that it has to be “conservative” when adding new code to corecrypto to ensure it can keep pace with reviewing it.

今年早些时候，苹果安全团队表示，形式化验证在其用于加密的“corecrypto”库中发现的一些问题，是无法通过其他任何方式发现的。但该公司补充说，在向 corecrypto 添加新代码时必须保持“保守”，以确保能够跟上审查进度。

Two cybersecurity executives at major companies that haven’t formally verified any code say they aren’t sure whether automation will make it worthwhile. But the executives, who weren’t authorized to speak publicly, say they could imagine paying major AI labs for “verified” AI-generated code.

两家尚未对任何代码进行形式化验证的大型公司的网络安全高管表示，他们不确定自动化是否会让这项工作变得物有所值。但这些未获授权公开发言的高管表示，他们可以想象向大型人工智能实验室付费购买“经过验证”的人工智能生成代码。

Developers of open source software projects, which are the bedrock of many apps, are increasingly experimenting with AI-aided verification. The nonprofit Beneficial AI Foundation used a grant from Anthropic to validate the same encryption code this year as Sun did at Stanford. Michael Rosenberg, a maintainer of the library known as curve25519-dalek, hopes sustainable funding emerges for ongoing verification efforts. “I have no ideas as to how that’s going to happen, though, and we certainly shouldn’t rely on the goodwill of the AI companies,” he says.

作为许多应用程序基石的开源软件项目的开发人员，正越来越多地尝试人工智能辅助验证。非营利组织 Beneficial AI Foundation 今年利用 Anthropic 的一笔赠款验证了与孙在斯坦福大学所验证的相同的加密代码。名为 curve25519-dalek 的库的维护者迈克尔·罗森伯格（Michael Rosenberg）希望为持续的验证工作提供可持续的资金。“不过，我不知道这该如何实现，我们当然不应该依赖人工智能公司的善意，”他说。