Imandra Markets: Autopilot®

Venue-specific Reinforcement Learning (RL) trading agents trained on precise and faithful venue models and their order flow. Delivered as a high-performance library and may be seamlessly integrated into your SOR and other trading systems. Recalibrated and updated daily. Built with breakthrough AI for reasoning about infinite state-spaces of venue logic - including order types, trading modes and messaging protocols.


4X increased access to liquidity due to optimally calibrated parameters (e.g. order size, timing, aggressiveness), taking into account the full venue logic and flow statistics.


A logically precise model of the venue, all of its order types and state transitions is infused into the Autopilot agent.


The more a trading participant trades on a venue, the more information they have on the underlying parameters. We level the playing field without compromising privacy.


The Autopilot is shipped as a library supporting major programming languages. We spent considerable time to ensure you can seamlessly integrate it into your tech stack.


Use of AI in safety-critical industries requires ‘explainability’. One of Autopilot’s unique features is complete transparency into its decision making.


The Autopilot is built with knowledge of trading protocols and their nuanced implementation by the venues.

Powered by breakthrough AI for algorithm analysis

Imandra is a cloud-native automated reasoning engine for the analysis of algorithms and data. One of its core features is Region Decomposition - an automated analysis of algorithms' state-spaces. It is inspired by Cylindrical Algebraic Decomposition (CAD), a well established technique for analysis of real-valued functions in mathematics. Region Decomposition "lifts" CAD to algorithms at large. We have already successfully applied Region Decomposition to testing complex trading systems and interfaces.

As applied to venue trading strategy development, Region Decomposition is a fundamental scientific breakthrough that allows us to model venues' entire state-spaces as state transition graphs.

Imandra Markets: Autopilot - Agent

Seamless integration, deployment and monitoring

The Autopilot libraries come in the form of libraries targeting all of the major programming languages. Note that we update the model data daily and make it available via several market data providers.

Imandra Markets: Autopilot - Integration

Strategy Interface

The Autopilot libraries come in the form of libraries targeting all of the major programming languages. Note that we update the model data daily and make it available via several market data providers.


The Autopilot has a rich interface for expressing your trading preferences and objectives.

Market Conditions

The calibrated state transitions depend on several statistical factors including the current market conditions.

Toxicity Analysis

One of the key Autopilot parameters is the ability to control the type of liquidity you are interacting with.

More technical details

Applying AI to venue trading is a well-versed topic in academic literature and is a common approach in the industry. What separates our approach is that recent breakthroughs in automated reasoning allow us to precisely model the logical state transitions (of which there are virtually infinitely many) of a venue and use them to develop bespoke strategies.

Imandra Markets: Autopilot - Details

Step 1
During the first step, we construct an Imandra model of the venue and ensure that we can co-simulate it with production data to achieve at least 99% accuracy. We have developed a highly efficient methodology for modeling venues as infinite state machines. For a typical venue, this step would require 2-3 weeks of a single engineer’s time.

Step 2
Next, we will use Imandra to analyze the formal model and compress its state-space (which is virtually infinite) into a finite number of symbolic regions. These regions represent all of the unique behaviors of the venue and when combined, completely replicate behavior of the model.

Step 3
The resulting regions of the state-space are then transformed into a symbolic state transition graph which represents all of the possible ways that a venue can operate along with the decisions that an Autopilot agent can make. After analyzing the data, we further augment the state transition graph with transition probabilities and expected rewards.

Step 4
In the last step, we combine the precise state-transition model with transition probabilities and market state classifier into a single RL agent. The model parameters are recalibrated daily and the logical state transitions are changed to reflect any system upgrades on the venue side. The agent comes in a form of a library so you can easily integrate it into your tech stack.

For traders

Step 1:
Subscribe to the venue
The first step is for you to download libraries and setup the daily model data download. Browse the list of supported venues on our website and select the venue you would like to use the Autopilot for. We are currently working with many trading venues and exchanges, so please let us know if there is a specific ones we should prioritize.

Step 2:
Install Autopilot library
The next step is to integrate the Autopilot library into your Smart Order Router (or any other system that makes routing decisions). The library is available in a number of programming languages with extensive instructions. Pleasure ensure that the model data feed is setup correctly and automatically updates the files used by Autopilot.

Step 3:
Happy trading!
After the installation is complete and is correct (documentation has instructions on this), you are all ready to go. Make sure to check out the monitoring tools to gain insight into the Autopilot decision making process.

For venues

Step 1:
Model the venue
The first step is to create a formal (mathematically precise) model of the venue. We will work with you to encode your business logic, connectivity specification and other relevant documents into a model Imandra can reason about and that we can reconcile with the production data.

Step 2:
Reconcile model with data
Once we have encoded the full operational model of the business logic, we will reconcile it with your production data to achieve at least 99% alignment. This will ensure us that there are no mistakes and that we are correctly accounting for the state transitions. If there are deviations, we will work with you to eliminate them.

Step 3:
Setup a calibration process
Once we have a formal model of the venue and can systematically reconcile it (by performing co-simulation) against the production data, we will work with you to automate this process whereby Imandra recalibrate the data daily and provides your trading participants with up-to-date precise information on how to trade on your platform.

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