Imandra is a cloud-native
automated reasoning engine.

Imandra's groundbreaking AI helps ensure
the algorithms we rely on are safe,
explainable and fair.

Sept 21, 2018: Spotlight on an Imandra user:

In 2017 Aesthetic Integration partnered with Goldman Sachs to help deliver the SIGMA X MTF Auction Book, a new orderbook venue implementing periodic auctions. Aesthetic Integration 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.

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 proudly supports ReasonML and OCaml.

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 - function example
Diagram of the Imandra FV output
Command line - function example
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 Reasoning Studio

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.

Download VS Code plugin
Several examples of Imandra app UI

Imandra Reasoning Machines

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 contact@imandra.ai if you have a great use case that will push our technology to the limit.

Imandra API logo
Symbols representing different industries that benefit from Imandra implementation

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

Financial markets

Modern financial markets run on a multitude of complex trading systems, legal contracts, protocols, rules and regulations. The continuous stream of headlines with glitches in financial infrastructure demonstrate a dire need for a scientifically rigorous approach to designing, implementing and regulating these algorithms.

We have pioneered (patented) application of automated mathematical techniques to address this need and are working with the leading financial institutions to bring unprecedented rigour to critical financial infrastructure.

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

Robotics

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 (www.ros.org), 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

Machine Learning

Combining statistical and symbolic artificial intelligence (e.g. neural networks and automated theorem proving) is a longstanding deep problem in AI, one promising to pay enormous dividends to those who can scale it properly. We're working hard to crack this egg and make this combination a practical reality. One exciting current application: the use of Imandra's state-space decompositions to radically improve reinforcement learning.

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 Aesthetic Integration, 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 coming online 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.

Education

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

Research

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
Financial markets icon

Financial
markets

Read more

DLT icon

DLT

Read more

Robotics icon

Robotics

Read more

Safety-critical industries icon

Safety-critical
industries

Read more

Hardware icon

Hardware
manufacturing

Read more

Machine learning icon

Machine
learning

Read more

Regulators icon

Government
& regulators

Read more

Web development icon

Web
development

Read more

Education icon

Education

Read more

Research Icon

Research

Read more

Legal icon

Legal services

Read more

Community

Need help with your induction hypothesis? Or, perhaps the installer is acting up? Let's figure it out together - join our growing community on Discord.

Research

Research is the heart of what we do. This section showcases evolving technologies from our R&D engineers. From academic publications to new Imandra prototypes, join in the excitement as our new scientific results graduate into powerful products

Read More

Just give it a spin