# &Truth Launches With $70 Million to Automate Formal Verification, Betting AI-Written Code Will Need Mathematical Proof

Times of AI Desk · 2026-10-30 · Research

[https://timesof.ai/2026/10/andtruth-70m-formal-verification-code](https://timesof.ai/2026/10/andtruth-70m-formal-verification-code)

> &Truth, a public benefit corporation based in Palo Alto and Singapore, emerged from stealth on October 29 with $70 million in seed funding to build what it calls a universal verification machine: software that reads code in any language and proves it meets precise requirements. It builds on Lean and plans to open-source its core libraries. WIRED reports it joins rivals such as Harmonic and Theorem, while skeptics say proof is no substitute for testing.

Formal verification has spent decades as a tool for the few systems worth the cost, and &Truth's $70 million bet is that AI-generated code changes that math. The startup, which emerged from stealth on **October 29**, says it is building a "universal verification machine" to read code in any programming language and prove that it is "safe, secure, and correct," with proofs anyone can check.

## What &Truth says it is building

&Truth says it was founded in early 2026 as a public benefit corporation, with headquarters in Palo Alto and Singapore, and raised **$70 million** in seed capital from "AI safety and venture capital leaders" it does not name. It says it builds on the Lean proof system and open-source projects including CSLib, works with the Lean Focused Research Organization, and intends to release its foundational libraries as open source.

Its co-founders are Stanford professor **Clark Barrett** and **Chris Hsu**, who are co-CEOs, and **Ilya Sergey** of the National University of Singapore, its chief science officer. The company says its "specification factory" will turn business requirements into formal specifications. "Once we can state precisely what code must do, AI can help prove that it does it," Barrett said in the release.

## A crowded, unproven field

WIRED reports that &Truth joins a wave of startups using AI to automate verification. Harmonic says its Aristotle agent now verifies C software and Verilog hardware designs, and Anthropic and Theorem recently [used Claude to write machine-checked no-crash proofs](https://timesof.ai/2026/10/anthropic-theorem-claude-formal-proofs-123-oss-fuzz-libraries-risc-v) for open-source libraries. The same tools are behind recent [AI-assisted results in mathematics](https://timesof.ai/2026/10/axiom-lean-formalization-classification-finite-simple-groups).

WIRED also reports that the technology is still at the prototype stage and that it is unclear what customers will pay. Antithesis chief Will Wilson called formal verification "a trap" and said his company has found bugs in software customers had already verified, and Proofcraft's leaders warned that AI-written specifications could inspire "unjustified trust."

## Limits

- &Truth's speed-up claims are its own and come without published benchmarks; it has not named customers.
- The company does not name its investors or disclose a valuation.

## Sources

- [&Truth: &Truth Emerges From Stealth (October 29, 2026)](https://andtruth.com/press/andtruth-emerges-from-stealth/)
- [WIRED: The 'Pain in the Ass' Math That Could Save Vibe Coding From Itself (October 29, 2026)](https://www.wired.com/story/software-verification-is-the-hot-new-answer-to-the-ai-safety-crisis/)