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.
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.
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…
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
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.
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.
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.
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.
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.
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.