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 the programming 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
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.