Formal Verification Makes Software Safer. Chris Hsu Argues It Will Also Make Coding Faster, Possibly Fearless

As AI accelerates software development, &Truth is building a universal verification machine to make mathematical proof practical at scale, transforming software security while unlocking faster, more ambitious engineering.

By Exec Edge Editorial Staff

When you visit a website whose address starts with “https,” your browser runs a burst of math to scramble the data so outsiders can’t read it. In Chrome, some of that core math comes from Fiat Cryptography, an MIT project that writes the code automatically and proves, mathematically, that it does exactly what it’s supposed to do. The proven code runs as fast as the best versions written by hand, and by 2019 it was handling about 90% of Chrome’s secure connections. Almost nobody outside cryptography has heard of it.

Chris Hsu wants that kind of guarantee to stop being rare. In early 2026 he co-founded &Truth, a public benefit corporation where he is Co-Founder, Co-CEO and Executive Chairman, to leverage AI to make proofs like Fiat’s cheap and fast enough to cover far more of the world’s software. His reasoning is that as AI writes and attacks more of that code, software that probably works is no longer “good enough.” In a safer future, he proposes, code should be proven at scale. In the company’s framing, &Truth is building a “universal verification machine” for code: a system that reads software in any programming language and proves it satisfies precisely stated requirements for safety, security and correctness, with proofs that anyone can check independently rather than taking any one company’s word for it.

What Already Runs on Proof

A well known formal verification example is seL4, the small core of an operating system, known as a microkernel. Its code has come with a machine-checked mathematical proof of correctness since 2009. Under a DARPA program called HACMS, it was installed in the mission computer of a Boeing Unmanned Little Bird, a helicopter that flies without a pilot. A team of professional hackers got six weeks and full access to the code. They couldn’t break in.

So why isn’t all software built this way? Mostly because of cost. The original seL4 is about 8,700 lines of C, which is small by modern standards. Designing, building and proving it still took about 25 person-years of work. That price made sense for keeping a helicopter in the air, but for most software, it never has. The proof itself ran to about 200,000 lines of machine-checked script for those 8,700 lines of C, a ratio that explains why the method stayed rare.

Cost isn’t the only obstacle. Before a computer can prove that code is correct, someone has to write down, in precise mathematical terms, what “correct” means, and that turns out to be a big job.

Mathematicians have already done a version of it using Lean, a programming language for writing proofs that a computer can check step by step, invented by pioneering computer scientist Leonardo de Moura. A computer can’t check a proof about prime numbers until someone has defined, in Lean, what a prime number is. So over several years, hundreds of contributors built Mathlib, a shared library that now holds nearly 300,000 theorems from more than 700 contributors. AI systems that work on advanced math in Lean are built on top of it.

Software has nothing like it yet, because to prove what a program does, a computer needs exact descriptions of how the programming language behaves, how memory works, what happens when several tasks run at once, and even what a file is. Until recently, writing those descriptions has been slow manual work, done one definition at a time.

That work has now started in public. In early 2026, a group of researchers launched CSLib, a Mathlib for computer science. Its founding paper says CSLib “aims to be for computer science what Lean’s Mathlib is for mathematics.” The group includes Clark Barrett of Stanford, Swarat Chaudhuri, Jim Grundy, Pushmeet Kohli, Fabrizio Montesi and Leonardo de Moura, who created Lean. Separately, Ilya Sergey’s VERSE Lab at the National University of Singapore has built two verification tools. The first, Veil, checks distributed protocols, the rules that let many computers coordinate over a network. It was presented at CAV, one of the field’s leading conferences, in 2025. The second, Velvet, checks ordinary programs, and Velvet itself has been proven correct in Lean. It took a Distinguished Paper Award at CAV 2026, one of eight awards among 81 accepted papers drawn from 311 submissions. CSLib’s founding paper names the framework underneath Velvet as something it plans to build on. Stanford’s Clark Barrett and the National University of Singapore’s Ilya Sergey are also co-founders of &Truth with Chris Hsu.

All three projects are open source: CSLib, Veil and Velvet.

Why 2026 and Not 2016

The second thing that’s changed is the cost of the proofs themselves. Thanks to advances in AI, formalization work that once occupied expert teams for years is now being done in days, and the same capability that lets a model find and exploit a flaw lets it produce the proof that closes one.

Considerable public evidence arrived in the weeks before this article. On September 4, Anthropic reported that Claude had produced a complete, computer-checked Lean formalization of Fermat’s Last Theorem, roughly 13 million lines, in 11 days. On October 22, Anthropic reported that Claude had proved no-crash and memory-safety properties for 239 fuzzing entry points across 123 open-source libraries, working directly on compiled RISC-V machine code, and had found bugs along the way that years of fuzzing had missed. Those proofs establish one generic property, that a given test can never crash, under stated assumptions about the machine.

