Stanford AI safety researchers argue formal verification could make code "completely secure" in 3-5 years

The host frames AI safety debate as hysteria versus engineering

Opening the session, the host (identified in the description as Francois) argues that recent public discussion of AI safety has drifted from scientific rigor into "hysteria," comparing it to past panics over nuclear weapons, the internet and smartphones. He contrasts Yann LeCun's view that safety is "an engineering problem" with Jacob Coxen's claim that it is "more likely than not that humanity loses control to these AIs and could end in human extinction," saying he wants to present both sides without endorsing either.

He uses the OpenAI–Hugging Face incident as a case study in media distortion. According to the host, headlines claimed OpenAI said its models "acted on its own," but the actual technical report described a prompted exploit involving roughly 1,200 agents, with CO2 monitoring and production guardrails accidentally turned off rather than any autonomous "rogue" behavior.

He also challenges the commonly cited "10% in 10 years" extinction-risk figure, tracing it to a 2023 survey of about 1,200 AI researchers that actually asked about risk over all time and over 100 years, not 10. His own stated concern is narrower:

"My number one concern is... that really great open weight models allows for a lot more of the same from bad rogue actors or nation states."

He says he is skeptical that banning open weights or registering GPUs would work, and instead favors investing heavily in cyber defense.

Clark Barrett presents formal verification as a path to provably secure code

Clark Barrett, co-director of the Stanford Center for AI Safety, describes automated reasoning (AR) as "essentially computerized formal reasoning" already used in industry for safety assurance, contrasted with AI's lack of "correctness guarantees." He recounts pitching formal verification at a security workshop in 2023 and being dismissed as impractical, versus a more recent conference where "every talk before mine says... there is only one answer and the answer is formal methods."

He describes CSLib, a project modeled on Lean's math library, aimed at building a framework for proving code correct, and demonstrates translating a Rust cryptography library (Dalek) into the Bull language, generating 35 proof goals in Lean, most solved automatically via an SMT tactic. He also shows Verisforge, a tool that takes an English specification and automatically generates verified Rust code, and cites a recent result where a 30,000-line Rust crypto library that took three experts five months to verify manually was verified in 11 hours using his team's "crypto prover agent."

Barrett frames code reasoning as "a good base camp" for AI safety broadly, and previews his new company, And Truth, which aims to build "a universal code reasoning engine" producing "independently checkable certificates" rather than self-certified safety claims from labs.

Kochenderfer applies aviation safety methods to language models

Mykel Kochenderfer, from the Stanford Intelligent Systems Laboratory, explains that commercial aviation targets roughly "10 to the minus nine probability of catastrophic failure per flight hour," a standard applied in developing the ACAS X collision avoidance system. Direct simulation to detect such rare failures would require about 10^9 simulated hours, so his lab uses techniques like falsification, statistical modeling, and verification to validate systems before deployment.

He describes adaptive stress testing, originally developed by his former PhD student Richie Lee at NASA Ames for validating ACAS X, now adapted by students Hujun Liu and Amelia Hardy to probe language models for toxic outputs, using Llama Guard to measure toxicity and perplexity to find likely failures. He also discusses importance sampling methods (Gaussian processes, normalizing flows, diffusion models) to estimate failure probabilities and capture multiple failure modes, illustrated with an inverted pendulum example.

On neural network verification, he traces a collaboration with Barrett's lab that produced the Reluplex and later Marabou verification frameworks, originally explored for compressing ACAS X lookup tables. He also flags runtime monitoring, the BetterBench benchmark evaluation project, and a finding that human mental health professionals' judgments "vary widely" on sensitive topics like self-harm.

Both guests back an NTSB-style body for AI, with caveats

Discussing institutional responses, Kochenderfer notes commercial aviation is "80 times safer" than in the 1970s and credits independent, non-punitive incident reporting systems like the NTSB and ASRS. He suggests AI could benefit from something similar, though setting up a new government agency "is going to take a long maybe too long of a time."

Barrett says he was "encouraged" that frontier lab leaders have called for independent evaluators, and positions his company as trying to supply exactly that: checkable certificates rather than self-declared independence. Both researchers and the host flag the risk of regulatory capture, drawing analogies to ICANN and ride-hailing regulation, and the host proposes a "generally accepted AI principles" framework similar to accounting standards as a lighter-touch alternative to a new regulator.

Tractability of cybersecurity versus biological risks

Asked how tractable near-term AI safety risks are, Barrett predicts cybersecurity becomes "very tractable," saying:

"I will predict that within the next, I would say, 3 to 5 years... all our systems will be completely secure."

He argues the realistic path is securing boundaries around large models rather than trying to formally verify the models themselves, since reasoning about "a 500 billion parameter model isn't going to" be tractable.

Kochenderfer agrees on cybersecurity optimism but is more cautious on biology and chemistry risks, saying "you can't prove what's possible or what's not possible" there. Asked what he would do with $10 billion as a bank's security chief, Barrett says he would hire formal-methods experts, translate existing code into verifiable languages like Rust or Lean, and prove it correct, arguing this would make traditional unit testing largely obsolete since "the formal argument completely subsumes the tests."

Limits of formal methods and the role of specifications

Both speakers stress that formal guarantees depend on stated assumptions. Barrett notes that proving code "memory safe" makes buffer overflow attacks "100% impossible," but acknowledges some things, like formally specifying what a cat or dog looks like for a perception network, are "beyond what formal can do." Kochenderfer adds that formal methods require capturing real-world uncertainty in sets rather than probability distributions, and that those bounds may not always be realistic.

On the Swiss cheese model borrowed from aviation safety, Kochenderfer describes layered defenses, such as strategic separation, air traffic control, and collision avoidance, designed so vulnerabilities in different layers don't align. The host extends this to language models, describing layers from pretraining data filtering to runtime monitoring, and both guests agree human-level safeguards, since "a way to the typical way of breaking into a system is through human engineering," must complement technical layers. Barrett also argues AI agents can help generate specifications by anticipating edge cases, though audience questions raised the open problem of verifying agent-written specs match developer intent.