Imandra is AI for
the automated tomorrow

Our groundbreaking automated reasoning technology empowers intelligent machines and their designers to fulfill the promises of automation.

Spotlight on an Imandra user:

In 2017 Imandra Inc. partnered with Goldman Sachs to help deliver the SIGMA X MTF Auction Book, a new orderbook venue implementing periodic auctions. Imandra Inc. used Imandra, our own automated reasoning engine, to formally model the Goldman Sachs design of the SIGMA X MTF Auction Book, verify its key properties, and automate rigorous testing. Now that the venue is live, Imandra is being used to perform ongoing validations of trading operations.

WEF recognizes
Imandra's AI leadership

The World Economic Forum (WEF) in a detailed report recently highlighted Imandra's unique position to pave way for scalable and AI-powered Model-Based Software Engineering (MBSE) within financial markets as a key ingredient for modernization of financial infrastructure.

Imandra is
Reasoning as a Service®

Whether you're writing mission-critical code (who isn't today?) or need to understand the countless complex decisions that a system may make, Imandra brings the latest advances in automated reasoning to your fingertips. Imandra was designed at cloud-scale, so whether you're working on a school project or the next Mars rover - we've got you covered.

Imandra Core Demo Gallery

Check out our Demo Gallery containing a sortable diverse collection of Imandra examples.

Browse the Gallery

Where and how
we make a difference




Imandra Core - the mathemagic powering it all

Imandra Core is our underlying reasoning engine. It is available both as a standalone product and as a foundational technology for customized solutions for specific industry needs. Its features may be divided into two broad categories that we describe as (1) extracting algorithms from data and (2) extracting data from algorithms.

Extraction of logical rules from sequential data and anomaly detection

Extraction of logical rules from sequential data and anomaly detection

Formal verification, constraint solving, region decomposition

Formal verification, constraint solving, region decomposition

Imandra Core

Top Imandra Core features

Small, green Imandra logo

Formal verification

Historically, formal verification was reserved to highly specialised teams of PhDs at places like NASA. Imandra is changing this with unprecedented automation and interfaces to ReasonML and OCaml.

Imandra has many advanced features, including first-class computable counterexamples, symbolic model checking, support for polymorphic higher-order recursive functions, automated induction, state-space decompositions and more.

Command line - Concept of a 'verify' function example
Diagram of the Imandra's FV tools output
Command line - Concept of 'describe' function
Visual concept of the Imandra SR output
Small, blue Imandra logo

Symbolic reasoning

Algorithms are all around us. From legal contracts to system designs to corporate cap tables, we're constantly reasoning about what these algorithms can or cannot do. And when we can't keep up, bad things happen.

Most real-world systems can be in a virtually infinite number of possible states. Imandra's deep symbolic reasoning can describe, analyse and explore these infinite state spaces, giving you unprecedented insight into what you're up against.

Command line - function example
Visual concept of the Imandra SR output
Imandra logo

Rule synthesis

With Imandra, you can extract logical patterns from complex structured, sequential data and synthesize them into a single, executable and auditable model. You can further convert the model into various target programming languages and English-prose, and ask in-depth questions about its behavior. The model may be used to identify anomalies in out-of-sample data and generate corrective actions to rectify any detected issues.

Rule synthesis has applications in many industries and technologies, including financial services and RPA (Robotic Process Automation). For example, as part of our partnership with Itiviti, Imandra's Rule Synthesis feature is used to migrate legacy client connectivity systems.

Imandra Core User Interfaces

Visual concept of IDE

Great technology needs great UIs. Download our VS Code plugin here. Today you'll find the usual suspects - syntax highlighting, type checking, interactive docs, etc., with the Imandra REPL available for IDE integration. Soon you'll have asynchronous verification, machine-learning powered assistance and much more, all available within VS Code.

Several examples of Imandra app UI

Reasoning as a Service®

Imandra Reasoning Machines diagram

Need to add some reasoning to your product? Just use Imandra as an API! We're already working with a select group of companies on adding automated reasoning into their product lines. Soon, we'll open this up to the developer community at large. Email us at if you have a great use case that will push our technology to the limit.

Read more

Please check out our latest article:
Constraint solving your UIs

Further technical details

Imandra Core
Symbols representing different industries that will benefit from the implementation of Imandra

If software is eating the world,
we really should take it more seriously.

When the algorithms we rely on are unsafe, unfair or inexplicable, the results can be catastrophic. Imandra is powering a new generation of tools for the rigorous design, analysis and governance of complex algorithms.

