A $70 Million Seed to Make Code Prove Itself: Verification Startup &Truth Emerges From Stealth

A startup called &Truth came out of stealth this week with $70 million in seed funding and an ambition that sounds almost antiquated in the age of vibe coding: mathematically proving that software does what it is supposed to do. The company, incorporated as a public-benefit corporation with headquarters in Palo Alto and an international base in Singapore, wants to build what it calls a universal verification machine — a system that can read code in any programming language and produce machine-checkable proofs of safety, security and correctness under clearly stated assumptions.

The founding team is unusually academic for a company carrying this much seed capital. Co-founder and co-CEO Clark Barrett is a Stanford professor and one of the architects behind widely used SMT solvers, the automated reasoning engines that underpin much of modern hardware verification. Ilya Sergey, the chief science officer, founded the VERSE Lab at the National University of Singapore and has spent his career on program verification and proof engineering. Chris Hsu, co-CEO and executive chairman, came from a very different world: he previously ran Kilometre Capital and was a managing director at Citadel Investment Group. The round was funded by a group of AI safety and venture capital leaders the company has not named, and Singapore's economic development agency publicly welcomed the headquarters decision.

The timing is not accidental. AI coding tools now generate software faster than humans can review it, and a wave of startups is betting that generative models can make formal verification — historically a niche discipline confined to NASA missions, chip designs and a handful of cloud provider internals — practical for ordinary commercial code. Harmonic, the math startup cofounded by Robinhood CEO Vlad Tenev, said the same week that its Aristotle agent can verify C code and Verilog hardware designs. Anthropic has worked with the verification startup Theorem on finding bugs that trillions of tests missed, and former Microsoft Research scientist Madan Musuvathi has formed a company called Truidic to commercialize automated verification.

&Truth is building on Lean, the open-source proof system that has become the de facto standard for machine-checked mathematics, and says it will release its foundational libraries as open source. The company claims that AI can speed up verification by roughly 100 times, and that its own proof-automation stack adds another 100 times on top — figures nobody outside the company has checked. Those claims matter less than the structure of the pitch, though: the point of a formal proof is that anyone can independently verify it, separating the production of an assurance from any single vendor's word. "Trust in software should rest on independently checkable proof, not any company's word," Sergey said at launch. Leonardo de Moura, the creator of Lean, offered his own framing: "Testing provides confidence. Proof provides a guarantee."

There is early evidence that the approach can work on real code, with caveats. An earlier paper from one of the company's researchers describes using AI to verify a production cryptographic library in 11.4 hours, with about $466.99 in recorded API charges — starting from supplied contracts and a human-provided proof order, and covering functional correctness against those contracts rather than cryptographic security, side-channel resistance or the adequacy of the specifications themselves. The authors themselves warn against reading the runtime as a drop-in replacement for the eight-month human effort it echoes. The specification, in other words, remains a human accountability problem: a machine-checked proof of the wrong requirement is worthless.

Skeptics are not hard to find. Will Wilson, CEO of bug-hunting startup Antithesis, has called formal verification "a trap" on its own, noting his firm spent millions verifying defensive systems and still found more errors with plain testing tools. Ethereum creator Vitalik Buterin has similarly warned that formal verification is not a panacea. Several midsize companies told WIRED that waiting weeks for verification results slows development, and verification engineers remain scarce — so scarce, the report noted, that most midsize companies have formally verified at most one key feature of their software.

The commercial bet, then, is that AI collapses the labor cost of proof generation just as AI collapses the reliability of unverified code. If both curves hold, regulated industries — aerospace, finance, critical infrastructure — become the first customers, and "veri coding" becomes a budget line rather than a research curiosity. If the specifications stay too expensive to write, the $70 million will have funded a very rigorous demo. The field now has a well-capitalized new entrant, an open-source plan, and a testable promise: proofs that are independently checkable, at a price that ordinary software teams can pay.