Feature: Modelling dark pools with maths

Formal verification might be the testing tool that transforms the way financial firms trade in dark pools, say the mathematicians of Aesthetic Integration

Dark pool trading venues and other highly complex markets are worrying regulators. How can the firms that run those venues calculate where things might start to go wrong? What might prompt those markets to mis-behave? A rising star among fintech firms is Aesthetic Integration, a firm based in London, which believes it has the answer to that challenge in the discipline of formal verification.


Grant Passmore, Aesthetic Integration

The genesis of the company was at the University of Texas, where its two founders were room-mates 10 years ago. Denis Ignatovich went on to become a Wall Street and then moved to London where he headed the equity risk trading desk at Deutsche Bank. Grant Passmore, the other partner in Aesthetic Integration, went on to academia; ultimately teaching at Cambridge University.

Having found themselves both working in the UK, they decided to work together on a project to bring formal verification to finance. In 2014, they founded Aesthetic Integration, whose core product — the Imandra tool for testing financial systems – is based on formal verification.

Formal verification is, said Ignatovich, “reasoning in an automated way”.  Sitting at the crossing point of artificial intelligence, mathematics and computer science, formal verification differs from machine learning or artificial intelligence which, based on its most commonly-used definition, is based on statistical analysis and boils down to a process of working out the likelihood of something happening.

By contrast, said Ignatovich: “Formal verification can tell you if the design of your dark pool is consistent and compliant; whether or not there are corner cases where the logic may lead to violation of regulatory principles.”

“We are not looking at statistics to estimate likelihood of a violation occurring,” he says. Imandra analyses all possible behaviors of the design to assess whether a certain event is possible or not.”

Processor flaws

One of earliest industrial applications of formal verification is following the 1994 recall by Intel after a design flaw was discovered in its Pentium processors — the FDIV bug. The bug was expensive – Intel spent around $450 million on the recall. At the time, Intel’s major competitor, AMD, wanted to make sure that a similar flaw did not exist in their new K5 processor. So they it a team of mathematicians, specialising in formal verification, to prove that their processor could not experience a similar issue.

Denis Ignatovich, Aesthetic Integration

Denis Ignatovich, Aesthetic Integration

So, how does formal verification work in a financial markets context? The central problem of testing a dark pool, for example, is that the number of possible configurations of trades and outcomes is infinite. Formal verification can be used to analyse those infinite outcomes and break them down into a manageable number of regions – perhaps thousands  – where in each case the behaviour of the exchange is similar.

Ultimately, said Ignatovich, the formal verification process delivers the exchange operator to the place where he can symbolically describe the various types of behaviours, for example.

But why is a methodology that has for years been used extensively in the semi-conductor manufacturing and avionics so late to financial markets? The answer, suggests Grant Passmore is that, until recently, it was very difficult to apply formal verification to financial trading systems.

“Although issues facing complex systems in finance and in computer hardware, for example, are very similar, the mathematics required is very different,” he said. “Thanks to recent breakthroughs, we can finally apply formal verification to financial algorithms”.

At Deutsche Bank, Ignatovich’s most recent job had been the management of the risk trading desk responsible for centralising the dealer function of the bank’s cash equities business. Trading desks such as Deutsche Bank’s are representative of the investment banking industry’s drive over recent years to automate various risk management, trading and pricing functions.

SEC fines UBS

But what has changed the stakes has been the growing concern among regulators that the automation of trading desks and the creation of entirely new automatic markets spiralled out of the control of their managers.

Take, for example, the SEC’s fine of $14.4 million last year for UBS over the way the bank operated its dark pool, to allow hundreds of millions of illegal trades — trades banned because they were priced in increments of less than one cent.

For Ignatovich, that judgement illustrates the financial services industry’s ongoing struggles with the staggering (and growing) complexity of trading algorithms.  “It’s the worst-kept secret in finance,” he said, “As an industry, until now we had no method of precisely describing how systems should behave. Algorithms should be described using mathematics, not English prose.”

In a white paper published by their firm, Ignatovich and Passmore claim they can show how the formal verification technology in their product, Imandra, can automatically prove principles of fairness and best execution of venue designs, so that venue operators can institute rigorous governance processes around their most critical systems.

In particular, they say, Imandra can automatically detect and test for key recent issues raised by the SEC, and they used the case of UBS’s dark pool to illustrate their point. And it can be applied to a wide range of financial algorithms, including routing systems and smart contracts.

There is another reason that formal verification has become more applicable to financial markets now, says Ignatovich. Given the proliferation of trading systems within banks, and across the buy and sell divide, many developers, compliance officers, traders and risk managers are having to spend more and more time trying to understand how each other’s systems operate.

This proliferation is, in turn, partly a response to automation and the more complex requirements of the trading systems operated not just by investment banks, but also by their buy-side clients and exchanges.

The end-game may be inevitable. In the not too distant future, the trading systems currently operating within specific asset classes will be merged into one, turning investment banks into huge automated risk trading systems covering every asset class.

Getting there, however, is going to require a better way of modelling the underlying structures. “In the world of interconnected systems, lack of precise documentation is expensive for everyone,” said Ignatovich.

But even if formal verification holds the key to establishing that such systems could work without flaws, even as they grow more complex, it will be the regulators – rightly perhaps – that have to be convinced.

Last November the CFTC released draft proposals for the regulation of automated trading of derivatives contracts. These included the proposal that regulators should have access to financial firms’ source codes for algorithmic trading, so that in the event of a market disruption officials could check back to see if the cause lay with a particular firm. It is an idea that runs counter to what technologists and regulators should be trying to achieve, the Aesthetic Integration partners argue. Automated markets should be tested before they go wrong, not afterwards.

Additional information: see our video interview with Grant Passmore here, in which he explains in detail the maths developments behind formal verification. See a case study on the UBS dark pool produced by Aesthetic Integration here. And see the Aesthetic Integration white paper on formal verification here.


Tweet about this on TwitterEmail this to someoneShare on LinkedIn

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>