Grant Olney Passmore on Formal Verification of Financial Algorithms

On 25-Aug-2016, Grant Olney Passmore from Aesthetic Integration gave an invited talk at the ITP 2016 conference in Nancy, France. Here is the official announcement from the program:

Title: Formal Verification of Financial Algorithms, Progress and Prospects

Abstract:
Many deep issues plaguing today’s financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we’ve pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools), we’ll describe the landscape, and illustrate our Imandra formal verification system on a number of real-world examples. We’ll sketch many open problems and future directions along the way.

The session chair introduced the speaker as a colleague from the prover community who managed to get his private life covered by the NY Times.

Passmore then started his presentation with a promotional video, which is intended for people from the Financial Industry – without a background in formal logic or software verification. He pointed out that this is his first talk about the subject before an audience with expertise in theorem proving, and promised that many odd terms and buzzwords from the world of Finance would become clear later.

From his many slides, Passmore could fit only a small portion into the 60min time slot. A key point was the following Stack of Financial Algorithms (from top to bottom):

  • Collateral Trading
  • Inventory Management
  • Algo Containers
  • Trading Algorithms
  • Smart Order Routers
  • Venues

So far, Aesthetic Integration has mainly worked at the bottom: “Venues” are virtual places where trading happens, e.g. a “dark pool” as in the UBS Future of Finance Challenge (see also the white paper).

Passmore invited the prover community to participate in formal treatment of the whole stack given above. For example, full formalization of Financial Mathematics in Isabelle/HOL could support the slot “Trading Algorithms”.

He also presented the present flagship tool environment: Imandra. Here is a quotation from the official website:

What is Imandra?

AI’s Imandra is breakthrough artificial intelligence technology for ensuring financial algorithms are designed and implemented safely and fairly.

Powered by major recent advances in formal verification, Imandra:

  • Verifies correctness and stability of system designs for regulatory compliance
  • Uncovers nontrivial bugs
  • Tests – creates high-coverage test-suites
  • Saves – radically reduces associated costs

The system was demonstrated in two versions: one running on the local machine, and one running on a server (i.e. “in the cloud”). The interaction model is still mainly command-line based, but Aesthetics Integration is interested to improve on that.