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

For decades, developers have envisioned using math to prove that their software is bug-free. This process is long and laborious, requiring engineers to write precise statements about the goals of their software and convert their code into formulas that can be validated. While companies already run sophisticated tests to identify as many flaws in their software as possible, they rarely shell out for formal verification, which can catch even more erratic behavior.

Now, a wave of startups is betting that generative AI will make formal software verification both practical and essential. Among them is &Truth, which Sun joined in August and publicly launched on Thursday. Sun’s research demonstrated the technology’s potential by using AI to verify part of the code that encrypts conversations in the messaging app Signal.