Announcing CryptoSlate Research — gain an analytical edge with in-depth crypto insight. Learn more.

Microsoft announces VeriSol: Ethereum smart contract verification

Microsoft announces VeriSol: Ethereum smart contract verification

Microsoft announced the development of an open-source formal Ethereum smart contract verification scheme for the Solidity programming language.

Announced on the Microsoft blog, the tool will be called VeriSol–Verifier for Solidity. VeriSol will enable developers to write specifications for their contracts using an intermediate language that can then be tested using mathematical logic machinery.

The Microsoft blog states that “the VeriSol team used the verifier to formalize and check specifications of the smart contracts that govern consortium members in Ethereum on Azure and Azure Blockchain Service.”

VeriSol is currently a prototype but the team aims to cover most enterprise applications of smart contracts. The scheme is the product of a partnership between Microsoft’s Azure Blockchain and Research teams.

Formal Ethereum smart contract verification provides security

Security has long been an issue for smart contracts, as evidenced by the consistency of cryptocurrency theft and exchange hacks. Formal verification gives developers a protocol for checking the security of critical smart contract components.

The process generally requires specialized developers and long periods of time to execute, so it’s only reserved for the most important parts of a product. Smart contracts have certain properties that make it easier to do formal verification on them. As Microsoft Principal Researcher Shuvendu Lahiri explains,

“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 supplement Microsoft’s Azure Blockchain Development Kit and Workbench, which offers development templates and integrations for common Azure services like key management and identity. Formal verification tools like VeriSol make it easier for developers to check their work and catch bugs.

This provides developers with a more effective path to production. Solidity is the most popular language for programming smart contracts on Ethereum so an automated formal verification tool should make it easier for developers to improve the security of their dApps.

Filed Under: , Ethereum, Technology
Seth Goldfarb

Seth is a Seattle-based writer who helps businesses using blockchain tell the stories of their success. His work has been published in CryptoSlate, Hacker Noon, and Coin Review and clients have included Evernym and Aave. Seth also maintains a calendar of Seattle-area blockchain events at

View author profile

Disclaimer: Our writers' opinions are solely their own and do not reflect the opinion of CryptoSlate. None of the information you read on CryptoSlate should be taken as investment advice, nor does CryptoSlate endorse any project that may be mentioned or linked to in this article. Buying and trading cryptocurrencies should be considered a high-risk activity. Please do your own due diligence before taking any action related to content within this article. Finally, CryptoSlate takes no responsibility should you lose money trading cryptocurrencies.