AI for designing, auditing and calibrating complex trading systems

Imandra Markets

Imandra Markets is a suite of AI-powered technologies and services for designing, implementing and analysing financial trading venues. It leverages the latest advances in automated reasoning and machine learning to usher in new era of client experience and governance in financial markets.

Data + Logic = Actionable Intelligence

Financial markets are overwhelmed with data. Unfortunately most of it is noise.

What separates signal from distraction is one's ability to leverage information to affect change: a change that prevents a "glitch" or regulatory exposure, or a change that makes clear recommendations to your clients so as to improve their outcomes. With Imandra Markets, we leverage deep advances in AI to extract these insights from your venue automatically. Insights leading to actions. This is what we mean by actionable intelligence.

Venues are the cornerstones of financial markets that generate a lot of data and operate very complex systems. Until now, the data and the complexity have been entirely disjoint.

Ultimately, our objective is two-fold:

Empower you to understand every single decision that your venue makes

Empower your clients to take full advantage of your system's capabilities

Machine Reasonable Design

What do we need to create actionable intelligence?

The first step is to give precise meaning to the data your system produces by providing the logical context. A typical venue operates a myriad of complex rules - which we describe in a way that's susceptible to reasoning by machines. We will translate your English-prose documentation into a machine reasonable model - a specification format that's executable (e.g. like any computer program) and susceptible to automated reasoning (automatically translated to mathematical logic).

When you combine system data with the logic prescribed in this format, you get unprecedented insight into the operation of the venue. This insight empowers you to drive greater client participation, increase efficiency and create unprecedented governance.

Read more
Conceptual diagram of Imandra technology powering business, technology and compliance
Conceptual diagram of Imandra

Actionable data for intelligent conversations with your clients.

We combine the production trading data with Machine Reasonable Design to create actionable recommendations.

Here are some of the answers this data provides:
● What is the liquidity profile of the venue?
● How does client's order sizes affect their ability to execute?
● What is the client's average order rank in the book?
● When the client is outranked, which factors cause this?
● And much more…

This data is updated every day and may be exported in a variety of formats including self-contained reports, CSV files, or via an API.

Screens os Imandra Auditor Application


Imandra Markets Auditor is what governance of complex trading systems should look like.

Here are just some of the features our clients rely on daily basis:
Consolidation of internal log data, client flow, external market sources and simulation data
● Single consolidated timeline of all events occurring within the venue
● Full reconstruction of the order book state with individual state transitions
● Detailed description of expected vs. actual behavior of the system
● Automated alerting for rich sets of conditions
● Powerful search interfaces for identifying individual issues or whole groups of events meeting your criteria
● Much more…

Conceptual diagram of Imandra technology


In banking technology, ability to make changes is the new alpha. Imandra Markets is Model-Based Development as it's meant to be.
The precise model at the heart of Imandra Markets connects all of the stakeholders (business, developers and compliance) over precise, executable and machine reasonable design.

Here's how you cut out the noise:
● Translate business requirements and marketing statements into verifiable model properties
● Ensure the model is correct with respect to those properties
● Use the design to automatically test the implementation
● Use the design to audit production data once the system has gone live



Mission to Mars


Formal executable specification


Model verification

Implementation testing


Auditor (historical)

Auditor (intraday)


Logic Insight

Client Assist

How does it work?

Imandra Core + Venue Toolbox

The underlying technology behind Imandra Markets is the Imandra Core reasoning engine. We've spent the last 5 years developing this technology and working with our industrial partners to ensure it can tackle even the most complex real-world systems. Moreover, we've developed a set of techniques and libraries on top of Imandra Core for quickly translating traditional, English-prose design documents into mathematically precise models.

Illustration of Imandra toolset

Formal verification

Formal verification offers a powerful alternative to traditional "testing" by using computers to reason about infinitely many possible system behaviors.

For example, a typical property one may wish to verify about a venue is that it will never generate a fill price that is outside the primary market BBO. If you were to use traditional testing approaches, then you'd write up a few examples and prove that the design does not violate the property for those specific cases. But, of course, you would have left out the infinitely many other possible events. Formal verification allows you to verify that a negative price will never be generated for all possible inputs into the system.

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

Read more
Illustration of concept of Formal verification
Illustration of an automatic testing


No doubt you know that trading systems should be "tested thoroughly" prior to releases. Just as likely, you've never heard anyone define what "tested thoroughly" means.

Until now.

One of the core features of Imandra is Region Decomposition - a novel technique powered by symbolic reasoning for automatically identifying system edge cases. For the first time ever, you know precisely what must be tested and how. With Region Decomposition, we can ensure that the production system is aligned with the specification much faster than through traditional financial IT QA processes.

Read more
Illustration of an automatic testing


Co-simulation refers to running the executable specification on the production data and analyzing the results to ensure they match production data. This means that every single decision that a system makes is reconciled against the verified specification. Any discrepancy is immediately highlighted to the venue operator with a full logic trace visually presented in the Auditor web platform.

Illustration of co-simulation.

Symbolic reasoning
and machine learning

When an order is sent to a venue, the response is a one-dimensional Yes/No. Either it is filled in one or a series of fills, or the order outright expires unfilled. Order size, price, resting time and other parameters (e.g. MAQ) dictate the probability of the fill, yet are set arbitrarily by the developers of the client trading systems. Misalignment of these parameters among the participants limits the crossing opportunities.

Every venue design has a particular "logical signature" resulting in a unique and non-trivial liquidity profile. We generate this profile by using symbolic reasoning to compute the what-ifs for each order sent to the venue (through its lifecycle), and then applying machine learning to create a consolidated conditional probability distribution which may be integrated into client trading systems directly or via a recommendation engine.

Illustration of symbolic reasoning combined with machine learning.

We'd love to show you a demo

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