Chuyue Sun says an AI tool helped finish an engineering project in less than half a day for under $500, work that had taken three highly skilled experts five months to complete by hand. The result is a sharp sign that vibe coding is moving into one of software’s most demanding jobs: proving code behaves as intended.
For decades, developers have talked about using math to show software is bug-free. Formal verification tries to do that by forcing engineers to write exact statements about what code should do, then turning the code into formulas that can be checked. It is powerful because it can catch erratic behavior that normal testing misses, but it has usually been too slow and expensive to spread far beyond the most critical systems.
Sun reported the time and cost reduction in a recent paper after using AI to verify part of the code that encrypts conversations in Signal. She joined &Truth in August, and the company publicly launched on Thursday after raising $70 million from investors. The goal is ambitious: &Truth wants to eventually verify any programming language, a shift that would matter if the method ever becomes practical outside elite research teams.
That is the promise now drawing in other companies. Harmonic, cofounded by Robinhood CEO Vlad Tenev, said this week that its AI agent Aristotle can support verification for software written in C and hardware designs in Verilog. It has raised $295 million, and it is testing the system with potential users including Tensordyne and Nvidia, whose venture capital arm is one of its investors. Anthropic and Theorem said last week that they used AI to help find bugs in open source software that trillions of tests had failed to detect, and they released an add-on for Claude to help other developers do the same work.
But the field still runs into the same objection, even from people building it. Will Wilson called formal verification a trap for math nerds like himself, even as Antithesis spent millions of dollars to formally verify some of its cybersecurity defenses. He also described the process as a pain in the ass, and said Antithesis still uncovered additional errors with its own tool, including bugs in software that several customers had already formally verified. That is the part AI has not erased: formal proofs can still miss problems that show up in the real world when people make mistakes or hardware fails.
That leaves vibe coding with a hard test of its own. The technology is still in the prototyping stage, companies already rely on sophisticated testing, and no one is yet clear on what customers will pay for AI-assisted verification. If the tools keep shrinking five months of labor into a morning’s work, the question will stop being whether formal verification can be done at all and become whether software teams can afford not to use it.
