# CheckINN: Wide Range Neural Network Verification in Imandra (Extended)

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 13 of its 46 references that are in the map.
- First posted on arXiv 21 Jul 2022.

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

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Quantizing deep convolutional networks for efficient inference: A whitepaper](https://mlsanity.com/paper/1806.08342/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Unconstrained Monotonic Neural Networks](https://mlsanity.com/paper/1908.05164/) (2019)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Neural Network Compression Framework for fast model inference](https://mlsanity.com/paper/2002.08679/) (2020)
- [PaRoT: A Practical Framework for Robust Deep Neural Network Training](https://mlsanity.com/paper/2001.02152/) (2020)
- [The Imandra Automated Reasoning System (system description)](https://mlsanity.com/paper/2004.10263/) (2020)
- [Neural Networks in Imandra: Matrix Representation as a Verification Choice](https://mlsanity.com/paper/2205.09556/) (2022)
- [Differentiable Logics for Neural Network Training and Verification](https://mlsanity.com/paper/2207.06741/) (2022)

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

- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)

## Abstract (arXiv)

Neural networks are increasingly relied upon as components of complex safety-critical systems such as autonomous vehicles. There is high demand for tools and methods that embed neural network verification in a larger verification cycle. However, neural network verification is difficult due to a wide range of verification properties of interest, each typically only amenable to verification in specialised solvers. In this paper, we show how Imandra, a functional programming language and a theorem prover originally designed for verification, validation and simulation of financial infrastructure can offer a holistic infrastructure for neural network verification. We develop a novel library CheckINN that formalises neural networks in Imandra, and covers different important facets of neural network verification.