Microsoft announces in its official Azure blog the release of VeriSol (short for Verifier for Solidity). VeriSol is an open-source formal verification tool for Solidity smart contracts. Developers can use VeriSol 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. This makes it harder to introduce bugs into smart contract code.
Microsoft claims that VeriSol has already been used to verify a diverse set of smart contracts in the Azure Blockchain ecosystem. In one application, the VeriSol team used the verifier to formalize and check specifications of the smart contracts that govern consortium members in Ethereum on Azure and the Azure Blockchain Service.
VeriSol is still a prototype and covers only a subset of Solidity. By open-sourcing VeriSol, Microsoft hopes to leverage the wider Solidity development community to improve VeriSol.