Microsoft, in further evidence of its intentions to aid blockchain development, has released a new tool called VeriSol that verifies and analyzes smart contracts developed in the Solidity programming language. The Microsoft Azure Blockchain team published a blog post on June 3 titled “Researchers work to secure Azure Blockchain smart contracts with formal verification”.
With new open-source formal verification tool VeriSol, Microsoft researchers are helping developers author safer and higher-quality smart contracts in @Azure Blockchain offerings: https://t.co/dzL84z1p3F
— Microsoft Research (@MSFTResearch) June 3, 2019
The blog post states that the team behind Azure’s blockchain development services has taken the potential security issues in smart contracts seriously and to that end has developed the formal verification tool that checks the correctness of software programs or, in other words,
Developers can begin to express the desirable behaviors of smart contracts written in a subset of the popular Solidity language and then use mathematical logic machinery to rigorously check those specifications against the implementation.
Microsoft Principal Researcher, Shuvendu Lahiri, said that the tool would help eliminate the resource costs associated with verification,
The use of formal verification for production software requires individuals skilled in highly specialized formal languages and tools, which imposes on development teams a steep learning cost and often several person-years of investment to break down the highly sophisticated task of verification into those that can be discharged mechanically by the verification tools.
The team states that the tool has already been used successfully applied to smart contracts on Azure. In one instance, the tool was used to formalize and check specifications of smart contracts that govern the consortium of Ethereum on Azure and the Azure Blockchain Service.
Microsoft Keen on Blockchain
Microsoft has shown great interest in the blockchain space. Besides launching the Azure blockchain workbench, it has also released a developer’s kit on Azure for millions of Ethereum developers, and is building a decentralized identity service called ION.
The research team has also said that VeriSol is not the end of its blockchain plans – it also aims at bringing formal verification to mainstream smart contract development through open collaboration.
We envision empowering not just Azure Blockchain developers and customers, but contributing to a full blockchain ecosystem that is safer and helping people realize the full potential of the technology without being plagued by the costly mistakes in smart contracts, says Lahiri
