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.
NEW! 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.
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.
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
Formal verification, constraint solving, region decomposition
Top Imandra Core features
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.
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.
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
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.
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 email@example.com
if you have a great use case that will push our technology to the limit.
If software is eating the world, we really should take it more
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.
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
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.
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
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
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.
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.
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
Imandra bridges this gap, allowing you to teach logic and formal verification in a
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!
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.
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!
Government & regulators
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: