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. Venus implements a MILP-based verification method whereby it leverages dependency relations between the ReLU nodes to reduce the search space that needs to be considered during branch-and-bound. It additionally implements methods based on symbolic interval propagation and input domain splitting. 

Keywords:  formal verification; local adversarial robustness; neural networks.