At Imandra, our mission is
to revolutionize algorithm design,
regulation, transparency and governance
by democratizing automated reasoning.

Our mission

Fundamentally, the algorithms we depend on have become too complex to design and implement ‘by hand.’ The problem is that the mathematical tools available to do this right — formal verification and automated reasoning — have classically been inaccessible to those without a PhD in the field and have often not scaled to relevant "real-world" problems.

We founded the company to change this. Based upon deep advances in (both symbolic and statistical) AI, we’ve built Imandra to make automated reasoning scalable and accessible.

What is Imandra?

Imandra is a cloud-native automated reasoning engine for analysis of algorithms bringing unprecedented rigor and automation to algorithm design and governance.

By automated reasoning, we mean automated mathematical techniques combining symbolic (e.g., automated theorem proving) and statistical (e.g. neural networks) AI for performing reasoning tasks such as analyzing all possible behaviors of an algorithm or controller, or synthesizing solutions to complex planning or constraint problems.

By analysis we mean both mathematically verifying algorithm properties and systematically exploring, enumerating and elucidating possible algorithm behaviors.

By algorithms we mean of course computer programs, but also virtually any computational system such as planning problems, jet fighter controllers, financial stock exchanges, logistics systems, legal contracts, autonomous systems, etc.

By cloud-native we mean Imandra was designed with scalability, seamless cloud-based toolchain integration and continuous improvement in mind.

Imandra Core

Top features

Over the last decade, there have been many disparate advances in the field of formal verification.
We've spent the last five years carefully crafting an engine that combines these advances into a highly automated reasoning engine for scalable analysis of real-world algorithms.

Let us briefly go through some of the distinct features of Imandra:

Unprecedented automation - traditionally formal verification required a PhD in the domain to be involved because the machines had to be guided to produce results; with Imandra, many deep analyses are completely push-button. Moreover, Imandra has a seamless integration of bounded model-checking and full-featured interactive theorem proving, giving users the freedom to choose how deep they’d like to go (in terms of state-space exploration) on various algorithm analysis tasks, with verification explanations that can be directly incorporated into safety and audit cases.

