&Truth Secures $70M to Automate Code Safety Proofs

&Truth, a startup focused on mathematically verifying software safety, has exited stealth with $70 million in seed funding. The company aims to build a system that can analyze code in any language and generate verifiable proofs of its correctness, security, and safety—something that has historically required years of expert effort. The round, backed by investors with ties to AI safety and venture capital, marks an unusual bet on scaling formal verification beyond its traditional niche.

The company’s technology draws on established research in automated reasoning, using Lean, an open-source proof assistant, and Mathlib, a vast library of mathematical definitions. &Truth’s "specification factory" is designed to help organizations convert business requirements into formal specifications, allowing proofs that don’t rely on testing or vendor assurances. Co-CEO Clark Barrett, a Stanford professor and automated reasoning expert, argues that software lacks a standardized foundation for verification akin to what Lean and Mathlib provide for mathematics. Co-Chief Science Officer Ilya Sergey, who leads the VERSE Lab at the National University of Singapore, frames the mission as shifting trust from corporate claims to independently checkable evidence.

The $70 million investment stands out in a field where formal verification has been too costly and complex for widespread adoption. While the technique has been used in critical systems like aerospace and defense, it has remained out of reach for most developers. &Truth’s announcement points to recent AI breakthroughs as a turning point, citing examples where AI models have formalized complex proofs in days rather than years. The company claims its automation can accelerate proof generation by orders of magnitude compared to manual methods, though these figures have yet to be demonstrated at scale.

The urgency behind &Truth’s work is tied to rising concerns about software vulnerabilities. The company highlights recent incidents, including a large-scale attack exploiting flaws in widely used software and a surge in reported vulnerabilities. Industry trends, such as the increasing use of AI-generated code and its associated security risks, have amplified calls for more reliable verification methods. &Truth’s pitch is that formal verification, long limited to high-assurance sectors, could now become viable for broader software development.

The team behind &Truth includes academic leaders in automated reasoning and experienced investors. Barrett and Sergey bring deep expertise in the field, while Executive Chairman Chris Hsu, a former Citadel managing director, adds institutional investing experience. The company operates out of Palo Alto and Singapore, with plans to expand its Singapore office—a move aligned with the city-state’s efforts to position itself as a hub for trusted AI. &Truth also collaborates with the Lean Focused Research Organization and intends to open-source its foundational libraries, suggesting an effort to standardize verification across programming languages.

The funding round raises questions about whether AI-accelerated formal verification can deliver on its promises. While &Truth’s rapid progress—founded in early 2026 and emerging from stealth within months—is notable, its claims of dramatic speedups remain untested in real-world scenarios. The cybersecurity market has seen similar hype before, with tools promising to revolutionize code review or vulnerability detection, only to face adoption challenges. &Truth’s success will depend on whether its technology can handle the complexity of production codebases, not just controlled examples. If it works, it could redefine how developers and enterprises approach software safety, particularly as AI-generated code becomes more common.

For now, the $70 million seed round is a notable signal. Such large seed investments are uncommon for infrastructure plays, especially in a specialized field like formal verification. The involvement of AI safety leaders and venture capitalists suggests a belief that the market for provably safe software is poised for growth. Whether &Truth can turn mathematical guarantees into a widely adopted product remains an open question—one that will determine whether this funding is an early bet on the future of software trust or a cautionary tale about overpromising in a high-stakes field.

Sources: unite.ai