&Truth launches AI startup focused on formal software verification

&Truth has publicly launched a startup focused on automating formal verification, a process that turns software requirements and code into mathematical formulas to validate behavior. A paper by Chuyue Sun and other Stanford researchers reported that an AI tool completed in less than half a day and for under $500 an engineering project that took three experts five months to do manually; the system was also used to verify part of the encryption code in Signal. &Truth has raised $70 million and aims to eventually support any programming language.

Harmonic also announced its Aristotle agent, which verifies software written in C and hardware designs in Verilog, while Anthropic and Theorem said they used AI to find bugs in open-source software that had gone undetected by trillions of tests. The technology remains at the prototype stage: experts note that it may not catch errors caused by users or hardware failures, and that exhaustive testing is still needed.