Milan Ganai's paper accepted to CoRL 2026
10 Oct 2026
DIRECT: When and Where Should You Allocate Test-Time Compute in Embodied Planners? by Jadelynn Dao, Milan Ganai, Yasmina Abukhadra, Ajay Sridhar, Mozhgan Nasr Azadani, Katie Luo, Clark Barrett, Jiajun Wu, Chelsea Finn, and Marco Pavone has been accepted to the Conference on Robot Learning (CoRL 2026) in Austin, Texas.
DIRECT: When and Where Should You Allocate Test-Time Compute in Embodied Planners?Project Website
Samuel Akinwande's paper accepted to CDC 2026
10 Oct 2026
The FABRIC Strategy for Verifying Neural Feedback Systems by Samuel Akinwande, Sydney Katz, Mykel Kochenderfer, and Clark Barrett has been accepted to the 65th IEEE Conference on Decision and Control (CDC 2026) in Honolulu, Hawaii.
The FABRIC Strategy for Verifying Neural Feedback Systems4 papers from Centaur at FMCAD 2026
14 Sep 2026
Four papers from Centaur have been accepted to FMCAD 2026 in Graz, Austria: Nazrin: An Atomic Neural Proof Automation Tactic in Lean 4 by Leni Aniva and colleagues; PICID: Proof-Driven Clause Learning in Neural Network Verification by Omri Isac and colleagues; Extending an SMT Solver with LIA⋆ Constraints by Mudathir Mohamed and colleagues; and Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean, with Abdalrhman Mohamed and Liza Pertseva among the authors. Clark Barrett also gave an invited talk at the conference.
FMCAD 2026 Accepted PapersDaneshvar Amrollahi's paper accepted to Findings of ACL: EMNLP 2026
20 Aug 2026
Faithful Autoformalization via Roundtrip Verification and Repair by Daneshvar Amrollahi, Jerry Lopez, and Clark Barrett has been accepted to Findings of the Association for Computational Linguistics: EMNLP 2026. The paper checks whether an LLM's formalization of natural language is faithful by translating it back and re-formalizing, then diagnoses and repairs the step that went wrong.
Faithful Autoformalization via Roundtrip Verification and RepairHaoze Wu's paper at IJCAI 2026
18 Aug 2026
Lookahead Branching for Neural Network Verification by Liam Davis, Duo Zhou, Huan Zhang, Guy Katz, Clark Barrett, and Haoze Wu appears at the 35th International Joint Conference on Artificial Intelligence (IJCAI-ECAI 2026) in Bremen, Germany.
Lookahead Branching for Neural Network Verificationcvc5 and Bitwuzla win FLoC Olympic Games awards at FLoC 2026
28 Jul 2026
Two solvers developed at Centaur were honored at the FLoC 2026 Olympic Games award ceremony in Lisbon. cvc5 received the award for Best Overall Ranking in SMT-COMP 2025 and 2026, for winning the best overall ranking in three of the four main tracks of SMT-COMP 2026 (Single Query, Incremental, and Model Validation) and in all four main tracks in 2025 (adding Unsat Core). Bitwuzla, developed by Aina Niemetz and Mathias Preiner, received an award for consistently outstanding performance in bit-vector logics. The cvc5 award recognizes Haniel Barbosa, Clark Barrett, Lydia Kondylidou, Hanna Lachnitt, Daniel Larraz, Abdalrhman Mohamed, Mudathir Mohamed, José Neto, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, and Yoni Zohar.
FLoC Olympic Games 2026SMT-COMP 2026
cvc5
Bitwuzla
3 papers from Centaur at IJCAR 2026
26 Jul 2026
Three papers from Centaur appear at the 13th International Joint Conference on Automated Reasoning (IJCAR 2026), also part of FLoC 2026 in Lisbon: Benjamin Przybocki and Clark Barrett's paper on the termination of Nielsen transformations for word equations with length constraints, a paper on checking regular expression reasoning in cvc5 proofs, and Ethos, a fast proof checker for the Eunoia logical framework.
The Termination of Nielsen Transformations Applied to Word Equations with Length ConstraintsChecking Regular Expressions in cvc5 Proofs
Ethos: A Fast Proof Checker for the Eunoia Logical Framework
3 papers from Centaur at CAV 2026
26 Jul 2026
Three papers from Centaur appear at CAV 2026, part of FLoC 2026 in Lisbon, Portugal: the Distinguished Paper Award winner on extensional constant arrays by Mathias Preiner, Aina Niemetz, and Clark Barrett; Liza Pertseva's paper on automating bitvector and finite field equivalence proofs in Lean; and a paper on the cooperating proof calculus behind cvc5's proofs, with Jibiana Jakpor, Hanna Lachnitt, Abdalrhman Mohamed, Aina Niemetz, Mathias Preiner, and Clark Barrett among the authors.
Satisfiability Modulo Extensional Constant ArraysAutomating Bitvector and Finite Field Equivalence Proofs in Lean
The Cooperating Proof Calculus: Comprehensive Proofs for an SMT Solver
CAV 2026 Distinguished Paper Award for Mathias Preiner, Aina Niemetz, and Clark Barrett
26 Jul 2026
Satisfiability Modulo Extensional Constant Arrays by Mathias Preiner, Aina Niemetz, and Clark Barrett received a Distinguished Paper Award at the 38th International Conference on Computer Aided Verification (CAV 2026) in Lisbon, Portugal.
Satisfiability Modulo Extensional Constant ArraysCAV 2026
2 papers from Centaur at the SMT 2026 workshop
24 Jul 2026
Two papers from Centaur have been accepted to the 24th International Workshop on Satisfiability Modulo Theories (SMT 2026), held with IJCAR at FLoC 2026 in Lisbon: Accelerating Parallel SMT Solving with Fixed First Decisions by Amalee Wilson and colleagues, and Automated Reasoning with Nested Datatypes by Tomer Hakak, Yoni Zohar, Andrew Reynolds, Clark Barrett, and Cesare Tinelli.
SMT 2026 Accepted PapersMilan Ganai's paper at RSS 2026
13 Jul 2026
Self-Supervised Bootstrapping of Action-Predictive Embodied Reasoning by Milan Ganai, Katie Luo, Jonas Frey, Clark Barrett, and Marco Pavone appears at Robotics: Science and Systems (RSS 2026) in Sydney, Australia.
Self-Supervised Bootstrapping of Action-Predictive Embodied ReasoningProject Website
Samuel Akinwande's paper at L4DC 2026
17 Jun 2026
Verifying Nonlinear Neural Feedback Systems using Polyhedral Enclosures by Samuel Akinwande, Chelsea Sidrane, Mykel Kochenderfer, and Clark Barrett appears at the 8th Annual Learning for Dynamics and Control Conference (L4DC 2026) in Los Angeles.
Verifying Nonlinear Neural Feedback Systems using Polyhedral EnclosuresPono 2.0 wins the FM 2026 Best Tool Paper Award
18 May 2026
Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness by Aron Perez-Lopez, Po-Chun Chien, Florian Lonsing, Samantha Archer, Ahmed Irfan, and Clark Barrett received the Best Tool Paper Award at the 27th International Symposium on Formal Methods (FM 2026) in Tokyo, Japan.
Pono 2.0: A Versatile SMT-Based Model Checker for Safety and LivenessFM 2026
Scott Viteri and Max Lamparth's paper at ICLR 2026
23 Apr 2026
Markovian Transformers for Informative Language Modeling by Scott Viteri, Max Lamparth, Peter Chatain, and Clark Barrett appears at the Fourteenth International Conference on Learning Representations (ICLR 2026) in Rio de Janeiro, Brazil.
Markovian Transformers for Informative Language ModelingBitwuzla and Mallob paper wins three awards at ETAPS 2026
15 Apr 2026
Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob by Dominik Schreiber, Aina Niemetz, and Mathias Preiner received the ETAPS Best Tool Paper Award, the TACAS Distinguished Paper Award, and the TACAS Distinguished Artifact Award at ETAPS 2026 in Turin, Italy.
Massively Parallel Bit-Precise Verification with Bitwuzla and MallobETAPS Awards
CVC4/cvc5 wins the Rance Cleaveland Test-of-Time Tool Award at ETAPS 2026
15 Apr 2026
The SMT solver CVC4/cvc5 has received the 2026 Rance Cleaveland Test-of-Time Tool Award from ETAPS, which recognizes research tools with a lasting impact on the community. Developed and maintained at Stanford University and the University of Iowa over the past 17 years, CVC4 and its successor cvc5 are open-source and have been built on by many tools in formal methods.
ETAPS Awardcvc5
5 papers from Centaur at TACAS 2026
11 Apr 2026
Five papers from Centaur appear at TACAS 2026, part of ETAPS 2026: papers by Aina Niemetz and Mathias Preiner on Bitwuzla, a study of the SMT-LIB benchmark library, Rachel Cleaveland's work on string reasoning in symbolic execution of C programs, and VeriStruct by Chuyue (Livia) Sun, Yican Sun, Daneshvar Amrollahi, and colleagues.
Massively Parallel Bit-Precise Verification with Bitwuzla and MallobBit-Precise Interpolation in Bitwuzla
Exploring the SMT-LIB Benchmark Library
Integrating String Reasoning in Symbolic Execution of C Programs
VeriStruct: AI-Assisted Automated Verification of Data-Structure Modules in Verus
Launch of CSLib, the Lean Computer Science Library
20 Feb 2026
CSLib, an open-source effort to formalize computer science in the Lean 4 theorem prover, has officially launched. Inspired by Mathlib's impact on mathematics, CSLib has two pillars: formalizing core computer science concepts in Lean, and building Lean infrastructure for reasoning about real-world code. The project also aims to advance neurosymbolic approaches that connect modern AI with formal reasoning. Clark Barrett serves on the CSLib Steering Committee with Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, and Leo de Moura. Researchers, practitioners, and enthusiasts are invited to get involved.
CSLibWhite Paper
How to Contribute
3 papers from Centaur at AAAI 2026, plus papers at VMCAI and CPP 2026
20 Jan 2026
Papers by Haoze Wu, Min Wu, and Pei Huang appear at AAAI 2026 in Singapore, covering cube-and-conquer tuning, compact formal explanations, and transformer verification. In January, Omri Isac's paper on proof minimization in neural network verification appeared at VMCAI 2026, and a paper with Harun Khan and Abdalrhman Mohamed on formalizing incremental linearization appeared at CPP 2026.
Cubing for TuningEfficiently Computing Compact Formal Explanations
Parameterized Abstract Interpretation for Transformer Verification
Proof Minimization in Neural Network Verification
Formalization of a Proof Calculus for Incremental Linearization
Certificates in AI: Learn but Verify in Communications of the ACM
01 Dec 2025
Clark Barrett, Thomas Henzinger, and Sanjit Seshia make the case for pairing machine learning with formal certificates in the December 2025 issue of Communications of the ACM.
Certificates in AI: Learn but VerifyAbdalrhman Mohamed and Harun Khan's paper in PACMPL
12 Oct 2025
Interactive Bitvector Reasoning using Verified Bit-Blasting, with Abdalrhman Mohamed, Harun Khan, and Clark Barrett among the authors, appears in Proceedings of the ACM on Programming Languages.
Interactive Bitvector Reasoning using Verified Bit-Blasting4 papers from Centaur at FMCAD 2025
06 Oct 2025
Papers by Amalee Wilson, Daneshvar Amrollahi, and Aron Perez-Lopez and colleagues, along with a paper on solving set constraints with comprehensions, appear at FMCAD 2025.
Per-Instance Subproblem Generation for Strategy Selection in SMTTowards SMT Solver Stability via Input Normalization
Automated Translation Validation of a Compiler for Statically Scheduled Accelerators
Solving Set Constraints with Comprehensions and Bounded Quantifiers
Hanna Lachnitt's paper at ITP 2025
28 Sep 2025
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL by Hanna Lachnitt, Jibiana Jakpor, Clark Barrett, and colleagues appears at the 16th International Conference on Interactive Theorem Proving (ITP 2025).
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOLAI For Math Fund Awards Stanford University Centaur Lab $1,000,000
17 Sep 2025
The Stanford Center for Automated Reasoning (Centaur) has been awarded $1,000,000 as part of the AI for Math Fund, managed by Renaissance Philanthropy in partnership with founding donor XTX Markets. With this award, Centaur will have the opportunity to develop a two-pronged approach to formal theorem proving. One is a more transparent, search-based white-box algorithm for general machine-assisted theorem proving. The other one is an SMT-solver based tactic for Lean 4.
NewsFunded Projects
Chuyue (Livia) Sun's paper at SAIV 2025
21 Jul 2025
ClassInvGen: Class Invariant Synthesis using Large Language Models by Chuyue (Livia) Sun, Clark Barrett, and colleagues appears at the 2nd International Symposium on AI Verification (SAIV 2025).
ClassInvGen: Class Invariant Synthesis using Large Language Models4 papers from Centaur at CAV 2025
21 Jul 2025
Four papers from Centaur appear at CAV 2025 in Zagreb, Croatia: two connecting Lean 4 with automated reasoning (Lean-SMT by Abdalrhman Mohamed, Harun Khan, Yicheng Qian, and colleagues, and Lean-auto by Yicheng Qian), Liza Pertseva's work on integer reasoning modulo different constants, and a relational Hoare logic for machine code.
Lean-SMT: An SMT Tactic for Discharging Proof Goals in LeanLean-auto: An Interface between Lean 4 and Automated Theorem Provers
Integer Reasoning Modulo Different Constants in SMT
Relational Hoare Logic for Realistically Modelled Machine Code
Leni Aniva's paper at TACAS 2025
03 May 2025
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4 by Leni Aniva, Chuyue (Livia) Sun, Clark Barrett, and colleagues appears at TACAS 2025.
PantographSophie Andrews's paper at DATE 2025
31 Mar 2025
Efficient SAT-Based Bounded Model Checking of Evolving Systems by Sophie Andrews, Matthew Sotoudeh, and Clark Barrett appears at the Design, Automation and Test in Europe Conference (DATE 2025).
Efficient SAT-Based Bounded Model Checking of Evolving SystemsA New Course on Lean 4
02 Feb 2025
In Spring 2025, Centaur Lab will launch a new course: CS 99 Functional Programming and Theorem Proving in Lean 4, covering from functional programming, theorem proving, to metaprogramming. The instructors will be Leni Aniva and Abdalrhman Mohamed. The course is designed to systematically cover Lean 4's features and working principles.
Explore CoursesPreview
Ying Sheng's SGLang paper at NeurIPS 2024
10 Dec 2024
SGLang: Efficient Execution of Structured Language Model Programs by Ying Sheng, Chuyue (Livia) Sun, Clark Barrett, and colleagues appears at NeurIPS 2024.
SGLang: Efficient Execution of Structured Language Model Programs4 papers from Centaur have been accepted to FMCAD 2024!
26 Sep 2024
Papers by Udayan Mandal, Ross Daly, and Rachel Cleaveland as well as a tool paper 'SMT-D: New Strategies for Portfolio-Based SMT Solving' have been accepted to FMCAD2024.
Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier CertificatesEfficiently Synthesizing Lowest Cost Rewrite Rules for Instruction Selection
Memory Consistency Model-Aware Cache Coherence for Heterogeneous Hardware
SMT tutorial paper has been selected as distinguished tutorial at FM 2024
26 Sep 2024
Satisfiability Modulo Theories: A Beginner's Tutorial by Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, and Yoni Zohar has been selected as a distinguished tutorial at the 26th International Symposium on Formal Methods located in Milan, Italy!
Satisfiability Modulo Theories: A Beginner’s TutorialClark Barrett and David Dill received the CAV Award
29 Jul 2024
Clark Barrett received his second, and David Dill his third, CAV Award for developing the Reluplex algorithm!
2024 CAV awardReluplex algorithm
Udayan Mandal received the Cristofer Stephensen Memorial Award
23 Jun 2024
Udayan Mandal has been awarded the Cristofer Stephensen Memorial Award for his master's thesis!
Ying Sheng joining UCLA
23 Jun 2024
Ying Sheng has accepted a faculty offer from UCLA!
Benjamin Przybocki received the Firestone Medal
14 Jun 2024
Benjamin Przybocki has been recognized with the Firestone Medal for his undergraduate thesis, Theoretical Aspects of Satisfiability Modulo Theories!
List of 2024 Firestone Medal winnersBenjamin Przybocki's paper accepted to FM 2024
10 Jun 2024
The nonexistence of unicorns and many-sorted Löwenheim–Skolem theorems by Benjamin Przybocki, Guilherme Toledo, Yoni Zohar, and Clark Barrett has been accepted to the 26th International Symposium on Formal Methods located in Milan, Italy!
Haoze Wu received the Centennial Teaching Assistant (CTA) Award
28 May 2024
Haoze (Andrew) Wu has been recognized with the Centennial Teaching Assistant (CTA) Award for his service as a teaching assistant (TA)!
List of 2024 CTA winnersSMT tutorial paper accepted to FM 2024
24 May 2024
Satisfiability Modulo Theories: A Beginner's Tutorial by Clark Barrett, Cesare Tinelli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds and Yoni Zohar has been accepted to the 26th International Symposium on Formal Methods located in Milan, Italy!
Nestan Tsiskaridze's paper accepted to IJCAR 2024
19 May 2024
Generalized Optimization Modulo Theories by Nestan Tsiskaridze, Clark Barrett and Cesare Tinelli has been accepted to the 12th International Joint Conference on Automated Reasoning located in Nancy, France!
Generalized Optimization Modulo TheoriesChuyue Sun and Ying Sheng's paper accepted to SAIV2024
19 May 2024
Clover: Closed-Loop Verifiable Code Generation by Chuyue Sun, Ying Sheng, Oded Padon and Clark Barrett has been accepted to the 7th International Symposium on AI Verification co-located with CAV in Montreal, Canada!
Clover: Closed-Loop Verifiable Code GenerationPei Huang's paper accepted to SAIV2024
19 May 2024
Parallel Verification for δ-Equivalence of Neural Network Quantization by Pei Huang, Yuting Yang, Haoze Wu, Ieva Daukantas, Min Wu, Fuqi Jia and Clark Barrett has been accepted to the 7th International Symposium on AI Verification co-located with CAV in Montreal, Canada!
Haoze Wu's paper accepted to CAV2024
15 May 2024
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks by Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz and Clark Barrett has been accepted to the 36th International Conference on Computer Aided Verification located in Montreal, Canada!
Marabou 2.0: A Versatile Formal Analyzer of Neural NetworksAlex Ozdemir's paper accepted to CAV2024
15 May 2024
Split Gröbner Bases for Satisfiability Modulo Finite Fields by Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett and Işil Dillig has been accepted to the 36th International Conference on Computer Aided Verification located in Montreal, Canada!
Split Gröbner Bases for Satisfiability Modulo Finite FieldsAina Niemetz and Mathias Preiner's paper accepted to CAV2024
15 May 2024
Scalable Bit-Blasting with Abstractions by Aina Niemetz, Mathias Preiner and Yoni Zohar has been accepted to the 36th International Conference on Computer Aided Verification located in Montreal, Canada!
Benjamin Przybocki awarded Churchill Scholarship
18 Jan 2024
Benjamin Przybocki was awarded the Churchill Scholarship for a year of independent research at Cambridge and selected as a runner-up for the Computing Research Association (CRA) Outstanding Undergraduate Research Award!
Stanford News on Churchill ScholarshipCRA Announcement
Haoze Wu joining Amherst College
04 Jan 2024
Haoze (Andrew) Wu will be joining Amherst College as an Assistant Professor in the Computer Science Department starting Fall 2024!
Benjamin Przybocki named a runner-up for the CRA Outstanding Undergraduate Researcher Award
02 Jan 2024
Benjamin Przybocki has been named a runner-up for the Computing Research Association's 2024 Outstanding Undergraduate Researcher Award, which recognizes undergraduate students in North American universities who show outstanding potential in an area of computing research. Ben's research in automated reasoning includes results on the theory of finite sequences and on combinations of first-order theories.
CRA AnnouncementCRA Outstanding Undergraduate Researcher Award