The IEX Auction: Pursuing Greater Clarity

Today, the behaviour of most complex financial systems such as stock exchanges, alternative trading systems (dark pools) and smart order routers are specified in long handwritten PDF documents. They are often riddled with ambiguity, missing information and even contradictions!

Here at Aesthetic Integration we care a lot about clear and transparent specifications. In financial markets, ambiguity can lead to unpredictable and potentially unfair behaviour. To this end, we have developed Imandra Markets, a tool suite which allows trading venues to encode their specifications in a precise manner and to rigorously analyse their possible behaviours. Imandra then connects these precise specifications with the production system through the automatic generation of high-coverage test suites and high-performance monitoring and auditing tools. This precise specification can then be distributed to clients, allowing them to explore various edge cases not covered by the examples in the current specification.

Imandra offers rigorous analysis, high-coverage test generation and online/post-trade monitoring

IEX is the newest addition to the growing list of US stock exchanges. After gaining exposure from Michael Lewis’s “Flash Boys”, IEX became an official exchange in 2016, and in October 2017 they received SEC approval to become a listing venue. They are expected to begin listing companies in early 2018. In anticipation of this, IEX have designed an auction process for conducting opening and closing auctions (as well as halt, volatility and IPO auctions).

IEX promote themselves as “a fair, simple, and transparent stock exchange” and we believe that the launch of their auction process offers a chance to raise the bar for transparency in the financial industry.

Unfortunately, IEX is currently following the standard practice of providing a long, ambiguous textual description of their auction process. At the time of writing, this document consisted of 34 pages, mainly devoted to long sections of prose describing how various aspects of the auction logic work. At the end of the document IEX provide 12 explicit examples of expected auction behaviour. The problem is that these examples do not, and can not, cover all the different complex behaviours of the system. In particular, all the examples focus on the “common case”, they do not, for example, cover cases where the short sale circuit breaker is in effect, or where the NBBO is one or zero-sided, etc.

To be clear, IEX’s auction specification is well written and very detailed. It is certainly better than similar offerings from many of IEX’s competitors. Our objection is not to the quality of IEX’s specification in particular, but to the very nature of how such specifications are presented.

To illustrate the power of formal specifications, and to better understand the many nuances of the IEX auction logic, we have built a simple model of IEX’s auction logic using the Imandra Modelling Language (IML), a programming language based on OCaml with tools allowing users to analyse and verify their code. In the rest of this blog we provide a brief overview of this model and we show how Imandra can be used to analyse its behaviour.

To give an idea of the amount of work involved in building such a model: everything described here was developed by a single Research Intern over the course of approximately 6 weeks, starting with no understanding of the IEX auction process nor any experience using the tools in Imandra Markets.

DISCLAIMER: This model was not developed in collaboration with IEX. The information presented here is based on of our understanding of the information disclosed in IEX’s public documentation and may not reflect the intended meaning of that documentation, or the actual behaviour of IEX. In places we discovered that certain behaviours were ambiguous or unspecified. In these cases we made a choice for how the system should behave. Again, this may not reflect the actual or intended behaviour of the IEX auction logic. Any claims made here apply to the model that we have developed, and not to IEX’s production system. Any misunderstandings or mistakes are entirely ours.

A Primer on IEX Auctions

At a high level, IEX auctions work as they would on any exchange: orders are collected for auction, the price which maximises the volume traded is calculated, and orders are selected to trade based on some notion of priority.

In the case of IEX auctions, orders come from one of two sources. Either from the Continuous Book, the collection of orders available for continuous trading at the time of the auction match, or from the Auction Book, the collection of orders queued prior to the auction match, such as On-Open or On-Close orders. These two books are combined (except for certain “auction ineligible” orders) to form the Order Book, which is used to calculate the clearing price and to match orders.

(Note that in the case of halt/volatility/IPO auctions trading will be halted before the auction match and hence the Continuous Book will be empty.)

Order types

IEX supports three classes of order types: limit, market and pegged orders. The auction match can include all three of these order types (although only the closing auction can include pegged orders). Market orders do not rest on the Continuous Book and pegged orders do not rest on the Auction Book. Limit orders can rest on both books. These order types are described in more detail on IEX’s website.

Non-displayed orders

One interesting feature of the IEX auction process is the way that it treats non-displayed orders. The specification states:

For the Opening/Closing Auction, non-displayed buy (sell) orders on the Continuous Book with a resting price within the Reference Price Range will be priced at the Protected NBB (NBO) for the purpose of determining the clearing price, but will be ranked and eligible for execution in the Opening/Closing Auction match at the order’s resting price.

This means that the auction process can be decomposed into two stages:

