# The Imandra Automated Reasoning System (system description)

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Apr 2020.

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

- [A Certified Proof Checker for Deep Neural Network Verification in Imandra](https://mlsanity.com/paper/2405.10611/) (2024)
- [Towards a Certified Proof Checker for Deep Neural Network Verification](https://mlsanity.com/paper/2307.06299/) (2023)
- [CheckINN: Wide Range Neural Network Verification in Imandra (Extended)](https://mlsanity.com/paper/2207.10562/) (2022)
- [Proof-Carrying Neuro-Symbolic Code](https://mlsanity.com/paper/2504.12031/) (2025)

## Abstract (arXiv)

We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-Moore family like ACL2, and interactive proof assistants for typed higher-order logics. Imandra's logic is computational, based on a pure subset of OCaml in which all functions are terminating, with restrictions on types and higher-order functions that allow conjectures to be translated into multi-sorted first-order logic with theories, including arithmetic and datatypes. Imandra has novel features supporting large-scale industrial applications, including a seamless integration of bounded and unbounded verification, first-class computable counterexamples, efficiently executable models and a cloud-native architecture supporting live multiuser collaboration. The core reasoning mechanisms of Imandra are (i) a semi-complete procedure for finding models of formulas in the logic mentioned above, centered around the lazy expansion of recursive functions, and (ii) an inductive waterfall and simplifier which "lifts" many Boyer-Moore ideas to our typed higher-order setting. These mechanisms are tightly integrated and subject to many forms of user control. Imandra's user interfaces include an interactive toplevel, Jupyter notebooks and asynchronous document-based verification (in the spirit of Isabelle's Prover IDE) with VS Code.