This approach first learns a recurrent network that represents an implicit distribution over future feature values of a dynamic process.

Scenic is a domain-specific probabilistic programming language for modeling the environments of cyber-physical systems like robots and autonomous cars.

Trinity implements a model-based quantitative assurance framework for autonomous systems that uses predictive coding (PC).

Venus is a state-of-the-art sound and complete verification toolkit for Relu-based feed-forward neural networks. It can be used to check reachability and local adversarial robustness properties.

VerifAI is a software toolkit for the formal design and analysis of systems that include artificial intelligence (AI) and machine learning (ML) components.

Verisig is a tool for verifying safety properties of autonomous systems with neural network (NN) controllers.  Verisig  supports sigmoid and tanh-based networks and exploits the fact that the sigmoid (and the tanh) is the solution to a