1. Price determination: in this stage non-displayed orders (including midpoint peg orders) on the Continuous Book which are currently resting within the spread will be priced at the NBBO. We then calculate the price which maximises the number of shares traded.
2. Order matching: with the clearing price fixed, we now match orders based on price/display/time priority (full details given in the auction specification). In this stage, non-displayed orders are priced at their original resting price.

This special treatment of non-displayed orders results in some interesting behaviour, as we’ll see later.

Building Better Specifications

As discussed earlier, specifications for all sorts of complex systems, such as modern stock exchanges, are currently presented in long handwritten PDF documents riddled with ambiguities and contradictions. Often they leave readers unsure of how the system will behave under certain conditions.

At Aesthetic Integration we’re pioneering an alternative, mathematically rigorous approach. Rather than providing textual descriptions of a system, we propose that venues provide executable specifications that allow clients to experiment with various behaviours of the system. Armed with a precise specification, we can apply deep advances in the field of formal verification, which are already widely used in fields such as avionics and microprocessor design. These techniques then allow venue operators to analyse their matching logic design with respect to statements made in marketing material and disclosures to regulators, and to then use powerful formal verification techniques to derive high-coverage test suites and live market monitors to ensure their production systems behave in line with the verified design. For example, we have previously used these tools to analyse whether a venue’s design would ever allow sub-penny prices to be displayed (prohibited by Regulation NMS). For further information on our vision for the future of financial markets see our comment letters submitted to the CFTC, the SEC and the SEC again, with the final example also regarding IEX. You can also learn more about our approach both from our coverage in the media and from our academic publications.

Note that this is not the same as suggesting that companies release the source code for their matching engines/trading systems, which contain valuable intellectual property. Rather, the formal model is an abstracted, though fully executable and precise, specification of the essential components of the matching logic. Here are two key differences:

1. Efficiency: much of the value in the source code for an exchange’s matching engine lies in the fact that this code has been carefully optimised to process events at an incredibly high rate (on the order of microseconds per event). In contrast, the specification need not provide such a high level of performance and so this IP will not be leaked.
2. Abstraction: proprietary parts of the specification can still be left abstract. For example, IEX supports a feature known as the “crumbling quote signal” which predicts if the NBBO is about to change and may prevent certain pegged orders from trading. In our model this signal is simply a flag, it is either on or off, the model does not encode how this signal is calculated. This means that the way this signal is calculated can be kept proprietary while still allowing clients to investigate how the system behaves when the signal is active.

It is then possible to use automated tools to generate high coverage test suites which link such a specification to the production system. This process can also help to identify bugs in the production system by looking for differences from the model. Identifying bugs before they become a problem can save venue operators from significant fines.

An Imandra Model

To illustrate how our approach works, we have developed a simple model of IEX’s auction logic using our Imandra Markets framework. This involves building a precise encoding of the specification using the Imandra Modelling Language (IML), a subset of the OCaml programming language.

As an example of what this looks like, consider the top-level function in the model. Below, we show (a simplified version of) this function:

This function describes the main auction process, and can be read as follows:

1. Try to calculate the clearing price:
   match calc_clearing_price(buys, sells, mdata) with
2. If there is no crossing interest (the result of step 1 is None) then we do not conduct an auction (the overall result is None). Otherwise, we compute a list of fills which result from the auction match. To do this we filter any orders which are not eligible for the auction, sort the remaining orders into priority order and then conduct the auction match:
   auction_loop(buys, sells)

This code makes explicit the fact that the clearing price is calculated in a separate step to the actual order matching, as discussed above.

The full source code for the model can be found on GitHub. Since IML is a subset of OCaml, all you need to experiment with the code is an OCaml interpreter/compiler. The source also includes several examples which demonstrate interesting and (potentially) unexpected behaviours of the logic.

Probing the Model

Now that we have a precise model of the IEX auction logic we can use it to test our intuitions about how the auction process works. For example, the auction is supposedly designed to maximise the total volume traded, and so one might expect that the more orders that participate in the auction match, the more volume will trade in the auction. We can use Imandra to test this assumption.

Let’s start by stating precisely what we expect to be true about the system:

In the above we are conjecturing a new theorem which states that: for any order, any collection of buys and sells, and any market data — assuming all the orders have a strictly positive quantity (i.e. the inputs are valid) — then if we conduct an auction with the original set of buys and sells, and we conduct an auction with the extra order added to the Order Book, then the volume traded in the first auction should be less than or equal to the volume traded in the second auction. That is, adding an extra order into the auction does not reduce the volume traded.

