Formal verification

Aug 28, 2026

Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS

Varun Pant introduces formal verification as the solution to reliably validate AI-generated code, proposing a division where humans define specifications and machines handle code and proof. He details Lean's role as a unified language for code and proof, exemplified by an AI rewriting zlib with 32,000 lines of proof, and AWS's Cedar using Lean specs with Rust production code reconciled by 100 million nightly tests. The talk also covers deductive verification with solvers and future cross-language verification with Strata, aiming for "provably correct" software.

Aug 27, 2026

Analyzing Group Chat Encryption in Messaging Applications

This talk details a formal security analysis of group chat encryption algorithms in popular messaging applications like MLS, Session, and Keybase. It introduces Symmetric Sign Encryption (SSE) to model these protocols, identifying critical vulnerabilities such as insider replay and reordering attacks in MLS and Session due to insufficient context binding. The analysis highlights the complexities of key-dependent messages and key reuse, demonstrating how formal methods can pinpoint subtle design flaws and suggest robust mitigations for real-world secure communication.

Aug 26, 2026

🔬 The Physical World Is More Forgiving Than You Think — Anima Anandkumar, Caltech

Anima Anandkumar discusses her vision for AI in science, moving beyond language models to apply machine learning to the physical world. She introduces neural operators, especially Fourier neural operators, as a solution to data scarcity and resolution challenges in domains like weather, climate, and fusion. These models integrate physical constraints and data to achieve unprecedented speed and accuracy, even on consumer hardware, enabling capabilities from early hurricane prediction to digital twins for fusion reactors and inverse design for advanced materials. The conversation highlights the need for principled AI design for scientific discovery and advocates for distinct regulatory approaches for AI in science.

Jun 30, 2026

Session on Reasoning

This session features two talks on optimizing and verifying AI reasoning. Hongxiang Fan discusses cross-stack co-design for efficient AI, focusing on Test-Time Scaling (TTS) challenges, optimal verification granularity, and system-level optimizations for edge deployments. Nagarajan Natarajan introduces 'Advancing Verified Reasoning' with the InterVent platform, aiming to ensure AI agents comply with complex policies through formal verification, dynamic steering, and leveraging verification signals for training. Both emphasize addressing the computational and reliability costs of advanced AI.

May 07, 2026

Language-Agnostic Detection of Bugs in Zero-Knowledge Proof Programs

A summary of a talk on a new language-agnostic approach using abstract interpretation to find critical vulnerabilities in Zero-Knowledge Proof (ZKP) programs by modeling and detecting mismatches between prover computations and verifier constraints.

Mar 20, 2026

Terence Tao – Kepler, Newton, and the true nature of mathematical discovery

Terence Tao uses the story of Kepler's discovery of planetary motion as an analogy for AI's role in science. He argues that AI excels at broad, high-temperature idea generation but requires a robust verification process to be useful. The bottleneck in science is shifting from hypothesis generation to verification and curation, a challenge current scientific structures are not equipped to handle. Tao foresees a future of human-AI collaboration where humans provide deep insights and AI explores the vast breadth of possibilities, ultimately making scientific papers richer but not necessarily deeper.