Microsoft has released a new open source tool that will allow for the verification and analysis of smart contracts written in the popular Solidity programming language that is commonly used on the Ethereum blockchain.
The new tool is called VeriSol – short for Verifier for Solidity – and allows developers to express the “desirable behaviours of smart contracts written in a subset of the popular Solidity language” and then use “mathematical logic machinery” to check a specification against a given smart contract implementation.
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
Senior software engineer on the Azure Blockchain team Cody Born said: “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.”
Encouraging open source collaboration
While VeriSol is still a prototype primarily driven so far by smart contracts in Azure, the researchers have lofty goals for the verification tool, saying that they are looking to “encourage open collaboration to help bring advances in formal verification to mainstream smart contract development”.
Microsoft principal researcher Shuvendu Lahiri concluded: “We envision empowering not just Azure Blockchain developers and customers, but contributing to a full blockchain ecosystem that is safer and helping people realise the full potential of the technology without being plagued by the costly mistakes in smart contracts.”
Disclaimer: The views and opinions expressed by the author should not be considered as financial advice. We do not give advice on financial products.