The Luna Bound Propagator for Formal Analysis of Neural Networks

Researchers have introduced Luna, a C++ implementation of the alpha-CROWN neural network verification method. Luna provides competitive performance with existing Python implementations while offering better integration capabilities for production systems and DNN verifiers.

• →Luna is a new C++ bound propagator that implements alpha-CROWN analysis for neural network verification.
• →The tool supports Interval Bound Propagation, CROWN analysis, and alpha-CROWN analysis over general computational graphs.
• →Luna achieves competitive performance with state-of-the-art Python implementations in both bound tightness and computational efficiency.
• →The C++ implementation enables better integration into existing DNN verifiers and production-level systems.
• →Performance was validated on benchmarks from VNN-COMP 2025.