Axoni releases AxLang for formal verification of Ethereum smart contracts

Axoni, a New York-based capital markets technology firm that specializes in distributed ledger infrastructure is today announcing AxLang, a new programming language that supports functional programming and enables formal verification of smart contracts for Ethereum-compatible networks.

AxLang is based on Scala and enables secure and full-featured smart contract development by supporting both functional programming and formal verification. Its design is driven by the rigorous requirements for solutions serving the world’s largest financial institutions.

AxLang is part of Axoni’s blockchain infrastructure, which underpins the broadest reaching and most ambitious permissioned ledger production projects in the world, including $11 trillion of credit derivatives, the world’s leading foreign exchange connectivity network, and various other industry implementations.

The Need for Formal Verification

When smart contract code is deployed onto a blockchain, it can be used to power sophisticated, synchronous processing across many machines on a network, ultimately leading to substantial inter-party automation. Before the advent of blockchain technology, processes had to be independently built by each party on a network, which has led to high and redundant operational costs, both from the duplication of development across firms, as well as from the resulting breaks and required reconciliations. In a blockchain network, where each party is executing the same code in the same deterministic environment, those costly disagreements can be eliminated, but this can also amplify the effect that an error in the single implementation of a process has on all parties who depend on shared software. In order to capture the benefits of blockchain technology synchronicity and cross-system automation, while also minimizing the risk of such errors, extra precautions to ensure smart contracts are error-free can be extremely valuable.

We have seen firsthand the difficulties of building enterprise-grade applications with existing smart contract programming languages, and we’re not alone: Over the past two years, more than $500mm has been stolen or lost due to faulty smart contracts on the public Ethereum network, and recent research has found 34,200 contracts with similar existing vulnerabilities. This is due, at least in part, to limitations in Solidity, the dominant language used to write Ethereum smart contracts. One manifestation of those limitations is the inability to use techniques like formal verification to prove the correctness of smart contract code prior to deploying the contracts on the live network.

Formal verification is a rigorous mathematical method used to prove the correctness of computer programs. Historically, this methodology has been used to fortify software and hardware logic in military systems, transportation infrastructure, cryptography, and microprocessors. More recently there is increased awareness of the benefits of formal verification for smart contract code.

Designing AxLang

When designing AxLang, our goal was to maximize security while enabling broad adoption as much as possible. With most programming languages, substantial trade-offs need to be made between those priorities. For example, languages like Haskell or OCaml are known for their powerful functional programming capabilities, but their adoption tends to be limited to relatively small (albeit decidedly passionate) communities. Blockchains and the smart contracts that live on them intrinsically benefit from widespread adoption, so a language which is easy to learn, use, debug, and maintain, all without compromising on security, is ideal.

Enter Scala: a statically-typed language that compiles to the Java Virtual Machine (JVM) and is a blend of object-oriented and functional programming paradigms. This means that developers can leverage easier, imperative and object-oriented programming features for everyday tasks, or employ the more disciplined coding practices to enable formal verification, all in the same language. Furthermore, Scala (which stands for Scalable Language) was “designed to grow with the demands of its users” [Odersky et.al] which is why Scala is often lauded for its enablement of Domain Specific Languages (DSL). DSLs enable specialized modifications to be made to the language to apply to specific markets or industries, a powerful concept in an enterprise setting wherein large-scale systems rely on repeated, specialized data objects or logic.

In order to leverage the flexibility described above, AxLang is a “Core DSL” built using Scala, Domain Specific Languages (DSLs), and annotations, which can be compiled down to JVM and now cross-compiled to any Ethereum Virtual Machine (EVM) blockchain network, including Axoni’s AxCore. AxLang is designed to support both public Ethereum as well as private Ethereum projects, and because of its basis in Scala, can be used to develop more specialized DSLs on top of it. This means developers can quickly adopt the language while also being able to leverage much of the existing tooling.

Summary and Outlook

AxLang is unique among blockchain languages to address smart contract fragility issues by leveraging the power of an existing and proven programming language, Scala, which is already widely utilized, has a large user base, a highly developed tools ecosystem, including for formal verification, and is already widely deployed within the financial services industry.

As of the date of this announcement, AxLang is not yet an open source language, primarily so that the Axoni team can drive it quickly and efficiently to production readiness, at which time we will make it widely available. Our team will provide additional details and updates leading up to that point, which is expected in the second half of 2018. In the meantime, the video below provides a demo of AxLang in action which involves Scala cross-compiling to EVM bytecode, formal verification and deploying the contract to the public Ethereum blockchain.