A group of startups is using AI to automate formal verification, the painstaking process of translating software requirements and code into mathematical statements that can be proved. The goal is to extend stronger guarantees beyond the small set of safety-critical systems that can justify extensive manual proof work.
Stanford researcher Chuyue Sun reported that an AI tool completed one verification project in under half a day for less than $500, compared with five months of work by three experts. Her research included verifying part of the code used to encrypt Signal conversations. Sun has since joined &Truth, a startup that launched publicly with $70 million in funding.
Competitor Harmonic says its Aristotle agent can now verify C software and Verilog hardware designs. Anthropic and Theorem recently reported using AI-assisted verification to find bugs that large test campaigns had missed. These examples show why proofs can complement testing: tests sample selected executions, while a proof checks whether stated properties hold across all covered cases.
The difficult part is writing correct specifications and trusting the translation between production code and the mathematical model. A proof can faithfully certify the wrong requirement. The technology remains at the prototype stage, and broad adoption will depend on integration costs, supported languages and independent evidence that generated proofs are easier to audit than the code they protect.