The tool allows verifying and analyzing smart contracts using the Solidity programming language
Through its official Twitter account, Microsoft Research announced that it launched a new open source tool that will allow auditing and analyzing smart contracts written in the programming language Solidity, which is commonly used in the Ethereum blockchain.
The name of the new Microsoft tool is VeriSol; this is in order to abbreviate the name Solidity Verifier. This development allows auditing smart contracts with the aim to verify in which stage of the process they are.
“With new open-source formal verification tool VeriSol, Microsoft researchers are helping developers author safer and higher-quality smart contracts in @Azure Blockchain offerings”, Microsoft’s message says.
In this way, programmers can express the desirable behavior of smart contracts written in a subset of the popular programming language Solidity”, the company explained. The objective is that the tool can use the mathematical logic machinery to audit the phase in which any requirement is, when a specific smart contract is implemented.
As part of the development, VeriSol was also incorporated into Azure’s smart contract development line. Senior software engineer of the Azure team, Cody Born, commented about this point.
“VeriSol allows us to iterate more quickly because of the automatic and continuous checking, and it allows us to catch bugs faster without having to worry about potentially affecting customers”, he said.
Contributing to a safer ecosystem
Although VeriSol is still a prototype powered mainly by smart contracts at Azure, researchers have more goals for the verification tool. They say they are looking to encourage open collaboration to help bring advances in formal verification to mainstream smart contract development.
Shuvendu Lahiri, Main Investigator of Microsoft, commented: Our vision is to empower not only the developers and users of the Azure blockchain, but also to contribute to a safer blockchain ecosystem and help people to take advantage of the full potential of the technology, without being affected by costly errors in contracts”.
Lahiri added that 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.
Microsoft has developed a number of software suites for building decentralized tech, such as its cloud-based blockchain development kit, Visual Studio for Ethereum dapps, and a decentralized digital identity management system.
Recently, the Bill Gates-founded company even gave Louis Vuitton a tool to verify the authenticity of luxury items on the blockchain and seems to still be interested in blockchain technology to develop more projects. Now, the company is focused especially on the advantages that smart contracts offer.
One of the key drivers making blockchain-based applications programmable, accessible to enterprise customers, and able to meet the diverse needs of a variety of sectors are smart contracts, a post of Microsoft says.
The company also cites research by consulting firm Gartner, which suggests blockchain tech can bring businesses added value upwards of $360 billion by 2026.
By María Rodríguez
