&Truth Raises $70 Million to Automate Formal Software Verification

&Truth raised $70 million in seed funding to build tools that check code against formal requirements and produce inspectable proofs, adding a new company to a field with recent AI-assisted verification work.

The public benefit corporation was founded in early 2026 and has its U.S. headquarters in Palo Alto, California, and its international headquarters in Singapore. &Truth said it emerged from stealth Thursday, Oct. 29. The company said the round came from AI-safety and venture-capital leaders, but it did not name investors or disclose a valuation.

The system is intended to check code across programming languages against formal requirements, then generate proofs other people can inspect. &Truth is building on Lean and open-source projects such as CSLib. It plans to release its foundational libraries as open-source software.

Formal verification uses mathematical specifications to check whether software meets defined requirements. A proof covers the specification and model used to produce it; it does not show that the requirements capture every user need or that the model accounts for every real-world condition. The scope depends on what the specification asks and what the model represents. A result can establish a stated property while leaving behaviors outside that property unaddressed. This separates checking whether code follows a rule from deciding whether that rule covers the intended use.

Anthropic and Theorem recently verified specified security properties at 239 entry points across 123 open-source libraries. Those figures describe different units: code entry points and libraries. The work depended on conditions that included modeled Linux behavior and single-threaded, statically linked RISC-V binaries. Those conditions limit what the results establish. Our Oct. 23 report covered this verification work.

&Truth says AI can accelerate formal verification by at least 100 times and that its own proof automation adds a further 100-fold gain. The company estimates that work taking months or years could be shortened to hours or minutes. Its announcement did not include benchmark results for those performance claims.

“Trust in software should rest on independently checkable proof, not any company's word, including ours,” said Ilya Sergey, &Truth's co-founder and chief science officer.