Imandra comes with many tools which allow us to test hypotheses, such as the above, and hopefully either refute them (find a counterexample) or prove them correct. One such tool is Imandra’s dash command, which checks the property on a large collection of test cases generated using a symbolic Monte Carlo sampling method. Using the dash command to test this goal, we discover that it is in fact not true!

Consider the following example, the NBB is $10.00 and the NBO is $10.04, and the order book for the closing auction contains three orders:

• A midpoint peg order to buy 500 shares at $10.02
• A limit-on-close order to buy 100 shares at $10.01
• A limit-on-close order to sell 1000 shares at $10.01

The auction process proceeds as shown below:

The original order book is shown in step 1. Because the midpoint peg is a non-displayed order resting inside the spread, it is priced at the NBB for the price determination phase. This gives us the order book shown in step 2. For this book, volume is maximised at $10.01 where O2 and O3 can trade 100 shares. Therefore the clearing price is determined to be $10.01. We then put the midpoint peg back where it was (shown in step 3) and conduct the actual auction match which results in O1 trading with O3 for 500 shares and O2 trading with O3 for 100 shares, giving a total volume of 600 shares.

If we now add a limit-on-close order to sell 200 shares at $10.00 then the auction instead proceeds like so:

The new order book is shown in step 1. Again, the midpoint peg is priced at the NBB for the price determination phase. This gives us the order book shown in step 2. For this book, volume is now maximised at $10.00 where O4 can trade 200 shares with O1 and O2 (only 100 shares will trade at $10.01). Therefore the clearing price is determined to be $10.00. We then put the midpoint peg back where it was (shown in step 3) and conduct the actual auction match. Since O3 is not eligible to trade at $10.00, this results in O1 trading 200 shares with O4. The total volume traded is 200 shares, less than the 600 we had before.

So, using Imandra we have found that our intuitions about the auction process were wrong and have discovered some (potentially) counter-intuitive behaviour. However, we might still be interested in knowing whether this is the only situation where our intuition fails or whether there are other counterexamples due to different, distinct, behaviours.

If we investigate further we discover that this is in fact not the only source of counterexamples! We can find other situations where this intuition fails to hold. Another situation where this property fails to hold relates to the way that IEX handles short sale orders while the short sale circuit breaker is active (in order to comply with Rule 201 of Regulation SHO).

As we use Imandra’s tools to find counterexamples we can update our goal to try and exclude these counterexamples. Eventually we reach a goal where we can no longer find any counterexamples:

This is the same as the previous goal, except that we now only consider cases where the new order does not change the clearing price and where IEX’s short sale order handling (for Reg. SHO) is not triggered during the auction. Apart from these two extra assumptions the goal is unchanged.

We can now use Imandra’s theorem proving tools to actually go ahead and prove that this theorem is always true. This is a much stronger guarantee than simply testing because the tests can never cover all the possible states of the system. Only using these theorem proving tools can we know that this property will always hold, for all inputs.

More details about this proof, including the definitions of the predicates and supporting lemmas, as well as proofs about other parts of the model, such as order priority, are available on GitHub. If you want to check the proofs and experiment for yourself then you’ll need access to Imandra Markets. Public access to our tools should be launching in the near future, for now you can register on our website to be notified as soon as they go live!

Conclusions

In this blog we’ve shown how tools and techniques from formal verification and artificial intelligence can allow us to encode precise specifications, to explore the behaviour of these specifications and to verify logical properties of the system in question.

We believe that these techniques, already ubiquitous in safety-critical fields such as avionics, can provide huge benefits to all participants in financial markets:

• Venue operators can leverage these tools to rigorously analyse their designs, generate high-coverage test suites and production system monitors and discover flaws before they become a problem — potentially avoiding huge fines.
• Clients can better understand the complex behaviour of these systems, giving them greater confidence when trading on the venue. Rather than studying an ambiguous text document to try and decipher how different orders types operate, how various prices are calculated, or what possible messages they might receive, clients can instead use the formal model to pose queries, test their intuitions and simulate their trading strategies.
• Regulators can verify that these systems adhere to various regulations. For example checking that venues do not allow sub-penny pricing, or do not execute short sale orders at or below the NBB while the short sale circuit breaker is in effect.

Full details of the model, including the source code, various Imandra proofs and several examples of interesting behaviour, can be found on GitHub.

To learn more about Aesthetic Integration and Imandra Markets visit our website.

Who are we? — Aesthetic Integration (AI) is a financial technology startup based in the City of London. Created by leading innovators in software safety, trading system design and risk management, AI’s patent-pending Imandra formal verification technology is revolutionising the safety, stability and transparency of global financial markets.

About the author — this article and the model described here were produced by Ian Orton, a research intern at Aesthetic Integration. Ian is currently studying for a PhD in homotopy type theory at the University of Cambridge.