GBM is a software framework that enhances the robustness of neural architectures through the computation of Growth Bound Matrices. It supports LSTM, S4, and CNN models by automatically deriving robustness regularizers that constrain the amplification of input perturbations. Given a trained or partially trained model, GBM performs local linearization of its dynamics to estimate sensitivity via the growth bound matrix, which quantifies how perturbations propagate across layers or timesteps. These bounds are then integrated into training to jointly optimize accuracy and adversarial robustness.

The Neural Control Invariance Checker is a Python package designed to assess the invariance (safety) properties of a continuous-time linear system when controlled by a neural network controller. The proposed algorithm present the advantage of being complete. This package provides tools to analyze and evaluate the safety of the closed-loop system in various scenarios. The tool relies on the use of continuous piece-wise affine (PWA) activation functions (e.g. ReLU) which render the NN a PWA continuous function while providing safety certificates through the use of Nagumo’s theorem.

This library implements different methods to prove specification of controllers of dynamical systems based on Neural Networks. We provide a DDPG implementation using TensorFlow that allows to train some agents on problem environments that should have a similar structure to OpenAI's Gym env structure. Feed-forward neural networks that model the controller and are implemented on TensorFlow with only monotonous activation functions can also be used to study the reachability set of the dynamical system. We provide example of both applications on concrete problems.