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 and 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, 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.


The use of AI in safety-critical industries requires "explainability." One of Autopilot's unique features is complete transparency in its decision-making.


The Autopilot is built with the 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 - automated analysis of algorithms' state-spaces. It is inspired by Cylindrical Algebraic Decomposition (CAD), a well-established technique for analyzing 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 critical Autopilot parameters is the ability to control with what type of liquidity you are interacting.

More technical details

Applying AI to venue trading is a thoroughly discussed topic in academic literature and a common industry approach. 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 venue's unique behaviors and, when combined, completely replicate the model's behavior.

Step 3
The resulting regions of the state-space are then transformed into a symbolic state transition graph representing 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 the 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 to download libraries and set up the daily model data download. Browse the list of supported venues on our website and select the venue for which you would like to use the Autopilot. We are currently working with many trading venues and exchanges, so please let us know if we should prioritize a specific one.

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. Please ensure that the model data feed is set up 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) venue model. 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 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