With Denis Ignatovich and Grant Passmore, Co-Founders of Aesthetic Integration
We were college roommates at UT Austin and both ended up in the UK around the time of the Knight Capital and BATS IPO incidents. At that time, Grant was doing research in the field of formal verification related to safety of autopilot algorithms at the University of Cambridge and Denis was running a trading desk at DB London. It was then we realised a deep connection between the issues of complex algorithms plaguing finance and those faced by other safety-critical industries like avionics.
The field of formal verification (FV), an intersection of mathematics, computer science and artificial intelligence, is dedicated to analysing the behaviour of complex algorithms to make sure they are designed and implemented correctly. FV is already relied upon to manage and regulate complex algorithms in safety-critical industries like avionics and hardware design. It’s difficult to image modern life without FV. FV is fundamentally different from the simulation of algorithms. With simulation, one only ever executes an algorithm within a finite number of scenarios. But typical safety-critical systems (e.g., the autopilot algorithm of a commercial jet) can be in an infinite (or virtually infinite) number of scenarios. With FV, we can analyse every possible behaviour of an algorithm to help understand what can possibly go wrong before the algorithm is deployed.
FV is now within financial markets for the first time. We have been working with one of our clients, a tier one investment bank, to create a formal model of their European dark pool, and use our work to verify fairness properties of the matching engine (such as those at the centre of recent regulatory fines in the US). After mathematically verifying those properties of the design, we can deconstruct the infinite state space of the venue model to generate high-coverage test suites to help ensure the system is thoroughly tested prior to deployment. This approach brings unprecedented levels of rigour and governance to the design and compliance of the dark pool. The proofs of properties of the design and test suite coverage metrics that we generate can be used as evidence to regulators, in a similar way to how systems are regulated in avionics.
FV will change the way we communicate specifications of our systems with each other. By way of example, consider the current method of disclosing the numerous rules by which a typical exchange operates with those trading on it. Of course, there are standardised protocols like FIX, but these standards only cover the messaging formats, completely ignoring the logic of the systems ‘behind’ them. So exchanges’ clients are stuck with hundreds of pages of rules and disclosures written in lawyerly prose. They have to hire people to understand those essays and figure out how to make sure their systems are consistent and compliant with exchanges’ rules and disclosures. But, with FV, that information can be specified in a mathematically precise format, which will allow clients to leverage modern scientific tools to ensure their systems fully appreciate all of the intricacies of trading on those venues and are compliant.
The exchange community is missing out on a great revenue opportunity: a considerable portion of budgets banks and hedges funds spend on connecting to exchanges (everything from figuring out how they work to producing regulator audits) may be captured by the exchange operators. By providing clients with precise specs allowing them to leverage FV, exchanges can monetise part of the cost savings. Not to mention that precise specs will allow clients to connect faster and send more orders to those exchanges… This is a win/win for everyone.
Both the CFTC and SEC have proposals for new regulations around disclosure and testing of algorithms in financial markets. The SEC is looking to add more transparency to dark pools and the CFTC wants to analyse the behaviour of trading algorithms. In the same way that a breathalyser transforms the qualitative problem of arguing someone is intoxicated into the scientific domain of chemistry, FV will transform regulatory compliance around financial algorithms into the domain of mathematics. After all, algorithms are mathematical objects, so mathematics should be used to describe and analyse them.
We’d love to hear your feedback on this article. Please click here
Mathematically Verifying Algorithms
