What did &Truth launch with $70 million?
&Truth, a public benefit corporation, emerged from stealth on October 29, 2026 with $70 million in seed funding. The company says it will build a "universal verification machine" that reads code in any programming language and proves it meets precise requirements. It is headquartered in Palo Alto, California, with an international base in Singapore.
The startup was founded in early 2026. Its announcement describes the round only as coming from "a group of formative AI safety and venture capital leaders", and it does not name a single investor. That gap matters, because the identities of early backers often signal which institutions will fund the next round.
The leadership is unusually academic. Clark Barrett, a Stanford computer science professor and project lead for the cvc5 reasoning engine, is co-CEO. Ilya Sergey, who founded the VERSE Lab at the National University of Singapore, is chief science officer. Sebastian Ullrich, a co-architect of the Lean 4 theorem prover, is also on the team. Barrett and Sergey have spent their careers building verification tools rather than consumer products.
Chris Hsu, a former Citadel managing director, is the other co-CEO and executive chairman. Gregory Malecha, who previously led formal methods work at BlueRock Security, and Drew Harman, a former chief commercial officer at Fastino Labs, complete a group that mixes proof engineering with enterprise sales.
&Truth's central claim is speed. The company says AI has already accelerated formal verification by "100x or more", and that its own proof automation adds another 100x. It says work that once took years or months can now take hours or minutes. Those multipliers are company claims, not independently verified results.
The harder problem is the specification. A proof is only as good as the statement it proves, and most software has no precise statement of intended behavior. &Truth says it is building a "specification factory" that converts human intent and business requirements into formal specifications. Wired reports that the technology remains at the prototyping stage.
The company builds on Lean, an open-source proof assistant, and Mathlib, a library of more than two million lines of mathematical definitions and theorems. It says it works with the Lean Focused Research Organization and intends to release its foundational libraries as open source. That commitment is a promise, not a shipped product.
Why is formal verification suddenly a startup race?
The timing follows a change in how software is written. AI systems now generate code faster than humans can review it, and the same models help attackers find flaws. Anthropic notes that the Linux kernel, one of the most heavily tested codebases in existence, recently disclosed more than 1,000 vulnerabilities.
Testing has not kept pace. Fuzzing throws random inputs at a program and hopes to trigger a crash, but it cannot prove that no input will. Formal verification attacks the problem differently, by proving a property for every input within a defined model. That distinction is the reason labs are pouring money into proofs now.
Anthropic and the startup Theorem published a large demonstration on October 22, 2026. Claude wrote machine-checked proofs for 239 entry points across 123 open-source libraries. The company says the effort found bugs that had survived trillions of test runs, and the proofs cover compiled RISC-V binaries rather than source code.
Harmonic moved five days later. On October 27 it extended its Aristotle agent from mathematics to software and hardware, starting with C and Verilog. Wired reports that Harmonic has raised $295 million and was co-founded by Robinhood chief executive Vlad Tenev. Nvidia's venture arm is an investor, and the startup is evaluating the tool with Tensordyne and Nvidia.
&Truth is the third major announcement in the same fortnight. It arrives with less capital than Harmonic and a broader promise: any language, any codebase, proofs that outsiders can check. Smaller players are moving too. Madan Musuvathi left Microsoft Research after more than 20 years to found Truidic, and Proofcraft says inquiries now outpace its capacity.
The competitive question is distribution. Wired reports that startups are unsure whether to sell directly to enterprises or through intermediaries such as Anthropic. A proof tool that lives inside a coding assistant reaches more developers. A direct contract reaches the security team that signs the check.
How much faster and cheaper is AI-assisted verification?
The clearest public numbers come from a paper by Chuyue Sun and seven co-authors, including Barrett. Their system, CryptoProver, produced an independent proof for the cryptography library curve25519-dalek and verified RustCrypto's chacha20 implementation against RFC 8439. The paper was first posted in August 2026 and revised on October 16.
The baseline is striking. The library's original developers reported a focused five-month effort by three people to verify curve25519-dalek. CryptoProver synthesized the internal specifications and proofs in 11.4 hours, with $466.99 in recorded API costs. Wired summarized the result as less than half a day for under $500.
The code is not academic. The paper says these cryptographic lineages underpin deployed systems including Signal and Shadowsocks, and it estimates Signal at 218 million global downloads. A proof about that code therefore speaks to software that protects real conversations, not a toy example.
Anthropic's project ran at a much larger scale. Its 239 proofs total about 180 million lines of Rocq, a proof assistant, with a typical proof around 600,000 lines. The median binary under verification held 18,000 RISC-V instructions. Anthropic describes it, to its knowledge, as the first large-scale effort to apply formal verification to production software at the assembly level with AI.
Harmonic's case studies are smaller but concrete. At chipmaker Tensordyne, Aristotle found bugs up to 110,000 cycles deep in the block the team considered hardest to verify. On LibTomMath, the big-number library behind Tcl and Dropbear SSH, it fixed three bugs and made modular exponentiation 31% to 38% faster in company benchmarks, with the faster code proved against the same specification.
For context, verification has always been expensive. The seL4 operating system kernel took two person-years to implement and 20 person-years to verify, according to Anthropic. The promise of these tools is not that proofs become free. It is that the cost curve bends enough for ordinary products to afford them.
What can a formal proof actually guarantee?
A formal proof establishes that code satisfies a specification for every input the specification covers, under stated assumptions. It does not establish that the specification matches what users need. Anthropic is blunt about this: "Formally verified" does not mean "bug-free."
The assumptions can be narrow. Anthropic's proofs cover single-threaded, statically linked RISC-V binaries using musl libc and a fixed memory budget. Most production software runs on x86 or ARM chips and links dynamically against glibc. Anthropic says closing that gap would require accurate semantics for more architectures and operating systems.
Scope is another limit. Anthropic proved that fuzz-test entry points cannot crash on inputs under 64 MB, including AddressSanitizer failures. AddressSanitizer does not catch every memory-safety bug, and verifying every entry point still would not cover dead code. A caller can also misuse a verified library and corrupt its own memory.
The trusted base is smaller but not empty. Developers must trust the formal models of RISC-V and Linux processes, the exact theorem statements, and the Rocq proof checker. Anthropic argues this is a far more tractable set of artifacts than every line of application code, which is a fair point and not a guarantee.
Apple offers the production example. Its security team verified the ML-KEM and ML-DSA post-quantum algorithms in corecrypto against the FIPS 203 and FIPS 204 standards, and published the proofs for outside review. Apple says corecrypto runs on more than 2.5 billion active devices and that the work achieved the strongest known correctness results for a widely deployed production implementation of the algorithms.
Apple also shows the cultural cost. Wired reports that its security team said some issues found in corecrypto could not have been found any other way. The same team said it must stay conservative about adding code, because every addition must be reviewed and proved.
Barrett's argument is that software lacks what mathematics gained. "Software has lacked an equivalent foundation," he said, referring to Lean and Mathlib. In his view, once code can be described precisely, AI can prove that it does what the description says. The specification, not the prover, is the bottleneck.
Who is using formal verification today?
Formal verification is already inside critical systems. Boeing aircraft, Amazon's servers and Apple devices contain at least some verified code, according to company disclosures cited by Wired. The verified parts are usually security-sensitive: encryption, access control, memory management.
Amazon Web Services treats it as a customer trust tool. Byron Cook, a distinguished scientist and vice president at AWS, told Wired that verification eased customer concerns about cloud security and helped internal teams move faster by catching large bugs early. That is a business case, not a compliance box.
Adoption thins out below that tier. Several midsized technology companies told Wired they have verified one key feature at most, and often none at all. They cite a shortage of verification engineers, costs that exceed the perceived risk, and delays of weeks before code can ship.
Open-source projects are experimenting with grants rather than budgets. The nonprofit Beneficial AI Foundation used an Anthropic grant to validate the same encryption code Sun's team worked on. Michael Rosenberg, a maintainer of curve25519-dalek, hopes sustainable funding appears, but says he has no idea how it will happen.
Pricing is still unsettled. Harmonic sells Aristotle self-serve with consumption-based pricing and offers enterprise deals with on-premises deployment. &Truth has not announced a product or a price. Wired reports that some security executives could imagine paying AI labs for "verified" AI-generated code, which would turn verification into a feature of a coding assistant.
Skills are the quiet constraint. Proof engineering requires familiarity with tools such as Lean, Rocq, Isabelle and Verus, and with the mathematics behind them. Apple says the formulas can be extremely large and need specialized engineering skill. AI lowers the labor per proof, but it does not remove the need for someone who can read the result.
Why are some experts skeptical?
Will Wilson, who runs the bug-hunting startup Antithesis, is the sharpest critic in Wired's account. He calls formal verification "a trap" for mathematically minded engineers. His company spent millions verifying its own cybersecurity defenses, a process he describes as "a pain in the ass", and still found errors with its own testing tool.
His deeper point is about assurance. "It can give you some assurance, but only robust exhaustive testing can prove your assurance is true," he said. Antithesis has also found bugs in software that several customers had formally verified, which suggests proofs can miss the failures that matter in production.
Vitalik Buterin, the Ethereum creator, reached a similar conclusion in a blog post this year. He wrote that "formal verification is not a panacea", while still treating it as an important defense against AI-enabled attacks. The disagreement is about scope, not about whether proofs work.
Proofcraft, one of the few companies that has long offered traditional verification, sees both sides. Chief executive June Andronick and chief scientist Gerwin Klein told Wired that interest now outpaces what they and their competitors can deliver. They also worry that AI-generated specifications could inspire "unjustified trust" in results that may not mean what they appear to.
That worry is structural. If the same model writes the specification and the proof, an error in one can be mirrored in the other. &Truth says it relies on Lean and independently checkable proofs to limit that risk. Anthropic derives its specifications from existing fuzz tests and publishes its trusted components and a subset of proofs for review.
None of this makes verification useless. It makes it a complement to testing, not a replacement. The strongest results in this batch combine fuzzing, patching and proofs: Anthropic let Claude fix the bugs it found, then proved the patched code crash-free.
What should developers and buyers watch next?
The first test for &Truth is whether "any language" becomes a product. Its release describes a universal vocabulary for software, but the company has not published supported languages, benchmarks or prices. Until it does, the $70 million buys a research program with a commercial plan attached.
The second test is measurement. Vendors and researchers still measure verification with their own benchmarks and case studies. Buyers should ask three questions before trusting a demo: which specification was proved, which assumptions the proof depends on, and whether an independent checker can reproduce the result.
The third is the cost curve. Anthropic says proofs can consume hundreds of millions of tokens, which makes verification a compute purchase as much as a license. It reports that Opus 5.5 proves half of 36 sample tasks with about 40% fewer tokens than Opus 5, and that agents sharing proofs used 17% fewer tokens. Reuse, not raw model power, may decide which vendor wins.
Watch the dependency graph as well. Anthropic's collaborator Theorem is working toward verifying the Nix ecosystem, including glibc, OpenSSL and cURL. If a small set of shared libraries is proved once, a large share of software inherits the guarantee. That is the same leverage that made Mathlib useful to mathematics.
For engineering teams, the practical steps are modest. Start with code that handles secrets or untrusted input, where a bug is expensive. Keep tests and fuzzing, because proofs only cover what the specification describes. Ask vendors to publish their trusted base and their failure cases, not just their wins.
The shift is real even if the marketing is ahead of it. Until recently, a five-month proof by three experts looked like a reasonable use of specialist time. This month, a paper put a comparable proof at 11.4 hours and $467. Harmonic is selling the idea that this can happen on every commit, and &Truth has $70 million to build it. The proof still has to be checked, and the specification still has to be right. But the queue for verification is finally moving.