AxLang Case Study: A Formally Verifiable Derivatives Contract Library (VIDEO)
April 23, 2018 (New York) — In our previous update we introduced AxLang, a new smart contract programming language based on Scala that supports functional programming and enables formal verification of smart contracts for Ethereum-compatible networks.
Today, we are excited to share a specific use case for AxLang: a standardized financial products modeling library for use by the derivatives industry. Below is a video demonstrating a prototype implementation of the ISDA Common Domain Model leveraging the functional programming capabilities of Scala, as well as an overview of AxLang’s potential impact on the deployment of these standardized models more broadly.
ISDA Common Domain Model
The International Swap Dealers Association (ISDA) has been leading efforts to standardize the modeling of financial instruments for many years, including the development of the widely-used Financial products Markup Language (FpML) in 1999.
FpML was developed to standardize the communication of complex derivatives contract information between counter-parties, and it succeeded in simplifying messaging of key data. Even with standardized messaging, firms still used individual processes to model, persist, and value complex derivatives. In a coordinated effort to address this issue, ISDA, in partnership with its member firms, recently released the first version of the ISDA Common Domain Model (ISDA CDM).
As defined by ISDA, the CDM is designed to be a “standardized model for the post-execution trade lifecycle, focusing on the non-differentiating aspects of that trade lifecycle that are candidates for mutualization by the industry.”
ISDA CDM, serving as a data model specification, is agnostic to technology implementation, although ISDA has mentioned that the specification “is targeted at distributed ledgers (DLs) to exploit their embedded lineage and consistency properties.”
Distributed ledgers are designed to automate data and synchronize state, so layering a common domain model on that infrastructure can help achieve the core goal of enabling all counterparties to be fully synchronized on the state of their derivatives contracts.
With regards to unified blockchain implementations of the ISDA CDM specification, the programming language choice for that data model will inherently be a critical decision.
Implementing the CDM in AxLang
As discussed in more detail in the previous article, AxLang is based on Scala and enables secure, full featured smart contract development by supporting both functional programming and formal verification. It is designed to work within the Ethereum ecosystem, including AxCore, Axoni’s blockchain implementation. AxCore underpins the broadest reaching and most ambitious permissioned ledger projects in the world, including $11 trillion of credit derivatives, the world’s leading foreign exchange connectivity network, and various other industry implementations.
AxLang can be used standalone to write more secure smart contracts but can also allow the development of specialized Domain Specific Languages (DSLs). However, as is best practice for software development in general, its impact on building a more secure infrastructure for the OTC derivatives industry will be greatly magnified if AxLang is used to build standard, thoroughly tested, and formally verified libraries, which in turn can be used by others to build their high-level applications.
Marrying the principles of the ISDA CDM with AxLang enables the industry to: agree on a data model, ensure that model is executed properly through formal verification, and deploy that formally verified and unified data model into an infrastructure that enables full state synchronization between parties.
Additionally, AxLang is valid Scala and can compile to either the Java Virtual Machine (JVM) or to the Ethereum Virtual Machine (EVM). It can be used to write formally verified code for use on a distributed ledger or run locally off-ledger in a standard Java environment, enabling substantial flexibility to test various infrastructure alternatives without substantial re-writes of the application code.
