&Truth emerged from stealth on October 29, 2026, disclosing $70 million in seed funding to build what it calls a universal verification machine for code. The public benefit corporation, founded in early 2026, says the system will read code in any programming language and produce mathematical proof that it is safe, secure and correct. Backers are described as formative AI safety and venture capital leaders. For business, the claim matters because AI now writes most new code while testing catches only part of the defects.
Seed funding and a machine for checkable proofs
The company positions formal verification as a replacement for reliance on testing and vendor assurances. Instead of test coverage, customers would receive proofs that anyone can independently check. &Truth says AI has already accelerated formal proof work by 100x or more, and its own proof automation adds another 100x, compressing work that took years or months into hours or minutes. The second pillar is specification factory technology that translates human intent and business requirements into precise formal specifications at scale. The headquarters are split between Palo Alto and Singapore, with the Singapore office set to expand across research, engineering, product and go-to-market.
The technical base is Lean, an open-source proof system, and Mathlib, a library of more than two million lines of mathematical definitions and theorems, plus open-source technologies including CSLib. &Truth describes the goal as a universal formal vocabulary for software: mathematical models of languages and systems, proof techniques and precise specifications that allow automated verification across languages. It works with the Lean Focused Research Organization and intends to release its foundational libraries as open source. The long-term vision is framed as a move from vibe-coding to veri-coding, where AI-generated code is verified before deployment and agents run inside provably contained environments.
Formal verification has existed for decades but stayed limited to a handful of critical systems because experts formulated proofs manually at high cost. The classic example cited is the seL4 microkernel, whose original proof required about 20 person-years for about 8,700 lines of code, later used in Boeing Unmanned Little Bird under DARPA HACMS program that a professional red team could not breach. The urgency argument rests on new scale: Sundar Pichai said 75% of new code at Google is now AI-generated, while Veracode 2026 testing found models failed on nearly half of security-relevant tasks. September 2026 brought 14,959 published vulnerabilities, 3.5 times more than a year earlier, plus a campaign where an attacker used hundreds of AI agents against 395 organizations in 48 countries via print-management software.
What verified code means for companies
For companies that deploy AI-generated software, the practical effect would be a different form of acceptance: a checkable guarantee instead of a test report. Large enterprises with regulated systems, embedded software and critical infrastructure could add verification to release gates for new services, agent actions and legacy modernization. Small firms without formal-methods teams could gain access to the same control if it arrives as an automated service built on shared libraries. The value appears in procurement and audits, where a Lean proof offers an artifact that internal security and external reviewers can validate without repeating all the work.
The limits remain substantial and deserve direct questions to the vendor. It is unclear which languages, frameworks and system properties the machine covers first, how complete the specifications must be, and what happens with incomplete or changing business requirements. The cited demonstrations, including Anthropic model formalizing Fermat Last Theorem proof in Lean in 11 days and a Lean version of zlib compression library built with Claude, show capability but do not by themselves prove routine industrial throughput. Buyers should ask about proof-checking workflow, integration with development pipelines, handling of third-party dependencies, and ownership of specifications. This news alone does not mean verified code is already available as a product.
The marker to watch is whether &Truth publishes its foundational libraries as open source and names pilot verifications with measurable time and scope. The team brings relevant weight: Stanford professor Clark Barrett, VERSE Lab founder Ilya Sergey, Lean 4 co-architect Sebastian Ullrich and Lean creator Leonardo de Moura in a roundtable, plus Singapore official Low Jin Yong supporting the base. If independent engineers reproduce proofs in Lean within hours, verification becomes a procurement requirement. If releases stall, it stays a research promise.
