Pomegra
&Truth emerged from stealth on October 29, 2026 with $70M in seed funding to build a universal verification machine that mathematically proves code is safe and correct.
Key Takeaways
- &Truth disclosed $70M in seed capital on October 29, 2026, with no lead investor or valuation named.
- The Palo Alto and Singapore company claims proof work can fall from months or years to hours or minutes.
- Its founders come from Stanford, the National University of Singapore and the team behind the Lean proof system.
Lead
&Truth, a public benefit corporation founded in early 2026, announced on October 29, 2026 that it has raised $70 million in seed capital. The company is building what it calls a "universal verification machine": a system meant to read code in any programming language and produce a mathematical proof that the code is safe, secure and correct. Anyone can check those proofs independently.
The company is headquartered in Palo Alto, California, with an international base in Singapore. It did not name its investors, describing them only as a group of formative AI safety and venture capital leaders. It disclosed no lead investor and no valuation.
Who Is Behind &Truth?
The founding team mixes academic formal-methods researchers with an investor-operator. Clark Barrett, a Corbel Professor at Stanford and founding co-director of the Stanford Center for AI Safety, is co-founder and co-CEO. Ilya Sergey, who founded the VERSE Lab at the National University of Singapore, is co-founder and chief science officer.
Chris Hsu, a former Citadel managing director, is co-founder, co-CEO and executive chairman. The roster also includes Sebastian Ullrich, a co-architect of Lean 4 and co-founder of the Lean Focused Research Organization, and Gregory Malecha, who works on systems code verification and previously worked at BlueRock Security. Linus Lee, formerly a managing partner at Kilometre Capital, and Drew Harman, formerly chief commercial officer at Fastino Labs, round out the group named in the announcement.
What Does a Universal Verification Machine Actually Do?
It takes source code and returns a machine-checkable proof that the code behaves as specified. That is formal verification, a discipline that has existed for decades but has stayed confined to a handful of critical systems because human experts had to write the proofs by hand.
&Truth's approach rests on Lean, an open-source proof system, and on open-source projects including CSLib, co-created by Barrett, and the cvc5 automated reasoning engine. The company says AI can accelerate formal verification by at least 100 times, and that its own proof automation adds a further 100-fold gain. On that basis it projects work that once took months or years can finish in hours or minutes. Those figures are the company's own and have not been independently demonstrated at scale.
The company also describes a "specification factory" that translates business requirements into formal specifications. This addresses the harder half of the problem: a proof only guarantees that code matches a specification, so a wrong specification yields a correct proof of the wrong thing.
Why Does Verification Matter Now?
AI coding tools now generate software faster than humans can review it. &Truth frames the answer as a shift from "vibe coding" to "veri coding," in which AI-written code is verified before deployment and AI agents run inside provably contained environments. Its stated aims also include modernizing legacy software and protecting critical infrastructure with independently checkable guarantees.
Sergey put the company's pitch plainly: "Trust in software should rest on independently checkable proof, not any company's word." Leonardo de Moura, creator of Lean, offered a shorter version: "Testing provides confidence. Proof provides a guarantee."
How Does the Round Compare With Rivals?
&Truth is not alone. Wired reported the launch as part of a wave of startups betting that generative AI can make formal verification practical. Harmonic, for one, announced that its math-focused agent, Aristotle, can verify software written in C and hardware designs in Verilog. Nvidia's venture arm is an investor in Harmonic, not in &Truth.
A $70 million seed is large by conventional standards, and the absence of a named lead or valuation limits what the round reveals. Without investor names, the figure signals appetite for the category but says little about who is underwriting the company's claims. The AI safety framing in the investor description suggests backers motivated by risk reduction as much as by software-tooling returns.
What Are the Risks?
The central risk is the gap between demonstration and deployment. Proof automation works best on well-bounded code, and real enterprise systems carry legacy dependencies, undocumented behavior and ambiguous requirements. Writing correct specifications remains the bottleneck, and no tool fully removes human judgment there.
There is also a market question. Most software teams ship on testing and code review, and few pay for guarantees until a failure costs them. Regulated and critical sectors, such as aerospace, finance and infrastructure, are the likelier early buyers.
Outlook
&Truth enters with $70 million, a team tied to Lean and Stanford and NUS research, and a claim of 10,000-fold speedups that remains unproven in public. The undisclosed investors and valuation leave the round's quality hard to judge. Product releases, named customers and published benchmarks will decide whether the "universal" label holds.
