The event combines an opening talk on AI-safety concerns with presentations on formal verification and empirical validation, followed by a panel discussion.

Opening: Avoiding Hype While Taking Safety Seriously

• The host argues that AI-safety debates should rely on scientific rigor, measurable claims, and evidence, rather than sensational headlines.
• He cautions that past technologies—from nuclear weapons to the internet—also inspired alarming predictions, some of which proved inaccurate.
• He disputes portrayals of an OpenAI–Hugging Face incident as an AI system acting independently: he says the agent was prompted, safeguards were disabled outside production, and monitoring could have detected the issue.
• He also challenges claims that AI experts broadly predict extinction within ten years, noting that a cited survey asked about much longer time horizons.
• His main near-term concern is that open-weight models could help malicious actors conduct cyberattacks, fraud, or other harmful activity.
• He argues that banning open models or tracking GPUs would be difficult to enforce. Instead, organizations should strengthen cyber defenses, fix basic security weaknesses, and use capable AI systems to help defenders keep pace.

Clark Barrett: Combining AI with Automated Reasoning

Automated reasoning (AR) uses computers to check formal proofs. Unlike AI systems that can make mistakes or hallucinate, formal methods can provide strong correctness guarantees—provided their assumptions and specifications are sound.

Barrett presents CS lib, a project to build a shared framework for reasoning about software:

1. Translate code from different programming languages into a common intermediate language.
2. Generate verification conditions.

3. Prove those conditions in Lean, a theorem-proving system that checks every proof step.

4. A prototype translated Rust code from a cryptography library into an intermediate language, generated Lean goals, and proved them using the lab’s Lean SMT tool.

5. Verisforge demonstrates a more automated workflow: describe a task in English, review a structured specification, then generate and formally verify code.
6. Barrett reports that a crypto library requiring months of expert effort to verify was processed by their agent in about 11 hours.
7. A major remaining challenge is writing the right specifications—the properties the code is supposed to satisfy. AI can help suggest specifications, but people still need to confirm they reflect the intended behavior.
8. Barrett sees formal code reasoning as a foundation for stronger cybersecurity and for systems that can present independently checkable proof that their code behaves as claimed.
9. He also describes formal verification as a form of containment: an AI agent restricted to proving code properties has a narrower role than a general-purpose agent.

Michael Kochenderfer: Validating AI Systems Before and After Deployment

Kochenderfer’s Stanford lab studies how to build confidence in systems that include learned components.

• Safety-critical systems need evidence before deployment, but rare failures are difficult to estimate by brute-force simulation. For example, demonstrating a failure rate near (10^{-9}) per flight hour would require enormous numbers of simulated hours.
• The lab uses multiple complementary approaches:
• Falsification: search for scenarios that make a system fail.
• Failure-probability estimation: use statistical models to estimate how likely failures are.
• Formal verification: prove properties under explicitly stated assumptions.
• POMDP planning: make robust decisions under uncertainty about states, outcomes, interactions, and models.
• Adaptive stress testing searches for likely failure scenarios. The lab has adapted this approach to language models, using toxicity measures and language-model perplexity to find likely harmful outputs.
• Importance sampling focuses simulations on important scenarios and reweights results to estimate the probability of failure.
• The lab also studies methods such as neural-network verification, reachability analysis, and planning for aircraft, autonomous vehicles, spacecraft, and medical evacuation.
• Safety work must continue after deployment through runtime monitoring of inputs, internal behavior, and outputs.
• Benchmarks also need ongoing evaluation: they can saturate, contain errors, or fail to reflect changing language and behavior. Kochenderfer’s group publishes BetterBench to document benchmarks and evaluation practices.
• His new book, Algorithms for Validation, brings together statistical, formal, and reachability methods.

Discussion: Regulation, Assumptions, and Practical Safety

