# A Formally Verified Robustness Certifier for Neural Networks (Extended Version)

arXiv: https://arxiv.org/abs/2505.06958 · HTML: https://mlsanity.com/paper/2505.06958/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 31 references that are in the map.
- First posted on arXiv 11 May 2025.

## Builds on (most cited first, 15 of 15)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Certified Robustness to Adversarial Examples with Differential Privacy](https://mlsanity.com/paper/1802.03471/) (2018)
- [Regularisation of Neural Networks by Enforcing Lipschitz Continuity](https://mlsanity.com/paper/1804.04368/) (2018)
- [Adversarial Robustness Toolbox v1.0.0](https://mlsanity.com/paper/1807.01069/) (2018)
- [Sorting out Lipschitz function approximation](https://mlsanity.com/paper/1811.05381/) (2018)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [Adversarial Robustness of Deep Neural Networks: A Survey from a Formal Verification Perspective](https://mlsanity.com/paper/2206.12227/) (2022)
- [Fast Geometric Projections for Local Robustness Certification](https://mlsanity.com/paper/2002.04742/) (2020)
- [Efficient Bound of Lipschitz Constant for Convolutional Layers by Gram Iteration](https://mlsanity.com/paper/2305.16173/) (2023)
- [Verification of Neural Networks' Global Robustness](https://mlsanity.com/paper/2402.19322/) (2024)
- [Getting a-Round Guarantees: Floating-Point Attacks on Certified Robustness](https://mlsanity.com/paper/2205.10159/) (2022)

## Built on by (most cited first, 1 of 1)

- [Lipschitz-Based Robustness Certification Under Floating-Point Execution](https://mlsanity.com/paper/2603.13334/) (2026)

## Abstract (arXiv)

Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural networks, which employ a function to certify that the classification of an input cannot be altered by such a perturbation. Outputs that pass this test are called certified robust. However, to the authors' knowledge, these certification functions have not yet been verified at the implementation level. We demonstrate how previous unverified implementations are exploitably unsound in certain circumstances. Moreover, they often rely on approximation-based algorithms, such as power iteration, that (perhaps surprisingly) do not guarantee soundness. To provide assurance that a given output is robust, we implemented and formally verified a certification function for globally-robust neural networks in Dafny. We describe the program, its specifications, and the important design decisions taken for its implementation and verification, as well as our experience applying it in practice.