London Fintech Firm Launches Formal Verification Platform for Blockchain-Based Smart Contracts
Aesthetic Integration , a London-based fintech that applies “formal verification” to analyze safety and fairness of algorithms in financial markets, recently announced the launch of Imandra Contracts, a solution the company calls the world’s first platform using formal verification for blockchain-backed smart contracts.
The announcement was made at the Devcon2 conference as part of International Blockchain Week in Shanghai.
Imandra Contracts apply for advances in artificial intelligence, mathematics, and computer science to bring improved rigor to the electronic financial markets and other industries. It does this by providing greater transparency to the development and regulation of smart contracts.
To Be Used By Ethereum
The new cloud-based platform will be used initially by Ethereum, a decentralized blockchain app platform that runs smart contracts.
“Imandra is a tool for analyzing smart contracts to help individuals understand what they do, why they do it, and what can possibly go wrong,” Dr. Grant Passmore, Aesthetic Integration’s co-chief executive, and co-founder told CCN.com. “Imandra is powered by recent advances in formal verification, a field at the intersection of computer science, mathematics, and artificial intelligence focused on reasoning about the possible behaviors of algorithms.”
The platform will enable users to identify and fix anomalies in financial algorithms. It will also enable them to protect businesses from negative impacts before they take effect. Customer privacy is ensured by industry best practices, including virtual private clouds.
Banks Already Use Imandra
Imandra is already in use at some top investment banks to analyze the safety and fairness of their financial algorithms, Passmore noted. He pointed out that Aesthetic Integration won the 2015 UBS Future of Finance Challenge for the use of Imandra in analyzing regulatory properties of dark pools. “Imandra Contracts brings these techniques to blockchain smart contracts for the first time, all available in the cloud,” he added.
Platform interoperability is a major focus for Aesthetic Integration, Passmore observed. “We’re developing versions of Imandra Contracts for many blockchain smart contract platforms. However, we began with Ethereum as its virtual machine is well specified (i.e., the Ethereum yellow paper) and, given recent events, the Ethereum community has strongly recognized the need for formal verification.”
The platform allows users to review contract designs and algorithms, including those hosted on decentralized smart contract platforms and apps, such as Ethereum. Reviewing designs and algorithms can ensure they meet agreed specifications and that they do not contain unwanted glitches.
What About DAO Breach?
“The security breach faced by The DAO (Distributed Autonomous Organization), which used the Ethereum Blockchain, highlights the urgent need for a more rigorous analysis of smart contracts in financial services,” said Passmore. “The lesson of the DAO is clear: Smart contract development must be approached rigorously with engineering discipline, more akin to building a safety-critical control algorithm than building a web app.”
Would Imandra Contracts have prevented the DAO breach? “It’s impossible to say,” Passmore responded when CCN.com posed the question. “If we change the question to ‘Could Imandra Contracts have prevented the DAO breach?’ then the answer is clearly ‘yes.’ For example, we can encode the issues that led to the DAO breach as verification goals in Imandra and have Imandra automatically check a wide class of smart contract designs to ensure they don’t exhibit the same issues.”
Finance Leads Smart Contracts
Passmore is not surprised to see the financial industry taking the lead in investing in smart contracts.
“From clearing to automatic management and pricing of structured product portfolios, finance recognizes the need to move to more robust, efficient, and automatically analyzable system architectures,” he said. “Pricing of derivatives is a major issue. If a bank goes all-in on smart contracts, three years from now they may have portfolios of hundreds of thousands of smart contracts.”
“They then need to understand their risks, calculate exposure, compute Greeks, etc.,” Passmore continued. “You can’t do that without analyzing the code underlying the smart contracts. This is a very exciting application area for Imandra Contracts that we’re working on actively.”
Passmore noted that other safety-critical industries such as hardware manufacturing and avionics already rely on formal verification to make algorithms safe. “As our mainstream engagement with blockchain increases, so too does the need for safety protocols to vet the algorithms being created,” he noted.s
Furthermore, Aesthetic Integration already offers Imandra Markets and Imandra Venues formal verification solutions. Imandra Markets is a cloud-based ecosystem for client-facing algorithm specifications that simplifies the designing, testing, and compliance processes for trading systems.
Imandra Venues analyzes regulatory properties of trading venues, establishing a new standard for the stability and transparency of exchanges and dark pools after the recent increase in glitches and fines. Such incidents have highlighted the costly nature of unknown mistakes in algorithmic designs.
Aesthetic Integration plans to launch a pre-sale of discounted access to Imandra Contracts to provide early adopters access to the platform in the first week of October. Users will be able to analyze and review smart contracts designs remotely from mobile devices.
Images from Shutterstock and Aesthetic Integration.