Icon close

Distributed Ledger Technology

Distributed Ledger Technology shows promise in helping to fix some of the issues facing financial markets. However, as many high-profile costly DLT bugs have shown, the code running on such systems is very difficult to get right, and must be subjected to formal verification.

In 2015, we pioneered the application of formal verification to DLT. In fact, we were the first to create a formal model of the Ethereum Virtual Machine, empowering Imandra to reason about the possible behaviours of Ethereum smart contracts. As new blockchain protocols and stacks are developed, Imandra is powering a new generation of tools helping to ensure the safety and correctness of these systems.

DLT icon Imandra Contracts Creating Safe and Fair Markets


As robots become more ubiquitous and complex, we need to understand and stay in control of what they can and cannot do. We have created an Imandra interface to Robot OS (, allowing you to leverage an existing widely popular framework and write code that you can verify for safety and correctness properties. The Imandra-ROS package is open source and is available here.

Safety-critical industries

From aerospace to railroads to self-driving cars, the systems we rely on most run on heavily regulated algorithms. Imandra's automated reasoning technology is changing how these industries create and regulate their algorithms by:

1. Providing an accessible and scalable methodology for writing and verifying specs and production-level code, and

2. Providing a scientifically sound methodology for requirements traceability, backed by Imandra's symbolic reasoning and state-space decompositions.

Imandra can be easily plugged in as a reasoning backend into many safety-critical toolchains.

Hardware manufacturing

Modern hardware designs are incredibly complex and leading designers already rely on formal verification to ensure key aspects of their correctness. Imandra's embedding in a high-performance programming language (OCaml), first-class support for computable counterexamples, seamless integration of symbolic model checking and automated and interactive theorem proving (including automated induction, lemma-based conditional rewriting and forward-chaining, decision procedures for nonlinear real arithmetic and more), make it an ideal framework for the most demanding hardware verification tasks.

Hardware icon Ripple carry adder

Government & regulators

The effective regulation of algorithms is of paramount importance. The safety of shared infrastructure and protection of private information must be checked by governments and properly enforced.

At Imandra, we continue to be vocal about the need for government regulators to leverage deep advances in automated reasoning for powerful and cost-effective algorithm governance.

Web development

Bad things happen when hackers know more about your web application than you. With GDPR (The General Data Protection Regulation)’s implementation in 2018, companies can face fines as much as 4% of their annual revenue. With Imandra, you can bring the most rigorous software development techniques to bear on web development.

Imandra supports ReasonML, an OCaml language created by Facebook for web development. We’re actively working on an interface to React, one of the most popular Javascript frameworks.


Historically, computer science departments have often had a separation between theory and practice. Often, the mathematics underlying program correctness is restricted to upper theory courses, far removed from programming practice. It's time we change that!

Imandra bridges this gap, allowing you to teach logic and formal verification in a real-world language that your students can apply immediately in a real-world setting. Imandra's automation allows students to verify deep properties of their code (and crucially, obtain counterexamples to their often false conjectures) long before they understand predicate calculus or induction!

Education icon


The computational modelling of chemical, biological and physical systems is a foundation of modern science, with much analysis happening from a stochastic or continuous perspective. The phrasing of the evolution of a system as an "algorithm" is key.

Automated reasoning can bring powerful new analyses to bear on such problems, especially when it comes to taming nontrivial discrete combinatorics of interactions. From drug discovery to CRN correctness, we'd love to help you apply Imandra to your deepest problems.

Research Icon

Legal services

Contractual agreements have a lot in common with algorithms. In fact, many contracts can be directly represented in a machine-reasonable way, making it possible to apply automated reasoning to understand their implications, edge-cases and potential exploits.

Imandra's cloud-native automated reasoning APIs are the ideal foundation for building next-generation contract analysis tools. We'd love to help you get started!

Legal icon
DLT icon


Read more

Robotics icon


Read more

Safety-critical industries icon


Read more

Hardware icon


Read more

Regulators icon

& regulators

Read more

Web development icon


Read more

Education icon


Read more

Research Icon


Read more

Legal icon

Legal services

Read more

Where to go next...

While the menu at the top of the page has the full site map, here are some resources you might find interesting:


Learn more about the science underlying Imandra

Learn more

Discord Server

Get in touch with us on Discord

Join our server


Find out the latest news on Imandra

See more


Become part of the community with our global meetups

Check it out
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