A Palo Alto startup called &Truth is working on technology meant to catch software bugs before they ever ship, using mathematical proof rather than conventional testing. The company is one of several building this kind of verification technology, according to The New York Times, which describes Silicon Valley as racing to build AI systems that aim to eliminate the dangerous flaws, or bugs, buried in the world's computer software.
&Truth is pursuing that goal with Lean, a specialized programming language used for formal verification, according to the same Times report. The paper identifies Clark Barrett, a Stanford University professor, as among the company's founders and its co-chief executive. Barrett's academic work sits at the center of the pitch: a mathematical proof, rather than a battery of tests, as the standard for trusting that a piece of software actually does what it claims to do.
Why Proof Is Different From Testing
The distinction between testing and proof is not just semantic in this corner of computer science. Testing can show that software behaves correctly in the scenarios engineers thought to check, but it cannot rule out every possible input or edge case. A formal proof, by contrast, is meant to hold for every case within its stated bounds — which is part of why &Truth and companies like it see Lean, described as an open-source proof system, as foundational to the effort.
That approach is already showing up in industry research. Anthropic, working with a company called Theorem, used its Claude AI model to prove security properties at the assembly-code level across more than 100 real-world open-source software libraries, according to Anthropic. In one part of that effort, Claude proved there were no crashes on any input up to 64 megabytes for 239 entry points spanning 123 different OSS-Fuzz libraries. Anthropic says Claude also surfaced bugs that had gone undetected for years, despite trillions of test runs, and the companies are publishing a subset of the proofs so outside researchers can verify and reuse them.
The Scale of the Security Problem
The urgency behind this push traces back to a widening gap between how much code AI now writes and how secure that code actually is. Veracode's 2026 GenAI Code Security Report found that roughly 44% of AI code-generation tasks introduced a risky security vulnerability during testing, with an average security pass rate across models of just 56%. Even the strongest performer in Veracode's tests, GPT-5.5, passed only 68% of security tasks — meaning it still failed close to a third of them.
Veracode's findings also show the problem is uneven across vulnerability types. Models handled SQL injection fairly well, passing 83% of those tests, and reached 87% on cryptographic algorithms. But performance fell sharply on cross-site scripting, at just 15%, and log injection, at 12%. The report frames it simply: syntax is effectively solved, with models generating syntactically correct code nearly 100% of the time, but secure coding has not followed the same curve.
Vulnerability Counts Keep Climbing
Those gaps are landing at a moment when publicly tracked software vulnerabilities are accumulating faster than ever. The CVE List v5 recorded 14,959 published vulnerabilities in September 2026, up 21.5% from 12,315 in August, which Vulnerability-Lookup called the highest monthly volume ever recorded at the time. The same report tallied 43,109 sightings across 15,296 distinct vulnerabilities for the month, a 27.8% increase over August, and found that 166 distinct vulnerabilities entered at least one tracked Known Exploited Vulnerabilities catalog, compared with 102 the month before.
It's against that backdrop that &Truth and its peers are positioning formal verification as more than an academic exercise. The Times names &Truth alongside other Silicon Valley startups, Axiom and Logical Intelligence, as well as established AI labs Anthropic and OpenAI, as organizations chasing some version of provable software correctness. Anthropic's own writeup offers a sense of just how labor-intensive that work has historically been: implementing the seL4 operating-system kernel took about two person-years, the company says, but formally verifying it took roughly 20 person-years — a gap that AI-assisted proof tools are meant to close.
&Truth's basic premise, as reported, is that software trust should come from a verifiable mathematical guarantee rather than from a vendor's assurances or a test suite's track record. Whether that premise translates into a working, deployed product at scale remains to be seen, and claims about the company's internal methods, funding, and specific performance gains fall outside what has been independently confirmed by the sourcing in this report. What's clear from the available reporting is that &Truth has entered a field already crowded with major AI labs and fellow startups, all wagering that proof — not just testing — is where software security is headed next.
