Imandra Markets for Systems and Connectivity

Financial markets run on many thousands of interconnected and complex systems. Imandra's automated reasoning technology ensures they're designed correctly, rigorously tested and calibrated to achieve maximum financial performance. We have two specifically tailored products for systems and their connectivity.

Systems P e r f o r m a n c e T e s t i n g Connectivity T e s t i n g Im a n d r a ' s A I au t o m a t i c a l l y c o n s t r u c t s t e s t c a s e s t o g i v e y o u u n p r e c e d e n t e d c ov e r a g e o f t h e e x p e c t e d b e h a v i o r . D e s i g n Mo s t s y s t e m s ' b u s i n e s s l o g i c i s h i g h l y n o n - t r i v i a l ; I m a n d r a s h i n e s a l i g h t o n t h e n o n - t r i v i a l k n o c k - o n e f f e c t s . P e r f o r m a n c e Im a n d r a h e l p s y o u f i n e - t u n e y o u r s y s t e m ' s d e c i s i o n m a k i n g a n d c l i e n t u s a g e t o a c h i e v e m a x i m a l f i n a n c i a l p e r f o r m a n c e . Im a n d r a c u t s d o w n mo n t h s o f m a n u a l e f f o r t a n d d e l i v e r s u n p r e c e d e n t e d au t o m a t i o n a n d r i g o r i n c o n n e c t i v i t y t e s t i n g . Im a n d r a a n a l y z e s t h e t r a f f i c w i t h y o u r c l i e n t s / c o u n t e r p a r t s t o u n d e r s t a n d h o w t h e s y s t e m i s u s e d a n d w h a t s h o u l d b e t e s t e d . E x c l u s i v e p a r t n e r s h i p w i t h I T IV I T I L e a r n m o r e L e a rn m o r e L e a rn m o r e

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