Formal Guarantees for Frontier AI

Formal verification is often dismissed as too rigid, complex, or unscalable for frontier AI systems (LLMs, VLMs, agentic systems), pushing many researchers and developers toward less rigorous alternatives like benchmarking, red teaming, and adversarial attacks. This talk presents a new class of efficient formal verification methods that certify safety properties such as secure code generation and catastrophic conversational risks, delivering stronger generalization guarantees than standard evaluation approaches and positioning formal verification as a necessary foundation for reliable systems at scale.