Title: (Preliminary) Mathematical Superintelligence

Bio: Tudor Achim is the CEO and Co-Founder of Harmonic, the AI lab building the world’s most advanced reasoning engine. Under his leadership, Harmonic has pioneered the concept of Mathematical Superintelligence – the next generation of artificial intelligence that eliminates hallucinations by reasoning through mathematics as opposed to language prediction – and released the world’s first consumer-facing MSI model, Aristotle. Aristotle recently achieved a gold medal-level performance at the 2025 International Mathematical Olympiad, demonstrating problem-solving capabilities that exceed human benchmarks. Before founding Harmonic, Tudor co-founded and served as the CTO at Helm.ai, an autonomous driving software company. Tudor holds a B.S. in Computer Science from Carnegie Mellon University and was a Ph.D. Candidate in Computer Science at Stanford. He brings a rare combination of deep technical expertise and a vision to make mathematically grounded, provably accurate AI broadly available to individuals and institutions worldwide.

Title: CSLib: Building a Platform for AI-assisted Formal Verification in Lean

Abstract: I will explain the new CSLib initiative, with a focus on its code reasoning effort, which aims to build a new industrial-strength formal verification platform in Lean for verifying real-world code. I'll describe the principles and design decisions behind the CSLib code reasoning effort. I'll then illustrate it with an end-to-end example that brings together: AI-assisted code generation and code specification; the Boole language and the Strata framework for language-agnostic code reasoning; trustworthy verification condition generation; and Lean automation through Lean-SMT and AI-assisted theorem proving.

Bio: Clark Barrett is a Professor (Research) of Computer Science at Stanford University. His expertise is in automated reasoning and its applications. He was an early pioneer in satisfiability modulo theories, formal hardware verification, and neural network verification. More recently, he has also pioneered efforts in AI-assisted formal verification. He is the director of the Stanford Center for Automated Reasoning (Centaur), co-director of the Stanford Center for AI Safety, and a member of the CSLib steering committee. He is an ACM Fellow and a two-time winner of the Computer Aided Verification (CAV) award (2021, 2024).

Title: Formal methods for robotics in the age of big data

Abstract: Robots are physical machines interacting with the real world; they are difficult to model, yet we need to guarantee they will be safe. Making them even more difficult to verify is the growing approach of using data, and generative AI, to control them. Given this, what role can, and should, formal methods play in advancing robotics? In this talk I will give a few examples for what we can do with formal methods to "verify" robot behavior, discuss their promise and challenges, and describe the synergies I see with data-driven approaches.

Bio: Hadas Kress-Gazit is the Geoffrey S.M. Hedrick Sr. Professor at the Sibley School of Mechanical and Aerospace Engineering at Cornell University, and the Associate Dean for Diversity and Academic Affairs of Cornell Duffield College of Engineering. She received her Ph.D. in Electrical and Systems Engineering from the University of Pennsylvania in 2008 and has been at Cornell since 2009. Her research focuses on formal methods for robotics and automation and more specifically on high-level specifications and synthesis for robot control. Her group has explored different types of robotic systems including modular robots, soft robots and swarms, and how formal methods can be used for human-robot interaction. She received an NSF CAREER award in 2010, a DARPA Young Faculty Award in 2012, Cornell Engineering’s Excellence in teaching award in 2013 and 2019, and excellence in research award in 2021. She is an IEEE Fellow and has served on DARPA’s Information Science and Technology study group (ISAT), as the program chair for Robotics: Science and Systems (RSS) 2018, the program chair for the International Conference on Robotics and Automation (ICRA) 2022, and the president of the RSS board (2019-2023), among other leadership positions in the robotics community.

Title: (Preliminary) Automated Reasoning at AWS, Including Verification of Rust Programs

Title: Lean 4: A Unified Platform for Programming and Verification

Abstract: Lean 4 is an open-source functional programming language and interactive theorem prover based on dependent type theory. Its powerful type system enables users to write programs and prove properties about them within a single unified framework. In this talk, I will present the key design decisions behind Lean 4, its extensible infrastructure, and recent developments in proof automation, including the grind tactic and our current efforts on scalable verification condition generation. I will also discuss Lean 4's growing adoption by AI research teams, which have used Lean as the backbone for recent breakthroughs in AI-assisted mathematics, and its expanding ecosystem of libraries and users in both mathematics and software verification.

Bio: Leo is a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. In his spare time, he dedicates himself to serving as the Chief Architect of the Lean FRO, a non-profit organization that he proudly co-founded alongside Sebastian Ullrich. He is also honored to hold a position on the Board of Directors at the Lean FRO, where he actively contributes to its growth and development. Before joining AWS in 2023, he was a Senior Principal Researcher in the RiSE group at Microsoft Research, where he worked for 17 years starting in 2006. Prior to that, he worked as a Computer Scientist at SRI International. His research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. He is the main architect of several automated reasoning tools: Lean, Z3, Yices 1.0 and SAL. Leo's work in automated reasoning has been acknowledged with a series of prestigious awards, including the CAV, Haifa, and Herbrand awards, as well as the ACM SIGPLAN Programming Languages Software Award twice for Z3 and Lean. Leo's work has also been reported in the New York Times and many popular science magazines such as Wired, Quanta, Nature News, and Scientific American.

Title: Formal Verification in Practice: Interactive Theorem Proving for NASA Safety-Critical Systems