Since its arrival on the scene in the 1980s computerised trading has evolved fast thanks to ever increasing computing power and, courtesy of mathematics and physics whizzes, more and more sophisticated trading algorithms. With the technology now able to execute trades in milliseconds or even microseconds it is not surprising the need for human traders has been largely dispensed with.
A 2015 US Commodity Futures Trading Commission study provides a powerful indication of just how widespread the use of algorithmic trading has become across global markets. The CFTC found that over the two years to October 2014 market participation via algorithmic trading systems by at least one side of the trade took place in 80% of FX futures volume. On the same basis they were present in 67% of interest rate futures volume; 62% of equity futures; 38% of agricultural futures and 47% of metals and energy future trades.
Few argue against the efficiencies – such as lower cost, reduction in human error and greater productivity – algorithms bring to trading; nor that they are firmly on track to become even more pervasive and complex in the future. But even as algorithmic trading becomes more powerful and ubiquitous, concerns are mounting that the underlying programmes have now become so staggeringly complex that traditional tools and methods used to regulate them have little or no hope of being effective. Denis Ignatovich, a former head of a trading desk at Deutsche, believes one way, perhaps the only way, to address the regulatory challenges posed by these programmes is to fight like with like: interrogate the clever mathematics underpinning them, see if it ticks all the boxes with respect to design intentions and compliance, with an equally cunning mathematical technique called formal verification. It’s not just an idea either as together with an old college buddy, Grant Passmore, a formal verification boffin himself, Ignatovich has founded Aesthetic Integration, a two year old startup that offers formal verification solutions to the financial industry.
Interviewed by Fusionwire at the recent Misys Connect Forum in London, Ignatovich says the need for a radically new approach for checking that trading algorithms comply and conform with regulatory directives and marketing materials became clear to him in the final years of his posting at Deutsche. There he led a team of 15 distributed across the world and comprising quants, developers and traders: “I was responsible for the whole process. At any point in time, our system maintained billions of dollars of exposure out on the market. Anytime you have to make a change [in your positions], which you have to do constantly because that is how you make more money, you’ve got to make sure the change you or one of your team makes is not going to blow up the bank and get everyone fired.”
He cites the fiasco at US-based market maker and trader Knight Capital in 2012 as evidence of just how badly wrong things can go with algorithmic trading. In August of that year the firm shocked by revealing it lost $440m in just 30 seconds, blaming a software bug for it inadvertently buying up billions of dollars’ worth of shares in 148 stocks on the New York exchange.
In mulling over Knight’s experience and the challenges generally posed by algorithmic trading, Ignatovich and Passmore came to realise that there is “a deep connection” between the issues that avionics and hardware manufacturers have faced when it comes to things like autopilot system safety and chip design integrity respectively and certain problems in the financial space, specifically trading algorithms. “We realised we could take mathematical solutions [formal verification techniques] developed over many years by those sectors, incorporate some very recent technical breakthroughs and then scale them up to tackle financial algorithms.”
The “deep connection” between disparate sectors such as avionics and financial trading might not seem obvious but, as Ignatovich explains, there are some fundamental similarities: “With a commercial air jet the autopilot system flies it for it for the vast majority of the time and it relies on thousands of inputs and generates thousands of outputs. Modern aircraft contain millions of lines of complex software, quite a lot of it performing functions critical to safe flight. How do you make sure that there isn’t a glitch somewhere in there that’ll cause the plane to crash at some point in time? A long time ago people realised that you cannot simply go and test for things like that because the variables to test are almost infinite in terms of the combination of speed, wind and so on. They realised mathematical techniques were needed to minimise the possibilities. That is pretty much where we are at now with financial algorithms.”
Formal verification is now relied on by several major sectors including the aviation industry. The US Federal Aviation Authority, for instance, requires precise levels of system testing and formal verification of safety-critical algorithms such as those used by air traffic control, onboard autopilots and collision avoidance. Elsewhere, the US Department of Transportation is looking to create a formal verification framework for regulating the safety of autopilot algorithms inside self-driving cars and other autonomous vehicles – work that Aesthetic’s Passmore has been involved in. Perhaps not surprisingly, NASA is one of the biggest drivers in the field, the Mars rover mission being just one of its high profile projects that benefited from formal verification.
Elsewhere, the growing complexity of computer chips has led to hardware manufacturers adopting formal verification as a standard tool for ensuring the integrity of their designs. A notable trigger for its application by the sector was the experience of Intel in 1994 when it was forced to issue a recall of its then new Pentium processor due to a design flaw. It proved an expensive bug, with Intel forced to fork out $450m on the recall. At the same time Intel’s competitor AMD eyed the fiasco with trepidation and moved fast to make sure it’s upcoming K5 processor was not going to have similar flaws. It hired a team of mathematicians to create a mathematical version of the design of the microprocessor and verify its integrity before launch.
To enable the application of formal verification in the financial industry Ignatovich and Passmore have developed Imandra, a platform that houses three formal verification solutions. The first, Imandra Contracts, is a tool for analysing blockchain-backed smart contracts and enables users to identify and fix anomalies in financial algorithms. The second, Imandra Markets, offers a verification solution for client-facing algorithm specifications, simplifying the designing, testing and compliance processes for trading systems. Imandra Venues, meanwhile, is focused on analysing the regulatory properties of trading venues, establishing a new standard for the stability and transparency of exchanges and dark pools, an alternative trading system mostly used by institutional investors for block trades involving a large number of securities.
Imandra’s basic proposition to financial firms and regulators is that any trading system, whether it be an exchange or dark pool matching engine, or firms’ trading algorithms, is essentially a computer programme and once this is converted into language supported by Imandra, it can be interrogated at the press of a button. “Without knowing anything about formal verification you are armed with this engine that allows you to reason about what can possibly go wrong,” says Ignatovich. “And to make that happen we have had to leverage many recent breakthroughs in formal verification that only a handful of people in the world appreciate because it’s just not in text books right now. And on top of that, my co-founder [Passmore], who has got a PhD in this area, is developing other techniques that make it very easy for someone that doesn’t have any background in formal verification to start using our engine out of the bag.”
Dark pools are a prime example of how Imandra could help eradicate errors and shine a light on murky practices. They are intended to help asset managers trade large blocks of shares in private without moving the market against them but there is concern the pools have been infiltrated by high-frequency algorithmic traders who rig the market against customers. In February this year US regulators fined Barclays and Credit Suisse $154m in total for misleading investors about how they operated their dark pools, with Barclays accused of misrepresenting the level of aggressive high frequency trading activity in its dark pool to other clients. In July Deutsche Bank and UBS revealed their dark pools were also under investigation by the US Attorney General’s office.
“Imagine you are running a dark pool in the US and suddenly the regulator turns up and demands your data for the last five years. Now, you’ve never seen the source code. In fact, that source code maybe outsourced – pardon the pun – somewhere. But you need to follow this regulatory process to make sure that you’re not going get sued. You have umpteen word documents or PDFs describing what the algorithm is supposed to do. Why don’t we take that ambiguity, all that noise, paperwork and translate it into a mathematically precise specification of what the system is supposed to do? Once we do that, then we’re going have a whole bunch of questions to throw at it. For instance, is it possible for someone to jump the queue in the best bid and offer by submitting a sub-penny order? Will the system allow that? It’s illegal in the US. There are many different regulations and all the questions they pose can be encoded in a language Imandra understands and can interrogate for compliance and behaviour. With just the push of a button, you can generate compliance reports, send that evidence out to a regulator, a regulator can process it. That’s exactly the same way avionics works.
Aesthetics, which has raised £1m in seed funding so far, is certainly making waves with its Imandra proposition. Last year it won the first UBS Future of Finance Challenge, coming top out of 620 companies from 52 countries. It also won a Futures Industry Association Innovator Award at the FIA Expo 2015 in Chicago. Not surprising then that the company’s platform is being seriously looked over several leading institutions including UBS. “I think our key selling point to them is that it’s a way of making more money, either by it creating revenue opportunities or cutting costs by getting it right first time using the purity of mathematics not fuzzy prose.
Regulators struggling to keep up with ever more cunning algorithmic concoctions are also eyeing Aesthetic’s proposition, US Securities and Exchange commission among them. “We have talked to the SEC but we have many other such dialogues which I cannot go into at present. Generally speaking, I think there is this natural hesitation among regulators towards doing something drastic that hasn’t been done before. And that is perfectly understandable, especially considering the changes the industry is already going through. It’s good for regulators to be conservative in that sense.
“But I think interest and confidence in the Imandra products will grow as they become more widely tested and trialled. Our focus is to encourage institutions to adopt them first. No one wants to spend money on compliance for algorithms, right? If we as an industry can come together without all of the typical red tape, create an app store where we can share information about how algorithms are supposed to work with each other in a way that’s commercial, that can only be to everyone’s benefit.”