Interface languages - Imandra’s logic is built directly upon the high-performance functional programming languages OCaml and ReasonML ( and ( This means that Imandra can directly reason about programs written in these languages. Moreover, we’ve built interfaces for other popular languages such as Python.

Extensibility - Imandra’s interface languages allow you to express virtually any type of algorithm. Imandra can be further customized for particular domains (e.g., with customized nonlinear decision procedures for analyzing geometrical movements in avionics controllers).

Counterexamples - Imandra's reasoning engine is "complete for counterexamples" in a precise sense. Verification practitioners are well aware that one of the largest time sinks in verification comes from trying to prove false goals. With Imandra, we set out to eliminate this issue in a practical sense, by building a reasoning engine that can synthesize deep counterexamples to incorrect verification conjectures automatically, even in the presence of recursive functions and nonlinear arithmetic. Moreover, as Imandra’s logic is built on an executable programming language, all counterexamples are made “first-class” in Imandra and can be directly computed with and run through the code being analyzed.

Scalability - when analyzing algorithms, many techniques may be performed in parallel and cached. Imandra’s cloud-native architecture takes full advantage of this.

Graphical User Interface (GUI) - Imandra’s GUI integration includes Microsoft VS Code (you can download it as a plugin in the Microsoft VS Code Marketplace), Jupyter Notebooks, and is heavily extensible via the Language Server protocol.


Let’s now dive into the specifics with links to various interactive examples. As already discussed, Imandra has two core applications: formal verification and symbolic reasoning. Here we present both with relevant examples:


FV is a well-established field built around the mathematical verification of algorithm properties. Historically, and especially as it’s applied to verification of general software, this was a very manual effort requiring years of specialized training (PhD). Imandra is changing this.

The following are examples applications of Imandra verifying properties from different domains. You will notice that (1) you use the same language to write programs and properties you wish to verify, and (2) the level of FV expertise required to use Imandra and get results is minimal; indeed, we believe an typical engineering or computer science graduate can easily make serious use of Imandra out of the box.

Verifying a simple vehicle controller
Verifying a hardware component
Verifying a Robot OS node


STATE-SPACE DECOMPOSITION: Region Decomposition is inspired by Cylindrical Algebraic Decomposition, a fundamental technique for reasoning about nonlinear polynomial systems by decomposing Euclidean space into a finite number of connected regions s.t. within each region the behavior of the system under analysis is invariant. This effectively computes a “map” of all possible behaviors of the system, and facilitates a wide variety of nonlinear decision procedures over the reals and complexes.

Read a high-level overview Illustration demonstrating concept of region decomposition

Here are some of the use cases:

Testing - when it comes to testing complex systems, everyone agrees that they should be tested ‘thoroughly’, but what does that mean? What’s a scientifically-grounded technique for describing ‘thoroughness’? With Region Decomposition, you get precisely this - a quantitative measure of a system state-space. The Regions in this case represent the quantitative analogs of ‘edge cases’ that engineers typically construct ‘by hand’ or with help of random number generators.

Model-based engineering - Imandra paves way to true model-based development (MBE). A model developed in Imandra is:
● Susceptible to formal verification as discussed above
● Executable, so may be co-simulated with the actual implementation to audit performance
● May be used to automatically generate test cases with quantitative coverage metrics, through the application of Imandra’s Region Decomposition machinery.

Autonomous systems - as autonomous systems become ubiquitous, it is evermore important to ensure they’re tested thoroughly. Reliable simulation environments are used to test algorithms before they’re deployed in the real-world. But the question remains: how do we reason about thoroughness of the tests that these systems are subjected to? With Imandra, you may develop a model of the physical environment and derive the symbolic edge cases (or regions), and translate them into testing scenarios targeting specific simulation environments.

Example: Simple Stoplight Model

Explainability/Documentation generation - when Imandra computes regions, it reflects them back into the runtime so you may compute with them. We have example where we translate region descriptions into English-like prose which may serve as precise and automatically generated documentation of a model. In fact, our clients in financial services already rely on this technique for generating up-to-date and thorough documentation.

Reinforcement learning - when you’re training an image classifier, it’s important to make sure the training data is diverse. No single class is over-represented or under-represented. Any skew in the training data will lead to a bias in the classifier. How do we translate this to decision controllers trained using Reinforcement learning? Imandra’s Region Decomposition provides a methodology for ensuring the training of reinforcement learning algorithms is diverse. Naturally, this leads to better performance and faster convergence. We have results to demonstrate this which we can share if you’re interested. Moreover, we have developed a Python interface (discussed below) to make it easy to use Imandra together with the popular NN libraries like TensorFlow.

Planning - in complex domains, it may be the case that there are no ‘good’ solutions and the operator has to choose one among many and understand why those options were presented. Imandra is uniquely positioned to not only solve both traditional and highly nontraditional planning problems (e.g., through its decision procedures for recursive function unrolling integrated with SMT solving), but also to leverage its symbolic reasoning to explore, compare and explain the full spectrum of possible outcomes and generate concrete plans to accomplish them.

CONSTRAINT SOLVING - some problems require much more powerful means of expressing problems than what traditional constraint solvers provide. Imandra treats code as mathematical logic, allowing you to encode even the most complex problems as executable programs which can then be automatically analyzed with respect to a rich language of constraints (including recursive functions, higher-order functions, nonlinear real and floating point arithmetic and more):

Examples of Imandra solving constraints:

Crossing the river

OPTIMIZATION - similarly to constraint solving discussed above, Imandra may be used to search for a solution that not only satisfies a specified set of non-trivial constraints, but also maximizes (or minimizes) a specific penalty function. We will have examples of these solutions soon.

Use cases

There are 3 ways to use Imandra: (1) as a stand-alone tool for reasoning about code written in OCaml/ReasonML, (2) creating a Domain Specific Language (DSL) that translates into OCaml and is analyzed by Imandra, and (3) by integrating Imandra's Reasoning as a Service® APIs into a larger application:

1. A stand-alone tool for reasoning about code written in OCaml/ReasonML

Imandra use case

OCaml is a great open source general programming language. For its pure subset we have created mechanized formal semantics - code written in this pure subset Imandra automatically translates into axiomatic representation and analyzes. Imandra operates in two 'modes' - 'logic' for analyzing the pure subset of OCaml and 'program' which allows you to write impure OCaml code that

interacts with 'logic' mode. This flexibility allows you to write powerful applications leveraging automated reasoning. ReasonML is a new language built on OCaml designed primarily for web development (e.g. Facebook Messenger is written in ReasonML) which Imandra now supports.

2. Create a Domain Specific Language (DSL) "on top of" Imandra

Imandra use case

While OCaml/ReasonML are great general programming languages, many types of problems benefit from Domain Specific Languages. We have two examples of such languages - PyIDF and Imandra Protocol Language (IPL):
2.1. PyIDF is a Python interface to our Iterative Decomposition Framework (Region Decomposition optimized for analysis of multi-step behavior of state machines). We created the Python interface

to make this easily accessible for machine learning/AI developers.
2.2. IPL is a domain specific language for encoding system connectivity protocols. We designed it primarily for trading systems, but it's generic enough to be applied to any complex system. Our team has incredible language design and development expertise, so if you have a specific project in mind, please do not hesitate to contact us (

3. Integrate Imandra Core's APIs into another application

Imandra use case

Imandra Core's reasoning power may be seamlessly integrated into your application through its Reasoning as a Service® APIs. Imandra Core's features like region decomposition, constraint solving and optimization (mixing continuous and discrete decision variables) offer unprecedented capabilities for applications across numerous industries.

One example of such integration is our IPL Simulator product where a user can turn any IPL (Imandra Protocol Language) model into an on-demand simulation environment. There, Imandra automatically processes the generated model and acts as a library which synthesizes messages in response to user actions.

VS Code

The Imandra IDE is a VS Code Plugin available for download in the MS Visual Studio Marketplace. It provides the typical syntax highlighting and type checking services, and asynchronous reasoning with caching. While you type, Imandra works in the background to analyze the queries and presents the results right back into your editor window. Smart caching of the intermediate results means Imandra is only analyzing incremental changes creating an incredible user experience.

Download VS Code plugin
IML VS code example
Jupyter Notebooks Example

Jupyter Notebooks

Jupyter Notebook is one of key interfaces to Imandra. This is particularly useful when using Imandra for data-driven tasks and analyses. Furthermore, custom printer interface allows you to define HTML printers for Imandra values which will be automatically used by the Notebook cells.

Jupyter Notebooks Example


Imandra's command line interface is the hacker's tool of choice. It provides all of the features, the old school way.

IML terminal code example

Installation options

1. Single user local Imandra Core
The simplest way to run Imandra Core is by running it on a local machine either as a Docker container or native executables for *nix operating systems (eg. Mac OS or Linux). Note that this is only available for enterprise and Government users.

Imandra installation options
Imandra installation options

2. Single user Imandra Core in a Kubernetes cluster
Imandra is natively designed to take advantage of cloud computing. With Imandra Core running in Kubernetes, it takes advantage of parallelization and caching, significantly speeding up several important classes of queries like region decomposition and formal verification. We provide this as the default environment for our retail customers in Google Cloud and make it available for enterprise and Government users.

Imandra installation options

3. Multi-tenant Imandra Core in a Kubernetes cluster
Imandra Core caches intermediate results, so running a multi-tenant Kubernetes environment brings further speed improvements as Imandra reuses results from your colleagues' queries. Similarly to the setup #2 above, we provide this for retail customers in the public cloud, and enterprise and government customers (public cloud and on-premise).

Imandra installation options

Imandra vs.

Boyer-Moore: Like ACL2, Imandra’s logic is based on a mechanized formal semantics for an efficiently executable programming language (for ACL2, this is a first-order fragment of Lisp; for Imandra, this is a higher-order fragment of OCaml/ReasonML). This means that Imandra models are simultaneously executable programs (i.e., valid OCaml/ReasonML) and mathematical artifacts which may be subjected to rigorous formal analysis by Imandra’s reasoning engine. In Imandra, we have “lifted” many core Boyer-Moore ideas powering their remarkable successes in automating induction and simplification to our typed, higher-order setting.

HOL, Isabelle/HOL, Coq, Agda and Lean: Like provers in the HOL family (as well as those based on dependent types such as Coq, Agda and Lean), Imandra’s logic is strongly typed. Like HOL systems, Imandra is built upon a higher-order polymorphic type theory (a variant of Hindley-Milner corresponding to pure OCaml). Imandra supports a rich executable fragment of HOL, with automation including efficient higher-order rewriting and induction through first-order specialization.

SAT and SMT: Like SMT solvers, Imandra contains orchestrated combinations of high-performance CDCL-based SAT solving and decision procedures for theories relevant to program analysis. Crucially, Imandra’s proof procedures support the synthesis of reflected executable counterexamples (even of higher-order goals requiring function synthesis). All counterexamples constructed by Imandra are “first-class,” i.e., executable and available in the same runtime environment as the formal models themselves. This allows rapid prototyping iteration and model diagnostics, as counterexamples can be directly run through models. Imandra lifts SMT from (non-executable, monomorphic) first-order logic without recursion and induction to a rich executable, polymorphic higher-order logic with recursion and induction.

Integration of Model Checking and Theorem Proving: Imandra seamlessly integrates bounded model checking (lifted to operate modulo higher-order recursive functions over algebraic datatypes, integers, reals, etc.) and “full-fledged” interactive theorem proving. Every verification goal in Imandra may be analyzed in “bounded” and “unbounded” fashions, and bounded results may be turned into actual theorems (e.g., incorporating bounds on the datatypes involved explicitly in theorem hypotheses) automatically. This allows for powerful incremental approaches to verification, utilizing bounded verification to rapidly eliminate design flaws,“completing” the results to their unbounded form as necessary only after all flaws corresponding to counterexamples found by bounded verification attempts have been eliminated.

Nonlinear Decision Procedures for Hybrid Systems: Imandra has deep support for datatypes and decision procedures relevant to the analysis of hybrid systems. This includes model-producing decision procedures for the existential theory of real closed fields (nonlinear real arithmetic w.r.t. systems of many-variable nonlinear polynomial equations and inequalities) integrated with Imandra’s inductive “waterfall” proof procedure. Moreover, Imandra can natively compute with and reason about real algebraic numbers. Through our experience working with (and in many cases contributing to) hybrid systems verification tools such as KeYmaera, Flow*, dReal and dReach and HybridSAL, we recognize scalable nonlinear real decision procedures as one of the most important bottlenecks in hybrid systems verification. The derivation of computable counterexamples (dually, instances in the case of test-case generation) satisfying constraints on both the discrete and continuous components of the models is crucial to efficient V&V.

More on Region Decomposition

Region decomposition lifts CAD to algorithms through a combination of symbolic execution, automated induction and nonlinear decision procedures. The result is an automatic method for decomposing the state-space of a system (as given by the “step” function of an (infinite) state-machine) into a finite number of symbolically described regions s.t. (a) the union of all regions covers the entire state-space, and (b) in each region, the behavior of the system is invariant. Regions decompositions are computed subject to a basis, a collection of function and predicate symbols which are taken as “basic” and will be used in region descriptions, and side-conditions which may express queries to focus the decomposition on specific behaviors (i.e., compute all regions of the state-space s.t. the controller will result in the following bad state). Bases and side-conditions facilitate configurable abstraction boundaries and foci and allow the analysis of the state-space to be adapted for many different applications, from high-coverage test-suite generation to automated documentation synthesis to interactive state-space exploration.

Give it a spin

Try Imandra

and join us on

By using this website, you agree to our cookie policy

Please note that the Imandra website no longer supports Internet Explorer

We recommend upgrading to the latest Microsoft Edge, Google Chrome, or Firefox