As AI accelerates mathematical proof, &Truth is developing a “specification factory” to translate human intent into precise, mathematically verifiable specifications.
A mathematical proof can establish that software meets a specification. It cannot establish that the specification says what people actually meant. As AI makes formal verification increasingly practical, that distinction is becoming one of the central challenges in software safety.
Chris Hsu is Co-Founder, Co-CEO and Executive Chairman of &Truth, which emerged publicly in October to build a “universal verification machine” to establish specified safety, security and correctness properties of software. Its ambition extends beyond generating proofs: &Truth is developing a “science of specification” and, ultimately, a “specification factory” capable of translating complex human requirements into precise, reviewable statements at scale. The aim is not merely to prove that code works as written, but to establish whether it does what people intended.
Why Faster Proof Makes Specifications More Important
A specification defines what software must do, what it must not do and the assumptions under which those requirements apply. A proof can establish that code satisfies those conditions across the executions covered by its formal model. If the specification overlooks a critical failure, however, the proof may be entirely valid and the software still unsafe.
Historically, formal verification demanded extraordinary effort. The seL4 operating-system microkernel, roughly 8,700 lines of C in its original verified implementation, became a landmark demonstration of what rigorous assurance could achieve. Its development and verification required years of specialized work. That cost helped confine the most ambitious verification projects to high-assurance domains.
AI is beginning to change the economics. Anthropic has reported progress using Claude and the Lean proof assistant to produce machine-checked mathematical formalizations, including work on Fermat’s Last Theorem. The accomplishment illustrates the growing ability of AI systems to work with formal proofs, although the scope and assumptions of any claimed result matter.
Anthropic has also reported verifying selected no-crash properties for entry points in compiled open-source libraries, under specified limits and execution assumptions. Such results are significant but narrower than proving that entire libraries are correct or safe in every environment. Faster proof generation increases the value of a question that proof itself cannot answer: Were the right requirements specified?
Why Proof Alone Can’t Capture Human Intent
Consider software that calculates interest on a bank account. A proof might establish that the program consistently applies the rate supplied to it. That says nothing about whether the rate is contractually correct, how interest should accrue when terms change mid-period, or what should happen when an account closes on a payment date. Those are decisions about intended behavior, not gaps a proof checker can resolve.
Each decision must be expressed in a specification before it can be verified. AI can help infer requirements from code, documentation and examples, but existing code may preserve historical mistakes, and written requirements may conflict. Human review remains essential to deciding which behavior is legitimate and which is an accident.
This is the paradox at the center of Hsu’s argument. Formal verification can establish that software meets a precisely stated requirement while exposing uncertainty about whether that requirement captures the real objective. The goal is to expose the gap between human intent and machine behavior, scrutinize it, and ultimately close it through faithful specifications, human validation and mathematical proof.
A formal specification translates human intent into precise, mathematically defined properties against which software can be verified. Closing the gap between intent and implementation requires more than better proof tools: it requires a shared language for specifying what software must do, and the ability to prove that it does.
Software Needs a Language of Specification
Mathematics offers a useful comparison. Lean’s Mathlib library supplies a shared body of formal definitions and theorems on which researchers and AI systems can build. Before a computer can verify a proof involving prime numbers, it needs a precise definition of a prime number. That foundation is the product of years of collective work.
Software is less settled. Programming languages, operating systems, processors and dependencies change. The intended behavior of a banking system or medical device may be scattered across contracts, regulations, user expectations and undocumented practice. A useful specification must connect those human requirements to a rigorous model of how software actually executes.
&Truth is developing reusable foundations for that work, drawing on open-source efforts including CSLib, which seeks to give computer science some of the formal vocabulary that Mathlib provides for mathematics. Hsu co-founded &Truth with Clark Barrett, a Stanford computer scientist and founding co-director of the Stanford Center for AI Safety, and Ilya Sergey of the National University of Singapore, a co-creator of the open-source verification tools Veil and Velvet. Their approach emphasizes expressive specifications, reusable abstractions and modular proofs that can scale beyond isolated functions.
The difficulty is not only mathematical. Real systems encounter conditions their designers did not anticipate. As observed in comments reported by The New York Times, software eventually meets the messiness of the real world. Verification is powerful precisely because its assumptions can be stated and scrutinized; it does not make those assumptions automatically true.
Building a Specification Factory
&Truth’s emerging “specification factory” aims to transform specification from a largely manual, bespoke craft into a scalable, increasingly automated process. It would translate human intent and software requirements into precise formal specifications, identify ambiguities and omissions, and connect specified properties to code and independently checkable proofs. Crucially, human judgment remains essential to ensuring those specifications faithfully capture what the software is actually intended to do.
This goes far beyond translating natural language into mathematical notation. Such a specification factory must distinguish intended business rules from entrenched software bugs, define critical security and correctness properties, expose underlying assumptions, and make specifications understandable and reviewable by engineers and domain experts.
&Truth is also mapping open-source C software, distinguishing code that has been analyzed from properties that have actually been proved, and developing ways to visualize specifications and their links to verification results. These efforts can make assurance more transparent, but neither a map nor a generated specification establishes that the intended requirements are complete.
Proof automation has an unusually clear test: an independent checker accepts or rejects a proposed proof against a formal statement. Specification fidelity has no comparably simple universal test. Requirements can be incomplete, ambiguous or internally inconsistent. A successful specification factory will therefore need not just generation speed but methods for review, validation, traceability and revision as human needs evolve.
Hsu’s interest in the relationship between human intent and machine behavior extends beyond software engineering. Through the Infinitude Foundation, where he serves as President, he supports research into AI safety, consciousness and the philosophy of mind. His earlier career as CEO of Kilometre Capital and Managing Director at Citadel exposed him to the importance of precision and reliability in complex financial systems. Across these pursuits ran a common concern: distinguishing what systems demonstrably do from what humans assume or intend them to do, and establishing that distinction with rigor.
The potential payoff is substantial. Developers could verify AI-generated code against precise specifications rather than relying primarily on manual review and testing. Enterprises could mathematically verify that critical software meets defined business requirements. They could modernize legacy systems while preserving essential functionality and verify future changes against the properties their operations depend on. As AI generates increasingly complex software, specifications could become the essential bridge between human intent and machine behavior.
The ambition goes beyond automating mathematical proof. It is to make the specification of human intent a rigorous, scalable science. A specification factory could turn complex requirements into precise, reviewable statements, continuously refined and linked to independently checkable proofs. Hsu’s wager is that the gap between human intent and machine behavior can ultimately be closed by combining rigorous specification, human validation and mathematical proof, enabling software to be verified not just against formal requirements, but against what humans actually intend.
