A library for automatically computing differentiable verified output bounds for general computational graphs. Originally proposed in our NeurIPS 2020 paper, it is the core bound computation engine in the award-winning alpha-beta-CROWN.

A comprehensive neural network verification toolbox that consists of multiple complete verification algorithms (such as GenBaB) on top of auto_LiRPA. It is the 1st place winner at the annual VNN-COMP from 2021 to 2024.