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.

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.

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.

Smart contracts have certain properties that make it easier to do formal verification on them.

"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".

Formal verification tools like VeriSol make it easier for developers to check their work and catch bugs.

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.