• Both speakers support more serious AI-safety work but warn against treating worst-case predictions as certainties.
• Kochenderfer suggests borrowing from aviation: independent investigations, non-punitive reporting, and learning from incidents. A formal AI equivalent of the NTSB could help, though creating one may take time.
• Barrett emphasizes independent evaluation that produces certificates others can check, rather than relying on an evaluator’s assurances alone.
• They favor high-level standards and best practices over premature rules prescribing specific technologies. Market incentives may encourage adoption if formal methods demonstrably improve security.
• Formal proofs are always conditional on assumptions. They can establish properties such as memory safety, but they cannot guarantee every aspect of real-world behavior or prove that a perception model correctly identifies concepts that are difficult to specify formally.
• A security program should use multiple layers of defense—the “Swiss cheese” model—so that weaknesses in one layer do not align with weaknesses in others.
• The speakers stress that people remain a major security vulnerability; AI can assist with monitoring and defense, but human oversight still matters.
• Rapidly increased use of AI agents could overwhelm human-review systems, from security alerts to admissions and courts. More automation therefore requires rethinking how those systems scale.
• Benchmarks should be continuously monitored for distribution shifts, regularly updated, and maintained with better version control and issue reporting.

Main Takeaway

AI safety is not one technique or one prediction. The speakers advocate combining rigorous testing, statistical validation, formal verification, runtime monitoring, secure engineering, and independent oversight—while clearly stating assumptions, improving defenses, and avoiding unsupported claims. This summary reflects the speakers’ arguments and reported results, not independent verification of them.  ## Summary

The event features an opening talk on AI-safety concerns, presentations on formal verification and system validation, and a discussion about how to improve AI security.

Opening: Take AI Safety Seriously Without Hype

• The host calls for scientific rigor, measurable claims, and evidence rather than sensational headlines.
• He disputes portrayals of an OpenAI–Hugging Face incident as an AI acting on its own, arguing that the agent was prompted and that safeguards and monitoring were not enabled as they would be in production.
• He questions claims that experts predict human extinction within ten years, noting that a cited survey asked about much longer time horizons.
• His main near-term concern is that open-weight models could help malicious actors with cyberattacks and other harmful activity.
• He considers bans on open models or GPU tracking difficult to enforce and argues instead for stronger cyber defenses, better security practices, and AI tools that help defenders.

Clark Barrett: Formal Verification for Software

Automated reasoning uses computers to check formal proofs. It can provide strong guarantees about software, as long as the specifications and assumptions are appropriate.

• Barrett’s project, CS lib, aims to translate code from different languages into a common format, generate verification conditions, and prove them in Lean, a theorem-proving system.
• A prototype translated Rust code from a cryptography library into Lean goals and proved them using the lab’s Lean SMT tool.
• Verisforge demonstrates a more automated workflow: provide an English description, review a structured specification, then generate and verify code.
• Barrett reports that their agent verified a crypto library in about 11 hours, compared with months of expert effort.
• The main challenge is defining the right specification: AI can help propose requirements, but people must ensure they match the intended behavior.
• Barrett sees formal verification as a foundation for stronger cybersecurity and independently checkable evidence that software satisfies its requirements.

Michael Kochenderfer: Testing and Monitoring AI Systems

Kochenderfer describes methods for assessing systems with learned components, especially when failures are rare or difficult to simulate.

• Falsification searches for scenarios that cause a system to fail.
• Statistical methods, including importance sampling, focus simulations on important scenarios and help estimate failure probabilities.
• Formal verification proves properties under stated assumptions; POMDP planning helps make decisions amid uncertainty.
• Adaptive stress testing searches for likely failures. The lab has adapted it to language models, using toxicity measures and perplexity to find likely harmful outputs.
• Validation should continue after deployment through runtime monitoring of inputs, internal behavior, and outputs.
• Benchmarks must also be checked and updated: they can contain errors, become outdated, or fail to capture changing language. The lab publishes BetterBench to document evaluation practices.

Discussion: What Effective Safety Requires

• The speakers support continued AI-safety research but caution against presenting uncertain worst-case outcomes as facts.
• They recommend learning from aviation: independent evaluation, incident investigations, and systems for sharing safety information.
• Formal guarantees depend on assumptions. They can establish properties such as memory safety, but cannot guarantee every aspect of real-world behavior.
• Effective security needs multiple layers of defense so that a weakness in one layer does not undermine the whole system.
• AI can help monitor threats, but human oversight remains important, and increased use of agents may overwhelm systems that depend on human review.
• Regulation may help, but speakers favor high-level standards and best practices over rules that prescribe specific technologies too early.

Main Takeaway

AI safety requires a combination of methods: rigorous testing, statistical validation, formal verification, runtime monitoring, secure engineering, and independent oversight. The speakers emphasize stating assumptions clearly, strengthening practical defenses, and avoiding unsupported claims.