Disclaimer: https://legal.codesolutionsllc.com/si-disclaimer — Notes of a public interview — not Code Solutions LLC views or advice. Lane: Digest More feed only. Not a Daily X release from this pack alone. Speaker claims: Figures, predictions, and accounts of events below are the speakers' own statements, attributed to them and marked [unverified]; they are not checked facts. Contest OUT.
Source: https://x.com/ycombinator/status/2111472682571374601 (1:37:07). Host Francois Chaubard; guests Clark Barrett and Mykel Kochenderfer, co-directors of the Stanford Center for AI Safety. Times are approximate.
- [0:00] Chaubard opens the session and says the SI safety conversation should return to the scientific method: falsifiable claims, measurement, and peer review ("Science fiction versus science facts").
- [4:30] He contrasts two narratives: safety through engineering, like making aircraft safe (citing Yann LeCun and Jensen Huang), versus high-risk "p_doom" estimates, which he says he is giving airtime to without judging.
- [6:13] OpenAI–Hugging Face incident (Chaubard's account) [unverified]: Chaubard says some headlines described the incident as an agent acting on its own or going rogue, and says "It's not what happened." In his account, "It was prompted," and he cites a ~60-page incident technical report. He says chain-of-thought monitoring was turned off and that production guardrails were off because it wasn't in production, and that, per the report as he describes it, either safeguard would have caught the issue. These details are his account, not established fact.
- [8:00] He says the "10% in 10 years" figure traces to a 2023 survey of researchers who publish in the field, and argues the survey questions were about all time and the next 100 years, not the next 10 years [unverified].
- [11:00] His top concern is not machines developing a will of their own, but strong open-weight models helping bad actors with cyberattacks, ransomware, terrorism, or bioweapons. He mentions a friend's local hospital in Poland being shut down for three weeks by hackers [unverified].
- [17:25] Barrett, "When AI met AR": SI handles messy data well but offers no correctness guarantees; automated reasoning (formal methods) gives correctness guarantees and is already used in industry for safety assurance.
- [18:30] He says formal verification was long seen as too costly to be practical, and he now sees a shift, with many in security pointing to formal methods as SI raises attackers' capabilities against legacy code.
- [20:30] He describes CS lib, inspired by Mathlib, with a steering committee that includes Lean author Leo de Moura: code in many languages translated to a common intermediate language, compiled into Lean theorems, and proved, with his lab's Lean SMT tool proving many goals in milliseconds.
- [25:30] He cites a recent arXiv submission: a 30,000-line Rust crypto library that took "five experts three months, or three experts five months" verified in 11 hours fully automatically by an agent [unverified].
- [26:00] "If AI safety is a Mount Everest... code reasoning is a good base camp." He closes by describing his new company, which is building a code reasoning engine.
- [27:55] Kochenderfer asks what evidence justifies deploying a system with learned parts, like aircraft auto-landing. He says the ACAS X collision avoidance system was held to about 10^-9 catastrophic failures per flight hour, which direct simulation can't practically show [unverified].
- [30:00] He covers estimating failure probability with a trusted model and says there is "no one silver bullet": formal verification, done in collaboration with Barrett's lab, is one of several approaches. "Our inferences about safety is only as good as the simulator."
- [32:10] Adaptive stress testing, first used to help validate ACAS X, is now applied to language models: for example, searching for likely prompts that produce toxic output, scored with Llama Guard.
- [40:00] After deployment: runtime monitoring and assurance (including work with Airbus on vision-based systems), and the BetterBench project on benchmark best practices (betterbench.stanford.edu).
- [44:00] Barrett says the future has high uncertainty, so investing in safety research makes sense, and that stressing worst cases without real probabilities isn't helpful.
- [45:00] Kochenderfer suggests borrowing from aviation, such as an NTSB-style body for SI. He says commercial aviation is 80 times safer than in the 1970s, the NTSB was set up as an independent agency in 1967, and non-punitive reporting helped the industry learn from every accident [unverified].
- [49:00] Barrett says he is encouraged that frontier lab leaders call for independent evaluators. He says his company aims to be one, producing independently checkable certificates.
- [52:30] Barrett predicts that within three to five years "all our systems will be completely secure," through SI-driven defense combined with formal methods [unverified]. He says securing the boundaries around large models is tractable, while proving properties of the models themselves is not.
- [55:00] Asked what he would do with a large security budget at a major bank, Barrett says: hire formal methods experts, build infrastructure, and prove existing code or translate it to Rust or Lean and prove it there.
- [56:30] Kochenderfer says adaptive stress testing is released in Julia and Python and that his group recently published AST Prompter. Even for ACAS X, he says, failure probability is not zero. "Anyone claiming a completely safe real-world system, I would not believe."
- [1:03:00] Kochenderfer explains aviation's "Swiss cheese" model: layered defenses whose holes shouldn't line up. He calls the chain-of-thought monitor in Chaubard's opening example one such layer [unverified].
- [1:06:00] On code with no specification, Barrett says specs become the hard part once writing and verifying code is easy. Some specs are universal (memory safety), others are domain-specific (a bank never losing funds), and agents can help draft them.
- [1:10:30] On regulation, Kochenderfer favors high-level best practices and standards over prescriptive rules and industry cooperation on safety. Barrett expects market forces to drive formal adoption if it scales. Chaubard says frontier labs signed a White House document on independent audits and guardrails, "all six of the labs" [unverified].
- [1:30:26] Chaubard on scale: "more is just so different." He cites ICLR receiving 60,000 submissions in a year and predicts human traffic will be ~0% of internet traffic [unverified].
- [1:33:54] On evolving harms, a panelist suggests monitoring benchmarks continuously. A panelist says a former student found ~30% of answers in one SQL benchmark were wrong [unverified] and calls for version control and issue tracking for benchmarks. Chaubard closes with a startup idea: a curated "App Store of benchmarks."