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.
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.
Carina Hong, Founder & CEO of Axiom, discusses building a self-improving AI reasoning engine that combines generation and verification. Starting with formal mathematics, Axiom's system has achieved superhuman results on the notoriously difficult Putnam Exam by leveraging formal languages like Lean to overcome the probabilistic and unverifiable nature of standard LLMs. Hong explores how this technology can solve major bottlenecks in hardware and software verification, code migration, and database consistency, and what it means for the future of mathematical research.
A detailed overview of the formal verification of Apple's iMessage PQ3 protocol using the Tamarin prover. The talk covers PQ3's hybrid cryptographic design, its post-quantum security goals like forward secrecy and post-compromise security, the powerful adversary model it resists, and the successful formal analysis of its unbounded double ratchet structure.