Sanjit A. Seshia

The intersection of formal methods (FM)/automated reasoning and artificial intelligence (AI)/machine learning (ML) has been an active research topic of mine for over 25 years. This research comprises two inter-related thrusts:

• AI-Enabled Formal Methods: Perform tasks in formal methods by reduction to synthesis, and perform synthesis by integrating AI/ML with deductive procedures. The following position paper, first published in 2011-2012, outlines this approach and initial results.
      Sanjit A. Seshia. Combining Induction, Deduction, and Structure for Verification and Synthesis. Proceedings of the IEEE, 103(11):2036–2051, 2015.
  See also this 2025 talk (video) describing my work in this thrust over 25+ years. Our UCLID5 open-source project implements this approach.


• Verified AI: Develop and employ novel formal methods for safe and trustworthy AI systems. The following position paper, first published in 2016, outlines this approach and describes preliminary results:
      Sanjit A. Seshia, Dorsa Sadigh, and S. Shankar Sastry. Toward Verified Artificial Intelligence. Communications of the ACM, 65(7):46–55, 2022.
  See this 2024 colloquium lecture (video) describing this approach. This approach is implemented in our open-source tools Scenic and VerifAI.

I take a full stack approach to formal methods, meaning that my group works on all of the layers that make up formal tools: (i) computational engines such as satisfiability (SAT/SMT) solvers that underpin automated reasoning; (ii) algorithmic strategies for verification and synthesis that build on those engines; and (iii) formalisms and languages for modeling and specifying problems and systems from a variety of domains. Our work has been applied to improving the safety, security, and dependability of software, hardware, distributed systems, AI/ML, robotics, cyber-physical systems, and biological systems, impacting societal-scale applications in several domains including cloud computing, transportation, healthcare, and education. Our research is made available to the broader community in a range of open-source tools.

Here is a selection of some of our most impactful research contributions:

• SMT Solving and SMT-based Verification: We developed UCLID (pronounced "Euclid"), one of the first satisfiability modulo theories (SMT) solvers and SMT-based verifiers. We continue to work on new SMT solvers (e.g., Algaroba), along with verifiers (e.g., UCLID5) applied to novel motivating applications. See this brief video for a perspective on our contributions to SMT solving at the 2021 CAV Award presentation.
• Algorithmic Formal Synthesis: We have contributed to the development of fundamental techniques in the synthesis of programs and other formal artifacts, including counterexample-guided inductive synthesis (CEGIS), syntax-guided synthesis (SyGuS), and oracle-guided inductive synthesis (learning), as well as applications of AI/ML-based formal synthesis including specification synthesis, timing analysis of embedded software, program synthesis, controller synthesis, and algorithmic improvisation. See this brief video for a perspective on oracle-guided inductive synthesis presented during the Most Influential Paper award session at ICSE 2020.
• Verified AI and AI-Enabled Autonomy: We have developed formal methods to address the topics of AI Safety and Trustworthy AI, implemented in open-source tools Scenic and VerifAI, which we have demonstrated for the design and verification of AI-enabled autonomous and semi-autonomous cyber-physical systems (such as autonomous vehicles including industrial-scale systems). In the VeHICaL project, we pioneered several techniques for Human-CPS, cyber-physical systems that operate in concert with humans (also called human-robot systems).
• Formal Methods for Secure and Distributed Computing: Our work has addressed formal modeling and verification of secure and distributed systems, in collaboration with and having industrial impact at several companies including Microsoft, Amazon (AWS), and Intel. Contributions include verification of software written for and designs of trusted execution environments; specification and verification of microarchitectural side-channel attacks, and to the P modeling and testing framework, particularly its compositional modeling and testing tools, and its formal verifier, the P Verifier. Most of these contributions build on our UCLID5 open-source project.

Over the years, our research has had substantial industrial impact through our open-source projects. My research has also contributed to the founding of a few startup companies, Decyphir, Inc. (in the area of automotive powertrain systems) and 20ⁿ Labs, Inc. (based on the ACT project addressing modeling, verification, and synthesis problems in synthetic biology).

I co-developed, with Edward A. Lee, an undergraduate course on Embedded, Cyber-Physical Systems. We also published an accompanying textbook Introduction to Embedded Systems: A Cyber-Physical Systems Approach currently in its second edition published by MIT Press. Our textbook has been adopted in over 50 countries. In 2014, we offered one of the first "massive open online courses" (MOOCs) on Cyber-Physical Systems on the edX platform: EECS149.1x. This MOOC was the first, to our knowledge, to employ formal verification in the automatic grading system (which was designed using inductive synthesis). More information about the automatic grading software, CPSGrader, is available here. I also taught a graduate-level course on Formal Methods for Engineering Education, one of the early classes to explore the use of AI/ML in CPS and robotics education at scale.

In 2024, I helped create a new international conference on Neuro-Symbolic Systems (NeuS), and serve on its steering committee.

Selected talks and further details on research and teaching are available. A good starting point is to browse my recent publications.

Note to prospective students and postdocs