# CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 52 references that are in the map.
- First posted on arXiv 7 Jun 2022.

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

- [Deep Learning with Differential Privacy](https://mlsanity.com/paper/1607.00133/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [Concolic Testing for Deep Neural Networks](https://mlsanity.com/paper/1805.00089/) (2018)
- [Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition](https://mlsanity.com/paper/2104.06718/) (2021)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [Perfectly Parallel Fairness Certification of Neural Networks](https://mlsanity.com/paper/1912.02499/) (2019)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [Output Range Analysis for Deep Neural Networks](https://mlsanity.com/paper/1709.09130/) (2017)
- [Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification](https://mlsanity.com/paper/1902.09866/) (2019)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Efficient Neural Network Analysis with Sum-of-Infeasibilities](https://mlsanity.com/paper/2203.11201/) (2022)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Robustness Verification of Support Vector Machines](https://mlsanity.com/paper/1904.11803/) (2019)

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

- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [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)
- [Neural Network Verification with PyRAT](https://mlsanity.com/paper/2410.23903/) (2024)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [Compiling High-Level Neural Network Specifications into VNN-LIB Queries](https://mlsanity.com/paper/2402.01353/) (2024)
- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025)
- [VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification](https://mlsanity.com/paper/2605.07451/) (2026)
- [The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification](https://mlsanity.com/paper/2506.12084/) (2025)

## Abstract (arXiv)

We present CAISAR, an open-source platform under active development for the characterization of AI systems' robustness and safety. CAISAR provides a unified entry point for defining verification problems by using WhyML, the mature and expressive language of the Why3 verification platform. Moreover, CAISAR orchestrates and composes state-of-the-art machine learning verification tools which, individually, are not able to efficiently handle all problems but, collectively, can cover a growing number of properties. Our aim is to assist, on the one hand, the V&V process by reducing the burden of choosing the methodology tailored to a given verification problem, and on the other hand the tools developers by factorizing useful features-visualization, report generation, property description-in one platform. CAISAR will soon be available at https://git.frama-c.com/pub/caisar.