تلاش استارتاپ‌ها برای استفاده از هوش مصنوعی جهت اثبات صوری کدهای نرم‌افزاری

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.

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 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.

“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 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Some of the startups eager to expand verification also aren’t sure whether to deploy their tools directly to customers or through intermediaries like Anthropic. Their general plan is to use AI to automate much of the work involved in defining how a program is supposed to behave. For example, specifications for a data table might require that it contain the same items before and after sorting, just in a different order. Further automation efforts, which may not involve AI, would translate that code into a format that math tools like Lean, Rocq, and Isabelle can use to check whether the code works as intended.

Another recent entrant to the formal verification field is Madan Musuvathi, who left Microsoft Research after more than 20 years to found the startup Truidic. After incidents like the OpenAI hack of Hugging Face, he felt there was an urgent need to commercialize his studies. “AI in the hands of attackers can be extremely powerful,” Musuvathi says, but verification can “make AI safe and secure for everyone, everywhere.”

Proofcraft, one of the few companies that has long offered traditional verification, says growing excitement about the process is translating into a flood of inquiries from potential customers. June Andronick, the company’s CEO, and Gerwin Klein, its chief scientist, say interest easily outpaces what they and their competition can provide.

But both worry that AI-generated specifications could inspire “unjustified trust” in the results. Verifiers are also eager to preserve the joy their work brings them. Klein calls it “pretty addictive, like a puzzle game.” If all goes well, he’ll be doing more solving than ever.