IT giant Microsoft has released a new open source tool for verifying and auditing smart contracts written in the Solidity programming language, which is very popular in the Ethereum blockchain.

The new Microsoft tool for smart contracts auditing is called VeriSol (short for “verifier for solidity”). This tool allows developers 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.”

“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,” says Cody Born, Senior Software Engineer on the Azure Blockchain team.


VeriSol was also included in the Azure Blockchain’s continuous integration pipeline for smart contract development.

“With new open-source formal verification tool VeriSol, Microsoft researchers are helping developers author safer and higher-quality smart contracts in Azure Blockchain offerings,” said Microsoft in an announcement.

In May 2018, a group of researchers led by Associate Professor at University College London and St. Petersburg State University graduate Ilya Sergey created a test duplicate of the Ethereum blockchain and launched various scripts on it to search for vulnerabilities. They analyzed approximately one million smart contracts. The study revealed that 34,200 smart contracts on Ethereum contain critical vulnerabilities.