VerifAI is a software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components. VerifAI particularly seeks to address challenges with applying formal methods to perception and ML components, including those based on neural networks, and to model and analyze system behavior in the presence of environment uncertainty. The current version of the toolkit performs intelligent simulation guided by formal models and specifications, enabling a variety of use cases including temporal-logic falsification (bug-finding), model-based systematic fuzz testing, parameter synthesis, counterexample analysis, and data set augmentation.


This work is supported in part by the  DARPA Assured Autonomy  program.


University of California, Berkeley, California, USA


Tommaso Dreossi

Daniel J. Fremont

Shromona Ghosh

Edward Kim

Hadi Ravanbakhsh

Marcell Vazquez-Chanlatte

Sanjit A. Seshia