Financial markets run on complex algorithms. The industry uses several protocols to describe how their systems are expected to communicate with others - effectively, describing their APIs. One such protocol is FIX (Financial Information eXchange) - widely used for quite some time. Financial services firms (e.g. exchanges, hedge funds and investment banks) share such specifications with their counterparts to allow them to connect to their systems. The protocol specification is relatively vague and informal - at AI, we’re changing this.
Our formal verification system, Imandra, is designed for analysing complex algorithms to ensure they’re designed and implemented safely and fairly. We have created a DSL with Xtext for expressing FIX specifications that trading system developers may share with one another. A specification written in this DSL is then translated into Imandra Modelling Language (IML), a subset of OCaml for which we’ve created a formal semantics. The generated IML code is in turn analysed by Imandra to verify that the specification meets the rules of the protocol and automatically discover non-trivial behaviour that should be tested by the specification’s clients.
In this session, I’d like to describe the application domain and the decisions we made when creating the DSL. I’ll especially cover the important decisions ensuring that the DSL is translatable into a formal language and the generated code is susceptible to formal verification.
5