&Truth’s ambition goes further: proving full functional correctness, establishing not merely that software avoids crashes, but that it behaves exactly as specified. Historically, such proofs required months or years of expert effort. AI is now accelerating proof generation by approximately 100x, while &Truth’s proprietary proof automation aims to deliver another 100x improvement. Together, &Truth anticipates, these advances will reduce verification from years or months to hours or minutes, making rigorous, independently checkable software correctness practical at scale.

Chris Hsu has made the same observation about timing: AI has amplified the threat to software and, over the same stretch, made the defense tractable. His larger argument is that once AI writes and attacks much of the world’s code, probability stops being good enough and systems need proof.

He co-founded &Truth in early 2026 with Clark Barrett, founding co-director of the Stanford Center for AI Safety and director of the Stanford Center for Automated Reasoning, and Ilya Sergey, founder of the VERSE Lab at the National University of Singapore. Established as a public benefit corporation with the mission of ensuring AI develops safely for humanity, &Truth is building a universal verification machine to make mathematically provable software safety, security, and correctness practical at scale.

The company is building its verification engine on Lean, so a third party can recheck any proof it produces with the same public tool, and it plans to release the foundational libraries it builds as open source. The PBC, with U.S. headquarters in Palo Alto and international headquarters in Singapore, was funded with $70 million of seed capital from leading AI safety and venture investors. Its stated reason for building in the open is structural: a verification layer the world relies on “can’t depend on any single company, including ours.”

Hsu came to &Truth from investing, philanthropy, and technology. He was Founding Partner and CEO of Kilometre Capital, Managing Director of Citadel Investment Group, and is Chief Investment Officer of his family office, Rocketeer Management. He is also a member of the Lean FRO Strategic Advisory Board. Through the Infinitude Foundation, where he is President, he has funded formative research on AI safety and formal verification.

The Case for Speed

Safety is the usual reason to want proof. There’s also Hsu’s case that it will make software faster to build and improve.

When a software team slows down, people tend to blame headcount or technical debt, the pile of old shortcuts that makes code hard to change. Uncertainty slows teams down too. Before each release, teams rerun large batches of tests to make sure nothing that used to work has broken, and the release waits until they finish. A fix that would plainly make a program faster often doesn’t ship at all, because nobody can be sure it won’t change how the program behaves somewhere else. Banks and government agencies keep decades-old code running for the same reason. Changing it could cause a failure with no limit on the damage, while leaving it alone mostly costs money and patience.

Proof goes straight at that uncertainty: if each change comes with a proof, a developer can read a short specification, a precise description of what the code is supposed to do, instead of thousands of lines of AI-generated code, and let the checker confirm the rest. Hsu calls this “fearless veri-coding”: AI-generated code accompanied by independently checkable mathematical proofs. Unlike “vibe coding,” where developers rely on AI-generated code without rigorous guarantees of correctness, veri-coding preserves the speed of AI development while replacing uncertainty with mathematical assurance.

A slow piece of code can be swapped for a faster one, along with a proof that the two give the same results. That’s roughly what Fiat Cryptography already does inside Chrome. Similarly, legacy C code can be rewritten in a memory-safe language, with mathematical proofs establishing that the new implementation preserves the original program’s intended behavior.

What Still Stands in the Way

None of this has been shown yet across general-purpose software at commercial scale. A system can be entirely correct with respect to a specification that asks for the wrong thing, and Hsu and others maintain that the remaining challenge is capturing human intent: translating what people actually mean into precise mathematical requirements. On top of its verification engine, &Truth’s answer is what it calls a “specification factory,” technology designed to translate business requirements and human intent into formal specifications at scale, though that work is earlier-stage than the proving. Deciding what a system must guarantee, and what it must never do, ultimately requires human judgment. Mathematical proof establishes that software satisfies those specifications under stated assumptions; it does not determine whether the specifications themselves are right.

According to Hsu, the challenge is not simply to prove more code, but to establish the right guarantees across increasingly complex systems. Memory safety, freedom from data races and undefined behavior, and preservation of intended functionality are foundational properties that can be precisely specified and mathematically verified. By automating both specification and proof generation, &Truth aims to make these guarantees routine, enabling developers and AI agents to modify, optimize and rebuild software with far greater confidence.

Safety and speed are usually treated as a trade-off. But much of the friction in software development comes from uncertainty about changing code that nobody fully understands. Mathematical proof could remove much of that uncertainty, enabling more aggressive optimization and faster innovation without sacrificing specified correctness guarantees.

Hsu’s vision is a fundamental shift in how software is built: from hoping code works to mathematically proving it does, unlocking a future where software development is “safer, faster and bolder at the same time.”