Microsoft announces VeriSol: Ethereum smart contract verification

[Magician]

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.

Source