&Truth Launches With $70M to Use AI for Formal Code Verification
A wave of startups, including &Truth, Harmonic and an Anthropic-Theorem partnership, bet AI can finally make mathematical proof of code correctness practical.
What to know
- &Truth launched publicly with $70 million in funding, aiming to use AI to automate formal verification — mathematically proving code is bug-free.
- Stanford researcher Chuyue Sun's prototype verified part of Signal's encryption code in under half a day for under $500, versus five months for three expert engineers.
- Rivals Harmonic (backed by Robinhood CEO Vlad Tenev) and a joint Anthropic-Theorem project have made similar AI-verification announcements within the same month.
- Skeptics like Antithesis CEO Will Wilson question whether formal verification can scale beyond critical systems or catch bugs from user error and hardware failure.
“The big promise is a future where software runs more reliably with fewer security headaches. But whether AI can bring formal verification beyond the most critical systems at organizations like NASA and Apple and into widespread use remains an open question.”
Wired, Reporting · Wired ↗ · Oct 28
Chuyue Sun Stanford researcher, &Truth team memberIlya Sergey &Truth chief science officer
Vlad Tenev Robinhood CEO, Harmonic cofounderWill Wilson CEO of Antithesis&Truth AI formal-verification startupAnthropic / Theorem AI company and verification startup partnership
How it unfolded 2 developments, newest first · click a bar or a number to jump articlesposts
-
2
Coverage of the &Truth launch spreads via Techmeme and social media
Wired's story on AI-driven formal verification startups was picked up and reposted by aggregators and individuals on Mastodon and Bluesky, amplifying the launch news.
“Formal verification, which mathematically proves code correct, attracts startups like &Truth ($70 million) and Harmonic as AI-written code multiplies…”
— @druce.ai, Bluesky user · source -
“The big promise is a future where software runs more reliably with fewer security headaches. But whether AI can bring formal verification beyond the most critical systems at organizations like NASA and Apple and into widespread use remains an open question.” [embedded post]
2 more of the top 3 · 3 posts in this stretch
-
S
This is definitely reading like @ CraigStuntz launched a stealth startup on vibe coding. https://www. wired.com/story/software-verif ication-is-the-hot-new-answer-to-the-ai-safety-crisis
-
Formal verification, which mathematically proves code correct, attracts startups like &Truth ($70 million) and Harmonic as AI-written code multiplies
-
-
1
Antithesis CEO calls formal verification impractical at scale
Will Wilson, who runs bug-hunting AI startup Antithesis, said formal verification is 'a trap' for math enthusiasts and described his own company's effort to formally verify its cybersecurity defenses as a 'pain in the ass,' noting it still missed bugs his tool later found.
“a trap…”
— Will Wilson -
first by Wired, 14d ago
-
-
background
&Truth publicly launches with $70 million raised — Startup &Truth, which Stanford researcher Chuyue Sun joined in August, launched publicly, building on her research showing an AI tool verified part of Signal's encryption code in under half a day for under $500 versus five months of expert work.
-
background
Harmonic's Aristotle adds C and Verilog verification support — Harmonic, cofounded by Robinhood CEO Vlad Tenev and backed by $295 million in funding, announced its math-focused AI agent Aristotle now supports verifying software in C and hardware designs in Verilog, and is evaluating the tech with chipmakers Tensordyne and Nvidia.
-
background
Anthropic and Theorem announce AI-found bugs missed by tests — Anthropic and verification startup Theorem jointly announced they used AI to help find bugs in open source software that trillions of tests had failed to catch, and introduced a Claude add-on for verification.