Microsoft recently announced the development of an open source verification tool called VeriSol for Ethereum’s smart contract and the Solidity programming language.
Announced on Microsoft’s official blog, the tool is called VeriSol as an abbreviation of Verifier for Solidity.
Partnership with the Azure group
Today, Solidity is the most widely used programming language for the development of smart contracts and Ethereum dApps.
VeriSol will allow developers to write specifications for their smart contracts using an intermediate language that can be tested using mathematical logic mechanisms.
Today VeriSol is still a prototype, but the team aims to cover as soon as possible all possible uses of the main business applications.
VeriSol is the final product of the partnership between the Azure Blockchain group and Microsoft’s Research group.
Verification required to ensure greater security
Security has long been the main problem for Ethereum’s smart contracts, as evidenced by the number of cryptocurrency thefts and exchange hacks. Formal verification provides developers with an effective protocol for testing the safety of the most critical components in their code.
The process generally requires specialised developers and long time periods to run, so it is recommended that it be reserved only for the most important parts of the product.
One of Microsoft’s leading researchers, Shuvendu Lahiri, said:
“The modest code size and the sequential execution semantics of smart contracts make them amenable to scalable verification, and the open operating environment substantially reduces the need to manually model the environment in which a smart contract operates”.
VeriSol will integrate the development kit and workbench for Microsoft’s own Azure blockchain, which offers development models and integrations with all the typical services of Azure.
This tool aims to provide developers with a more straightforward way of developing and will give them the ability to easily find any bugs in the code.
