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

For decades, developers have aimed to use math to confirm their software is free of bugs. This painstaking process involves engineers crafting precise statements about the software's objectives and translating their code into formulas for validation. Enterprises frequently conduct rigorous testing to uncover as many flaws as possible, yet they seldom invest in formal verification, which can unearth even more elusive issues.

Now, a surge of startups believes generative AI will make formal software verification both feasible and indispensable. One such startup, &Truth, recently launched, with Sun's research showcasing its potential in verifying encryption code used in the Signal messaging app. Ilya Sergey, &Truth's chief science officer, posits that the same rigorous mathematical reasoning used in constructing bridges and buildings should apply to software. &Truth has amassed $70 million from investors and plans to verify any programming language in the future.

Another competitor, Harmonic, co-founded by Robinhood CEO Vlad Tenev, has raised $295 million in funding and is testing its math-driven AI agent Aristotle with potential clients like chipmaker Tensordyne and Nvidia. Recently, Anthropic and verification startup Theorem jointly announced using AI assistance to detect bugs in open-source software that previous tests had missed.

They also unveiled an add-on for Claude to aid other developers in verification. The potential payoff is a more dependable software ecosystem with fewer security vulnerabilities. However, whether AI can bring formal verification to the masses and not just the most critical systems at tech giants like NASA and Apple remains uncertain.

The technology is still in its experimental phase, and while demand is strong, it is unclear how customers will pay for and adopt the technology. Formal verification depends on assumptions about computer and user interactions, and some experts are doubtful about its effectiveness in catching bugs caused by user mistakes and hardware malfunctions.

Will Wilson, who runs the bug-hunting AI startup Antithesis, describes formal verification as a "pain in the ass" for math enthusiasts like himself. Despite the skepticism, Antithesis has still managed to uncover additional errors using its tool and has identified bugs in software that several of its clients had formally verified.

"It can provide some assurance, but only rigorous exhaustive testing can prove your assurance is true," Wilson asserts. As Vitalik Buterin, the creator of Ethereum cryptocurrency, noted in a recent blog post, "formal verification is not a panacea." However, proponents still maintain that it will play a crucial role in defending against AI-powered cyber attacks.

Today, Core Security components of Boeing planes, Amazon servers, and over 2.5 billion active Apple devices incorporate some formally verified software, primarily in security-related areas. Although the code in question may cause significant harm if exploited, substantial verification is typically reserved for security-critical features, balancing the costs against the potential risks and concerns about potential delays in innovation.

Apple's security team revealed that some issues uncovered by formal verification in its encryption library, "corecrypto," could not have been identified through alternative methods. Two undisclosed cybersecurity executives, who have not formally verified their own code, are unsure whether automation will justify the investment. However, they acknowledge that they might consider paying major AI labs for "verified" AI-generated code.

Open-source software developers, which form the backbone of many applications, are also exploring AI-aided verification. The nonprofit Beneficial AI Foundation, funded by Anthropic, recently validated encryption code used in the curve25519-dalek library, similar to Sun's verification at Stanford. Michael Rosenberg, a maintainer of curve25519-dalek, hopes for sustainable funding to support ongoing verification efforts, but he cautions that it should not rely solely on the goodwill of AI companies.

Some startups exploring verification expansion are uncertain whether to offer their tools directly to customers or through intermediaries like Anthropic. Their strategy generally involves using AI to automate the definition of a program's behavior, translating the specifications into a format suitable for implementation.