A field of mathematics and computer science that has labored in obscurity for decades is suddenly relevant to coding, Wired reported Thursday.
Formal verification uses proofs to show a program does what it claims. The work is slow, because engineers must state their goals precisely and translate code into formulas that a checker can validate. Companies run elaborate test suites, but rarely pay for proofs, even though proofs catch erratic behavior that tests miss.
Stanford researcher Chuyue Sun and colleagues built an AI tool that completed an engineering project in under half a day for less than $500. The same work took three highly skilled experts about five months by hand. Sun used the approach to verify part of the encryption code inside Signal.
A new startup called &Truth, which Sun joined in August, launched publicly Thursday with $70M raised and an eye on eventually covering any programming language. Its chief science officer, Ilya Sergey, notes that bridges and buildings stand because people did the math before construction, and asks why code should be exempt. Rival Harmonic, cofounded by Robinhood chief executive Vlad Tenev, has $295M and this week said its agent Aristotle can verify C code and Verilog hardware designs.
The case is straightforward. If models produce more software than humans can audit, the only affordable check is a machine-checkable proof rather than another model’s opinion. The caution is equally plain. Antithesis founder Will Wilson calls verification a trap for mathematicians and says only exhaustive testing proves that assurance is real. Vitalik Buterin has written that it is not a panacea. It is arriving anyway.
