# A Certified Proof Checker for Deep Neural Network Verification in Imandra

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 45 references that are in the map.
- First posted on arXiv 17 May 2024.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [Exploiting Verified Neural Networks via Floating Point Numerical Error](https://mlsanity.com/paper/2003.03021/) (2020)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Catala: A Programming Language for the Law](https://mlsanity.com/paper/2103.03198/) (2021)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [DNN Verification, Reachability, and the Exponential Function Problem](https://mlsanity.com/paper/2305.06064/) (2023)
- [Robustness Assessment of a Runway Object Classifier for Safe Aircraft Taxiing](https://mlsanity.com/paper/2402.00035/) (2024)
- [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)
- [CheckINN: Wide Range Neural Network Verification in Imandra (Extended)](https://mlsanity.com/paper/2207.10562/) (2022)
- [A formalization of convex polyhedra based on the simplex method](https://mlsanity.com/paper/1706.10269/) (2017)
- [Securing Verified IO Programs Against Unverified Code in F*](https://mlsanity.com/paper/2303.01350/) (2023)
- [ACL2 Proofs of Nonlinear Inequalities with Imandra](https://mlsanity.com/paper/2311.08861/) (2023)

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

- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Proof Minimization in Neural Network Verification](https://mlsanity.com/paper/2511.08198/) (2025)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)
- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025)
- [Uncovering Bugs in Formal Explainers: A Case Study with PyXAI](https://mlsanity.com/paper/2511.03169/) (2025)
- [On Improving Deep Active Learning with Formal Verification](https://mlsanity.com/paper/2512.14170/) (2025)

## Abstract (arXiv)

Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safety-critical ones. However, DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and numerical imprecision; this, in turn, has raised the question of trust in DNN verifiers. One prominent attempt to address this issue is enhancing DNN verifiers with the capability of producing certificates of their results that are subject to independent algorithmic checking. While formulations of Marabou certificate checking already exist on top of the state-of-the-art DNN verifier Marabou, they are implemented in C++, and that code itself raises the question of trust (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou certificate checking in Imandra -- an industrial functional programming language and an interactive theorem prover (ITP) -- that allows us to obtain full proof of certificate correctness. The significance of the result is two-fold. Firstly, it gives stronger independent guarantees for Marabou proofs. Secondly, it opens the way for the wider adoption of DNN verifiers in interactive theorem proving in the same way as many ITPs already incorporate SMT solvers.