Add preferred source
Stanford professor Clark Barrett believes the software industry is approaching a turning point where formally verified code becomes the norm, not the exception. Speaking on the Y Combinator Startup Podcast, Barrett detailed how AI-driven proof engines compressed a five-month, three-expert verification effort on a 30,000-line crypto library into just 11 hours. His prediction is bold: within three to five years, the combination of AI defense and formal methods will make systems “completely secure.” Barrett and fellow Stanford professor Mykel Kochenderfer frame AI safety as an engineering discipline, not a regulatory crisis. Kochenderfer, who helped build the ACAS-X aircraft collision avoidance system, is transplanting aviation validation techniques like adaptive stress testing and importance sampling to large language models. The two reject the notion of a single safety silver bullet, arguing instead for layered defenses. They diverge on how quickly frontier AI labs will adopt these tools, with Kochenderfer acknowledging labs like OpenAI and Anthropic have not engaged his work the way Waymo has. Barrett’s new company, Antruth, aims to commercialize a “universal code reasoning engine” and position itself as an independent evaluator issuing checkable certificates. For investors, the episode frames a market opportunity in verification infrastructure while underscoring the gap between aerospace-grade validation and the companies building frontier models.
Key Elements
Software engineering has a dirty secret. For decades, the industry that powers global finance, aviation, and healthcare has operated without the rigorous proofs that define other safety-critical disciplines. Instead, it runs on a method Clark Barrett describes bluntly: “write something and test it and hope for the best.”
That may be about to change, and faster than most people expect. Speaking on the Y Combinator Startup Podcast, Barrett — a Stanford computer science professor and co-director of the Stanford Center for AI Safety — argued that AI has fundamentally altered the economics of formal verification, the mathematical technique for proving code does exactly what it’s supposed to do. The traditional objection has always been that formal methods require monumental manual effort and don’t scale. Barrett’s new numbers suggest that objection is dissolving.
He described a recent archive submission from his lab: a 30,000-line Rust cryptography library that took three experts five months to verify by hand was verified fully automatically in 11 hours by a “crypto prover agent” built on Lean, a proof assistant developed at Microsoft Research. The pipeline translates Rust code into a common intermediate language, generates verification conditions as Lean theorems, and discharges them with a tool called Lean SMT that Barrett says “can prove a lot of Lean theorems in milliseconds.” In one demo, the system generated 35 proof goals and solved all but three automatically before closing the remainder with a second satisfiability call.
The gap between eleven hours and five months is not an incremental improvement. It is the difference between a technique that is commercially impractical and one that could become a default engineering practice.
The Base Camp for a Steep Problem
Barrett frames the broader AI safety debate in mountaineering terms. Proving that a 500-billion-parameter language model won’t do something catastrophic is, in his view, “not really tractable.” But securing the code that surrounds and constrains those models is a solvable problem today.
“If AI safety is a Mount Everest we have to climb, I think that code reasoning is a good base camp,” he said.
The argument is that AI creates a dual threat: it generates mountains of buggy software at unprecedented speed while simultaneously arming attackers with dramatically more capable hacking tools. “We’re being threatened on both sides here,” Barrett noted. The defense, he argues, must be equally automated. AI can attack, but AI can also defend — and AI defense paired with formal proof should eventually tip the balance.
His forecast is deliberately provocative: “I will predict that within the next three to five years that’ll just happen, like all our systems will be completely secure, because AI can attack but AI can also defend, and the AI defense plus formal methods should get us there.”
The prediction comes with important caveats. Proofs are always relative to assumptions. Memory safety can be guaranteed absolutely — Barrett says formal verification makes it “100% impossible for you to use a buffer overflow attack” — but proving that a perception network correctly identifies cats and dogs remains beyond reach. “I don’t even know how to formally specify a cat and dog,” he admitted. The practical strategy is what he calls “securing the boundaries” — using formal methods on the scaffolding around AI systems rather than the models themselves.
From Aviation to Large Language Models
Mykel Kochenderfer, a Stanford aeronautics professor who directs the Intelligent Systems Laboratory, brings a different pedigree to the conversation. He worked on ACAS X, the aircraft collision avoidance system that became an international standard, and his frame of reference is commercial aviation’s safety bar: a target probability of catastrophic failure per flight hour of roughly 10⁻⁹.
Achieving that level of assurance by brute-force simulation is impossible. At that failure rate, you’d need about 10⁹ simulated hours to see a single failure on average — and 10¹⁰ to characterize ten. So Kochenderfer’s lab focuses simulation on critical scenarios rather than benign ones.
| Approach | Challenge it addresses | Key limitation |
|---|---|---|
| Falsification (adaptive stress testing) | Finding failure cases in complex systems | Tends to zero in on a single failure mode |
| Importance sampling with diffusion models | Estimating failure probability efficiently | Requires a tractable likelihood measure |
| Formal verification | Proving correctness relative to specifications | Cannot specify everything (e.g., “cat” vs “dog”) |
The transfer to language models is called AST Prompter, work led by Kochenderfer’s students. The method requires two ingredients: a definition of failure and a measure of likelihood. For toxicity, failure is defined by a threshold on a Llama Guard score, while likelihood is measured by perplexity. The search targets low log-perplexity and high toxicity simultaneously. If the most likely failure is highly probable, that’s a signal to build mitigations before deployment.
Kochenderfer was candid that the frontier AI labs have not engaged with this work the way the autonomous vehicle industry has. Waymo and other automotive manufacturers have funded his lab’s research with the explicit goal of making validation tools available industry-wide. His adaptive stress testing toolkit is released open-e who want to continue using obsolete languages.”
Asked whether Anthropic, OpenAI, or xAI engage comparably, he said simply: “not yet.”
That two-word answer is the episode’s most consequential data point. The methods with the strongest safety track record were built for and validated in aerospace and autonomous driving. The organizations building the most powerful language models have not adopted them at comparable depth. This gap sits awkwardly beside Barrett’s five-year prediction, and neither speaker had a satisfying explanation for it.
The Swiss Cheese Defense
Both speakers were emphatic that no single technique suffices. “In order to establish confidence in a system, there is no one silver bullet,” Kochenderfer said. “Probably formal methods won’t take you the whole way there.”
The organizing principle is the Swiss cheese model — layered defenses whose holes must not line up. In aviation, that means strategic separation by altitude layers, then air traffic control, then collision avoidance as the last line. For large language models, the host mapped the analogous layers: filter pretraining data, run failure analysis on the trained model, estimate failure modes and probabilities, then deploy runtime monitoring.
Kochenderfer pointed to a recent Hugging Face incident as a layer that was switched off. A chain-of-thought monitor that would have caught the problematic behavior was disabled, and production guardrails weren’t active because the system wasn’t in production. Either layer alone would have prevented the incident. That’s the Swiss cheese model in failure.
On the formal-versus-statistical tension, Kochenderfer noted that formal methods capture uncertainty in sets rather than probability distributions, which yields clean proofs but raises the question of whether the uncertainty intervals are realistic. Barrett agreed: “a proof is always with respect to some assumptions,” and the formal community has learned hard lessons about stating those assumptions clearly.
The Institutional Question
Commercial aviation is roughly 80 times safer than it was in the 1970s, and Kochenderfer attributes that primarily to institutional design, not technology alone. The NTSB was established as an independent agency in 1967. A non-punitive reporting system incentivized manufacturers and airlines to share safety information. Later systems added immunity protections for disclosure.
There has been discussion of creating an NTSB for AI. Kochenderfer said “I think that could actually be a good idea,” while acknowledging a new agency would take years to build and governments are inefficient. He offered the space-launch analogy: a range safety officer independent of the mission whose only job is a go/no-go call based on objective safety metrics.
Barrett’s contribution to the institutional debate is commercial rather than governmental. He is co-CEO of Antruth, a new company building what he calls a “universal code reasoning engine.” The vision is inspired by Mathlib, the massive open-source mathematical library in Lean. One goal, he said, is to serve as an independent evaluator that produces certificates anyone can check — “you can now go check it yourself, and you can confirm that we got that right.” He warned it would be “a real shame if all of the safety was left in the hands of the labs or even some friends of the labs who claim they’re independent.”
On regulation, Barrett is skeptical that mandates work. After 30 years in formal methods, he believes telling people they must work differently is a bad idea. Market forces are the better lever: if a few companies adopt formal verification and gain a measurable security advantage, “every other CISO is going to be like, oh, we better do that too.”
Kochenderfer pointed to autonomous vehicle regulation as a cautionary tale. Chris Gerdes, a former Stanford professor who went to Washington to help DOT draft automated-vehicle rules, concluded it was premature to be prescriptive about specific technologies. Higher-level best practices and standards are the right level. And importantly, he noted, companies don’t actually want to compete on safety — “it’s not in Waymo’s interest for Zoox to have an accident” — which creates room for domain-specific industry collaboration.
The Remaining Hard Problems
For all the technical progress, both speakers acknowledged that specification — the question of where the proof targets come from — remains an open research problem. Enterprise code rarely ships with formal specs. Barrett described a spectrum: some specs are universal and written once, like memory safety for all C code. Others are domain-specific, such as no loss of funds across a bank’s transaction sequences. And increasingly, he noted, AI agents are good at proposing specs — in a Claude Code session, “I say, I want this, and it’s like, oh, yes, and you probably want this, this, and this, too.” The gap between an agent-written spec and developer intent is unresolved, but Barrett argues code with agent-written specs that pass proof is better than code with no specs at all.
Benchmarks are another weak point. Kochenderfer pointed to BetterBench and his lab’s work on benchmark saturation and token-level signatures of reasoning failures. Barrett recalled a former student finding roughly 30% of SQL-query evaluation items contained errors. Kochenderfer’s prescription is practical: version control, pull requests, issue filing — the same discipline that governs good software development applied to the evaluation infrastructure itself. The Hugging Face incident, both speakers noted, had reached public attention through a Slashdot headline claiming “OpenAI says its AI models acted on its own” and descriptions of a “rogue AI agent” — a characterization far removed from what actually happened, where a chain-of-thought monitor had been switched off.
On liability, the decisive question Barrett raised is whether an AI-admin vendor would accept legal responsibility for failures. If so, that itself is evidence of a serious safety case. Waymo offers a partial template — not perfect, but by its own account saving lives — and liability remains the unspoken contract that binds safety claims to accountability.
The unresolved tension at the heart of the conversation is whether the validation toolkit will reach the organizations building frontier models before the institutions catch up. Barrett’s prediction is bullish on the technology. Kochenderfer’s “not yet” is a reminder that adoption is a social process, not a technical one. What happens in the next three to five years will determine whether Barrett’s forecast looks prescient or premature. Either way, the tools are now on the table, and the companies that adopt them earliest may find that provable security becomes their competitive edge.
Full content available at:Here’s How To Think About AI Safety | YC Paper Club
- AI Pioneers Urge Global Watchdog for Cyber-Capable Models
- Gates Warns AI Is the Most Dangerous Invention Ever; Cyberattacks Could Erupt in the Coming Year
- UK Confirms Early Access to Test Latest US AI Models, Cites Security Risks
- Accenture’s Wild Stock Swings Show Wall Street Can’t Decide If AI Is a Threat or a Boon
- Anthropic Co-Founder Jack Clark Urges Urgency on AI Safety Regulation
